2
$\begingroup$

I am trying to prove that the monad induced by an adjunction is indeed a monad.

Recall that for a given adjunction $F : \mathbb{C} \to \mathbb{D}$ and $G : \mathbb{D} \to \mathbb{C}$ with $F$ left adjoint to $G$, the unit is given by $\eta : 1_\mathbb{C} \Rightarrow GF$ and the co-unit is given by $\epsilon : FG \Rightarrow 1_\mathbb{D}$. The adjunction induces an endofunctor on $\mathbb{C}$ given by $T = GF$. Moreover, we can define a 'unit' simply as $\eta : 1_\mathbb{C} \Rightarrow GF$ and a 'multiplication' $\mu : T^2 \Rightarrow T$ as $\mu_C = G(\epsilon_{FC})$. The claim is that this defines a monad structure on $T$. Let's verify that. We have to show that the following diagrams commute. Notice that all arrows of the diagrams `live' in the functor category $[\mathbb{C},\mathbb{C}]$. I.e. they are natural transformations between endofunctors on $\mathbb{C}$.

First we verify the diagram for the unit.

For the left triangle, we have that $G(\epsilon_{FC}) \circ \eta_{GFC} = id_{GFC}$. For the right triangle, we have that $G(\epsilon_{FC}) \circ GF\eta_C = G(\epsilon_{FC} \circ F(\eta_C)) = G(id_{FC}) = id_{GFC}$.

The second diagram we need to check is the following. We need to verify that `associativity of multiplication': $$ G(\epsilon_{FC}) \circ GFG(\epsilon_{FC}) = G(\epsilon_{FC}) \circ G(\epsilon_{FGFC}). $$

However, here is where I'm stuck, does someone know the approach to verify this equation?

$\endgroup$
2
$\begingroup$

Use naturality of $\varepsilon:FG\Rightarrow 1_{\Bbb D}$ with the arrow $\varepsilon_{FC}$: $$\matrix{FG\,FGFC & \overset{\varepsilon_{FGFC}}\longrightarrow & FGFC \\ {\scriptstyle FG\,\varepsilon_{FC}}\downarrow\phantom{\scriptstyle FG\, \varepsilon_{FC}} && \phantom{\scriptstyle \varepsilon_{FC}} \downarrow {\scriptstyle \varepsilon_{FC}}\\ FGFC & \underset{\varepsilon_{FC}}\longrightarrow & FC}$$ and apply $G$ on this commutative square.

$\endgroup$
  • $\begingroup$ That's it, thanks! Just wondering, how do you draw diagrams on stack exchange? $\endgroup$ – Ordinalz Nov 3 at 13:36
  • $\begingroup$ You can right-click and see the latex code, alternatively you can initiate an edit to view it, then cancel. By the way, I use \matrix. $\endgroup$ – Berci Nov 3 at 13:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.