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 and functors and . are said to be adjoint i.e if there exists a natural isomorphism of Hom-sets for all . Equivalently, by the unit=counit definition, if there exists the pair of natural transformations (unit) and (counit) which satisfy the following commutative diagrams:

Throughout the post, I’ll represent natural transformations by the symbol . 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 is a natural transformation of functors whose components are given by for an object in . If is another functor, then I’ll represent the components of the induced natural transformation by .

If instead, there is a functor , then I’ll represent the components of the natural transformation by where is an object in .

# Monad

Let’s say that is an endofunctor equppied with two natural transformations (unit) and 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 where and , then we can consider the following endofunctor on defined form .

For the unit ,we use the unit obtained from the unit-counit definition, i.e . Define the multiplication 2-cell by . Essentially we have to verify the following commutative square commutes.

Now, notice that this is just the diagram obtained by applying the functor to the naturality square of on (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 , equipped with multiplication and the unit . 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 of , called the carrier and define an algebra over the monad as follows:

An algebra over a monad is the pair where is a morphism called the structure map in which satisfies the following commutative diagrams.

If we think of our endofunctor as a way of assigning formal expressions of type consisting of elements of type . If is the category of sets then $. Immediately, one can make sense of the morphism . The unit assigns an ‘atomic’ expression for .

The map 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 to the atomic expression, we get back the element by the axiom. . But what does the multiplication mean?

represents formal expressions over formal expressions. The multiplication map which returns a formal expression from a formal expression over a formal expression. Phew!

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

Consider the vector spaces generated by sets. The endofunctor takes a set and returns all finite linear combinations obtained from the elements of . Every element of looks like 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 . An element of looks like

The coherence axioms basically say that first reducing the inner sums involving and lifting to the entire sum to get is the same thing as first reducing to get a linear combination over elements of through the map and then evaluating. This is just associativity and distributivity of and .

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

where the unit and multiplication map are given as follows:

sends where is the unit of . Multiplication is given by . Verifying that the axioms hold is trivial.

So, we have a monad . 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 which satisfies and 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 and where are the evaluation maps and are the defining objects of the algebra. A morphism between the algebras is a morphism 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 is simple. It is just the category of all algebras over where the morphisms are exactly the ones defined above. We call this category where is just the category on which the endofunctor is defined. We have just constructed a free object. We have a forgetful functor which takes a and returns the defining object . maps a morphism between T algebras to a morphism between their defining objects.

For the right adjoint, consider the functor which sends an object to the data where is the evaluation map obtained from the component of the multiplication natural transformation on the monad. All the axioms follow from the definition of a monad. also takes a morphism to the morphism between algebras .

Now, we simply need to check that this an adjunction. Let’s evalaute and and see what we get:

and

It seems like one can define the unit as literally the exact same unit used for the monad, that is, a natural transformation . What about the counit?Well, we have the evaluation map . Hmm, that’s great but that is just the defining obejct, does it extend to a morphism of algebras?

That follows directly from the definition of an algebra over a monad using the map . Now notice that the counit-unit triangular identities are:

The left diagram commutes from the forgetful functor . All that remains to see is that in the second diagram that 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 , let’s call the Kleisli category whose objects are the objects of .

If are two objects in then there exists a morphism if there exists a morphism in from to the ‘higher type’ of , that is, a morphism . Succinctly,

Now, we just need a rule for composition. Consider two maps and $g:Y \to TZ$ where we write the corresponding maps in instead of for simplicity. Define by

The identity morphism is just obtained from the unit map of the monad,i.e .

It may be best to just reframe the language a little for convenience. If is a morphism in , then define as

where is the multiplication map of the monad.

In particular, this means that the composite in the Kleisli category. Also, we have by defintion of composition.

A Kleisli triple is the following data:

- A map
- An object map on
- For every map , a map , 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. 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 defined by and

for . The notation is a little misleading as is mapped to a function of type which corresponds to a morphism . I just felt that this is cleaner.

Now, consider a functor where and which sends a morphism to .

We get that . So, . The composition on objects is trivial. The unit of the adjunction is simply the unit of the monad whereas the counit is . I leave it to the reader to check that this is an adjunction.

you are a god in math dude

LikeLike