You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Under what conditions do finitary monads have terminal coalgebras?
There are more general answers, but perhaps your situation is nice enough that this works. If your monads are algebraically-free, then:
@Nathanael Arkor Thanks! I'm particularly interested in Lawvere theories with models in CompSet (computably enumerable sets and computable functions). The specific theory I'm looking at is the theory of Heyting algebras, with binary function symbols for ∧, ∨, and →, nullary symbols for ⊤ and ⊥, and the equations relating them; it's not clear to me whether the corresponding monad has a terminal coalgebra.
Does algebraic freedom mean that presentations of the theory lack equations (that is, the theory is generated only by an algebraic signature rather than a signature plus equations)? If so, that wouldn't apply to this case.
I should clarify what you mean by "coalgebra for a monad", as this is not well-defined in general. You could mean a coalgebra for the underlying endofunctor, but in this case algebraic freeness seems like a reasonable assumption, or you are knowingly losing information by passing to the underlying endofunctor.
Finitary functors may be presented by operators and "flat" equations (i.e. equations involving non-nested terms), as described in Adámek–Milius–Moss–Urbat's On finitary functors and their presentations. I think this means that the Lawvere theories corresponding to algebraically free monads are precisely those with flat equations, which discounts Heyting algebras.
@Nathanael Arkor Thanks again! You say the notion of coalgebra for a monad is not well-defined in general. On the nlab page "coalgebra for an endofunctor", I just found this statement: "If is equipped with the structure of a monad, then a coalgebra for it is equivalently an endomorphism in the corresponding Kleisli category. In this case the canonical monoidal category structure on endomorphisms induces a tensor product on those coalgebras." That makes it sound like monads always have coalgebras (though it says nothing about finality). Can you expand on what you meant?
Mike Stay said:
Nathanael Arkor Thanks again! You say the notion of coalgebra for a monad is not well-defined in general. On the nlab page "coalgebra for an endofunctor", I just found this statement: "If is equipped with the structure of a monad, then a coalgebra for it is equivalently an endomorphism in the corresponding Kleisli category. In this case the canonical monoidal category structure on endomorphisms induces a tensor product on those coalgebras." That makes it sound like monads always have coalgebras (though it says nothing about finality). Can you expand on what you meant?
This is still only a coalgebra for the underlying functor and doesn't interact with the structural isomorphisms of the monad... unlike the a coalgebra for a comonad or an algebra for a monad.
@Cole Comfort Thanks!
Yes, this confused me for a while, reading Jacobs' paper on coalgebras for certain monads. I think that it is terrible that the term is overloaded.
Does algebraic freedom mean that presentations of the theory lack equations (that is, the theory is generated only by an algebraic signature rather than a signature plus equations)? If so, that wouldn't apply to this case.
Looking at the definition on the nLab, I see algebraic freedom for a monad means that its category of algebras (the Eilenberg-Moore category) is equivalent to the category of free algebras of its underlying functor. So the only examples I can think of coming from Lawvere theories are those from theories with no equations.
Not the category of free algebras: the category of all algebras for the underlying endofunctor, in which case you may have (a restricted class) of equations.
Oh.