monadicity – Dan Marsden

An application of monadicity

Now we have seen the basic ideas of monadicity, and Beck’s monadicity theorem, it’s time to look at an important application. Although the result in question belongs to the area of topos theory, to avoid pulling in too much additional theory we will consider a concrete example, and then sketch how this extends to the abstract setting.

Subsets and the contravariant powerset

For our motivating example, we are going to consider the category $\mathsf{Set}$ of sets and functions. The set

$\{ \mathsf{true}, \mathsf{false} \}$

which we shall denote $2$ will play an important role. For any set $X$ , a function $\chi : X \rightarrow 2$ corresponds to a subset of $X$ :

$\{ x \mid x \in X \;\text{and}\; \chi(x) = \mathsf{true} \}$

and given any subset $U \subseteq X$ , we can define a function:

$x \mapsto \begin{cases} \mathsf{true} & \text{ if } x \in U \\ \mathsf{false} & \text{otherwise} \end{cases}$

In this way, we can go back and forth between subsets and what are known as their characteristic functions. For a fixed set $X$ , we can consider the set $2^X$ of characteristic functions of subsets of $X$ . The mapping

$X \mapsto 2^X$

extends to a functor. For $f : X \rightarrow Y$ we get a function in the opposite direction $2^f : 2^Y \rightarrow 2^X$ with action:

$\chi \mapsto \chi \circ f$

It is straightforward to check that this satisfies the functor axioms, so we have a functor:

$2^{(-)} : \mathsf{Set}^{op} \rightarrow \mathsf{Set}$ ,

sometimes referred to as the contravariant powerset functor. This functor has a left adjoint, which we shall also denote

$2^{(-)} : \mathsf{Set} \rightarrow \mathsf{Set}^{op}$ .

Notice the only difference here is whether we choose to put the “op” on the domain or codomain. Establishing that these two functors form an adjunction is straightforward, as we have natural bijections between:

Functions $2^X \rightarrow Y$ in $\mathsf{Set}^{op}$
Functions $Y \rightarrow 2^X$ in $\mathsf{Set}$
Functions $Y \times X \rightarrow 2$ in $\mathsf{Set}$
Functions $X \times Y \rightarrow 2$ in $\mathsf{Set}$
Functions $X \rightarrow 2^Y$ in $\mathsf{Set}$

We have seen a more abstract version of this proof before, as this is a special case of the adjunction that induces the continuation monad, in this case for the endofunctor:

$2^{2^{(-)}} : \mathsf{Set} \rightarrow \mathsf{Set}$

The perhaps surprising observation is that the functor

$2^{(-)} : \mathsf{Set}^{op} \rightarrow \mathsf{Set}$

is monadic, meaning the Eilenberg-Moore category of $2^{2^{(-)}}$ is equivalent to $\mathsf{Set}^{op}$ . Put another way, $\mathsf{Set}^{op}$ is monadic over $\mathsf{Set}$ . Aside from being a rather startling fact, this gives a concrete description of the Eilenberg-Moore category of this special case of the continuation monad. Some duality theory tells us that the category of complete atomic Boolean algebras is equivalent to $\mathsf{Set}^{op}$ , and this gives us an even more concrete description of the algebras of this monad.

Generalising

At first glance, the argument above looks very specific to the category of sets and functions. Fortunately, there is a very large class of categories that look sufficiently like the category of sets to carry out this argument in the abstract.

As a first step, we look at the important role of the set $2$ . It allowed us to connect subsets and characteristic functions. To generalise this, we first adopt a more categorical perspective, and consider subobjects rather than subsets. A subobject of object $X$ , is isomorphism class of monomorphisms $U \rightarrowtail X$ . Spelling this out a bit more, two monomorphisms $m : U \rightarrowtail X$ and $m' : U' \rightarrowtail X$ are isomorphic if there exists an isomorphism $i : U \rightarrow U'$ such that $m = m' \circ i$ .

A subobject classifier is a categorical abstraction of the correspondence between subsets (subobjects) and characteristic morphisms. Writing $\mathsf{Sub}(X)$ for the collection of subobjects of $X$ , a category $\mathcal{C}$ with finite limits is said to have a subject classifier if and only if there is an object $\Omega$ and natural isomorphism:

$\mathsf{Sub}(X) \cong \mathcal{C}(X,\Omega)$

There are several equivalent definitions of subobject classifiers. The typical statement involves a generic subobject and a pullback condition, but as we won’t delve into the details, the statement above emphasises the relationship between subobjects and classifying morphisms.

