Todd Trimble Associated idempotent monad of a monad

Proof

Given a monad $M$, define a functor $M'$ as the equalizer $M u$ and $u 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

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

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

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

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

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.

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:

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

But the left-hand side is

whereas the right-hand side is

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