Dan Marsden

Distributive Laws and General Equations

We have seen we can distribute any monad $\mathbb{T}$ presented by linear equations over a commutative monad $\mathbb{S}$ . There is a balance between the assumptions on these two monads that yields a distributive law, but it is not the only choice. This time we look at strengthening our assumptions about the monad $\mathbb{S}$ so that we can weaken the restriction to presentations by linear equations on monad $\mathbb{T}$ and still have a distributive law.

The plan is quite simple. The previous results hinged on closure properties of multilinear extensions. Our approach is to consider classes of monads where we get stronger closure properties of multilinear extensions, so we continue to use uniqueness of multilinear extensions as our proof principle.

Special Classes of Monads

Throughout this post, $\mathbb{S}$ will denote a commutative monad on a category with finite products.

Recall that $\mathbb{S}$ is:

Affine if $\langle \mathbb{S} \pi_1, \mathbb{S} \pi_2 \rangle \cdot \mathsf{dst} = \mathsf{id}_{\mathbb{S}(X) \times \mathbb{S}(Y)}$ .
Relevant if $\mathsf{dst} \cdot \langle \mathbb{S}\pi_1, \mathbb{S}\pi_2 \rangle = \mathsf{id}_{\mathbb{S}(X \times Y)}$
Cartesian if it is both affine and linear.

Frustratingly, there are several unrelated notions of Cartesian monad used in the literature, so some caution with this terminology is required.

Multilinear Extensions for Affine Monads

We begin by investigating a special case of when we can delete inputs and still get multilinear extensions.

Assume $\mathbb{S}$ is an affine monad, and

\hat{h} : \mathbb{S}(X) \rightarrow \mathbb{S}(X)

is the multilinear extension of

h : X \rightarrow X

then the composite

\hat{h} \cdot \pi_1 : \mathbb{S}(X) \times \mathbb{S}(X) \rightarrow \mathbb{S}(X)

is the multilinear extension of

h \cdot \pi_1 : X \times X \rightarrow X

Intuitively, we can drop the second input and still get a multilinear extension.

To confirm multilinearity,

\hat{h} \cdot \pi_1 \cdot \mu \times \mu = \hat{h} \cdot \mu \cdot \pi_1 = \mu \cdot \mathbb{S}(\hat{h}) \cdot \pi_1

= \mu \cdot \pi_1 \mathbb{S}(\hat{h}) \cdot \pi_1 \cdot \langle \mathbb{S}\pi_1, \mathbb{S}\pi_2 \rangle \cdot \mathsf{dst} = \mu \cdot \mathbb{S}(\hat{h}) \cdot \mathbb{S}\pi_1 \cdot \mathsf{dst}

where the second step uses the assumed multilinearity of $\hat{h}$ , and the third step uses the assumption $\mathbb{S}$ is affine.

Verifying the extension property is a routine application of naturality.

Generalising from this special case, multilinear extensions of affine monads are closed under deleting variables. Using the same argument as the previous post, affine monads preserve equations that delete but don’t duplicate variables. We will refer to such equations as strictly deleting, and use the term strictly deleting presentation in the obvious way.

Multilinear Extensions for Relevant Monads

We begin by looking at a special case of when we can duplicate inputs and still get a multilinear extension.

Assume $\mathbb{S}$ is a relevant monad, and

\hat{h} : \mathbb{S}(X) \times \mathbb{S}(X) \rightarrow \mathbb{S}(X)

is the multilinear extension of

h : X \times X \rightarrow X

then the composite

\hat{h} \cdot \Delta_{\mathbb{S}(X)} : \mathbb{S}(X) \rightarrow \mathbb{S}(X)

is the multilinear extension of

h \cdot \Delta_{X} : X \rightarrow X

(Here $\Delta$ is the usual diagonal or copying natural transformation.) Intuitively we can duplicate the input and still get a multilinear extension.

To confirm multilinearity,

\hat{h} \cdot \Delta \cdot \mu = \hat{h} \cdot \mu \times \mu \cdot \Delta = \mu \cdot \mathbb{S}(\hat{h}) \cdot \mathsf{dst} \cdot \Delta

= \mu \cdot \mathbb{S}(\hat{h}) \cdot \mathsf{dst} \cdot \langle \mathbb{S} \pi_1, \mathbb{S} \pi_2 \rangle \cdot \mathbb{S}(\Delta) = \mu \cdot \mathbb{S}(\hat{h}) \cdot \mathbb{S}(\Delta)

where the second step uses the assumed multilinearity, and the final step uses relevance of $\mathbb{S}$ .

Again, verifying the extension property is straightforward.

Generalising from this special case, multilinear extensions of relevant monads are closed under duplicating variables. Again, using the same argument as the previous post, relevant monads preserve equations that duplicate but don’t delete variables. We will refer to such equations as strictly duplicating, and use the term strictly duplicating presentation in the obvious way.

Consequences

Combining the proof principle of uniqueness of multilinear extensions with the additional closure properties above, we get a range of results. For a commutative monad $\mathbb{T}$ there is a distributive law:

\mathbb{T} \circ \mathbb{S} \Rightarrow \mathbb{S} \circ \mathbb{T}

$\mathbb{T}$ has a linear presentation.
$\mathbb{S}$ is affine and $\mathbb{T}$ has a strictly deleting presentation.
$\mathbb{S}$ is relevant and $\mathbb{T}$ has a strictly duplicating presentation.
$\mathbb{S}$ is Cartesian and $\mathbb{T}$ is any finitary monad.

Summary

The preservation theorems involving affine, relevant and Cartesian monads appear in the PhD thesis of Louis Parlant, although the proof strategy was somewhat different. Continuing Manes emphasis on multilinear maps provides a uniform perspective on all the different results.

Linearity, Laws and Liftings

We have seen that we can extend algebraic operations to powersets, and these extensions preserve linear equations. This allowed us to lift the powerset monad to the Eilenberg-Moore category of a monad presented by linear equations. Equivalently, this gives us sufficient conditions for a monad to distribute over the powerset monad.

Now we have some general results about multilinear extensions, we are finally at the point when we can:

Generalise the monad lifting and distributive law results we have seen so far beyond the powerset monad.
Identify what is special about linear equations that makes these constructions work.

The payoff will be theorems yielding lifted monads and distributive laws.

Closure Properties of Multilinear Morphism

We will work in a symmetric monoidal category, which we assume to be strict to keep discussions simple.

A first unsurprising result is that multilinear maps are closed under permutations of their arguments. Formally, if

\hat{f} : \mathbb{S}(X) \otimes \ldots \otimes \mathbb{S}(X) \rightarrow \mathbb{S}(X)

is the multilinear extension of

f : X \otimes \ldots \otimes X \rightarrow X

and

s_X : X \otimes \ldots \otimes X \rightarrow X \otimes \ldots \otimes X

is a natural transformation describing a permutation built using the symmetry natural transformation, then

\hat{f} \cdot s_{\mathbb{S}(X)} : \mathbb{S}(X) \otimes \ldots \otimes \mathbb{S}(X) \rightarrow \mathbb{S}(X)

is the multilinear extension of

f \cdot s_{X} : X \otimes \dots \otimes X \rightarrow X

The proof is a completely routine.

An important, and only slightly less obvious closure property is that multilinear extensions are closed under composition. For example, if

\hat{f}, \hat{g}, \hat{h} : \mathbb{S}(X) \otimes \mathbb{S}(X) \rightarrow \mathbb{S}(X)

are the respective bilinear extensions of

f,g,h : X \otimes X \rightarrow X

then the composite

h \cdot (f \otimes g) : \mathbb{S}(X) \otimes \mathbb{S}(X) \otimes \mathbb{S}(X) \otimes \mathbb{S}(X) \rightarrow \mathbb{S}(X)

is the multilinear extension of

h \cdot (f \otimes g) : X \otimes X \otimes X \otimes X \rightarrow X

The proof is another routine diagram chase.

Preservation of Linear Equations

We now return to the setting of algebraic structures on sets. Consider a structure with binary operations:

f,g,h : X \times X \rightarrow X

satisfying the linear equation:

h(f(w,x),g(y,z)) = h(g(y,z),f(w,x))

We can rephrase this in terms of composite morphisms as:

h \cdot (f \times g) = h \cdot (g \times f) \cdot s_X

where $s$ is the natural transformation that orders the arguments on the righthand side correctly.

Using the closure properties of multilinear extensions, the composites:

\hat{h} \cdot (\hat{f} \times \hat{g}) \quad\text{and}\quad \hat{h} \cdot (\hat{g} \times \hat{f}) \cdot s_{\mathbb{T}(X)}

are multilinear extensions of the left and right hand side of the previous equation. By the uniqueness of multilinear extensions:

\hat{h} \cdot (\hat{f} \times \hat{g}) = \hat{h} \cdot (\hat{g} \times \hat{f}) \cdot s_{\mathbb{T}(X)}

