Monads I: The Eilenberg-Moore category, Adjunction and Kleisli categories

This series(probably three posts) will be on the monad. The first part will deal with only an introduction to monads, algebras over moands and the adjunction problem . The second part will deal with coequalizers and Beck’s theorem in connection with Kleisli categories. In keeping with this blog’s slight CS tilt, the third part will deal with examples of monads from functional programming which I think are crucial to wholly understand the monad. I’ve noticed that I am running too many ‘series posts’ simultaneously. I am still working on the third part of the Grothendieck Spectral Sequence series and will continue the Hopf fibration post which I haven’t updated for a year!


I think that before I continue to introduce the main players of today’s post, I should review the definitions of an adjoint functor as it’ll be quite useful as a tool to see the power of monads.

Consider two categories C,D and functors F:D \to C and G:C \to D. F,G are said to be adjoint i.e F \dashv G if there exists a natural isomorphism of Hom-sets Hom-{C}(Fd,c) \simeq Hom_{D}(d,Gc) for all d \in D,c \in C. Equivalently, by the unit=counit definition, if there exists the pair of natural transformations \eta:1_{D} \Rightarrow GF(unit) and \epsilon:FG \Rightarrow 1_{C}(counit) which satisfy the following commutative diagrams:



Throughout the post, I’ll represent natural transformations by the symbol \Rightarrow. I recommend the confused reader to refer to Aluffi’s Algebra Chapter 0 book in the section on category theory and also my post on the importance of adjoint functors.

If \eta:F \Rightarrow G is a natural transformation of functors F,G: A \to B whose components are given by \eta_{X}:F(X) \to G(X) for an object X in A. If T:B \to C is another functor, then I’ll represent the components of the induced natural transformation HF \Rightarrow HG by (H\eta)_{X}=H(\eta_{X}).

If instead, there is a functor T:Z \to A, then I’ll represent the components of the natural transformation \eta Z:ZF \to ZG by (\eta Z)_{X}=\eta_{Z(X)} where X is an object in Z.


Let’s say that T:C \to C is an endofunctor equppied with two natural transformations \eta:1_{C} \Rightarrow T(unit) and \mu:TT \Rightarrow T such that the following diagrams commute:



The commutative diagram is a kind of generalization of associativity. I direct the reader to the nlab page to learn more about the basics of it. Much of the importance of monads is derived from its connection to adjoint functors and its connection to programming paradigms(see continuation monad for more information).

Let’s see how monads are connected to adjoint functors.

Consider an adjunction of functors  F \dashv G where F:D \to C and G:C \to C, then we can consider the following endofunctor on D defined form F,G.

T:D \to D :=G \circ F

For the unit \eta,we use the unit obtained from the unit-counit definition, i.e \eta:1_{D} \Rightarrow GF=T. Define the multiplication 2-cell \mu by \mu=G \circ \epsilon \circ F:GFGF=TT \to GF=T. Essentially we have to verify the following commutative square commutes.



Now, notice that this is just the diagram obtained by applying the functor g to the naturality square of \epsilon: FG \Rightarrow 1_{C} on F \circ G \circ F(Take some time to actually digest that).

Now, commutativity of the original square follows by definition of naturality.

As for the verification of the unit map commutative square given by


These are exactly one gets on combining the triangle identities for the unit-counit definition.

The next question is: Can one derive an adjunction from every monad?Thankfully, the answer is yes as we’ll soon see.

Algebra over a monad

So, let’s recall the data at hand. We have our endofunctor T:C \to C, equipped with multiplication \mu:TT \Rightarrow T and the unit \eta:1_{C} \to T. This data is collectively called a monad.

What does an ‘algebra over a monad’ even mean in this context. Obviously, whatever this is, we expect it to conform with the unit and multiplication maps. We first pick a particular object Aof C, called the carrier and define an algebra over the monad as follows:

An algebra over a monad T is the pair (A,v) where v:T(A) \to A is a morphism called the structure map in C which satisfies the following commutative diagrams.



