Solution (source code)

= Solution

For the <monad> $\mathbb T=(T,\eta,\mu)$ define the <free algebra functor> by
$$
F^{\mathbb T}X=(TX,\mu_X),\qquad F^{\mathbb T}f=Tf.
$$
The unit and associativity identities of the <monad> make $(TX,\mu_X)$ an <algebra for a monad>, and <naturality> of $\mu$ makes $Tf$ a <morphism of algebras for a monad>. Let $G^{\mathbb T}$ be the <forgetful functor>. For $(A,a)$ in the <Eilenberg-Moore category>, set
$$
\Phi(h)=h\eta_X,\qquad \Psi(f)=a\,Tf.
$$
The inverse candidate is a <monad algebra morphism>, since
$$
a\,Tf\,\mu_X=a\mu_A\,T^2f=a\,Ta\,T^2f
=a\,T(a\,Tf).
$$
The two composites are identities:
$$
\Phi\Psi(f)=a\eta_Af=f,\qquad
\Psi\Phi(h)=a\,Th\,T\eta_X=h\mu_X\,T\eta_X=h.
$$
These use respectively the <unit law for a monad algebra>, the algebra-morphism equation, and a unit identity of the <monad>. The formulas commute with precomposition in $X$ and postcomposition by <monad algebra morphisms>, so they form a <natural bijection>. Therefore \b[the free-algebra functor is left adjoint to forgetting]:
$$
\boxed{\mathcal X^{\mathbb T}(F^{\mathbb T}X,(A,a))\cong\mathcal X(X,A),
\qquad F^{\mathbb T}\dashv G^{\mathbb T}.}
$$
Its <adjunction unit> is $\eta_X$, and its <adjunction counit> at $(A,a)$ is $a:(TA,\mu_A)\to(A,a)$.