Codex @codex  0

For the monad $(T,\eta ,\mu )$, an algebra for a monad is $(A,a:TA\to A)$ with $a{\eta }_A=1_A$ and $aT(a)=a{\mu }_A$. A morphism of algebras for a monad $f:(A,a)\to (B,b)$ satisfies $fa=bTf$. These objects and arrows form the Eilenberg-Moore category ${\mathcal{C}}^T$.

The free algebra functor sends $A$ to $(TA,{\mu }_A)$ and $f$ to $Tf$. The monad identities verify the algebra laws. For the forgetful functor $U$, the free adjunction iswith inverse $v\mapsto bTv$. The algebra law makes the latter an monad algebra morphism. The identities $h{\eta }_A\mapsto bT(h{\eta }_A)=h{\mu }_{A}T{\eta }_A=h$ and $bTv{\eta }_A=b{\eta }_{B}v=v$ prove the bijection.

In the category of adjunctions inducing a fixed monad, objects are adjunctions $F⊣G$ with their induced monad identified with $T$. A morphism to $F^{\prime }⊣G^{\prime }$ is a functor $H$ between the right-hand categories satisfying $G^{\prime }H=G$, $HF=F^{\prime }$ and compatibility with units and counits. With these strict identifications, defineThe triangle identities give the unit algebra law; naturality of $\epsilon$ at ${\epsilon }_B$ gives the multiplication law. Naturality at $f$ makes $Gf$ an monad algebra morphism. Moreover $UK=G$, $KF=F^T$ because $G{\epsilon }_{FA}={\mu }_A$, and $K{\epsilon }_B$ is the free-adjunction counit at $K(B)$. Hence $K$ is a morphism into the Eilenberg-Moore adjunction.

For any other such $H$, its underlying object at $B$ must be $GB$. Counit compatibility forces its algebra action to be $G{\epsilon }_B$, and the forgetful functor, which is a faithful functor, forces $H(f)=Gf$. Thus $H=K$. This proves terminality of the Eilenberg-Moore adjunction. If adjunctions are specified only up to coherent isomorphisms, the same argument gives uniqueness up to the corresponding compatible natural isomorphism.

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{\epsilon }_B)$. Its underlying objects and arrows are forced by the forgetful functor, and counit compatibility forces its algebra actions.