Todd Trimble
Associated idempotent monad of a monad

Theorem (Fakir)

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

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

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

MMMuuMMM.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 α has been defined, put M α+1=M α; at limit ordinals β, define M β to be the inverse limit of the chain

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

where α ranges over ordinals less than β.

Since C 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 c. Hence the large limit E(M)=limαOrdM α 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) acquires a monad structure defined by the limit. Let η:1E be the unit and μ:EEE the multiplication of E.

  • Claim: E is idempotent.

For this it suffices to check that ηE=Eη:EEE. This may be checked objectwise. So fix an object c, and for that particular c, choose α so large that projections π α(c):E(c)M α(c) and π αE(c):EE(c)M αE(c) are isomorphisms. Clearly then u αM α(c)=M αu αc, since π α:EM α factors through the equalizer M α+1M α. Then, since π α 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) satisfies the appropriate universal property. Suppose T is an idempotent monad with unit v, and let ϕ:TM be a monad map. We define TM α by induction: given ϕ α:TM α, 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 ϕ α factors uniquely through the inclusion M α+1M α. This defines ϕ α+1:TM α+1; this is a monad map. The definition of ϕ α at limit ordinals, where M α is a limit monad, is clear. Hence TM factors (uniquely) through the inclusion E(M)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 CM equalizes the pair Mu,uM:MMM. Thus u factorizes uniquely through the equalizer i:MM as u=iu; this defines the unit u:1 CM. We define a multiplication m:MMM 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 m is ensured by showing that mMiiM equalizes the pair uM,Mu. This in turn follows if we show that the right square is serially commutative. The top square of the series (involving components of uM) commutes by naturality of u. To see that the bottom square (involving components of Mu) commutes, notice that both legs of the square are M-algebra maps, and so (by freeness of the domain MM) 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=Mui, 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