Todd Trimble
Associated idempotent monad of a monad

Proof

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

This $M\prime$ acquires a monad structure. 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

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 \mathrm{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 :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 }(c):E(c)\to M_{\alpha }(c)$ and ${\pi }_{\alpha }E(c):EE(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 $\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

so that ${\varphi }_{\alpha }$ factors uniquely through the inclusion $M_{\alpha +1}\hookrightarrow 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(M)\hookrightarrow M$, as was to be shown.