# Eilenberg Moore category

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?

-
On morphisms just Ff=Tf, no need for ordered pair, because morphism of T-algebras is just morphism in $C$ with some aditional properties. –  rafaelm Feb 26 '13 at 0:01
One way of "coding up" the Kleisli category in Haskell is to take the types as objects and functions a -> m b as morphisms from a to b. In a sense a "codes up" the free m algebra on a. When it comes to Eilenberg-Moore you can't take that route since you can't pair a type with a value in Haskell. What approach were you aiming for? –  Tom Ellis Feb 26 '13 at 22:05
@TomEllis Something like newtype Algebra t a = Algebra (t a -> a) and newtype Morphism t a b = Morphism (a -> b) - so you don't actually need to pair a type with a value, it's implicit in the definition. So given an algebra $(a,h:Ta \to a)$ and a morphism $f:a\to b$ you can't actually return the algebra that the morphism maps to, but you can check that some morphism $f:a\to b$ is an algebra homomorphism between $(a,h:Ta\to a)$ and $(b,k:Tb\to b)$ by checking (modulo newtypes) that $k\circ Tf = f\circ h$. –  Chris Taylor Feb 26 '13 at 22:20
Did you manage to construct E-M categories in Haskell? I'd be quite interested. –  Petr Pudlák Apr 1 at 20:05

I think there is no $\_$ at all:

Let $(A,h)$ and $(B,k)$ be $T$-algebras, then an arrow $f:A\to B$ itself is said to be a homomorphism, if $Tf$ and $f$ commute with $h$ and $k$.

You only have to check that $Ff:=Tf$ satisfies this commutativity condition.

-
I suppose my issue is that I'm actually trying to implement these things - my intuition was that an algebra homomorphism should be a function that returns $(B,k)$ when given $(A,h)$, but clearly that doesn't have to be the case. –  Chris Taylor Feb 26 '13 at 9:36

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$.

-