and so the equation lifts from $X$ to multilinear extensions of the operations on $\mathbb{S}(X)$ .

Note this argument would not work for equations that are not linear. The whole argument hinges on the proof principle that multilinear extensions are unique, but we have no closure property of multilinear extensions that allows us to drop or duplicate arguments. We will return to this topic in the next post.

We can generalise the above argument to an arbitrary linear equation, and so all such equations are preserved when extending operations to their multilinear extensions on $\mathbb{S}(X)$ .

Consequences

If monad $\mathbb{S}$ is commutative and monad $\mathbb{T}$ has a presentation only requiring linear equations:

The monad $\mathbb{S}$ lifts to the category $\mathsf{Set}^{\mathbb{T}}$ .
There is a distributive law of type $\mathbb{T} \circ \mathbb{S} \Rightarrow \mathbb{S} \circ \mathbb{T}$ .

Example: The multiset monad is both commutative and presented by linear equations. Therefore:

For any commutative monad $\mathbb{S}$ there is a distributive law of type $\mathbb{M} \circ \mathbb{S} \Rightarrow \mathbb{S} \circ \mathbb{M}$ .
For any monad $\mathbb{T}$ with a presentation by linear equations, there is a distributive law of type $\mathbb{T} \circ \mathbb{M} \Rightarrow \mathbb{M} \circ \mathbb{T}$ .

In particular, the multiset monad distributes over itself.

Summary

These results appear in Manes and Mulry “Monad Compositions I”, and many distributive laws arise in this way. These results are well-known, but the restriction linear equations is frustrating. In the next post, we will look at more recent results making a slightly different trade-off to circumvent the restriction to linear equations.

Monads and Multilinear Extensions

We have seen some general conditions under which we can lift the powerset monad to categories of algebras, or equivalently distribute other monads over it. In this post we look at the concrete construction we have been using for the powerset, and generalise the key ideas to a broader class of monads.

The Powerset Case

For a binary operation

\bullet : X \times X \rightarrow X

the extension to powersets

\hat{\bullet} : \mathcal{P}(X) \times \mathcal{P}(X) \rightarrow \mathcal{P}(X)

has some interesting properties.

Firstly, it commutes with units, in the following sense:

\{ u \} \hat{\bullet} \{ v \} = \{ u \bullet v \}

We can interpret this as saying $\hat{\bullet}$ extends the behaviour of $\bullet$ from individual elements to arbitrary sets.

Secondly, it commutes with unions in the following sense:

\bigcup \{ U \hat{\bullet} V \mid U \in \mathbf{U}, V \in \mathbf{V} \} = \bigcup \mathbf{U} \hat{\bullet} \bigcup \mathbf{V}

We can interpret this as requiring $\hat{\bullet}$ be a homomorphism with respect to unions in both its arguments. We say $\hat{\bullet}$ is bilinear in this case, borrowing terminology from linear algebra for argument-wise preservation of vector space structure.

The construction we are using yields a bilinear extension of any binary operation. Such extensions are unique, as we shall soon see as a corollary of a more general result. You may wish to consider how to prove this directly.

The General Case

The properties of the concrete construction we have been using that were identified above are crucial to its good behaviour. We now generalise those properties to more general monads.

Abstract Definitions

We can generalise the notion of extension to any monad $\mathbb{T} : \mathcal{C} \rightarrow \mathcal{C}$ on a monoidal category

(\mathcal{C}, \otimes, I)

For morphism

f : A \otimes B \rightarrow C

we say that morphism

f’ : \mathbb{T}(A) \otimes \mathbb{T}(B) \rightarrow \mathbb{T}(C)

is an extension of $f$ if

f’ \cdot \eta \otimes \eta = \eta \cdot f

To generalise bilinearity, we need to assume $\mathbb{T}$ is a commutative monad. For Eilenberg-Moore algebras

(A,\alpha), (B, \beta), (C,\gamma)

we say

g : A \otimes B \rightarrow C

is bilinear if

h \cdot \alpha \otimes \beta = \gamma \cdot \mathbb{T}(h) \cdot \mathsf{dst}

where $\mathsf{dst}$ is the double strength natural transformation given by our assumption that $\mathbb{T}$ is commutative.

Finally, we say that a morphism

h : \mathbb{T}(X) \otimes \mathbb{T}(Y) \rightarrow \mathbb{T}(Z)

is a bilinear extension of $f$ if it is an extension that is bilinear with respect to the free algebras

(\mathbb{T}(X), \mu_X), (\mathbb{T}(Y), \mu_Y), (\mathbb{T}(Z), \mu_Z)

