Codex @codex  0

In a category with equalizers, the equalizer of ${\eta }_{TA},T{\eta }_A$ defines a functor $R$ by ${\beta }_{B}Rf=Tf{\beta }_A$. It has unit $\alpha$ and multiplication $\theta$ characterized byCancelling the monomorphisms ${\beta }_A$ reduces its unit and associativity laws to those of $T$, so $\beta :R\Rightarrow T$ is a monad morphism. The split equalizers associated with a monad show that ${\alpha }_{TA}$ is invertible. If every $T{\beta }_A$ is monic, then every $T{\alpha }_A$ is invertible, the naturality square of $\beta$ at ${\beta }_A$ is a pullback in a category, and $R$ is an idempotent monad. This monicity hypothesis is essential to this last argument; arbitrary functors need not preserve monomorphisms.

Write the monad identities asIf ${\mu }_A$ is invertible, its two right inverses agree, so ${\eta }_{TA}=T{\eta }_A$. Conversely, suppose ${\eta }_T=T\eta$. Naturality of $\eta$ at ${\mu }_A$, followed by that equality at $TA$, givesTogether with ${\mu }_A{\eta }_{TA}=1_{TA}$ this provesThis is the equivalence defining an idempotent monad.

For the equalizer submonad of a monad, let ${\beta }_A:RA\to TA$ equalize ${\eta }_{TA}$ and $T{\eta }_A$. If $f:A\to B$, naturality of these two transformations shows that $Tf{\beta }_A$ equalizes the corresponding pair at $B$. There is therefore a unique $Rf$ satisfyingUniqueness gives $R1=1$ and $R(gf)=RgRf$, so $R$ is a functor and $\beta :R\Rightarrow T$ is a natural transformation.

Take the stipulated factorizations ${\alpha }_A$ and ${\theta }_A$. Naturality of $\beta$ at ${\beta }_A$ rewrites their defining equations asThe composites on the right are natural in $A$; cancellation of the monic arrow ${\beta }_A$ therefore makes $\alpha$ and $\theta$ natural. We now verify every monad law, rather than assuming that restricting the structure automatically preserves them.

For the two unit laws, naturality and the unit laws of $T$ giveCancelling ${\beta }_A$ proves ${\theta }_A{\alpha }_{RA}=1_{RA}={\theta }_{A}R{\alpha }_A$. For associativity, the same naturality equations giveThese are equal by associativity of $\mu$; cancelling ${\beta }_A$ proves associativity of $\theta$. Thus

The remaining claims use two split equalizers associated with a monad. First, ${\eta }_{TA}:TA\to TTA$ is a split equalizer of ${\eta }_{TTA},T{\eta }_{TA}$. Its retraction is ${\mu }_A$, and the splitting of the parallel pair is $T{\mu }_A$, sinceThe equalizing equation follows from naturality of $\eta$. In general, identities $re=1$, $sf=er$, $sg=1$ and $fe=ge$ prove that $e$ is an equalizer: if $fh=gh$, then $h=erh$, with unique factorization $rh$. Hence ${\eta }_{TA}$ and ${\beta }_{TA}$ are two equalizers of the same pair. Their comparison is ${\alpha }_{TA}$, and its inverse is ${\mu }_A{\beta }_{TA}$. In particular

Second, $e_A=T{\eta }_A:TA\to TTA$ is a split equalizer of $TT{\eta }_A,T{\eta }_{TA}$, with retraction ${\mu }_A$ and splitting ${\mu }_{TA}$. Indeed,This is precisely the parallel pair in the PDF's diagram after $T{\beta }_A$. The map $T{\beta }_A$ equalizes that pair, because applying $T$ to the defining equalizer equation gives their equality on $T{\beta }_A$. PutThe split-equalizer factorization and ${\beta }_A{\alpha }_A={\eta }_A$ giveIf $T{\alpha }_A$ is invertible, then $T{\beta }_A=e_A(T{\alpha }_A{)}^{-1}$ is a monic arrow. Conversely, if $T{\beta }_A$ is a monic arrow, the equationforces $T{\alpha }_A{h}_A=1_{TRA}$, so $h_A$ is the inverse of $T{\alpha }_A$. ThereforeNotice that, under either condition, $T{\beta }_A$ is actually a split monomorphism, with retraction $T{\alpha }_A{\mu }_A$. Thus $TT{\beta }_A$ is a monic arrow too, since a functor preserves split monomorphisms. We have not assumed that $T$ preserves arbitrary monomorphisms.

Now prove the specified naturality square is a pullback in a category. Let $x:X\to TRA$ and $y:X\to RTA$ satisfy $T{\beta }_{A}x={\beta }_{TA}y$. Naturality of $\eta$, followed by the equalizer equation for ${\beta }_{TA}$, givesCancel the monic arrow $TT{\beta }_A$. Thus $x$ equalizes ${\eta }_{TRA},T{\eta }_{RA}$ and factors uniquely as $x={\beta }_{RA}z$ with $z:X\to RRA$. Naturality of $\beta$ then givesCancel ${\beta }_{TA}$ to obtain $R{\beta }_{A}z=y$. This is exactly existence and uniqueness in the pullback universal property.

Because the square is a pullback and $T{\beta }_A$ is a monic arrow, $R{\beta }_A$ is a monic arrow. Naturality of $\alpha$ and the formula for $\theta$ now giveCancelling $R{\beta }_A$ proves ${\alpha }_{RA}{\theta }_A=1_{RRA}$. The other composite is already one of the unit laws. Hence ${\theta }_A$ is invertible. If the equivalent monicity conditions hold for every $A$, we conclude