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