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: Are monad liftings evil?

Ralph Sarkis (Jun 16 2023 at 15:42):

A monad $(\widehat{M},\widehat{\eta},\widehat{\mu})$ on $\mathbf{D}$ is called a lifting of monad $(M,\eta,\mu)$ on $\mathbf{C}$ along $U: \mathbf{D} \to \mathbf{C}$ if the following three equations hold:

$$U\widehat{M} = MU \quad U\widehat{\eta} = \eta U \quad U\widehat{\mu} = \mu U$$

Given a monad $\widehat{M}$ that lifts $M$ along $U$, a monad $\widehat{T}$ on $\mathbf{D}$ and a monad isomorphism $\widehat{\rho}: \widehat{M} \cong \widehat{T}$. Can I find a monad $T$ on $\mathbf{C}$ such that $\widehat{T}$ lifts $T$ and moreover there is an isomorphism $\rho: M \cong T$? (optionally it satisfies $U\widehat{\rho} = \rho U$). I summarized this situation in the picture below.
image.png

I don't believe this is true with no assumption on $U$ because I don't even know how to construct the functor $T$. If $U$ has a left adjoint $F$, then I can define

$$T = \mathbf{C} \xrightarrow{F} \mathbf{D} \xrightarrow{\widehat{T}} \mathbf{D} \xrightarrow{U} \mathbf{C}.$$

I am stuck here because I don't even know how to show $\widehat{T}$ is a functor lifting of $T$. However, the possibility that it is not a monad lifting breaks my mind, because it feels like functoriality or naturality of some stuff would fail in some way. Yet, I cannot prove how this does not work...

Mike Shulman (Jun 16 2023 at 15:58):

Right, that's not true with no assumptions on $U$. Your proposed $T = U\hat{T}F$ doesn't work either in general, because you have $TU = U\hat{T}FU$ which can't be expected to equal $U\hat{T}$ unless $FU=\rm Id$.

Mike Shulman (Jun 16 2023 at 15:59):

If you want to work in an isomorphism-invariant way, you can either talk about liftings up to isomorphism, or take $\mathbf{D}$ to be a [[displayed category]] over $\mathbf{C}$.

Ralph Sarkis (Jun 16 2023 at 16:12):

Mike Shulman said:

Right, that's not true with no assumptions on $U$. Your proposed $T = U\hat{T}F$ doesn't work either in general, because you have $TU = U\hat{T}FU$ which can't be expected to equal $U\hat{T}$ unless $FU=\rm Id$.

Exactly, but I am not able to think of an example because if $TU \neq U\widehat{T}$ it feels like the isomorphism $\widehat{\rho}$ has to make some weird choices of bijections that would not make it natural.

Ralph Sarkis (Jun 16 2023 at 16:14):

Mike Shulman said:

If you want to work in an isomorphism-invariant way, you can either talk about liftings up to isomorphism, or take $\mathbf{D}$ to be a [[displayed category]] over $\mathbf{C}$.

Thanks! I think that would probably work in my case, but unfortunately I want to work with monad liftings for Applications™. I guess this will just make my theorems a bit uglier.

Mike Shulman (Jun 16 2023 at 16:22):

Here's an easy way to see that it's not possible in general. Suppose there are two objects $d,d'\in \mathbf{D}$ such that $Ud = Ud' = c$, say. Then $U\hat{M}d = U\hat{M}d'$ since both equal $Mc$. But we can choose $\hat{T}$ in such a way that $U\hat{T}d \neq U\hat{T}d'$, which implies there cannot be a $T$ that is lifted by $\hat{T}$ since otherwise $U\hat{T} d$ and $U\hat{T}d'$ would both equal $Tc$.

Mike Shulman (Jun 16 2023 at 16:23):

And we can do that even if $U$ has a left adjoint.

Ralph Sarkis (Jun 16 2023 at 16:26):

It is this "we can choose" that makes me not totally convinced. Because after choosing that, we also need to choose $\widehat{\rho}_d$ and $\widehat{\rho}_{d'}$, and then you need to check that is compatible with possible morphisms between $d$ and $d'$.

Mike Shulman (Jun 16 2023 at 16:33):

It's easy to modify any functor by isomorphisms to a naturally isomorphic one. If $F:A\to B$ is any functor and you choose for every $a\in A$ an object $Ga\in B$ and an isomorphism $\alpha_a : Fa \cong Ga$, this choice of $G$ on objects extends uniquely to a functor $G:A\to B$ such that $\alpha$ is a natural transformation. For $f:x\to y$ in $A$, define $Gf = \alpha_y \circ Ff \circ \alpha_x^{-1}$, and then the naturality squares hold by definition.

Mike Shulman (Jun 16 2023 at 16:35):

So in this case, given the functor $\hat{M}$, we just need to choose some object $\hat{T}d$ such that $U\hat{T}d\neq U\hat{M} d$, and an isomorphism $\hat{M}d \cong \hat{T}d$, and set $\hat{T} x = \hat{M} x$ for all $x\neq d$. Then this makes $\hat{T}$ a functor isomorphic to $\hat{M}$, and we can transport the monad structure across that isomorphism.

Ralph Sarkis (Jun 16 2023 at 17:17):

Ah, thanks a lot. I am going to sleep better :smile: