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: theory: category theory

Topic: lifting monads to lax limit categories

Tom Hirschowitz (May 03 2022 at 12:44):

Given a monad morphism (F: ℬ → 𝒞, α: TF → FS) between monads S: ℬ → ℬ and T: 𝒞 → 𝒞, there appears to be a canonical way of lifting this to the lax limit category 𝒞↓F: we map any object x: c → Fb to Tc → TFb → FSb. Both projections functors induce "strict" monad morphisms, in the sense that the 2-cell part is an identity.

Does this construction have any nice universal property? And does it generalise to other kinds of weighted limits?

Mike Shulman (May 04 2022 at 02:57):

This is a special case of the general fact that for any 2-monad $M$, the 2-category of $M$-algebras and lax morphisms inherits oplax limits from the base 2-category, in such a way that the "basic" projections are strict $M$-morphisms and detect strictness. Here $M$ is the 2-monad on $\rm Cat$ whose algebras are categories equipped with a monad, and whose lax morphisms are (lax) monad morphisms, and you're considering the oplax limit of an arrow. (It's an oplax limit, not a lax limit.)

Mike Shulman (May 04 2022 at 02:59):

So yes, it has a universal property in the 2-category of categories-with-monads and lax monad morphisms, and it generalizes to other oplax limits, and even to some more general weighted limits than that. The first general results along these lines were proven by Steve Lack in Limits for lax morphisms, and then later he and I generalized them in Enhanced 2-categories and limits for lax morphisms.

Mike Shulman (May 04 2022 at 03:00):

The generalized version uses "$\mathcal{F}$-categories" to encode the strictness of the projections and the fact that they detect strictness.

Tom Hirschowitz (May 04 2022 at 06:25):

Mike Shulman said:

(It's an oplax limit, not a lax limit.)

Damn it, I really thought I had it right this time!

Tom Hirschowitz (May 04 2022 at 06:31):

But thanks a lot, this seems to be exactly what I was looking for! Actually, I'd come across the papers you mention, but didn't even know that categories-with-monads were 2-monadic over $\mathbf{Cat}$, so failed to see the connection. This last fact is really nice in its own right, imho.

Tom Hirschowitz (May 04 2022 at 09:04):

Mike Shulman said:

Here $M$ is the 2-monad on $\rm Cat$ whose algebras are categories equipped with a monad[.]

For those who wouldn't otherwise take the time to track this down, it is explained in Blackwell, Kelly, and Power, §6.1, with extra detail in Steve and Mike's paper linked to above.

Briefly, let $\Delta_+$ denote the free strict monoidal category on a monoid. A strict monoidal category is the same as a monoid in $\mathbf{Cat}$, so we get a 2-monad $\mathcal{C} \mapsto \Delta_+ \times \mathcal{C}$.
Algebras for this 2-monad are precisely categories equipped with a monad.

Indeed, writing $t^n$ for the nth monoidal power of the generating monoid object $t \in \Delta_+$, an algebra structure on a category $\mathcal{C}$ maps any pair $(t^n,c)$ with $c \in \mathcal{C}$ to some object $t^n c$, and the monad algebra laws ensure that $t^{m+n} c = t^m (t^n c)$ and $t^0 c = c$.

A perhaps fancier way of putting this is to say that a monad on $\mathcal{C}$ is the same as a strict monoidal functor $\Delta_+ \to [\mathcal{C},\mathcal{C}]$, which is in turn the same as a monoid action $\Delta_+ \times \mathcal{C} \to \mathcal{C}$, which is finally the same as algebra structure on $\mathcal{C}$.

Valeria de Paiva (May 04 2022 at 13:42):

thanks, I had no idea! and it feels very important for stuff I am thinking right now.

Tom Hirschowitz (May 04 2022 at 14:06):

Just in case, Blackwell et al. explain that the idea works much more generally, e.g., for categories equipped with a pair of monads and a distributive law between them.

Mike Shulman (May 04 2022 at 14:47):

It's intuitive if you think of a monad as equipping a category with "algebraic structure" and make analogies to algebraic structures on sets. A set equipped with an endofunction is an algebraic structure, hence so is a category equipped with an endofunctor. And just as you can assert additional axioms on that endofunctor, like that its square is the identity, you can add transformations relating composites of an endofunction to itself (or to other endofunctions).