Existence of Bilinear Extensions

With the terminology of the previous section, we can construct a bilinear extension of $f$ as

\mathbb{T}(f) \cdot \mathsf{dst} : \mathbb{T}(X) \otimes \mathbb{T}(Y) \rightarrow \mathbb{T}(Z)

To confirm this is an extension:

\mathbb{T}(f) \cdot \mathsf{dst} \cdot \eta \otimes \eta = \mathbb{T}(f) \cdot \eta = \eta \cdot f

For bilinearity

\mathbb{T}(f) \cdot \mathsf{dst} \cdot \mu \otimes \mu = \mathbb{T}(f) \cdot \mu \cdot \mathbb{T}(\mathsf{dst}) \cdot \mathsf{dst} = \mu \cdot \mathbb{T}(f) \cdot \mathbb{T}(\mathsf{dst}) \cdot \mathsf{dst}

Uniqueness of Bilinear Extensions

Assume $h$ and $k$ are bilinear, and they satisfy

h \cdot \eta \otimes \eta = k \cdot \eta \otimes \eta

This implies

\mu \cdot \mathbb{T}(h) \cdot \mathbb{T}(\eta \otimes \eta) \cdot \mathsf{dst} = \mu \cdot \mathbb{T}(k) \cdot \mathbb{T}(\eta \otimes \eta) \cdot \mathsf{dst}

Applying naturality, this is equivalent to

\mu \cdot \mathbb{T}(h) \cdot \mathsf{dst} \cdot \mathbb{T}(\eta) \otimes \mathbb{T}(\eta) = \mu \cdot \mathbb{T}(k) \cdot \mathbb{T}(\eta) \otimes \mathbb{T}(\eta)

Using the bilinearity property

h \cdot \mu \otimes \mu \cdot \mathbb{T}(\eta) \otimes \mathbb{T}(\eta) = k \cdot \mu \otimes \mu \cdot \mathbb{T}(\eta) \otimes \mathbb{T}(\eta)

Finally, using bifunctoriality and the right unit monad axiom:

h = k

As a pair of bilinear extensions of the same morphism satisfy our initial assumption, bilinear extensions are unique.

Summary

In this post we have abstracted some properties of the powerset monad to any commutative monad. Although these definitions isolate some interesting algebraic structure, they are perhaps slightly ill-motivated at this stage.

As is common in category theory, we have established an existence property that allows us to construct a gadget with desirable properties, and a uniqueness property that gives us a proof principle with which to reason about such gadgets. This perspective will be important when we look at the preservation of linear equations.

To keep things simple, we have concentrated on bilinearity. It is fairly straightforward to generalise further to multilinearity, which we leave to the enthusiastic reader.

More background on the machinery in this section can be found in:

Kock “Bilinearity and Cartesian Closed Monads”
Manes “A Class of Fuzzy Theories”
Jacobs “Semantics of weakening and contraction”

Distributing over the powerset

We saw in the previous post that we can lift the powerset monad to a monad on any category of algebras defined by linear equations. In this short post, we shall tidy some loose ends, leading to another perspective on what we have done.

Eilenberg-Moore Algebras

As we have discussed previously, every finitary monad

(\mathbb{T} : \mathsf{Set} \rightarrow \mathsf{Set}, \eta, \mu)

arises from the free / forgetful adjunction of an equationally defined category of algebras:

\mathsf{Alg}(\Sigma,E)

Furthermore, the Eilenberg-Moore category $\mathsf{Set}^{\mathbb{T}}$ is equivalent to $\mathsf{Alg}(\Sigma,E)$ .

Putting these two facts together, if $\mathbb{T}$ has a presentation only involving linear equations, the previous post shows that the powerset monad lifts to a monad:

(\hat{\mathbb{P}} : \mathsf{Set}^{\mathbb{T}} \rightarrow \mathsf{Set}^{\mathbb{T}}, \hat{\eta}, \hat{\mu})

Distributive Laws

We have encountered liftings to Eilenberg-Moore categories before. In that case, we were interested in lifting functors to Eilenberg-Moore categories. In this case, we are interested in lifting entire monads.

For monads:

(\mathbb{S}, \eta, \mu)\quad\text{and}\quad(\mathbb{T}, \eta, \mu)

there is a bijection between:

Liftings of the monad $\mathbb{S}$ to $\mathsf{Set}^{\mathbb{T}}$ .
Distributive laws of type $\mathbb{T} \circ \mathbb{S} \Rightarrow \mathbb{S} \circ \mathbb{T}$ .

This is a topic worthy of further discussion, which we will return to in a later post.

Combining this bijection with the previous observation, if the monad $\mathbb{T}$ has a presentation by linear equations, there is a distributive law:

\mathbb{T} \circ \mathbb{P} \Rightarrow \mathbb{P} \circ \mathbb{T}

Summing Up

Using some standard facts, and Gautam’s results about extending algebraic structure to powersets, we have found sufficient conditions for the existence of a distributive law of $\mathbb{T}$ over the powerset monad $\mathbb{P}$ .

Our next steps is to clarify at a higher level of abstraction what is going on, so we can move beyond the powerset to more general monads.

Lifting the Powerset Monad

In the previous post, we discussed extending algebraic operations on some set $X$ to operations on the powerset $\mathcal{P}(X)$ . It turned out that the construction we used preserved linear equations, such as those used to define monoids. As promised, we now relate these ideas to monads.

Categories of Algebras

We will work with a category of algebras $\mathcal{C}$ with:

Objects: A set $X$ , with a binary operation $\bullet: X \times X \rightarrow X$ and a constant $1 \in X$ .
Morphisms: A morphism $(X_1, \bullet_1, 1_1) \rightarrow (X_2, \bullet_2, 1_2)$ is a function $h : X_1 \rightarrow X_2$ that preserves the binary operation and constant.

Equationally, the homomorphism conditions are:

h(x \bullet_1 y) = h(x) \bullet_2 h(y) \quad\text{and}\quad h(1_1) = 1_2

The obvious forgetful functor $U : \mathcal{C} \rightarrow \mathsf{Set}$ will feature prominently in what follows.

Although we will restrict our discussions to this simple category of algebras, everything we discuss will generalise to categories of algebras with any number of operations with arbitrary arities.

Lifting the Powerset Functor

We would like to lift the powerset functor:

\mathcal{P} : \mathsf{Set} \rightarrow \mathsf{Set}

to a functor:

\hat{\mathcal{P}} : \mathcal{C} \rightarrow \mathcal{C}

By lift we mean that these functors will commute with the forgetful functor as follows:

U \circ \hat{\mathcal{P}} = \mathcal{P} \circ U

We already identified a suitable action on objects in the previous post. The lifting condition means there is only one potential action on morphisms:

\hat{\mathcal{P}}(h) = \mathcal{P}(h)

This will automatically commute with identities and composition, but we must verify that it yields a legitimate algebra morphism. For the binary operation:

\mathcal{P}(h)(U \hat{\bullet_1} V) = \{ h(u \bullet_1 v) \mid u \in U, v \in V \} = \{ h(u) \bullet_2 h(v) \mid u \in U, v \in V \} = \mathcal{P}(h)(U) \hat{\bullet_2} \mathcal{P}(h)(V)

and for the constant:

\mathcal{P}(h)(\hat{1_1}) = \{ h(1_1) \} = \{ 1_2 \} = \hat{1_2}

Lifting the Powerset Monad

As we have successfully lifted the powerset functor, our next steps is to lift the powerset monad

(\mathbb{P} : \mathsf{Set} \rightarrow \mathsf{Set}, \eta, \mu)

to a monad:

(\hat{\mathbb{P}} : \mathcal{C} \rightarrow \mathcal{C}, \hat{\eta}, \hat{\mu})

to $\mathcal{C}$ . By lifting, we mean a lifting of the powerset functor with unit $\hat{\eta} : 1 \rightarrow \hat{\mathbb{P}}$ and $\hat{\mu} : \hat{\mathbb{P}} \circ \hat{\mathbb{P}} \rightarrow \hat{\mathbb{P}}$ such that:

U \circ \hat{\eta} = \eta \circ U \quad\text{and}\quad U \circ \hat{\mu} = \mu \circ U

These conditions force that the unit and multiplication of the lifted monad have the same components as for the original powerset monad. We need to verify that these are legitimate algebra morphisms. For the unit:

\hat{\eta}(u \bullet_1 v) = \{ u \bullet_1 v \} = \{ u \} \hat{\bullet_1} \{ v \} = \eta(u) \hat{\bullet_1} \eta(v)

and for the multiplication:

\mathbf{U} \hat{\hat{\bullet}} \mathbf{V} = \bigcup \{ U \hat{\bullet} V \mid U \in \mathbf{U}, V \in \mathbf{V}\} = \{ u \bullet v \mid u \in \bigcup \mathbf{U}, v \in \bigcup \mathbf{V} \} = \mu(\mathbf{U}) \hat{\bullet} \mu(\mathbf{V})

That’s actually all we have to check. Naturality of the unit and multiplication, and the monad axioms follow from the forgetful functor being faithful, and the lifting conditions.

Summing up, we have shown that we can lift the powerset monad to the category $\mathcal{C}$ . Again, we can generalise, and lift the powerset monad to any category of algebraic structures.

Lifting the Powerset to Equational Classes

So far, we have lifted the powerset monad to categories of sets equipped with some completely unconstrained operations. This is moderately interesting, but normally we want such structures such as monoids which are required to satisfy some equations.

This is where the preservation of equations discussed in the previous post comes in. The object mapping

A \mapsto \hat{\mathbb{P}}(A)

is such that $\mathbb{P}(A)$ satisfies any linear equation satisfied by $A$ . This means we can restrict our lifted powerset monad to any class of algebras defined by linear equations. Intuitively, when we restrict to classes of algebras defined by linear equations, our lifted monad won’t “jump out” of the class we are interested in.

Example: The powerset monad lifts to the category of monoids, and the category of commutative monoids.

Example: This construction does not lift the powerset monad to the category of meet semilattices, as the idempotence equation is not linear, and will not be preserved in general.

Summing Up

We have shown that the powerset monad can be lifted to any category of algebras defined by linear equations. There are a few questions we should ask ourselves:

Can we generalise this construction beyond the powerset to other monads?
What’s going on with the mysterious linearity requirement on the equations?
Can we do anything with classes of algebras defined by more general equations?

We will move onto these questions in subsequent posts.

Lifting Algebras to Powersets

Lifting Monoids

Imagine I give you a monoid $(M,\times,1)$ , is there a way to construct a new monoid structure $(\mathcal{P}(M),\hat{\times},\hat{1})$ with underlying set the powerset of $M$ ?

A natural approach is to extend the monoid operations pointwise:

U \hat{\times} V = \{ u \times v \mid u \in U, v \in V \}

and

\hat{1} = \{ 1 \}

For this to yield a legitimate monoid, we need to verify the associativity and unit equations hold. For associativity:

U \hat{\times} (V \hat{\times} W) = \{ u \times (v \times w ) \mid u \in U, v \in V, w \in V \}

and

(U \hat{\times} V) \times W = \{ (u \times v) \times w \mid u \in U, v \in V, w \in W \}

The resulting sets are equal by the associativity of the original monoid multiplication. Similarly for the left unit axiom:

\hat{1} \hat{\times} U = \{ 1 \times u \mid u \in U \} = U

where the second equality uses the unit axiom of the original monoid. The other unit axiom follows symmetrically. The pointwise construction yields a monoid as we might have hoped.

Lifting special classes of monoids

As the obvious pointwise construction worked out nicely, allowing us to lift monoid structure to powersets, lets push our luck a bit. What if we want to lift commutative monoid structure in the same way? We then need to check that the commutativity axiom is also preserved by our construction:

U \hat{\times} V = \{ u \times v \mid u \in U, v \in V \} = \{ v \times u \mid v \in V, u \in U \} = V \hat{\times} U

Again, the only interesting step is to exploit the new assumption of commutativity for the underlying commutative monoid.

This is looking pretty good, maybe this construction always works? Let’s push our luck a bit further. Can we lift commutative, idempotent monoids (a.k.a semilattices) to powersets? We now need to verify that idempotence is preserved:

U \hat{\times} U = \{ u_1 \times u_2 \mid u_1,u_2 \in U \} \neq U

In this case we get into trouble, as applying the assumed idempotence of the underlying monoid doesn’t allow us to relate the left and right hand sides in general. Idempotence is not preserved by this construction. Disappointing, but at least we’ve learnt something. We also have an interesting question: which equations are preserved by the pointwise construction, and which ones are not?

When are Equations Preserved?

As we only have one example of an equation that breaks so far, we don’t have much to go on. Lets try and get another data point. Instead of assuming our original structure is a monoid, lets assume it satisfies the following annihilation property:

1 \times x = 1

Is this property preserved when we move to powersets?

\hat{1} \hat{\times} U = \{ 1 \times u \mid u \in U \}

We need to be a bit careful here. If $U$ is non-empty then the above is equal to $\hat{1}$ , but if $U$ is the empty set:

\hat{1} \hat{\times} \emptyset = \emptyset \neq \hat{1}

So the annihilation property is not preserved. (You may want to double-check the emptyset doesn’t cause any trouble for the previous equations we’ve looked at).

