Proving the equivalence of different definitions for idempotent monads

217 Views Asked by At

Let $T \in C^C$ be a monad with multiplication $\mu : T^2 \to T$ and unit $\eta : 1_C \to T$. I am trying to prove that the following definitions for an idempotent monad are equivalent,

  1. The arrows $(\mu_c)_{c \in C}$ are monomorphisms.
  2. $\mu$ is a natural isomorphism.
  3. $T\eta = \eta T$.

Since $\mu T\eta = 1_C$, the components of $\mu$ are always split epis and this proves $(1) \Rightarrow (2)$, and the implication $(2) \Rightarrow (3)$ is simply because $ \mu T \eta = 1_C = \mu \eta T$ and so by inspecting the equality component by component and using that each $\mu_c$ is a monomorphism, we get $T \eta = \eta T$.

Finally, I'm left with $(3) \Rightarrow (1)$ which I haven't managed to prove. Considering a pair of arrows $a,b : c \to T^2x$ such that $\mu a = \mu b$, I don't see how to relate $(3)$ with $\mu$, as in the 'monad diagrams' the latter is involved by post composing and thus the only way I see of 'cancelling it' is via intercalating $\eta T$. An entry on the $n$Lab gives a proof/reference, but it uses terms which I haven't yet covered. I'd appreciate any hints which can help me go in the right direction, without (much) additional theory. Thanks in advance!

1

There are 1 best solutions below

1
On BEST ANSWER

Following Arnaud's hint, I think I have found an answer: fixing a component $\mu_x : T^2x \to Tx$, an instinctive choice for a left inverse would be $\eta_{Tx} : Tx \to T^2x$. By naturality of $\eta$, we have that

$$ \eta_{Tx}\mu_x = T\mu_x\eta_{T^2x} $$

and the latter is in fact the identity because $(T,\mu, \eta)$ is a monad and we are assuming $(3)$:

$$ T\mu_x\eta_{T^2x} = T\mu_x (\eta T)_{Tx} \stackrel{(3)}{=} T\mu_x (T \eta)_{Tx} = T(\mu_x\eta_{Tx}) = T((\mu \cdot \eta T)_x) = T(1_{Tx}) = 1_{T^2x}. $$