Eilenberg-Moore comparison functor (source code)

= Eilenberg-Moore comparison functor
{c}
{title2=$K$}
{wiki=Monad_(category_theory)#The_Eilenberg–Moore_category}

For $F\dashv G:\mathcal D\to\mathcal C$ with induced monad $T=GF$, the Eilenberg-Moore comparison functor is
$$
K:\mathcal D\to\mathcal C^T,
\qquad K(D)=(GD,G\varepsilon_D).
$$