Lets recap, and see if we can spot a pattern. The following equations are preserved:

Associativity: $x \times (y \times z) = (x \times y) \times z$
Left unit: $1 \times x = x$
Right unit: $x \times 1 = x$
Commutativity: $x \times y = y \times x$

On the other hand, the following equations are not preserved:

Idempotence: $x \times x = x$
(Left) annihilation: $1 \times x = 1$

If you’ve made it this far, you may wish to pause before continuing and see if you can conjecture what the key difference between these two classes of properties is. You may wish to experiment with a few more equational properties to gather more data points.

Looking at the equations above, there is a pattern in terms of how variables are used:

For equations that are preserved the same set of variables appear on the left and right hand side, and they each appear exactly once.
Otherwise the equation is not preserved.

We say that an equation is linear if it satisfies this property.

Of course, this observation applies more generally, to algebraic structures with arbitrary signatures. Linear equations are exactly the equations that are preserved when lifting algebraic structure pointwise to the powerset.

This result in due to Gautam “The Validity of Equations of Complex Algebras”.

Where are the Monads?

This is supposed to be a blog about monads, but we have not mentioned them so far. In fact, Gautam’s work is a first step into some interesting ideas involving monads; we will start to explore the implications in the next post. Enthusiastic readers might want to speculate how the observations above can be applied.

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:

A collection of objects $X,Y,\ldots$ .
For every pair of object $X,Y$ , a hom object $\mathcal{A}(X,Y)$ .
For each object $X$ , an identity $\mathcal{V}$ -morphism $j_X : I \rightarrow \mathcal{A}(X,X)$ .
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:

A $\mathcal{V}$ -enriched category with set of objects $O$ .
A monad on $O$ in $\mathbf{Mat}(\mathcal{V})$ .
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:

A collection of objects $X,Y,Z$ , each with an associated extent, given by a 0-cell $\mathsf{ext}(X)$ in $\mathcal{W}$ .
For every pair of objects $X,Y$ , a hom 1-cell $\mathcal{A}(X,Y) : \mathsf{ext}(X) \rightarrow \mathsf{ext}(Y)$ .
For every object $X$ , an identity 2-cell $j_A : \mathsf{Id}_{\mathsf{ext}(X)} \Rightarrow \mathcal{A}(X,X)$ .
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:

An object, with extent a 0-cell $\mathcal{C}$ in $\mathcal{W}$ .
A single hom 1-cell $\mathbb{T} : \mathcal{C} \rightarrow \mathcal{C}$ .
An identity 2-cell $\eta : \mathsf{Id} \Rightarrow \mathbb{T}$ .
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:

An internal category in $\mathcal{C}$ .
A monad in $\mathbf{Span}(\mathcal{C})$ .
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.

Algebras are regular quotients of free algebras

The aim of this post is to show that for a monad

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

every Eilenberg-Moore algebra $(A,\alpha : \mathbb{T}(A) \rightarrow A)$ is given as the coequalizer of a parallel pair of morphisms between free algebras in $\mathcal{C}^{\mathbb{T}}$ . In this case, we say that $(A,\alpha)$ is a regular quotient of free algebras. Notice we are not making any any assumptions about the base category $\mathcal{C}$ such as (co)completeness, so we don’t have a lot to work with. Really the only available structure is:

The unit and multiplication of the monad, and the axioms they satisfy.
The two axioms that every Eilenberg-Moore algebra satisfies relating its structure map to the unit and multiplication.

So we have a handful of morphisms, and some equations that they satisfy, and that’s it. Let’s have a look at how this magic trick is performed.

A parallel pair of algebra morphisms

As a first step, we note that for an Eilenberg-Moore algebra $(A,\alpha)$ , we have a parallel pair of $\mathcal{C}^{\mathbb{T}}$ morphisms:

$\mu_A, \mathbb{T}(\alpha) : F^{\mathbb{T}}(\mathbb{T}(A)) \rightarrow F^{\mathbb{T}}(A)$

Expanding the action of the free algebra functor, this is a pair of morphisms:

$\mu_A, \mathbb{T}(\alpha) : (\mathbb{T}^2(A), \mu_{\mathbb{T}^2(A)}) \rightarrow (\mathbb{T}(A), \mu_A)$

That $\mu_A$ is an algebra morphism is equivalent to the Eilenberg-Moore algebra multiplication axiom. That $\mathbb{T}(\alpha)$ is an algebra morphism is simply naturality of the monad multiplication.

