###### Theorem (Fakir)

Let $C$ be a complete, well-powered category, and let $M:C\to C$ be a monad with unit $u:1\to M$ and multiplication $m:MM\to M$. Then there is a universal idempotent monad, giving a right adjoint to

$\mathrm{IdempotentMonad}\left(C\right)↪\mathrm{Monad}\left(C\right)$IdempotentMonad(C) \hookrightarrow Monad(C)
###### Proof

Given a monad $M$, define a functor $M\prime$ as the equalizer $Mu$ and $uM$:

$M\prime ↪M\stackrel{\stackrel{uM}{\to }}{\underset{Mu}{\to }}MM.$M' \hookrightarrow M \stackrel{\overset{u M}{\to}}{\underset{M u}{\to}} M M.

This $M\prime$ acquires a monad structure (lemma; proof given below). It might not be an idempotent monad (although it will be if $M$ is left exact). However we can apply the process again, and continue transfinitely. Define ${M}_{0}=M$, and if ${M}_{\alpha }$ has been defined, put ${M}_{\alpha +1}={M}_{\alpha }\prime$; at limit ordinals $\beta$, define ${M}_{\beta }$ to be the inverse limit of the chain

$\dots ↪{M}_{\alpha }↪\dots ↪M$\ldots \hookrightarrow M_{\alpha} \hookrightarrow \ldots \hookrightarrow M

where $\alpha$ ranges over ordinals less than $\beta$.

Since $C$ is well-powered (i.e., since each object has only a small number of subobjects), the large limit

$E\left(M\right)\left(c\right)=\underset{\alpha \in \mathrm{Ord}}{\mathrm{lim}}{M}_{\alpha }\left(c\right)$E(M)(c) = \underset{\alpha \in Ord}{\lim} M_\alpha(c)

exists for each $c$. Hence the large limit $E\left(M\right)=\underset{\alpha \in \mathrm{Ord}}{\mathrm{lim}}{M}_{\alpha }$ exists as an endofunctor. The underlying functor

$\mathrm{Monad}\left(C\right)\to \mathrm{Endo}\left(C\right)$Monad(C) \to Endo(C)

reflects limits (irrespective of size), so $E=E\left(M\right)$ acquires a monad structure defined by the limit. Let $\eta :1\to E$ be the unit and $\mu :EE\to E$ the multiplication of $E$.

• Claim: $E$ is idempotent.

For this it suffices to check that $\eta E=E\eta :E\to EE$. This may be checked objectwise. So fix an object $c$, and for that particular $c$, choose $\alpha$ so large that projections ${\pi }_{\alpha }\left(c\right):E\left(c\right)\to {M}_{\alpha }\left(c\right)$ and ${\pi }_{\alpha }E\left(c\right):EE\left(c\right)\to {M}_{\alpha }E\left(c\right)$ are isomorphisms. Clearly then ${u}_{\alpha }{M}_{\alpha }\left(c\right)={M}_{\alpha }{u}_{\alpha }c$, since ${\pi }_{\alpha }:E\to {M}_{\alpha }$ factors through the equalizer ${M}_{\alpha +1}↪{M}_{\alpha }$. Then, since ${\pi }_{\alpha }$ is a monad morphism, we have

$\begin{array}{ccc}\eta E\left(c\right)& =& \left({\pi }_{\alpha }{\pi }_{\alpha }\left(c\right){\right)}^{-1}\left(u{M}_{\alpha }\left(c\right)\right){\pi }_{c}\\ & =& \left({\pi }_{\alpha }{\pi }_{\alpha }\left(c\right){\right)}^{-1}\left({M}_{\alpha }u\left(c\right)\right){\pi }_{c}\\ & =& E\eta \left(c\right)\end{array}$\array{ \eta E(c) & = & (\pi_\alpha \pi_\alpha (c))^{-1} (u M_\alpha(c))\pi_c \\ & = & (\pi_\alpha \pi_\alpha (c))^{-1} (M_\alpha u(c))\pi_c \\ & = & E \eta(c) }

as required.

Finally we must check that $M↦E\left(M\right)$ satisfies the appropriate universal property. Suppose $T$ is an idempotent monad with unit $v$, and let $\varphi :T\to M$ be a monad map. We define $T\to {M}_{\alpha }$ by induction: given ${\varphi }_{\alpha }:T\to {M}_{\alpha }$, we have