If we think of our endofunctor T as a way of assigning formal expressions of type T consisting of elements of type A. If C is the category of sets then $. Immediately, one can make sense of the morphism v:T(A) \to A. The unit \eta:A \to T(A) assigns an ‘atomic’ expression "a" for a \in A.

The map v:T(A) \to A can be understood as evaluating expressions built from these expressions.

The coherence axioms for an algebra over a monad make sense in the following manner:

If we apply v to the atomic expression, we get back the element by the axiom. v(\eta_{A}(a))=a. But what does the multiplication mean?

T(T(A)) represents formal expressions over formal expressions. The multiplication map \mu:T(T(A)) \to T(A) which returns a formal expression from a formal expression over a formal expression. Phew!

What do the axioms say?They say that applying \mu to a formal expression over a formal expression reduces to a formal expression. Applying the evaluation map v to this result is the same as thing as lifting the evaluation map through Tand then evaluating. One nice example of this lies in vector spaces.

Consider the vector spaces generated by sets. The endofunctor T takes a set X and returns all finite linear combinations obtained from the elements of X. Every element of T(X) looks like a_{1}x_{1} + \cdots+a_{n}x_{n} where the $a_{i}$ lie in some field.  An evaluation map $v:T(X) \to X$ essentially tells us that we can consider this linear combination to be in X. An element of T(T(X)) looks like

b_{1}(a_{1,1}x_{1}+\cdots+a_{1,n_{1}})+\cdots+b_{n}(a_{n,1}x_{1}+\cdots +a_{n_{m}})

The coherence axioms basically say that first reducing the inner sums involving a_{i}'s and lifting to the entire sum to get b_{1}A_{1}+\cdots +b_{n}A_{n} is the same thing as first reducing b_{i}a_{i,j} to get a linear combination over elements of X through the map \mu and then evaluating. This is just associativity and distributivity of + and X.

Let’s look at another example which I find more interesting. Consider a group G and a set X and consider an endofunctor T on Set given by:

T(X)=G \times X where the unit and multiplication map are given as follows:

\eta : X \to G \times X sends x \mapsto (e,x) where e is the unit of G. Multiplication is \mu: G \times (G \times X) \to G \times G given by (g_{1},(g_{2},x)) \mapsto (g_{1}g_{2},x). Verifying that the axioms hold is trivial.

So, we have a monad (T,\eta,\mu). The important question here is: What is an algebra over this monad? Let’s explicitly write out everything to see it.

First, we have an evaluation map v: T(X) \to X which satisfies h(g_{1}g_{2},x)=h(g_{1},h(g_{2},x)) and h(e,x)=x which is exactly the condition for a group action! and the first condition is the ‘associativity of the action’. It is this interpretation of action which is atleast partially useful in understanding the algebra over a monad even in the general case.

Morphism between algebras over a monad

Consider two algebras over a monad represented by (A,v_{A}) and (B,v_{B}) where v are the evaluation maps and A,B are the defining objects of the algebra. A morphism between the algebras is a morphism f:A \to B which ‘commutes with both actions’, that is it satisfies the following commutative diagram:



Eilenberg-Moore category, deriving monads from adjoint situations

Now, we get to the meat of topic. We show that every monad has an associated adjunction. The Eilenberg-Moore category of a monad (T,\eta,\mu) is simple. It is just the category of all algebras over T where the morphisms are exactly the ones defined above. We call this category C^{T} where C is just the category on which the endofunctor T is defined. We have just constructed a free object. We have a forgetful functor G^{T}:C^{T} \to C which takes a T-algebra (A,v) and returns the defining object AG^{T} maps a morphism between T algebras to a morphism between their defining objects.

For the right adjoint, consider the functor F^{T} which sends an object X to the data (TX, \mu_{X}) where \mu_{X} is the evaluation map obtained from the component of the multiplication natural transformation \mu:TT \to T on X the monad. All the axioms follow from the definition of a monad. F^{T} also takes a morphism X_{1} \to X_{2} to the morphism between T-algebras Tf:T(X_{1}) \to T(X_{2}).