By naturality of $\mu$ , we note that there is an algebra morphism in the opposite direction:

$\mathbb{T}(\eta_A) : (\mathbb{T}(A), \mu_A) \rightarrow (\mathbb{T}^2(A), \mu_{\mathbb{T}^2(A)})$

Furthermore, by the monad right unitality axiom

$\mu_A \cdot \mathbb{T}(\eta_A) = \mathsf{id}_{\mathbb{T}(A)}$

and by the algebra unit axiom:

$\mathbb{T}(\alpha) \cdot \mathbb{T}(\eta_A) = \mathsf{id}_{\mathbb{T}(A)}$

Therefore these three morphisms form a reflexive pair.

A coequalizer in the base category

We now apply the forgetful functor $U^{\mathbb{T}} : \mathcal{C}^{\mathbb{T}} \rightarrow \mathcal{C}$ , yielding a parallel pair.

$U^{\mathbb{T}}(\mu_A), U^{\mathbb{T}}(\mathbb{T}(\alpha)) : U^{\mathbb{T}} \circ F^{\mathbb{T}}(\mathbb{T}(A)) \rightarrow U^{\mathbb{T}}(\alpha) : U^{\mathbb{T}} \circ F^{\mathbb{T}}(A)$

which if we unpack the definitions is simply a parallel pair of $\mathcal{C}$ -morphisms:

$\mu_A, \mathbb{T}(\alpha) : \mathbb{T}^2(A) \rightarrow \mathbb{T}(A)$

Our current aim is to find a coequalizer of this pair, knowing it must have codomain $A$ . The obvious choice is to consider

$\alpha : \mathbb{T}(A) \rightarrow A$

as our candidate universal coequalizer morphism. By the algebra multiplication axiom, we have

$\alpha \cdot \mu_A = \alpha \cdot \mathbb{T}(\alpha)$

which is an encouraging first step to establishing this forms a coequalizer diagram. To establish the universal property, we are going to need a bit more. Using components of the monad unit, we get two other useful $\mathcal{C}$ -morphisms:

$\eta_A : A \rightarrow \mathbb{T}(A)$ .
$\eta_{\mathbb{T}(A)} : \mathbb{T}(A) \rightarrow \mathbb{T}^2(A)$ .

By the algebra unit axiom

$\alpha \cdot \eta_A = \mathsf{id}_A$

and by the monad left unitality axiom

$\mu_A \cdot \eta_{\mathbb{T}(A)} = \mathsf{id}_{\mathbb{T}(A)}$

Finally, by naturality:

$\mathbb{T}(\alpha) \cdot \eta_{\mathbb{T}(A)} = \eta_A \cdot \alpha$ .

We have shown the our parallel pair form a contractible coequalizer in the base category, and further that the parallel pair of algebra morphism:

$\mu_A, \alpha : F^{\mathbb{T}}(\mathbb{T}(A)) \rightarrow F^{\mathbb{T}}(A)$

form a reflexive $U^{\mathbb{T}}$ -contractible pair.

An algebra coequalizer

We would now like to conclude we have a coequalizer in the Eilenberg-Moore category. Recall that the forgetful functor $U^{\mathbb{T}} : \mathcal{C}^{\mathbb{T}} \rightarrow \mathcal{C}$ creates colimits that are preserved by $\mathbb{T}$ and $\mathbb{T}^2$ . As contractible coequalizers are absolute colimits, we can apply this result to lift the coequalizer to the Eilenberg-Moore category.

Finally, we note that $\alpha$ is in fact an algebra morphism of type:

$F^{\mathbb{T}}(A) \rightarrow (A,\alpha)$

by the Eilenberg-Moore algebra multiplication axiom. Therefore

$F^{\mathbb{T}}(\mathbb{T}(A)) \xrightarrow{ \mu_A, \alpha} F^{\mathbb{T}}(A) \xrightarrow{\alpha} (A,\alpha)$

is a coequalizer diagram in the Eilenberg-Moore category, and $(A,\alpha)$ is a regular quotient of free algebras as claimed.

Conclusion

We encountered reflexive $U$ -contractible coequalizers in the statement of Beck’s monadicity theorem. In this post, we have seen one example of why these particular absolute colimits are important in the theory of monads, as they can be used to construct every Eilenberg-Moore algebra as a quotient of a free algebra.

Proving this result from very few assumptions, beyond some morphisms satisfying certain equations, leads us to the construction of coequalizers which are defined by by equations between morphisms. Such constructions are necessary absolute, and this at least partially explains the significance of absolute colimits in this context.

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.