= Monad algebra forgetful functor creates limits
{title2=$p_i a=a_iT(p_i)$}
Given a diagram of <algebras for a monad>, take any chosen limit $L$ of its underlying diagram. The displayed equations uniquely determine $a:TL\to L$, because their right-hand sides form a cone. Joint monicity of the limit projections proves $a\eta_L=1$ and $aT(a)=a\mu_L$. The same projection argument proves that every induced mediating map preserves the algebra action. Thus the forgetful functor strictly creates this limit with the prescribed underlying cone, without assuming the monad preserves limits.
Back to article page
