Associated idempotent monad of a monad

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

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).

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