$\left({u}_{\alpha }{M}_{\alpha }\right){\varphi }_{\alpha }={\varphi }_{\alpha }{\varphi }_{\alpha }\left(vT\right)={\varphi }_{\alpha }{\varphi }_{\alpha }\left(Tv\right)=\left({M}_{\alpha }{u}_{\alpha }\right){\varphi }_{\alpha }$(u_\alpha M_\alpha)\phi_\alpha = \phi_\alpha \phi_\alpha (v T) = \phi_\alpha \phi_\alpha (T v) = (M_\alpha u_{\alpha})\phi_\alpha

so that ${\varphi }_{\alpha }$ factors uniquely through the inclusion ${M}_{\alpha +1}↪{M}_{\alpha }$. This defines ${\varphi }_{\alpha +1}:T\to {M}_{\alpha +1}$; this is a monad map. The definition of ${\varphi }_{\alpha }$ at limit ordinals, where ${M}_{\alpha }$ is a limit monad, is clear. Hence $T\to M$ factors (uniquely) through the inclusion $E\left(M\right)↪M$, as was to be shown.

See also this MathOverflow discussion. The discussion is reprised in the proof below (using the notation of the present article).

###### Proof of lemma

By naturality of the unit $u$, we have that $u:{1}_{C}\to M$ equalizes the pair $Mu,uM:M\stackrel{\to }{\to }MM$. Thus $u$ factorizes uniquely through the equalizer $i:M\prime \to M$ as $u=i\circ u\prime$; this defines the unit $u\prime :{1}_{C}\to M\prime$. We define a multiplication $m\prime :M\prime M\prime \to M\prime$ as the unique map that renders the left square below commutative:

$\begin{array}{ccccc}M\prime M\prime & \stackrel{iM\prime }{\to }& MM\prime & \stackrel{\stackrel{uMM\prime }{\to }}{\underset{MuM\prime }{\to }}& MMM\prime \\ {}_{m\prime }↓& & {}_{m\circ Mi}↓& & {↓}_{Mm\circ MMi}\\ M\prime & \underset{i}{\to }& M& \stackrel{\stackrel{uM}{\to }}{\underset{Mu}{\to }}& MM\end{array}$\array{ M' M' & \stackrel{i M'}{\to} & M M' & \stackrel{\overset{u M M'}{\to}}{\underset{M u M'}{\to}} & M M M' \\ _\mathllap{m'} \downarrow & & _\mathllap{m \circ M i} \downarrow & & \downarrow _\mathrlap{M m \circ M M i} \\ M' & \underset{i}{\to} & M & \stackrel{\overset{u M}{\to}}{\underset{M u}{\to}} & M M }

where the existence of $m\prime$ is ensured by showing that $m\circ Mi\circ iM\prime$ equalizes the pair $uM,Mu$. This in turn follows if we show that the right square is serially commutative. The top square of the series (involving components of $uM$) commutes by naturality of $u$. To see that the bottom square (involving components of $Mu$) commutes, notice that both legs of the square are $M$-algebra maps, and so (by freeness of the domain $MM\prime$) it suffices to check the claim that

$Mm\circ MMi\circ MuM\prime \circ uM\prime =Mu\circ m\circ Mi\circ uM\prime .$M m \circ M M i \circ M u M' \circ u M' = M u \circ m \circ M i \circ u M'.

But the left-hand side is

$\begin{array}{ccc}M\left(m\circ Mi\circ uM\prime \right)\circ uM\prime & =& uM\circ \left(m\circ Mi\circ uM\prime \right)\\ & =& uM\circ \left(m\circ uM\circ i\right)\\ & =& uM\circ i\end{array}$\array{ M(m \circ M i \circ u M') \circ u M' & = & u M \circ (m \circ M i \circ u M') \\ & = & u M \circ (m \circ u M \circ i) \\ & = & u M \circ i }

whereas the right-hand side is

$Mu\circ m\circ uM\circ i=Mu\circ i$M u \circ m \circ u M \circ i = M u \circ i

and since $uM\circ i=Mu\circ i$, the claim is verified.

From there, the monad axioms are tedious but straightforward to verify. (I may come back to this later.)

Revised on November 8, 2013 08:25:20 by Todd Trimble