Example: The set $2$ is the subobject classifier in $\mathsf{Set}$ . Subobjects correspond to subsets which correspond to characteristic functions.

The class of categories that look sufficiently like the category of sets for our purposes are known as toposes. A topos is a finitely complete, Cartesian closed category with a subobject classifier. (There are almost as many equivalent definitions of a topos as there are books on the subject, depending on the perspective the author wishes to emphasize. We choose this one as it is reasonably straightforward.). There are many examples of toposes that crop up in mathematical practice.

Example: The category $\mathsf{Set}$ is a topos, and in many ways the motivating example for the abstraction. The full subcategory of finite sets is also a topos.

Example: For any small category $\mathcal{C}$ , the category of presheaves over $\mathcal{C}$ is a topos. This is simply the category with objects functors $\mathcal{C}^{op} \rightarrow \mathsf{Set}$ and morphisms natural transformations between them. This construction can be generalised greatly to various notions of categories of sheaves, but we avoid entering into what would be a sizeable technical detour.

For a topos $\mathcal{C}$ , by analogy with the set theoretic situation, as we have exponentials and a subobject classifier, it is natural to consider the functor:

$\Omega^{(-)} : \mathcal{C}^{op} \rightarrow \mathcal{C}$

It is a non-trivial observation that this functor is monadic. As a concrete argument is no longer possible, this is typically established using a monadicity theorem. Interested readers that are prepared for a bit of topos theory can find the details in any good book on topos theory. Slightly confusingly, topos theorists also refer to this result as the (topos theoretic) monadicity theorem.

This result has an immediate pay-off. As a topos is finitely complete, $\mathcal{C}^{op}$ is also finitely complete. In other words, $\mathcal{C}$ is finitely cocomplete. Finite cocompleteness was actually included in the original definition of a topos, until it was shown that it followed from the other axioms. Monadicity is a particularly elegant way of establishing this fact.

Conclusion

Our discussion of topos theory has been deliberately somewhat sketchy, to avoid pulling in too many technical details. Topos theory is a vast subject, with connections to many parts of mathematics, and would probably warrant a blog of its own.

Further reading: Readers interested in filling in some of the topos theoretic technical details could look at one of the standard sources, such as volume 1 of Johnstone’s “Sketches of an Elephant”, Moerdijk and MacLane’s “Sheaves in Geometry and Logic” or volume 3 of Borceux’s “Handbook of Categorical Algebra”.

Beck’s Monadicity Theorem

Now we have introduced the idea of monadicity, we move onto the most important theorem in this area. Beck’s monadicity theorem tells us that a functor $U: \mathcal{B} \rightarrow \mathcal{C}$ is monadic if and only if the following three conditions hold:

U has a left adjoint.
U reflects isomorphisms.
$\mathcal{B}$ has coequalizers of reflexive $U$ -contractible pairs, and $U$ preserves them.

The aim of this post is to unpack these three conditions, and to justify why they are at least necessary for a monadic functor. That they are also sufficient is a rather amazing fact that we may delve into in another post. The first two conditions are relatively trivial, but the third will require more consideration.

Left adjoints

The first condition, that $U$ has a left adjoint is the most trivial. By definition, we require a monadic functor to be a right adjoint so we can consider the comparison functor to the Eilenberg-Moore category.

Isomorphism reflection

A functor $U$ is said to reflect isomorphisms, or to be conservative, if for every $f$ , $U(f)$ is an isomorphism implies $f$ is.

Remark: Isomorphism reflection is a statement about morphisms not objects. It does not say that if $U(A)$ is isomorphic to $U(B)$ then $A$ is isomorphic to $B$ .

For a monad $\mathbb{T} : \mathcal{C} \rightarrow \mathcal{C}$ , if we have an Eilenberg-Moore algebra morphism $h : (A,\alpha) \rightarrow (B,\beta)$ , then in $\mathcal{C}$

$h \cdot \alpha = \beta \cdot \mathbb{T}(h)$ .

Now assume there exists $\mathcal{C}$ -morphism $g : B \rightarrow A$ such that

$g \cdot h = \mathsf{id}_{A}$ and $h \cdot g = \mathsf{id}_{B}$

then we would like to show $g$ is an algebra morphism of type $(B,\beta) \rightarrow (A,\alpha)$ . This is a straightforward calculation:

$g \cdot \beta = g \cdot \beta \cdot \mathbb{T}(h \cdot g) = g \cdot h \cdot \alpha \cdot \mathbb{T}(g) = \alpha \cdot \mathbb{T}(g)$ .