Now, we simply need to check that this an adjunction. Let’s evalaute G^{T}F^{T} and F^{T}G^{T} and see what we get:

G^{T}F^{T}(X)=G^{T}(TX,\mu_{X})=TX and


It seems like one can define the unit as literally the exact same unit used for the monad, that is, a natural transformation \eta: 1_{C} \Rightarrow T. What about the counit?Well, we have the evaluation map v:T(X) \to X. Hmm, that’s great but that is just the defining obejct, does it extend to a morphism of T-algebras?

That follows directly from the definition of an algebra over a monad using the map v_{T(X)}=\mu_{X}:TT(X) \to T(X). Now notice that the counit-unit triangular identities are:


The left diagram commutes from the forgetful functor G^{T}. All that remains to see is that in the second diagram that \mu_{X}=v_{T(X)} which we just proved above.

Klesili category

The interesting thing is that we have another solution to the question whcih we just answered: Does every monad arise from an adjoint situation?

The Kleisli Categroy is a more ‘natural’ answer to the above problem and also has some interesting interpretations in computer science which I’ll talk about at the end. For a monad on a category C, let’s call the Kleisli category C_{T} whose objects are the objects of C.

If x_{T},y_{T} are two objects in C_{T} then there exists a morphism f:x_{T} \to y_{T} if there exists a morphism in C from x_{T} to the ‘higher type’ of y, that is, a morphism x \to T(y). Succinctly,


Now, we just need a rule for composition. Consider two maps f:X \to TY and $g:Y \to TZ$ where we write the corresponding maps in C instead of C_{T} for simplicity. Define g \circ f:X \to TZ by

g \circ f=\mu_{Z} \circ T(g) \circ f

The identity morphism is just obtained from the unit map of the monad,i.e Id_{C^{T}}=(\eta_{X})^{*}.

It may be best to just reframe the language a little for convenience. If f:X \to TY is a morphism in C, then define f^{*}:TX \to TY as

f^{*}=\mu_{Y} \circ Tf where \mu is the multiplication map of the monad.

In particular, this means that the composite g \circ_{T} \circ f= g^{*} \circ f in the Kleisli category. Also, we have (g^{*} \circ_{T} f)*=g^{*} \circ f^{*} by defintion of composition.

A Kleisli triple (T,\eta,*) is the following data:

  1. A map \eta_{X}: X \to T(X)
  2. An object map T on C
  3. For every map f:X \to TY, a map f^{*}:TX \to TY, which we call the type lifting map or lifting map in short.

All the data of the monad lies in the Kleisli triple. Note that multiplication is packaged in the third axiom. This is also the standard definition of a monad in functional programming. T can essentially be thought of as a wrapper function. Anyways, I’ll get to that in the next post.

Adjunction from Kleisli Category

Consider the functor F:X \to X_{T} defined by F(X)=X_{T} and

for f: X \to Y,F(f)=(\mu_{Y} \circ f). The notation is a little misleading as f is mapped to a function of type X \to TY which corresponds to a morphism X_{T} \to Y_{T}. I just felt that this is cleaner.

Now, consider a functor G:C_{T} \to C where G(X_{T})=TX and which sends a morphism f':X_{T} \to Y_{T} to G(f')=\mu_{Y} \circ Tf'=f'^{*}.

We get that GF(f)=G((\nu_{Y} \circ f))=\mu_{Y} \circ T\eta_{Y} \circ Tf=id_{TY} \circ Tf=Tf. So, GF=T. The composition on objects is trivial. The unit of the adjunction is simply the unit of the monad whereas the counit is \epsilon=1_{TY}^{*}:(TY)_{T} \to Y_{T}. I leave it to the reader to check that this is an adjunction.





One thought on “Monads I: The Eilenberg-Moore category, Adjunction and Kleisli categories”

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s