Restriction of monad algebras ($(A,a:TA\to A)⟼(A,a{\alpha }_A:SA\to A)$)

A monad morphism $\alpha :S\Rightarrow T$ induces a functor ${\mathcal{C}}^T\to {\mathcal{C}}^S$ between Eilenberg-Moore categories, identical on underlying objects and arrows. Its unit equation gives the restricted algebra's unit law. Naturality and the multiplication equation give $(a{\alpha }_A)S(a{\alpha }_A)=aTa{\alpha }_{TA}S{\alpha }_A=a{\mu }_A^{T}T{\alpha }_A{\alpha }_{SA}=a{\alpha }_A{\mu }_A^S$. Naturality also preserves algebra morphisms.