Therefore $U^{\mathbb{T}}$ reflects isomorphisms. It is easy to verify that equivalences are also conservative, and conservative functors are closed under composition. As

$U = U^{\mathbb{T}} \circ K$

where $K$ is the comparison functor, if $U$ is monadic, it must be conservative. This condition is already sufficient to weed out various putative monadic functors.

Example: Let $\mathsf{Pos}$ be the category of posets and monotone maps, and $U : \mathsf{Pos} \rightarrow \mathsf{Set}$ the obvious forgetful functor. This functor has a left adjoint, and so satisfies the first condition of the monadicity theorem. Now consider the two element posets:

The poset $X$ , with underlying set $\{ x_1, x_2 \}$ with the discrete partial order.
The poset $Y$ , with underlying set $\{ y_1, y_2 \}$ with the least partial order such that $y_1 \leq y_2$ .

There is a bijective monotone map $h : X \rightarrow Y$ with $h(x_1) = y_1$ and $h(x_2) = y_2$ . This morphism has no inverse monotone map. On the other hand, the underlying function $U(h)$ has an obvious inverse in $\mathsf{Set}$ . Therefore $U$ is not conservative, and therefore cannot be monadic.

This argument is easily adapted to show the forgetful functor $\mathsf{Cat} \rightarrow \mathsf{Set}$ taking a small category to its set of objects is not monadic.

The coequalizer condition

We now need to untangle the final condition, and this will be a little bit more technical. We need to introduce two related notions.

Firstly, a parallel pair:

$d^0, d^1 : A \rightarrow B$

is said to be contractible (or split) if there exists $t : B \rightarrow A$ such that

$d^0 \cdot t = \mathsf{id}_B$ and $d^1 \cdot t \cdot d^0 = d^1 \cdot t \cdot d^1$ .

Notice that these conditions are asymmetrical in $d^0$ and $d^1$ .

Secondly, a contractible (or split) coequalizer consists of the following data:

A parallel pair $d^0, d^1 : A \rightarrow B$ .
A morphism $t : B \rightarrow A$ .
A morphism $d : B \rightarrow C$ .
A morphism $s : C \rightarrow B$ .

such that:

$d$ coequalizes the parallel pair, that is $d \cdot d^0 = d \cdot d^1$ .
$d^0$ has section $t$ , that is $d^0 \cdot t = \mathsf{id}_B$ .
$d$ has section $s$ , that is $d \cdot s = \mathsf{id}_C$ .
$d^1 \cdot t = s \cdot d$ .

Again, notice the asymmetry of the conditions. As suggested by the terminology, a contractible coequalizer is a coequalizer in the ordinary sense.

Furthermore, a contractible coequalizer is simply a collection of morphisms satisfying four equations. If we apply a functor to the morphisms, the resulting data will also satisfy the same equations, as functors preserve them, and will therefore also form a contractible coequalizer. Therefore contractible coequalizers are preserved by every functor. That is, they are an example of an absolute colimit.

A second useful fact, connecting these two notions, is that if a contractible pair $d^0, d^1 : A \rightarrow B$ has a coequalizer $d : B \rightarrow C$ , then there automatically exists an $s : C \rightarrow B$ such that it forms a contractible coequalizer.

A $U$ -contractible pair, is a pair $d^0, d^1 : A \rightarrow B$ such that $U(d^0), U(d^1) : U(A) \rightarrow U(B)$ has a contractible coequalizer. Notice this terminology is slightly misleading, we are requiring a contractible coequalizer, not just a contractible pair.

With that mass of terminology in place, we recall that for any monad $\mathbb{T}$ , the forgetful functor $U^{\mathbb{T}} : \mathcal{C}^{\mathbb{T}} \rightarrow \mathcal{C}$ creates colimits which exist in the base category and are preserved by $\mathbb{T}$ and $\mathbb{T}^2$ . $U$ -contractible pairs induce absolute coequalizers in the base category, which are therefore created by $U^{\mathbb{T}}$ . Secondly, although equivalences don’t necessarily create colimits that exist, they do preserve them. Therefore, if $U : \mathcal{B} \rightarrow \mathcal{C}$ is monadic, as

$U = U^{\mathbb{T}} \circ K$

$\mathcal{B}$ has coequalizers of $U$ -contractible pairs, and $U$ preserves them.

