Tell me more ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.
up vote 4 down vote favorite
1

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?

share|improve this question
2  
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 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 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 at 22:20

2 Answers

up vote 2 down vote accepted

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.

share|improve this answer
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 at 9:36
up vote 3 down vote

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

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.