Todd Trimble
Associated idempotent monad of a monad

Theorem (Fakir)

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

IdempotentMonad(C)Monad(C)IdempotentMonad(C) \hookrightarrow Monad(C)

Given a monad MM, define a functor MM' as the equalizer MuM u and uMu M:

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

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

M αM\ldots \hookrightarrow M_{\alpha} \hookrightarrow \ldots \hookrightarrow M

where α\alpha ranges over ordinals less than β\beta.

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

E(M)(c)=limαOrdM α(c)E(M)(c) = \underset{\alpha \in Ord}{\lim} M_\alpha(c)

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

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

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

  • Claim: EE is idempotent.

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

ηE(c) = (π απ α(c)) 1(uM α(c))π c = (π απ α(c)) 1(M αu(c))π c = Eη(c)\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 ME(M)M \mapsto E(M) satisfies the appropriate universal property. Suppose TT is an idempotent monad with unit vv, and let ϕ:TM\phi: T \to M be a monad map. We define TM αT \to M_\alpha by induction: given ϕ α:TM α\phi_\alpha: T \to M_\alpha, we have

(u αM α)ϕ α=ϕ αϕ α(vT)=ϕ αϕ α(Tv)=(M αu α)ϕ α(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 α+1M αM_{\alpha + 1} \hookrightarrow M_\alpha. This defines ϕ α+1:TM α+1\phi_{\alpha + 1}: T \to M_{\alpha + 1}; this is a monad map. The definition of ϕ α\phi_\alpha at limit ordinals, where M αM_\alpha is a limit monad, is clear. Hence TMT \to M factors (uniquely) through the inclusion E(M)ME(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 uu, we have that u:1 CMu: 1_C \to M equalizes the pair Mu,uM:MMMM u, u M: M \stackrel{\to}{\to} M M. Thus uu factorizes uniquely through the equalizer i:MMi: M' \to M as u=iuu = i \circ u'; this defines the unit u:1 CMu': 1_C \to M'. We define a multiplication m:MMMm': M' M' \to M' as the unique map that renders the left square below commutative:

MM iM MM MuMuMM MMM m mMi MmMMi M i M MuuM MM\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 mm' is ensured by showing that mMiiMm \circ M i \circ i M' equalizes the pair uM,Muu 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 uMu M) commutes by naturality of uu. To see that the bottom square (involving components of MuM u) commutes, notice that both legs of the square are MM-algebra maps, and so (by freeness of the domain MMM M') it suffices to check the claim that

MmMMiMuMuM=MumMiuM.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

M(mMiuM)uM = uM(mMiuM) = uM(muMi) = uMi\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

MumuMi=MuiM u \circ m \circ u M \circ i = M u \circ i

and since uMi=Muiu 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 at 08:25:20 by Todd Trimble