In fact, this is stronger than the proof of the monadicity theorem needs, and we can restrict our attention to a small class of coequalizers. A parallel pair $d^0, d^1 : A \rightarrow B$ is said to be reflexive if they have common section. That is, there exists an $r : B \rightarrow A$ such that

$d^0 \cdot r = \mathsf{id}_B = d^1 \cdot r$ .

Conclusion

Two out of the three conditions of the monadicity theorem are pretty routine. The third took a bit of unravelling, but enduring the technicalities is a worthwhile investment, as these special colimits arise again and again in the theory of monads. We will look in detail at the most important source of these special coequalizers in a later post.

Further reading: Our account owes a lot to that of Barr and Well’s in Toposes Triples and Theories. We have deliberately used similar notational choices to them in case readers want to consult their work for further details, which is highly recommended. Johnstone remarks in the Elephant that the restriction to reflexive pairs in condition three is omitted in many accounts, but is all that is needed. Toposes, Triples and Theories is also careful in this regard.

The Idea of Monadicity

Naively, for a given category $\mathcal{B}$ , we might wonder if it is equivalent to the Eilenberg-Moore category of a monad. This would help us deduce properties of $\mathcal{B}$ , such as (co)completeness, using facts we know about the Eilenberg-Moore construction.

Giving this a moments thought, it doesn’t sound quite right, as to deduce properties of an Eilenberg-Moore category, we need more information, for example about the base category. In order to reach a mathematically useful notion, we need to pin down exactly what we intend with regard to this equivalence.

We would like to know what the base category we’re interested in is, and how it relates to $\mathcal{B}$ , so it is natural to consider functors of the form.

$U : \mathcal{B} \rightarrow \mathcal{C}$

Intuitively this is a candidate forgetful functor from an Eilenberg-Moore category to its base category. If there is any hope of $\mathcal{B}$ being equivalent to an Eilenberg-Moore category, $U$ should have a left adjoint

$F : \mathcal{C} \rightarrow \mathcal{B}$ .

This gives us a bit more to work with, as adjunction will give us a monad

$\mathbb{T} = U \circ F$

We are now interested in when there is an equivalence:

$\mathcal{B} \simeq \mathcal{C}^{\mathbb{T}}$

To specify this equivalence more precisely, recall we have already seen the Eilenberg-Moore comparison functor, which relates resolutions of the same monad. Recall this is the unique functor

$K : \mathcal{B} \rightarrow \mathcal{C}^{\mathbb{T}}$

that commutes with the free and forgetful functors, in that:

$U^{\mathbb{T}} \circ K = U$ and $K \circ F = F^{\mathbb{T}}$ .

We have now arrived at the right notion. A right adjoint functor $U : \mathcal{B} \rightarrow \mathcal{C}$ is monadic if the comparison functor is an equivalence of categories. If there exist such a $U$ , we say that $\mathcal{B}$ is monadic over $\mathcal{C}$ .

Monadicity Theorems

Unsurprisingly, a monadicity theorem gives conditions under which a functor is monadic. The key result is known as Beck’s monadicity theorem, which gives precise conditions for monadicity. There are many variations, often with sufficient assumptions that are more convenient to establish in practice. There are also a family of related results, which don’t specifically establish monadicity, but rather other nice properties of the comparison functor.

In fact, if you have a specific functor with a left adjoint, it is often easier to establish monadicity by directly proving the required equivalence. So what’s the point of monadicity theorems? Their main application is when you are working more abstractly, aiming to show that under suitable assumptions that all functors of a certain type are monadic. This situation is similar to the use of adjoint functor theorems. Again, these are rarely applied to establish that a particular functor has an adjoint, but rather that in an abstract setting every functor satisfying certain axioms always has an adjoint.

In our discussions, we will focus on when the comparison functor is an equivalence. MacLane considers the stronger situation where the comparison functor is an isomorphism. We will pay this perhaps less categorically natural formulation less attention. It is however important to be aware that there are monadicity theorems of this type as well when looking at the wider literature.

If instead of the Eilenberg-Moore construction, we consider the Kleisli construction, we can ask similar questions. The situation is much simpler in this case, as was previously discussed.

Conclusion

The notions of monadicity and monadicity theorems are fundamental tools. Despite this, as they are used in more abstract work, they tend to be perceived as a more advanced topic. This is probably reinforced by the fact that the details of monadicity theorems are a little bit technical looking, with certain special classes of colimits having a prominent role. In reality, the details only involve elementary ideas, and are not particularly challenging. We will discuss the specifics of monadicity theorems, related results about comparison functors, and their applications in future posts.