Terminality of the Eilenberg-Moore adjunction
= Terminality of the Eilenberg-Moore adjunction
The free-forgetful <adjunction> for the <Eilenberg-Moore category> is terminal in the <category of adjunctions inducing a fixed monad>. The unique <morphism> into it is the <Eilenberg-Moore comparison functor> $B\mapsto(GB,G\varepsilon_B)$. Its underlying objects and arrows are forced by the forgetful <functor>, and counit compatibility forces its algebra actions.