Verifying that an adjunction induces a monad structure

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?

Solution 1:

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.