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: M M \to M$. Then there is a universal idempotent monad, giving a right adjoint to

$IdempotentMonad(C) \hookrightarrow Monad(C)$
Proof

Given a monad $M$, define a functor $M'$ as the equalizer $M u$ and $u M$:

$M' \hookrightarrow M \stackrel{\overset{u M}{\to}}{\underset{M u}{\to}} M M.$

This $M'$ 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}'$; at limit ordinals $\beta$, define $M_\beta$ to be the inverse limit of the chain

$\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(M)(c) = \underset{\alpha \in Ord}{\lim} M_\alpha(c)$

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

$Monad(C) \to Endo(C)$

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

• Claim: $E$ is idempotent.

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

$\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 \mapsto E(M)$ satisfies the appropriate universal property. Suppose $T$ is an idempotent monad with unit $v$, and let $\phi: T \to M$ be a monad map. We define $T \to M_\alpha$ by induction: given $\phi_\alpha: T \to M_\alpha$, we have

$(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 $\phi_{\alpha}$ factors uniquely through the inclusion $M_{\alpha + 1} \hookrightarrow M_\alpha$. This defines $\phi_{\alpha + 1}: T \to M_{\alpha + 1}$; this is a monad map. The definition of $\phi_\alpha$ at limit ordinals, where $M_\alpha$ is a limit monad, is clear. Hence $T \to M$ factors (uniquely) through the inclusion $E(M) \hookrightarrow 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 $M u, u M: M \stackrel{\to}{\to} M M$. Thus $u$ factorizes uniquely through the equalizer $i: M' \to M$ as $u = i \circ u'$; this defines the unit $u': 1_C \to M'$. We define a multiplication $m': M' M' \to M'$ as the unique map that renders the left square below commutative:

$\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'$ is ensured by showing that $m \circ M i \circ i M'$ equalizes the pair $u M, M u$. This in turn follows if we show that the right square is serially commutative. The top square of the series (involving components of $u M$) commutes by naturality of $u$. To see that the bottom square (involving components of $M u$) commutes, notice that both legs of the square are $M$-algebra maps, and so (by freeness of the domain $M M'$) it suffices to check the claim that

$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

$\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

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

and since $u M \circ i = M u \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