stringdiagram

Commutative Monads

We saw the two double strength natural transformations in the previous post:

$\mathsf{dst}, \mathsf{dst}' : \mathbb{T}(A) \otimes \mathbb{T}(B) \rightarrow \mathbb(T)(A \otimes B)$

A commutative monad is a strong monad for which $\mathsf{dst} = \mathsf{dst}'$ . We saw last time that the list monad is not commutative, but the powerset monad is. In this post we will restrict ourselves to examining some more instructive examples. This will help build our intuitions, and the examples lay the groundwork for discussions in later posts.

Example: For a set $E$ , there is a monad with:

Endofunctor: $(-) + E$ .
Unit: The unit maps an element into the left component of the coproduct $x \mapsto (1,x)$ .
Multiplication: The multiplication: $\mu_X : (X + E) + E \Rightarrow X + E$ does the “obvious thing”, $(1,(1,x)) \mapsto (1,x)$ , $(1,(2,e)) \mapsto (2,e)$ and $(2,e) \mapsto (2,e)$ .

The monad is sometimes referred to as the exception monad. Computationally, we can interpret a Kleisli morphism $X \rightarrow Y + E$ as a function that transforms elements of $X$ to elements of $Y$ , but may return error or exception values captured by $E$ . The first double strength for this monad is defined by the following cases:

$\mathsf{dst}((1,x), (1,y)) = (1, (x,y))$ .
$\mathsf{dst}((2,e),(1,y)) = (2,e)$ .
$\mathsf{dst}((1,x),(2,e)) = (2,e)$ .
$\mathsf{dst}((1,e_1),(1,e_2)) = (2,e_2)$ .

Notice that exception values are preferred, but there is rather arbitrary choice that has to be made in the fourth case. The second double strength agrees with the first, except for the final case, where it makes the other choice of exception to prefer:

$\mathsf{dst}'((1,e_1),(1,e_2)) = (2,e_1)$ .

So we see that the exception monad is only commutative if there’s exactly one exception. This special case is sometimes referred to as the maybe monad, as computationally it encodes functions that may fail.

Example: The multiset monad is commutative. To describe this, we shall introduce the notation

$\{ x_1 : k_1,\ldots, x_n : k_n \}$

for a multiset where element $x_i$ appears with multiplicity $k_i$ . The action of both double strength maps sends the pair of multisets:

$(\{ x_1 : k_1, \ldots, x_n : k_n \}, \{ y_1 : l_1,\ldots, y_m : l_m \})$

to the multiset:

$\{ (x_i , y_j) : k_i \times l_j \mid 1 \leq i \leq n, 1 \leq j \leq m \}$ .

The multiset monad is (isomorphic to) the Abelian monoid monad, so this monad is also commutative.

Example: Another monad that occurs commonly in practice is the finite probability monad on $\mathsf{Set}$ . This has:

Endofunctor: $\mathbb{D}(X)$ has elements finitely supported formal convex sums $\sum_i p_i x_i$ . These are weighted sum of elements of $X$ such that for each weight $p_i$ , $1 \leq p_i \leq 1$ , $\sum_i p_i = 1$ and only finitely many $p_i$ are non-zero. Alternatively, these can be thought of as functions $X \rightarrow [0,1]$ satisfying the previous conditions on the weights.
Unit: $\eta_X(x) = x$ . That is, the unit maps an element of $X$ to the corresponding trivial sum.
Multiplication: $\mu_X(\sum_i p_i (\sum_j q_{i,j} x_{i,j})) = \sum_i \sum_j (p_i \times q_{i,j}) x_{i,j}$ . This is simply flattening out a sum of sums.

This monad is commutative, with the action of both double strengths being:

$(\sum_i p_i x_i, \sum_j q_j y_j) \mapsto \sum_i \sum_j (p_i \times q_j) (x_i,y_j)$

For example:

$(\frac{1}{4}x + \frac{3}{4}x', \frac{1}{3} y + \frac{2}{3} y') \mapsto \frac{1}{12}(x,y) + \frac{1}{4}(x',y) + \frac{1}{6}(x,y') + \frac{1}{2}(x',y')$

In the next post we will explore a slightly misleading intuition that is commonly hinted at in the literature.

Other Monad Strengths

Last time, we saw the notion of strength for a monad. These were natural transformations

$A \otimes \mathbb{T}(B) \rightarrow \mathbb{T}(A \otimes B)$

which interact well with the monoidal and monad structure. As was mentioned last time, there are other ways we might consider commuting a functor with a monoidal structure. The obvious first choice is to consider a natural transformation of type

$\mathbb{T}(A) \otimes B \rightarrow \mathbb{T}(A \otimes B)$

again, interacting sensibly with the monoidal and monad structure (as before, we leave the details of what this means aside, to concentrate on the main ideas). Such a natural transformation is called a left-strength, denoted $\mathsf{st}'$ . The strength is often referred to as a right-strength for emphasis.

Example: If $\mathcal{V}$ is a symmetric monoidal category we can build a right-strength from a left-strength

$\mathsf{st}_{A,B} : A \otimes \mathbb{T}(B) \rightarrow \mathbb{T}(A \otimes B)$

as the composite:

$\mathbb{T}(A) \otimes B \xrightarrow{\sigma_{\mathbb{T}(A),B}} B \otimes \mathbb{T}(A) \xrightarrow{\mathsf{st}_{B,A}} \mathbb{T}(B \otimes A) \xrightarrow{\mathbb{T}(\sigma_{B,A})} \mathbb{T}(A \otimes B)$

Here $\sigma$ is the symmetry isomorphism from the symmetric monoidal structure. Intuitively, we just swap the inputs, use the strength and swap them back again.

As we know every $\mathsf{Set}$ monad is strong in a unique way, so it also has a unique left-strength. For example, the left-strength for the list monad acts as follows:

$([a_1,\ldots,a_n],b) \mapsto [(a_1,b),\ldots,(a_n,b)]$

Unsurprisingly, the left-strength for the powerset is very similar, visually we just swap square (list formation) brackets for curly (set formation) brackets.

$(\{a_1,\ldots,a_n\},b) \mapsto \{(a_1,b),\ldots,(a_n,b)\}$

We can consider left-strengths beyond symmetric monoidal categories, as their definition does not require the existence of a right-strength. In the cases that will be of interest to us, it will be the interplay between left and right strengths that will matter. To keep things simple, we will assume we are working in a symmetric monoidal category, so the left-strength can be derived from the right-strength (or vice-versa), as in the example above. (To move beyond this setting, we would need to assume further compatibility conditions between any choice of left and right strength, which are automatic when one is derived from the other via a monoidal symmetry.)

Once we have a right-strength $\mathsf{st}$ and a left-strength $\mathsf{st}'$ , we can build a natural transformation of type $\mathbb{T}(A) \otimes \mathbb{T}(B) \rightarrow \mathbb{T}(A \otimes B)$ . In fact, there are two ways we can do this, either by applying the right-strength first:

$\mathsf{dst} = \mathbb{T}(A) \otimes \mathbb{T}(B) \xrightarrow{\mathsf{st}_{A,B}} \mathbb{T}(\mathbb{T}(A) \otimes B) \xrightarrow{\mathbb{T}(\mathsf{st}'_{A,B})} \mathbb{T}^2(A\otimes B) \xrightarrow{\mu_{A \otimes B}} \mathbb{T}(A \otimes B)$

or applying the left-strength first:

$\mathsf{dst}' = \mathbb{T}(A) \otimes \mathbb{T}(B) \xrightarrow{\mathsf{st}'_{A,B}} \mathbb{T}(A \otimes \mathbb{T}(B)) \xrightarrow{\mathbb{T}(\mathsf{st}_{A,B})} \mathbb{T}^2(A \otimes B) \xrightarrow{\mu_{A \otimes B}} \mathbb{T}(A \otimes B)$

Both these composites are referred to as double strengths. Whenever we see two composites of the same type in category theory, it is natural to consider if they are always the same.

Example: For the list monad, we have:

$\mathsf{dst}([a,b],[c,d]) = [(a,c),(b,c),(a,d),(b,d)]$

whereas

$\mathsf{dst}'([a,b],[c,d]) = [(a,c),(a,d),(b,c),(b,d)]$

notice the difference in the order of the middle two elements.

On the other hand, for the powerset monad, essentially because there is no ordering in subsets:

$\mathsf{dst}(\{a,b\},\{c,d\}) = \mathsf{dst}'(\{a,b\},\{c,d\}) = \{(a,c),(b,c),(a,d),(b,d) \}$

This is not an isolated example, for the powerset monad $\mathsf{dst} = \mathsf{dst}'$ .

The previous examples show us that in general $\mathsf{dst} \neq \mathsf{dst}'$ , but the two composites may agree for some monads. This question, and its implications are another key topic in the theory of monads. We shall begin exploring the details in the next post.

A Note on Terminology

An earlier version of this post used the term costrength for what is termed a left-strength above. This terminology does not align well with the conventional use of “co” in category theory. Thanks to @varkor on mathstodon for persuading me that I should move to the more modern terminology.

There is also a discussion about this terminology on the NLab.

Strong Monads

Strong monads, the topic of this post, are a somewhat technical looking topic at first glance, requiring more definitions and machinery than we have seen up until now. Unfortunately, they are key to some more interesting topics, both mathematically and in terms of computer science application. As usual when dealing with new abstract ideas, it is useful to focus on intuitions and examples to get a feeling for the formal definitions. This post is longer than might be ideal, but there are plenty of examples.

For those interested in the technical details I skip, some recommended reading:

Monoidal categories: “Categories for the Working Mathematician” by Mac Lane has a very readable account of monoidal categories, despite its reputation for requiring a lot of mathematical background.
Enriched categories: Both volume 2 of Borceux’s “Handbook of Categorical Algebra”, and Riehl’s “Categorical Homotopy Theory” have brief introductions to monoidal categories, to set up a concise introduction to enriched category theory. The standard reference for enriched category theory is Kelly’s “Basic Concepts of Enriched Category Theory”, which also contains the necessary background on monoidal categories. This book can be difficult in places, but the material we require is covered at a reasonable pace.

Monoidal Categories

A monoidal category is a category $\mathcal{V}$ with a monoidal product bifunctor, typically denoted $\otimes$ , and a unit object, $I$ . Intuitively, this is a generalization of the notion of monoid from sets to categories. There are isomorphisms

$\lambda : I \otimes A \rightarrow A \qquad \rho : A \otimes I \rightarrow A$ ,

natural in $A$ , and referred to as the left and right unitor respectively. These encode that $I$ acts as a unit for the multiplication, up to isomorphism. There are also associator isomorphisms:

$\alpha : (A \otimes B) \otimes C \rightarrow A \otimes (B \otimes C)$ ,

natural in $A, B, C$ , encoding associativity up to isomorphism. The unitors and associator are required to satisfy some compatibility equations (referred to as coherence conditions). We won’t need the details, but they can be found in any standard category theory reference.

A symmetric monoidal category is a monoidal category with a further symmetry isomorphisms encoding commutativity up to isomorphism:

$\sigma : A \otimes B \rightarrow B \otimes A$

natural in $A,B$ . Again, the symmetry is required to satisfy some coherence conditions (equations) with respect to the other structure. Finally, a (symmetric) monoidal closed category is a (symmetric) monoidal category such that for each object $A$ , there is an adjunction:

$(-) \otimes A \dashv A \multimap (-)$

Example: Any category $\mathcal{C}$ with products is a symmetric monoidal category, with

$A \otimes B = A \times B \qquad I = 1$

The left and right unitors, associator and symmetry are the “obvious” canonical maps induced by the universal property of products. If $\mathcal{C}$ is Cartesian closed, then it is symmetric monoidal closed, with $A \multimap (-)$ given by the exponential $A \Rightarrow (-)$ .

In particular, the category $\mathsf{Set}$ is symmetric monoidal closed with monoidal product given by Cartesian products, and $A \multimap (-)$ given by the function space functor $A \Rightarrow (-)$ . This is the motivating example for much of what follows, and of practical interest in algebraic examples we shall see later. When working with $\mathsf{Set}$ , if not otherwise stated the monoidal structure is taken to be the Cartesian product structure.

Strength

For a monoidal category $\mathcal{V}$ , and endofunctor $T: \mathcal{V} \rightarrow \mathcal{V}$ , a strength (sometimes referred to as a tensorial strength) for $T$ is a natural transformation

$\mathsf{st}_{A,B} : A \otimes T(B) \rightarrow T(A \otimes B)$

which satisfies two coherence conditions with respect to the monoidal structure. A strong functor is a functor with a chosen strength. A strong monad is monad $\mathbb{T}$ with a strong underlying endofunctor, satisfying additional coherence conditions with respect to the monad unit and multiplication. Again, the actual coherence conditions can be found in standard sources, we shall focus on examples and intuitions.

Example: The list and powerset monads are both strong in a unique way, with strengths:

$(a, [b_1,\ldots,b_n]) \mapsto [(a,b_1),\ldots,(a,b_n)]$

$(a, \{ b_1,\ldots, b_n \}) \mapsto \{ (a,b_1), \ldots, (a,b_n) \}$

We shall shortly see that form (and uniqueness) of the strengths for the $\mathsf{Set}$ monads in the previous example are in no way special.

So a crude first sketch of a strength is that it is a well-behaved way of commuting an endofunctor and a monoidal product. You may notice that there are other ways you might imagine commuting an endofunctor with a monoidal product. We shall return to that thought in later posts.

To get a more principled mathematical perspective on strength, unfortunately we need to introduce further abstract machinery.

Enriched Categories

Enriched category theory is a large and potentially complex topic. Fortunately we will only need a few of the basic definitions, and no deep theory. The idea of an enriched category is that often for a category $\mathcal{C}$ , the homsets $\mathcal{C}(A,B)$ carry additional mathematical structure, and this structure interacts well with composition. For example:

Example: The homsets in the category $\mathsf{Pre}$ of preorders and monotone maps actually carry a natural pointwise order:

$f \leq g \Leftrightarrow \forall a. f(a) \leq g(a)$ .

This structure satisfies:

$f_1 \leq f_2 \;\wedge\; g_1 \leq g_2 \quad\Rightarrow\quad g_1 \circ f_1 \leq g_2 \leq f_2$

when the composites are well-defined. So the homsets are actually $\mathsf{Pre}$ -objects, and the composition maps are $\mathsf{Pre}$ -morphisms

$\mathsf{Pre}(B,C) \times \mathsf{Pre}(A,B) \rightarrow \mathsf{Pre}(A,B)$

A close relative of the previous example is the following:

Example: The homsets of the category of all (small) categories $\mathsf{Cat}$ are themselves categories, with morphisms the natural transformations. Furthermore, the composition maps are bifunctors

$\mathsf{Set}(B,C) \times \mathsf{Set}(A,B) \rightarrow \mathsf{Set}(A,C)$

An important trivial example is the following:

Example: The homsets of the category $\mathsf{Set}$ are $\mathsf{Set}$ -objects, and the composition maps are $\mathsf{Set}$ -morphisms

$\mathsf{Set}(B,C) \times \mathsf{(Set}(A,B) \rightarrow \mathsf{Set}(A,B)$

Finally, a slightly different example, which motivates the level of generalization of the formal definition.

Example: The homsets of the category of Abelian groups $\mathsf{Ab}$ can be given the structure of Abelian groups pointwise. With this structure, the composition maps satisfy:

$(g_1 + g_2) \circ f = (g_1 \circ f) + (g_2 \circ f) \qquad 0 \circ f = 0$

and the dual conditions for precomposition. This is not the same as saying the composition maps are $\mathsf{Ab}$ morphisms:

$\mathsf{Ab}(B,C) \times \mathsf{Ab}(A,B) \rightarrow \mathbb{Ab}(A,C)$

This temporarily breaks the pattern with the previous examples. However, there is a monoidal structure on $\mathsf{Ab}$ such that the composition maps are $\mathsf{Ab}$ -morphisms

$\mathsf{Ab}(B,C) \otimes \mathsf{Ab}(A,B) \rightarrow \mathsf{Ab}(A,C)$

In fact this monoidal structure arises via some rather beautiful monad theory, which we will hopefully get to in later posts.

The final example motivates defining enriched categories so that the hom objects can live in monoidal categories.

For a monoidal category $\mathcal{V}$ , a $\mathcal{V}$ -enriched category $\mathcal{C}$ has:

A collection of objects $A,B,\ldots$
For each pair of objects $A,B$ , a hom object $\mathcal{C}(A,B)$ in $\mathcal{V}$ .
For each object $A$ , a morphism $j_A : I \rightarrow \mathcal{C}(A,A)$ . Intuitively, these encode the the identities in the category.
For each triple of objects $A,B,C$ , a morphism $m_{A,B,C} : \mathcal{C}(B,C)\otimes \mathcal{C}(A,B) \rightarrow \mathcal{C}(A,C)$ . These encode composition of morphisms with the enriched category.

This data must satisfy some axioms, ensuring that composition is associative and has units the identities. In fact, some mathematical structures that are far away from our motivating examples are also enriched categories. The original surprising example was that a mild generalization of metric spaces can be seen as enriched categories, as shown by Lawvere.

Example: For any monoidal closed category $\mathcal{V}$ , we can regard $\mathcal{V}$ as a $\mathcal{V}$ -category, with hom objects

$\mathcal{V}(A,B) = A \multimap B$

The identity and composition maps are derived in a reasonably routine way, and can be found in standard sources. This is usually described as $\mathcal{V}$ being canonically enriched over itself.

To connect the worlds of ordinary and enriched categories, note that any $\mathcal{V}$ -category $\mathcal{C}$ , has an underlying ordinary category $\mathcal{C}_0$ , with the same objects, and homsets:

$\mathcal{C}_0(A,B) = \mathcal{V}(I, \mathcal{C}(A,B))$

Composition and identities in $\mathcal{V}_0$ are defined in a natural way. Strictly speaking, to give an enrichment for an ordinary category $\mathcal{C}$ is to give a $\mathcal{V}$ -category $\mathcal{C}'$ , and a specified isomorphism $\mathcal{C} \cong \mathcal{C}'_0$ . Generally, this isomorphism is ignored when there is a natural choice.

Once we’ve defined a new class of objects, we should consider the morphisms between them. A $\mathcal{V}$ -functor $F : \mathcal{C} \rightarrow \mathcal{D}$ consists of:

A mapping $F$ from $\mathcal{C}$ -objects to $\mathcal{D}$ -objects.
For each pair of $\mathcal{C}$ -objects, a $\mathcal{V}$ -morphism $\varphi_{A,B} : \mathcal{C}(A,B) \rightarrow \mathcal{D}(F(A),F(B))$ . Intuitively, these describe the action on morphisms of the functor.

The morphism $\varphi_{A,B}$ are required to satisfy axioms generalizing the usual idea that identities and composition are preserved.

Example: For the constructions we have seen previous:

A $\mathsf{Pre}$ -enriched functor is a functor which is monotone, in that $f \leq g \;\Rightarrow\; F(f) \leq F(g)$ .
A $\mathsf{Cat}$ -enriched functor is a (strict) 2-functor.
A $\mathsf{Set}$ -functor is an ordinary functor.
A $\mathsf{Ab}$ -functor is a functor such that $F(0) = 0$ and $F(f + g) = F(f) + F(g)$ .

Again, it is helpful to connect back to the world of ordinary category theory. A $\mathcal{V}$ -functor $F : \mathcal{V} \rightarrow \mathcal{D}$ induces an ordinary functor $F_0 : \mathcal{C}_0 \rightarrow \mathcal{D}_0$ that agrees with $F$ on objects. Morphisms $f : A \rightarrow B$ in $\mathcal{C}_0$ are $\mathcal{V}$ -morphisms $\hat{f} : I \rightarrow \mathcal{C}(A,B)$ . Then $F_0(f)$ is given by:

$I \xrightarrow{\hat{f}} \mathcal{C}(A,B) \xrightarrow{\varphi_{A,B}} \mathcal{D}(F(A),F(B))$ .

A $\mathcal{V}$ -functor $F : \mathcal{C} \rightarrow \mathcal{D}$ is said to an enrichment of ordinary functor $F' : \mathcal{C}_0 \rightarrow \mathcal{D}_0$ if $F' = F_0$ .

Finally, a $\mathcal{V}$ -natural transformation $\alpha : F \Rightarrow G$ is a family of $\mathcal{V}$ -morphisms $\alpha_A : I \rightarrow \mathcal{D}(F(A),G(A))$ satisfying an axiom generalizing the usual notion of naturality to the enriched setting.

Strength and Enrichment

Finally, we are in a position to relate strength and enrichment. If $\mathcal{V}$ is a monoidal closed category, and $T : \mathcal{V} \rightarrow \mathcal{V}$ an ordinary endofunctor, giving a strength for $T$ is “the same thing as” giving a structure for $T$ as a $\mathcal{V}$ -functor.

Lets unpack this a bit. As described above, we view $\mathcal{V}$ as being canonically enriched over itself. Giving an enriched structure, sometimes referred to as a functorial strength, for $T$ is to give a natural family of morphisms:

$\varphi_{A,B} : A \multimap B \rightarrow T(A) \multimap T(B)$

compatible with the identity and composition maps. That these maps are natural in the sense of ordinary category is equivalent to being an enrichment of the ordinary functor $T$ is an important point that is often skimmed over.

To build such a family given a strength

$\mathsf{st}_{A,B} : A \otimes T(B) \rightarrow T(A \otimes B)$

we form the composite:

$A \multimap B \otimes T(A) \xrightarrow{\mathsf{st}_{A \multimap B, A}} T(A \multimap B \otimes A) \xrightarrow{T(\epsilon)} T(B)$

where $\epsilon$ is the counit of the adjunction, which can be seen as an evaluation morphism for function spaces. Taking the transpose of this morphism gives a map:

$A \multimap B \rightarrow T(A) \multimap T(B)$

It takes some checking, but these form the components of an enrichment for $T$ as required. In the other direction, given an enrichment, we can form the composite:

$A \xrightarrow{\eta} B \multimap (A \otimes B) \xrightarrow{\varphi_{B, A \otimes B}} T(B) \multimap T(A \otimes B)$

where $\eta$ is the unit of the adjunction. Taking the transpose of this morphism gives a map:

$A \otimes T(B) \rightarrow T(A \otimes B)$

Again, after a bit of checking, it can be seen that this results in a strength for $T$ . The passages in the two directions are mutually inverse, so for monoidal closed category $\mathcal{V}$ to give a strength for $T$ is equivalent to giving an enrichment for $T$ . This dealt with the endofunctor component, but we are really interested in monads. Here, to give a strength for a monad $\mathbb{T}$ on monoidal closed $\mathcal{V}$ is equivalent to giving an enrichment for $\mathbb{T}$ .

Example: As a special case of this result, as every $\mathsf{Set}$ monad is (trivially) enriched over $\mathsf{Set}$ in a unique way. Therefore, given the observations above, every $\mathsf{Set}$ monad has a unique strength. This has a concrete description as:

$\mathsf{st}_{A,B}(a,t) = \mathbb{T}(\lambda b. (a,b))(t)$

This formula can seem slightly magical if given without context, but it is arrived at by unravelling the strength derived from the unique enrichment. Here we use $\lambda$ notion to define a simple function. The strengths given for the list and powerset monads in the earlier example arise via this construction.

As usual, it is useful to think about algebra examples. For a monad $\mathbb{T}$ given by some equational presentation $(\Sigma,E)$ , the unique strength is given on representatives by:

$\mathsf{st}_{A,B}(a, [t]) = [t[(a,b) / b \mid b \in \mathsf{var}(t)]]$

where $\mathsf{var}(t)$ is the set of variables appearing in the representative term $t$ . As usual, square brackets are somewhat overloaded, denoting both equivalence classes and the substitution operation. In words – we replace each variable $b$ appearing in the representative term $t$ with the variable $(a,b)$ .

A Taste of Monadicity

Now we have encountered comparison functors, we can introduce another classical topic in monad theory, that of monadicity. A functor $U : \mathcal{D} \rightarrow \mathcal{C}$ is monadic if it has a left adjoint, and the Eilenberg-Moore comparison functor for the induced monad is an equivalence of categories. Monadicity is a big topic, with a lot of new concepts and results to digest. For now, we shall restrict ourselves to some introductory examples. Along the way, we shall introduce a new class of monads, the idempotent monads.

Example: For any equational presentation $(\Sigma,E)$ , the obvious forgetful functor $\mathsf{Alg(\Sigma,E)} \rightarrow \mathsf{Set}$ is monadic. This example motivates the term Eilenberg-Moore algebra. For example the category $\mathsf{Ab}$ of Abelian groups is monadic over $\mathsf{Set}$ .

The previous example is important for intuitions about monadic functors. Informally, it is common to think of monadicity as evidence that a category is “algebraic” in nature. For monadic functors $\mathcal{D} \rightarrow \mathsf{Set}$ , this idea can be made mathematically precise, which we may pursue in detail in a later post.

Example: A reflective subcategory is a full subcategory such that the inclusion functor has a left adjoint. It is useful to know a subcategory is reflective, for example completeness and cocompleteness properties can then be established from standard results.

Reflective subcategories correspond to a special class of the monads. Every reflective subcategory induces an idempotent monad, that is one who’s multiplication is an isomorphism. Furthermore, the Eilenberg-Moore category of an idempotent monad is equivalent to a reflective subcategory of the base category, so these concepts are tightly connected.

For example:

A group is said to be torsion free if $x^n = 1$ implies $x = 1$ . The category of torsion free Abelian groups is a reflective subcategory of the category of Abelian groups. The category $\mathsf{TFAb}$ of torsion free Abelian groups is a reflective subcategory of the category of Abelian groups $\mathsf{Ab}$ .
The category of Abelian groups is a reflective subcategory of the category of groups.
The category of symmetric graphs is a reflective subcategory of the category of graphs.

The corresponding monads are all idempotent.

The notion of idempotent monad has many equivalent characterisations, which we may discuss in a later post.

Of course, not every functor with a left adjoint is monadic, so it would be useful to see some counterexamples.

Counterexample: Let $\mathsf{Pre}$ be the category of preorders and monotone maps. There is an obvious forgetful functor $U: \mathsf{Pre} \rightarrow \mathsf{Set}$ , and this has a left adjoint such that $F(X)$ has underlying set $X$ , and for all $x_1, x_2 \in X$

$x_1 \leq x_2 \quad\Leftrightarrow\quad x_1 = x_2$

This is sometimes referred to as the discrete preorder. The composite $U \circ F$ is the identity monad. $\mathsf{Set}^{\mathsf{Id}}$ is equivalence to $\mathsf{Set}$ , which is certainly not equivalent to $\mathsf{Pre}$ .

The following is a well-known counterexample, refuting a natural conjecture.

Counterexample: Monadic functors are not closed under composition. As we have seen, the there are monadic functors $\mathsf{TFAb} \rightarrow \mathsf{Ab}$ and $\mathsf{Ab} \rightarrow \mathsf{Set}$ . The composite functor

$U : \mathsf{TFAb} \rightarrow \mathsf{Ab} \rightarrow \mathsf{Set}$

has a left adjoint given by composing the two component left adjoints, but is not monadic. To see this, consider the action of the left adjoint. The groups in the image of the adjoint $\mathsf{Set} \rightarrow \mathsf{Ab}$ are all torsion free. Therefore the functor $\mathsf{Ab} \rightarrow \mathsf{TFGrp}$ leaves them unchanged up to isomorphism. Therefore the composite functor

$F : \mathsf{Set} \rightarrow \mathsf{Ab} \rightarrow \mathsf{TFAb}$

maps a set to the free Abelian group over that set. The algebras of the induced monad are simply the Abelian groups, and so the composite forgetful functor is not monadic.

Why would we care if a functor is monadic?

There are a lot of standard theorems allowing is to derive nice properties of Eilenberg-Moore categories from properties of the monad and its base category. For example, we might be able to establish the presence of certain limits or colimits, or that the category is regular or locally finite presentable. In some concrete situations, it might be easier to establish these properties via direct calculation, but monadicity results allow us to work axiomatically, simultaneously deriving results that apply in many situations.

Example Laws and Liftings

We have now seen both Kleisli and Eilenberg-Moore laws, and their associated notions of lifted functor. Despite introducing the appropriate definitions, and sketching their key theoretical properties, we haven’t really seen any examples yet. That is the issue we now address.

A standard source of both Kleisli and Eilenberg-Moore laws are the monad morphisms $\sigma : \mathbb{S} \rightarrow \mathbb{T}$ . This can be seen as both

A Kleisli law of type $\mathsf{Id} \circ \mathbb{S} \Rightarrow \mathbb{T} \circ \mathsf{Id}$ .
An Eilenberg-Moore law of type $\mathbb{S} \circ \mathsf{Id} \Rightarrow \mathsf{Id} \circ \mathbb{T}$ .

Therefore, each monad morphism $\sigma$ induces both:

A functor $\underline{\mathsf{Id}} : \mathcal{C}_{\mathbb{S}} \rightarrow \mathcal{C}_{\mathbb{T}}$ such that $\underline{\mathsf{Id}} \circ F_{\mathbb{S}} = F_{\mathbb{T}}$ .
A functor $\overline{\mathsf{Id}}: \mathcal{C}^{\mathbb{T}} \rightarrow \mathcal{C}^{\mathbb{S}}$ such that $U_{\mathbb{S}} = U_{\mathbb{T}} \circ \overline{\mathsf{Id}}$ .

(Notice the difference in direction between the two).

Example: For every monad, the unit $\eta : \mathsf{Id} \Rightarrow \mathbb{T}$ is a monad morphism. For the identity monad there are obvious isomorphisms:

$\mathcal{C}_{\mathsf{Id}} \cong \mathcal{C} \cong \mathcal{C}^{\mathsf{Id}}$

Up to composition with these isomorphisms, the functor $\underline{\mathsf{Id}} : \mathcal{C}_{\mathsf{Id}} \rightarrow \mathcal{C}_{\mathbb{T}}$ is the usual Kleisli free functor, and the functor $\overline{\mathsf{Id}} : \mathcal{C}^{\mathbb{T}} \rightarrow \mathcal{C}^{\mathsf{Id}}$ is the usual Eilenberg-Moore forgetful functor.

As is a recurring theme, we should always consider what a new feature of monad theory means in terms of algebra.

Example: Consider two equational presentations over the same signature $(\Sigma, E), (\Sigma, E')$ such that $E \subseteq E'$ , with respective induced monads $\mathbb{S}, \mathbb{T}$ . Then for a set $A$ , every equivalence class of terms in $\mathbb{S}(A)$ is contained in an equivalence class of terms in $\mathbb{T}(A)$ , as the latter theory satisfies more equations. This induces a monad morphism:

$\mathbb{S} \Rightarrow \mathbb{T}$

The induced functor $\overline{\mathsf{Id}} : \mathsf{Set}^{\mathbb{T}} \rightarrow \mathsf{Set}^{\mathbb{S}}$ picks out the subcategory of $\mathbb{T}$ -algebras (which satisfy more equations), within the larger category of $\mathbb{S}$ -algebras. For example, every commutative monoid is a monoid.

As usual, we can consider the morphisms of $\mathsf{Set}_{\mathbb{S}}$ and $\mathsf{Set}_{\mathbb{T}}$ as families of equivalence classes of terms in the respective theories. From this point of view, every equivalence class in the weaker theory can be promoted to the enclosing one in the stronger theory. This is the behaviour of the induced functor $\underline{\mathsf{Id}} : \mathsf{Set}_{\mathbb{S}} \rightarrow \mathsf{Set}_{\mathbb{T}}$ . For example, the term $x + y$ in the theory of monoids will be mapped to an equivalence class including $y + x$ in the theory of commutative monoids.

We can also find examples beyond monad morphisms to show the greater generality is useful.

Example: For every monad, the multiplication $\mu : \mathbb{T} \circ \mathbb{T} \Rightarrow \mathbb{T}$ is both:

A Kleisli law of type $\mathbb{T} \circ \mathbb{T} \Rightarrow \mathsf{Id} \circ \mathbb{T}$ .
An Eilenberg-Moore law of type $\mathbb{T} \circ \mathbb{T} \Rightarrow \mathbb{T} \circ \mathsf{Id}$ .

Up to the isomorphisms discussed in the earlier example:

The induced functor $\underline{\mathbb{T}} : \mathcal{C}_{\mathbb{T}} \Rightarrow \mathcal{C}_{\mathsf{Id}}$ is the usual Kleisli forgetful functor.
The induced functor $\overline{\mathbb{T}} : \mathcal{C}^{\mathsf{Id}} \rightarrow \mathcal{C}^{\mathbb{T}}$ is the usual Eilenberg-Moore free functor.

Finally, we sketch a key source of examples that needs proper account at a later date.

Example: For a pair of monads $\mathbb{S}, \mathbb{T}$ on the same base category, a natural transformation:

$\lambda : \mathbb{S} \circ \mathbb{T} \Rightarrow \mathbb{T} \circ \mathbb{S}$

which is simultaneously an Eilenberg-Moore and a Kleisli is known as a distributive law. This is an important notion, introduced by Beck, which allows us to build up monads in a principled way, by composing other monads together. Given such a $\lambda$ , the endofunctor $\mathbb{T} \circ \mathbb{S}$ carries the structure of a monad in a particularly well-behaved way. (In general, composing the underlying functors of two monads can result in a functor that carries no monad structure at all).

The existence of suitable distributive laws allows us to work with monads in a modular fashion. This topic is too important to skim over, so we shall postpone further discussions until more detailed future posts.

Monads, Laws and Liftings

Now we have seen both the Kleisli and Eilenberg-Moore categories, it is interesting to consider how we might construct “nice” functors between them. To do so, we fix a pair of monads $\mathbb{S} : \mathcal{C} \rightarrow \mathcal{C}$ and $\mathbb{T} : \mathcal{D} \rightarrow \mathcal{D}$ , and a functor

$H : \mathcal{C} \rightarrow \mathcal{D}$

We shall then consider the Eilenberg-Moore and Kleisli constructions separately.

Eilenberg-Moore Laws

Can we construct a functor $\overline{H} : \mathcal{C}^{\mathbb{S}} \rightarrow \mathcal{D}^{\mathbb{T}}$ in some natural way? This question gives us a bit too much freedom to narrow things down, so we restrict attention to functors that interact well with the forgetful functors, in that:

$U^{\mathbb{T}} \circ \overline{H} = H \circ U^{\mathbb{S}}$

We shall call such a functor an Eilenberg-Moore lifting of $H$ . The condition above means

$\overline{H}(A, \mathbb{S}(A) \xrightarrow{\alpha} A) = (H(A), \mathbb{T}(H(A)) \xrightarrow{\alpha'} H(A)) \qquad \overline{H}(h) = H(h)$

Where we must determine a suitable $\alpha'$ . Applying $H$ to $\alpha$ as an obvious first step yields:

$H(\mathbb{S}(A)) \xrightarrow{H(\alpha)} H(A)$

The domain is of the wrong type. If we had a morphism

$\lambda : \mathbb{T}(H(A)) \rightarrow H(\mathbb{S}(A))$

we could form a composite of the right type:

$\mathbb{T}(H(A)) \xrightarrow{\lambda} H(\mathbb{S}(A)) \xrightarrow{H(\alpha)} H(A)$

To do this uniformly for all Eilenberg-Moore algebras, we require $\lambda$ be natural in $A$ . The action of $\overline{H}$ on objects is then:

$(A,\alpha) \mapsto (H(A), H(\alpha) \circ \lambda_A)$

If we attempt to establish the resulting structure map satisfies the unit and multiplication axioms, we find that $\lambda$ must interact well with the monad structures, in that the following two axioms hold:

Unit axiom: $H(\eta^{\mathbb{S}}) = \lambda \circ \eta^{\mathbb{T}}_H$ .
Multiplication axiom: $\lambda \circ (\mu^{\mathbb{T}}_{H}) = H(\mu^\mathbb{S}) \circ \lambda_\mathbb{S} \circ \mathbb{T}(\lambda)$ .

Such a $\lambda$ satisfying these axioms is referred to as an Eilenberg-Moore law. In fact, there is a bijective correspondence between:

Eilenberg-Moore liftings of $H$
Eilenberg-Moore laws $\mathbb{T} \circ H \Rightarrow H \circ \mathbb{S}$ .

Verifying this is a bit fiddly, but routine once you figure out how to construct the components of an Eilenberg-Moore law from a lifting. We shall skip the details.

Kleisli Laws

We now consider how to lift $H$ to a functor $\underline{H} : \mathcal{C}_{\mathbb{S}} \rightarrow \mathcal{D}_{\mathbb{T}}$ . Again, we need to constrain the problem further. In this case it turns out to be best to consider functors that interact well with the free constructions, in that:

$\underline{H} \circ F^{\mathbb{S}} = F^{\mathbb{T}} \circ H$

We shall call such a functor a Kleisli lifting of $H$ . The condition above forces that:

$\underline{H}(A) = A \qquad \underline{H}(f : A \xrightarrow{f} \mathbb{S}(B)) = H(A) \xrightarrow{f'} \mathbb{T}(H(A))$

Where it remains to determine a suitable $f'$ . Having seen the drill for the Eilenberg-Moore construction, an intuitive plan is to form a composite:

$H(A) \xrightarrow{H(f)} H(\mathbb{S}(A)) \xrightarrow{\lambda_A} \mathbb{T}(H(B))$

for some natural transformation $\lambda : H \circ \mathbb{S} \Rightarrow \mathbb{T} \circ H$ . Of course, we need to verify that this mapping is functorial. In doing so, we find the need for the following axioms:

Unit axiom: $\lambda \circ H(\eta^{\mathbb{S}}) = \eta^{\mathbb{T}}_H$ .
Multiplication axiom: $\lambda \circ H(\mu^{\mathbb{S}}) = \mu^{\mathbb{T}}_H \circ \mathbb{T}(\lambda) \circ \lambda_{\mathbb{S}}$ .

Such a $\lambda$ is referred to as a Kleisli law. As we might expect from the previous construction, there is a bijection between:

Kleisli liftings of $H$ .
Kleisli laws $H \circ \mathbb{S} \Rightarrow \mathbb{T} \circ H$ .

Again, the proof requires a little bit of creativity to construct the components of a Kleisli law from a given lifting, and makes an instructive exercise.

There is also rather pleasing duality between the two results.

Acknowledgements: Thanks to Stefania Damato for pointing out three (gulp!) typos in the Eilenberg-Moore and Kleisli law axioms which have now been fixed.

What’s a monad (take two)?

We introduced monads on a category $\mathcal{C}$ as a triple consisting of an endofunctor and unit and multiplication natural transformations:

$(\mathbb{T} : \mathcal{C} \rightarrow \mathcal{C},\eta : \mathsf{Id} \Rightarrow \mathbb{T},\mu : \mathbb{T}^2 \Rightarrow \mathbb{T})$

The unit and multiplication are required to satisfy three axioms (which specify that they form a monoid in a suitably abstract sense). There is actually quite a bit of work implied in establishing we have a monad this way. We have to verify that:

Our construction $\mathbb{T}$ is a well-defined endofunctor on the base category.
Our candidate unit $\eta$ is a legitimate natural transformation.
Our candidate multiplication $\mu$ is a legitimate natural transformation.
The unitality and associativity axioms hold.

This actually can be quite fiddly to do in practice. For example, verifying the associativity axiom requires working with objects of the form $\mathbb{T}^3(A)$ . If our endofunctor is complicated, this can lead to cumbersome calculations, and scope for errors.

An Alternative Formulation

A monad in extension form (sometimes also referred to as Kleisli form) on a category $\mathcal{C}$ is a triple consisting of:

An operation on objects $\mathbb{T} : \mathsf{obj}(\mathcal{C}) \rightarrow \mathsf{obj}(\mathcal{C})$ .
An $\mathsf{obj}(\mathcal{C})$ -indexed family of unit morphisms $\eta_A : A \rightarrow \mathbb{T}(A)$ .
An extension operation on morphisms $(-)^* : \mathcal{C}(A,\mathbb{T}(B)) \rightarrow \mathcal{C}(\mathbb{T}(A),\mathbb{T}(B))$ .

These must satisfy three axioms:

$(\eta_A)^* = \mathsf{id}_{\mathbb{T}(A)}$ .
$f^* \circ \eta_A = f$ .
$g^* \circ f^* = (g^* \circ f)^*$ .

Although they might seem less natural from the point of view of category theory, these axioms can be significantly easier to verify in practice.

If we refer to our previous definition of monad as a monad in monoid form, we can convert freely between the two at our convenience.

Given a monad in monoid form $(\mathbb{T},\eta,\mu)$ , we can produce a monad in Kleisli form as follows:

The mapping $\mathbb{T}$ is the object mapping of the functor.
The unit components are those of $\eta$ .
The extension mapping is $A \xrightarrow{f} \mathbb{T}(B) \mapsto \mathbb{T} \xrightarrow{\mathbb{T}(f)} \mathbb{T}^2(B) \xrightarrow \mu_{B} \mathbb{T}(B)$ .

In the other direction, given a monad in extension form $(\mathbb{T}, (\eta_A)_{A \in \mathsf{obj}(\mathcal{C}}, (-)^*)$ , we construct a monad in monoid form as follows:

We extend $\mathbb{T}$ to an endofunctor by defining the action on morphisms as $f : A \rightarrow B \mapsto (\eta_B \circ f)^* : \mathbb{T}(A) \rightarrow \mathbb{T}(B)$ .
The components of the unit are the $\eta_A$ .
The component of the multiplication at $A$ is $(\mathsf{id}_{\mathbb{T}(A)})^* : \mathbb{T}^2(A) \rightarrow \mathbb{T}(A)$ .

Verifying that the required properties hold in each direction, and the these mappings are mutually inverse, is a routine if long-winded exercise. We shall omit the details.

The key new feature is the extension operation. As usual, it is interesting to consider what an operation is doing from the point of view of algebra. Consider a $\mathsf{Set}$ monad with equational presentation $(\Sigma,E)$ . Recall the elements of $\mathbb{T}(A)$ are equivalence classes of $\Sigma$ -terms, quotiented by provable equality in equational logic. As we have observed before, a function

$f : A \rightarrow \mathbb{T}(B)$

can be identified with an $A$ -indexed family of equivalence classes of term, which we shall denote:

$([t^f_x])_{x \in X}$

The action of $f^*$ is defined on representatives of equivalence classes as follows:

$[t] \mapsto [t[t^f/x \mid x \in X]]$

So the Kleisli extension is a substitution operation on representatives of equivalence classes.

Different Perspectives

Aside from the possible practical benefits in terms of easier verification, there are other reasons to prefer one form over another:

The monad in monoid form formulation is entirely in terms of categories, functors and natural transformations. We can therefore easily generalize this definition to any other bicategory. Categories become 0-cells, functors 1-cells and natural transformations 2-cells. This is an extremely fruitful direction of generalization. For example, it immediately yields a definition of monad suitable for enriched category theory.
The monad in extension form formulation emphasizes different aspects. There is a generalization of monads called relative monads, in which we move beyond endofunctors. The required definition takes as its starting point the extension formulation.

We shall talk about various generalizations of monads in later posts, once we have more basics under our belts.

Comparison Functors

We have now seen both the Kleisli and Eilenberg-Moore constructions for a monad $\mathbb{T}$ , and that they yield adjunctions that induce the original monad. Such an adjunction is sometime referred to as a resolution of $\mathbb{T}$ .

In order to compare different resolutions of a monad $\mathbb{T}$ on category $\mathcal{C}$ , we need a suitable category in which to compare them. Define $\mathsf{Adj}_{\mathbb{T}}$ as the category with:

Objects: Adjunctions $F \dashv U$ , where $U$ has codomain $\mathcal{C}$ , that induce $\mathbb{T}$ .
Morphisms: A morphism $(F \dashv U : \mathcal{D} \rightarrow \mathcal{C}) \rightarrow (F' \dashv U' : \mathcal{D}' \rightarrow \mathcal{C})$ is a functor $K : \mathcal{D} \rightarrow \mathcal{D}'$ such that $F' = K \circ F$ and $U = U' \circ K$ .

Note: All the adjunctions inducing $\mathbb{T}$ must have the same unit, and the counit of adjunction is determined by its unit. It is therefore sufficient to specify only the functors in the objects of $\mathsf{Adj}_{\mathbb{T}}$ .

Writing $\epsilon$ and $\epsilon'$ for the counits of the domain and codomain respectively, the conditions for $K$ being a $\mathsf{Adj}_{\mathbb{T}}$ -morphism imply

$K \epsilon' = \epsilon_K$

We shall refer to this equation as the key property. Establishing its validity requires some additional work, either via direct calculation, or invoking some theory of adjoint squares, which we shall omit. (Although I should point out there is a short string diagrammatic proof, for those that like that sort of thing!)

The Kleisli Construction

Clearly, $(F_{\mathbb{T}} \vdash U_{\mathbb{T}} : \mathcal{C}_{\mathbb{T}} \rightarrow \mathcal{C})$ is an object of $\mathsf{Adj}_{\mathbb{T}}$ . Let $(F \vdash U : \mathcal{D} \rightarrow \mathcal{C})$ be any other object, with counit of the adjunction $\epsilon$ . There is a morphism from the Kleisli adjunction to this object, referred to as the Kleisli comparison functor, given by a functor $K_{\mathbb{T}}$ . On objects:

$K_{\mathbb{T}}(A) = F(A)$ .

For a $\mathcal{C}_{\mathbb{T}}$ -morphism $f : A \rightarrow B$ , with underlying morphism $f : A \rightarrow UF(B)$ :

$K_{\mathbb{T}}(f) = F(A) \xrightarrow{F(f)} FUF(B) \xrightarrow{\epsilon_{F(B)}}F(B)$

That identities are preserved by $K_{\mathbb{T}}$ follows from the snake equation:

$K_{\mathbb{T}}(\eta_A) = \epsilon_{F(A)} \circ F(\eta_A) = \mathsf{id}_{F(A)}$

For the composition, noting that $\mu = U \epsilon_F$ , by definition:

$K_{\mathbb{T}}(\mu_C \circ \mathbb{T}(g) \circ f) = \epsilon_{F(C)} \circ FU(\epsilon_{F(C)}) \circ FUF(g) \circ F(f)$

Applying naturality, this is equal to:

$\epsilon_{F(C)} \circ \epsilon_{FUF(C)} \circ FUF(g) \circ F(f)$

Applying naturality again gives:

$\epsilon_{F(C)} \circ F(g) \circ \epsilon_{F(B)} \circ F(f)$

Which completes verification that composition is preserved by $K_{\mathbb{T}}$ . Verifying that the two equations required of morphisms hold is straightforward as well.

We would like to show that this is the unique such morphism in $\mathsf{Adj}_{\mathbb{T}}$ . This uniqueness is termed “obvious” in some accounts, which in my opinion is rather optimistic, so we sketch the main points. The action on objects of any putative morphism $K$ is easily seen to be forced by one of the equations required of morphisms in $\mathsf{Adj}_{\mathbb{T}}$ :

$F(A) = K(F_{\mathbb{T}}(A)) = K(A)$

We would like to show that the action on morphisms is also forced, this is a bit trickier. We first note that as $F_{\mathbb{T}}$ is identity on objects, every morphism in $\mathcal{C}_{\mathbb{T}}$ is the transpose of a morphism in $\mathcal{C}$ , that is, it is of the form:

$\epsilon^{\mathbb{T}}(B) \bullet F_{\mathbb{T}}(f)$

Furthermore, $f$ is the underlying $\mathcal{C}$ -morphism of the Kleisli morphism. (This may need a bit of thought about the Kleisli adjunction to convince yourself this is true). Above, we write the counit of the Kleisli adjunction as $\epsilon^{\mathbb{T}}$ . This deviates from our usual convention of using subscripts for Kleisli notions, but saves notational confusion when dealing with components of natural transformations.

Using functoriality:

$K (\epsilon^{\mathbb{T}}_B \bullet F_{\mathbb{T}}(f)) = K(\epsilon_B) \circ K(F_{\mathbb{T}}(B))$

Applying the key property, the previous expression is equal to

$\epsilon_K(B) \circ K(F_{\mathbb{T}(B)}(f))$

Finally, applying one of the equations for $K$ being a morphism, and its previously established action on objects, we get

$\epsilon_{F{B}} \circ F(f)$

This is exactly the expression for the action on morphisms in our definition of $K_{\mathbb{T}}$ . In summary, we have established that the Kleisli adjunction is the initial resolution of $\mathbb{T}$ .

We now quickly look at some important details of the universal morphisms from the Kleisli adjunction. $K_{\mathbb{T}}$ has image on objects those of the form $F(A)$ . For a morphism $F(A) \xrightarrow{f} F(B)$ , $K_{\mathbb{T}}(f)$ is given by taking the transpose of $f$ under the adjunction $F \dashv U$ , and is therefore a bijection between the two hom sets, showing the Kleisli comparison functor is full and faithful.

The Eilenberg-Moore Construction

The Eilenberg-Moore adjunction $(F^{\mathbb{T}}, U^{\mathbb{T}})$ also yields an object of $\mathsf{Adj}_{\mathbb{T}}$ . For any other $\mathsf{Adj}_{\mathbb{T}}$ -object $(F \vdash U : \mathcal{D} \rightarrow \mathcal{C})$ , we aim to show there is a unique morphism $K^{\mathbb{T}}$ to the Eilenberg-Moore adjunction. The equation $U^{\mathbb{T}} \circ K^{\mathbb{T}} = U$ tells us that

$K(A) = (U(A), \xi) \qquad K(f) = U(f)$

Where $\xi : UFU(A) \rightarrow U(A)$ is a to be determined structure map. Write $\epsilon^{\mathbb{T}}$ for the counit of the Eilenberg-Moore adjunction. This has components $\epsilon_{(A, \alpha)} = \alpha$ (This is just a matter of examining the details of adjunction if it is unfamiliar). Therefore $\epsilon_{K(A)} = \xi$ . Applying the key property, combined with the action of $K$ on morphisms, $\xi = U(\epsilon_A)$ . This completely fixes the only possible construction for $K$ . We must confirm that $U(\epsilon_A)$ is a valid algebra structure map. The unit axiom follows immediately from the snake equation:

$U(\epsilon_A) \circ \eta_{U(A)} = \mathsf{id}_{U(A)}$

For the multiplication axiom, recalling $\mu = U \epsilon_F$ , and applying naturality:

$U(\epsilon_A) \circ \mu = U(\epsilon_A) \circ U_{FU(A)} = U(\epsilon_A) \circ UFU(\epsilon_A)$

Functoriality is then obviously inherited from that of $U$ . We have therefore established that the Eilenberg-Moore adjunction is the terminal resolution of $\mathbb{T}$ . The universal morphisms are referred to as (Eilenberg-Moore) comparison functors.

An Important Relationship

As a special case of the initial and terminal resolutions above, there must be a unique morphism from the Kleisli to the Eilenberg-Moore resolution. On objects:

$K_{\mathbb{T}}(A) = F^{\mathbb{T}}(A) = (\mathbb{T}(A), \mu_A)$

and on morphisms

$K_{\mathbb{T}}(f) = \epsilon^{\mathbb{T}}_{F(A)} \circ F^{T}(f) = \mu_A \circ \mathbb{T}(f)$

From our previous remarks, this functor is full and faithful onto the full subcategory generated by objects of the form $F^{\mathbb{T}}(A)$ . Therefore, we can identify the Kleisli category with the full subcategory of free Eilenberg-Moore algebras.

The Kleisli Adjunction

The Kleisli category is an interesting construction, but as with the Eilenberg-Moore category, it has a deeper significance.

For a monad $\mathbb{T}$ on category $\mathcal{C}$ , there is a functor $U_{\mathbb{T}} : \mathcal{C}_{\mathbb{T}} \rightarrow \mathcal{C}$ with:

$U_{\mathbb{T}}(A) = \mathbb{T}(A) \qquad U_{\mathbb{T}}(f) = \mu \circ \mathbb{T}(f)$

There is also a functor $F_{\mathbb{T}} : \mathcal{C} \rightarrow \mathcal{C}_{\mathbb{T}}$ with:

$F_{\mathbb{T}}(A) = A \qquad F_{\mathbb{T}}(f) = \eta \circ f$

(Verifying that both these are legitimate functors is a useful exercise in applying the various axioms.)

In fact, $F_{\mathbb{T}} \dashv U_{\mathbb{T}}$ . To see this, we must show a natural bijection between:

Kleisli morphisms $F_{\mathbb{T}}(A) \rightarrow B$ .
$\mathcal{C}$ -morphisms $A \rightarrow U_{\mathbb{T}}(B)$ .

Recalling that Kleisli morphisms $A \rightarrow B$ are $\mathcal{C}$ -morphisms $A \rightarrow \mathbb{T}(B)$ , and expanding definitions:

A Kleisli morphism $F_{\mathbb{T}}(A) \rightarrow B$ is a $\mathcal{C}$ -morphism $A \rightarrow \mathbb{T}(B)$ .
A $\mathcal{C}$ -morphism $A \rightarrow U_{\mathbb{T}}(B)$ is a $\mathcal{C}$ -morphism $A \rightarrow \mathbb{T}(B)$ .

So the bijection holds trivially. I think we can probably guess what the monad induced by this adjunction is going to turn out to be, but lets check the details anyway.

Endofunctor: The endofunctor is $U_{\mathbb{T}} \circ F_{\mathbb{T}}$ . On objects this is $U_{\mathbb{T}}(F_{\mathbb{B}}(A)) = U_{\mathbb{T}}(A) = \mathbb{T}(A)$ . On morphisms $U_{\mathbb{T}}(F_{\mathbb{B}}(f)) = U_{\mathbb{T}}(\eta \circ f) = \mathbb{T}(\mu \circ \mathbb{T}(\eta \circ f)) = \mathbb{T}(f)$ .
Unit: The unit is the transpose of $\mathsf{id}_{F_{\mathbb{T}}(A)} : A \rightarrow A$ , which is $\eta_A$ .
Multiplication: The multiplication at $A$ is $U_{\mathbb{T}}(\epsilon_{F_{\mathbb{T}}(A)})$ , where $\epsilon_{\mathbb{F}(A)}$ is the transpose of $\mathsf{id}_{U_{\mathbb{T}}(F_{\mathbb{T}}(A))} : U_{\mathbb{T}}(F_{\mathbb{T}}(A)) \rightarrow U_{\mathbb{T}}(F_{\mathbb{T}}(A))$ . Expanding definitions slightly, $\epsilon_{\mathbb{F}(A)}$ is $\mathsf{id}_{\mathbb{T}(A)}$ . Then $U_{\mathbb{T}}(\mathsf{id}_{\mathbb{T}(A)})$ is $\mu \circ \mathbb{T}(\mathsf{id}_{\mathbb{T}(A)})$ , which is simply $\mu$ .

Summing up, for a monad $\mathbb{T}$ , the the monad induced by the Kleisli adjunction $F_{\mathbb{T}} \dashv U_{\mathbb{T}}$ is $\mathbb{T}$ itself.

We have now seen two different constructions, the Eilenberg-Moore and Kleisli constructions, and their corresponding adjunctions. Both adjunctions yield the original monad. The natural question we shall pursue next is the relationship between these two constructions and other adjunctions that induce the same monad.

Kleisli Categories

Last time, we discussed one of the standard categories associated with a monad, the Eilenberg-Moore category. This time, we discuss the other, the Kleisli category, and its significance.

For a monad $\mathbb{T}$ on $\mathcal{C}$ , the Kleisli category, denoted $\mathcal{C}_{\mathbb{T}}$ , has:

Objects: The objects of $\mathcal{C}$ .
Morphisms: A morphism of type $A \rightarrow B$ is a $\mathcal{C}$ -morphism of type $A \rightarrow \mathbb{T}(B)$ .

Unlike many simple categorical constructions, the composition and identities are not inherited from the base category. Instead, the identity at $A$ is given by the component of the unit at $A$ , $\eta_A$ . For two Kleisli morphisms $f : A \rightarrow B$ , and $g : B \rightarrow C$ , we shall write their composite as $g \bullet f$ . This is given by the following composite of their underlying $\mathcal{C}$ -morphisms:

$A \xrightarrow{f} \mathbb{T}(B) \xrightarrow{\mathbb{T}} \mathbb{T}^2(C) \xrightarrow{\mu_C} \mathbb{T}(C)$

A Computational Perspective

The popular intuition in computer science is that the Kleisli category of appropriately chosen monads can give a compositional model for various forms of effectful computation.

Example: For the list monad $\mathbb{L}$ , we can think of a Kleisli morphism $f : A \rightarrow B$ as producing a list of possible outputs. This can be seen as a crude form of non-deterministic computation. The identity $\mathsf{id}_A$ is the function of type $A \rightarrow \mathbb{L}(A)$ acting as:

$a \mapsto [a]$ .

So the identity “deterministically” returns its input as its output. Now if we consider two Kleisli maps $f : A \rightarrow B, g : B \rightarrow C$ , their composite acts as follows:

Input $a$ is mapped by $f$ to some list of possible outputs, say $[a_1,\ldots,a_n]$ .
The output of $f$ is transformed by applying $g$ element-wise to produce a list-of-lists $[g(a_1),\ldots,g(a_n)]$ .
The multiplication concatenates the results together into a single output list.

Encoding non-determinism via lists is favoured in many software programming contexts as they have an efficient representation as a datatype. A perhaps more satisfactory mathematical representation of (unbounded) non-determinism is the following.

Example: The Kleisli category of the powerset monad is equivalent to the category of sets and relations between them.

Example: Recall the state monad for a set $S$ , constructed from the Cartesian closure of $\mathsf{Set}$ . A Kleisli map $A \rightarrow B$ for this monad is a function of type $A \rightarrow S \Rightarrow (B \times S)$ . For $a \in A$ , $f(a)$ is a function taking a state value, and producing an element of $B$ and a new state value. The Kleisli composition of such maps does exactly what a programmer might hope, threading state and computation values through a composite of two such stateful computations.

An Algebraic Perspective

As well as this computational perspective, as has been the case for other aspects of monads, it is instructive to consider an algebraic point of view as well.

Consider an equational presentation $(\Sigma,E)$ , and the monad $\mathbb{T}$ it induces, as discussed in earlier posts. A Kleisli morphism $f : A \rightarrow B$ is a function $f : A \rightarrow \mathbb{T}(B)$ . We can think of this as an $A$ -indexed family of equivalence classes of terms with variables in $B$ , which we might write as $([t_a])_{a \in A}$ (Recall $[t]$ denotes an equivalence class with representative $t$ ). If we have a second morphism $g : B \rightarrow C$ , this is a function $g : B \rightarrow \mathbb{T}(C)$ , that is a $B$ -indexed family of terms with variables ranging over $C$ . Denote this family $([t'_b])_{b \in B}$ . The composite $g \bullet f$ will encode an $A$ -indexed family of terms with variables in $C$ . Formally, this family is:

$([t_a[t'_b / b \mid b \in B]])_{a \in A}$

Here the notation $t[t'_b / b \mid b \in B]$ denotes substituting each occurrence of variable $b$ appearing in term $t$ with $t_b$ .

So algebraically, the Kleisli category has morphisms families of (equivalence classes of) terms, and composition is substitution. From this point of view, the identity morphism at $A$ is $\eta_A$ , which corresponds to the trivial family:

$([a])_{a \in A}$

This family acts as a two sided identity with respect to substitutions as required.