Equalizer submonad of a monad (source code)

= Equalizer submonad of a monad
{title2=$\beta_A:RA\longrightarrow TA$}

In a <category> with <equalizers>, the equalizer of $\eta_{TA},T\eta_A$ defines a <functor> $R$ by $\beta_BRf=Tf\beta_A$. It has unit $\alpha$ and multiplication $\theta$ characterized by
$$
\beta_A\alpha_A=\eta_A,\qquad \beta_A\theta_A=\mu_AT\beta_A\beta_{RA}.
$$
Cancelling 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.