I've been trying to code up the Eilenberg-Moore category for a monad in Haskell.
As I understand it, given a category $C$ and a monad $(T,\eta,\mu)$ on $C$ we build the Eilenberg-Moore category $C^T$ as the category whose objects are algebras on $a$, i.e. pairs consisting of an object $a$ of $C$ and a map $h:Ta\to a$ satisfying some properties, and whose morphisms are algebra homomorphisms.
The functor $G:C^T \to C$ is a forgetful functor that acts like
$$G(a,h:Ta \to a) = a$$
$$G(f:a\to b,\, g:(Ta\to a)\to(Tb\to b)) = f$$
The functor $F:C\to C^T$ acts on objects as
$$Fa = (Ta,\,\mu)$$
but I don't understand what it does to morphisms. I have
$$Ff = (Tf,\, \_ )$$
but I don't understand what goes in the _.
I need to create something of type $(T(Ta) \to Ta)\to (T(Tb)\to Tb)$ out of
$$\mu:T(Ta)\to Ta$$
$$\eta:a\to Ta$$
$$f:a\to b$$
$$T:(a\to b)\to (Ta\to Tb)$$
But I can't see how to do it. I suppose one option would be the function that takes every algebra $h$ to $\mu$, i.e.
$$Ff = (Tf, \lambda h.\mu)$$
but I'm not even convinced that's an algebra homomorphism. Am I missing something?
Best Answer
The effect of the left adjoint $F$ on morphisms is already determined by the universal property of the units of the adjunction: given a map $f: x \to y$, consider the diagram
$$\matrix{ x & \mathop{\longrightarrow}\limits^{\eta_x} & GFx \cr {\scriptstyle f} \big\downarrow {\ } & & \cr y & \mathop{\longrightarrow}\limits_{\eta_y} & GFy \cr} $$
and let $Ff: Fx\to Fy$ be the unique map that corresponds to the composite $\eta_y\circ f: x\to GFy$.
In your example, if $(a,h:Ta\to a)$ is a $T$-algebra, a map $g: x\to a$ corresponds to $h\circ Tg: (Tx,\mu_x)\to (a,h)$ and consequently, for $f: x\to y$ we obtain:
$Ff = \mu_y\circ T(\eta_y\circ f) = \mu_y\circ T\eta_y \circ Tf = Tf$.