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”.

A monad is just a one object enriched category

We have seen that the notion of monad can be interpreted in any bicategory. The aim of todays post is to explain that for a bicategory \mathcal{W}, a monad in \mathcal{W} is the same thing as a one-object \mathcal{W}-enriched category. Or more tersely:

A monad is the same thing as a one-object \mathcal{W}-category.

Mostly, this is just a case of understanding the definitions, with no complicated translation between the two structures required.

Monads and enrichment

Recall that for a monoidal category (\mathcal{V}, \otimes, I), a \mathcal{V}enriched category, or \mathcal{V}-category \mathcal{A} is a generalisation of ordinary categories with:

  1. A collection of objects X,Y,\ldots.
  2. For every pair of object X,Y, a hom object \mathcal{A}(X,Y).
  3. For each object X, an identity \mathcal{V}-morphism j_X : I \rightarrow \mathcal{A}(X,X).
  4. For each triple of objects X,Y,Z, a composition \mathcal{V}-morphism m_{X,Y,Z} : \mathcal{A}(Y,Z) \otimes \mathcal{A}(X,Y) \rightarrow \mathcal{A}(X,Z).

These are subject to some natural axioms such that composition is associative, and unital with respect to the chosen identities. The motivating special case is that a \mathsf{Set}-enriched category is the same thing as an ordinary category.

It is a well-known fact of enriched category theory that a monoid in the monoidal category \mathcal{V} is the same thing as a one object \mathcal{V}-category. The even better known special case, which crops up in most introductions to category theory, is that a one object ordinary category is the same thing as a monoid.

Of course, the special case that we should be interested in as monad theorists is the monoidal category of endofunctors ([\mathcal{C}, \mathcal{C}], \circ, \mathsf{Id}_{\mathcal{C}}). Using the fundamental meme of monad theory, that a monad is just a monoid in the category of endofunctors, we can deduce that monads on \mathcal{C} are the same thing as one object [\mathcal{C},\mathcal{C}]-enriched categories. This claim works equally well if we consider monads in an arbitrary bicategory.

Example: We have seen previously that for a monoidal category \mathcal{V} with coproducts, a \mathcal{V}-enriched category is the same thing as a monad in the bicategory of \mathcal{V}-matrices, \mathbf{Mat}(\mathcal{V}). Applying the observation above, the following all describe the same data:

  1. A \mathcal{V}-enriched category with set of objects O.
  2. A monad on O in \mathbf{Mat}(\mathcal{V}).
  3. A one-object \mathbf{Mat}(\mathcal{V})(O,O)-enriched category.

Which is a bit of a funny conclusion, every multi-object enriched category is the same thing as a single-object enriched category over a different base. In particular, every ordinary (small) category with set of objects O is a one-object \mathbf{Mat}(\mathsf{Set})(O,O)-enriched category.

In the example above, it feels a bit clumsy to have to keep saying “…with set of objects O…”. To clean this up, and take this story a bit further, we are going to have to generalise our notion of enriched category, to categories enriched over a bicategory \mathcal{W}. Although this may sound a bit intimidating, it is actually only a small step beyond enrichment in a monoidal category.

A \mathcal{W}-enriched category \mathcal{A} consists of:

  1. A collection of objects X,Y,Z, each with an associated extent, given by a 0-cell \mathsf{ext}(X) in \mathcal{W}.
  2. For every pair of objects X,Y, a hom 1-cell \mathcal{A}(X,Y) : \mathsf{ext}(X) \rightarrow \mathsf{ext}(Y).
  3. For every object X, an identity 2-cell j_A : \mathsf{Id}_{\mathsf{ext}(X)} \Rightarrow \mathcal{A}(X,X).
  4. For every triple of objects X,Y,Z, a composition 2-cell m_{X,Y,Z} : \mathcal{A}(Y,Z) \circ \mathcal{A}(X,Y) \Rightarrow \mathcal{A}(X,Z).

As before, this data is subject to natural unitality and associativity axioms.

With this definition in place, naming things suggestively, a one object \mathcal{W}-category consists of:

  1. An object, with extent a 0-cell \mathcal{C} in \mathcal{W}.
  2. A single hom 1-cell \mathbb{T} : \mathcal{C} \rightarrow \mathcal{C}.
  3. An identity 2-cell \eta : \mathsf{Id} \Rightarrow \mathbb{T}.
  4. A single composition 2-cell \mu : \mathbb{T} \circ \mathbb{T} \Rightarrow \mathbb{T}.

This data satisfies exactly the axioms such that (\mathbb{T} : \mathcal{C} \rightarrow \mathcal{C}, \eta, \mu) is a monad. That is:

A monad in \mathcal{W} is the same thing as a one-object \mathcal{W}-category.

We rephrase the previous example in this more flexible setting.

Example: For a monoidal category \mathcal{V}, a \mathcal{V}-category is a one object \mathbf{Mat}(\mathcal{V})-enriched category.

A possibly more interesting example is as follows.

Example: We have seen previously that for a category \mathcal{C} with pullbacks, an internal category in \mathcal{C} is the same thing as a monad in the bicategory of spans \mathbf{Span}(\mathcal{C}). Now applying our previous observation, the following all describe the same data:

  1. An internal category in \mathcal{C}.
  2. A monad in \mathbf{Span}(\mathcal{C}).
  3. A one-object \mathbf{Span}(\mathcal{C})-enriched category.

This establishes a slightly surprising connection between internal and enriched category theory.

Conclusion

To an extent, this post is about almost trivial relationships between definitions that happen to coincide. This is not just an exercise in categorical showing-off or pointless abstraction. The relationship between monads and one-object enriched categories is really a matter of perspective. This may allow us to relate monads to other concepts, for example finitary monads and Lawvere theories can be connected in this way. Once monads are viewed as categories, we can consider categorical notions such as completion under certain limits or colimits, which again occur in connection with Lawvere theories. These ideas are used to startling effect in the work of Richard Garner and co-authors, which I highly recommend as further reading.