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: Understanding proof in Proposition 4.1.6 by Borceux Vol 2

Davi Sales Barreira (Dec 14 2023 at 16:17):

Hello, friends. I'm trying to understand a proof given in Proposition 4.1.6 by Borceux Volume 2.
The proposition is trying to show the functoriality of a functor $\phi$ where $\phi:\mathcal C_T \to CˆT$ such that $\phi(C) = (TC, \mu_C)$ and $\phi(f)= \mu_D \circ T f$ where $f:C \to TD$, i.e. $f:C \to D$ in $\mathcal C_T$. Note that here $T$ is a monad, and $\mu:TT\to T$.

In the proof the author starts by writing

$$\phi(g) \circ \phi(f) = \mu_C \circ T(g) \circ \mu_B \circ T(f) = \mu_C \circ \mu_{T(C)} \circ TT(g) \circ T(f)$$

I don't follow how the last equality here is true. Isolating the terms, it seems to me that the implication is that $T(g) \circ \mu = \mu T \circ TTf$. If so, how can one prove such equality? I was trying to use the naturality condition, but I wasn't able to figure out the solution.

Ralph Sarkis (Dec 14 2023 at 16:31):

That equality uses naturality and then the associativity of multiplication of the monad (the commutative square with many $\mu$). I would write it in two steps.

Davi Sales Barreira (Dec 14 2023 at 16:34):

Sorry, I don't follow... I'm having trouble to see how the naturality makes this equality true.

Ralph Sarkis (Dec 14 2023 at 17:21):

Wait sorry, I was on my phone and answered too quickly. That equality is only due to naturality. Here is a diagram with the usual naturality square on the left, the one we are using on the right and the replacements taking place in the middle, sorry for the weird formatting.
image.png

Davi Sales Barreira (Dec 14 2023 at 17:42):

Now it's very clear! Thank you, @Ralph Sarkis