Category Theory
Zulip Server
Archive

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.


Stream: learning: questions

Topic: Terminal coalgebras of finitary monads?


view this post on Zulip Mike Stay (Aug 24 2020 at 22:36):

Under what conditions do finitary monads have terminal coalgebras?

view this post on Zulip Nathanael Arkor (Aug 25 2020 at 14:11):

There are more general answers, but perhaps your situation is nice enough that this works. If your monads are algebraically-free, then:

view this post on Zulip Mike Stay (Aug 25 2020 at 17:23):

@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.

view this post on Zulip Nathanael Arkor (Aug 25 2020 at 22:19):

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.

view this post on Zulip Nathanael Arkor (Aug 25 2020 at 22:30):

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.

view this post on Zulip Mike Stay (Aug 26 2020 at 14:57):

@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 FF 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?

view this post on Zulip Cole Comfort (Aug 26 2020 at 15:03):

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 FF 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.

view this post on Zulip Mike Stay (Aug 26 2020 at 16:06):

@Cole Comfort Thanks!

view this post on Zulip Cole Comfort (Aug 26 2020 at 16:27):

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.

view this post on Zulip John Baez (Aug 26 2020 at 16:41):

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.

view this post on Zulip Nathanael Arkor (Aug 26 2020 at 16:46):

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.

view this post on Zulip John Baez (Aug 26 2020 at 17:32):

Oh.