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

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

is the multilinear extension of

h:XXh : X \rightarrow X

then the composite

h^π1:𝕊(X)×𝕊(X)𝕊(X)\hat{h} \cdot \pi_1 : \mathbb{S}(X) \times \mathbb{S}(X) \rightarrow \mathbb{S}(X)

is the multilinear extension of

hπ1:X×XXh \cdot \pi_1 : X \times X \rightarrow X

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

To confirm multilinearity,

h^π1μ×μ=h^μπ1=μ𝕊(h^)π1\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
=μπ1𝕊(h^)π1𝕊π1,𝕊π2𝖽𝗌𝗍=μ𝕊(h^)𝕊π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

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

is the multilinear extension of

h:X×XXh : X \times X \rightarrow X

then the composite

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

is the multilinear extension of

hΔX:XXh \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,

h^Δμ=h^μ×μΔ=μ𝕊(h^)𝖽𝗌𝗍Δ\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
=μ𝕊(h^)𝖽𝗌𝗍𝕊π1,𝕊π2𝕊(Δ)=μ𝕊(h^)𝕊(Δ)= \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}

if

  • \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:

  1. Generalise the monad lifting and distributive law results we have seen so far beyond the powerset monad.
  2. 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

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

is the multilinear extension of

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

and

sX:XXXXs_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

f^s𝕊(X):𝕊(X)𝕊(X)𝕊(X)\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

fsX:XXXf \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

f^,g^,h^:𝕊(X)𝕊(X)𝕊(X)\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:XXXf,g,h : X \otimes X \rightarrow X

then the composite

h(fg):𝕊(X)𝕊(X)𝕊(X)𝕊(X)𝕊(X)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(fg):XXXXXh \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×XXf,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))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(f×g)=h(g×f)sXh \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:

h^(f^×g^)andh^(g^×f^)s𝕋(X)\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:

h^(f^×g^)=h^(g^×f^)s𝕋(X)\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:

  1. The monad \mathbb{S} lifts to the category \mathsf{Set}^{\mathbb{T}}.
  2. 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:

  1. For any commutative monad \mathbb{S} there is a distributive law of type \mathbb{M} \circ \mathbb{S} \Rightarrow \mathbb{S} \circ \mathbb{M}.
  2. 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

:X×XX\bullet : X \times X \rightarrow X

the extension to powersets

^:𝒫(X)×𝒫(X)𝒫(X)\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}^{v}={uv}\{ 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:

{U^V|U𝐔,V𝐕}=𝐔^𝐕\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

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

For morphism

f:ABCf : A \otimes B \rightarrow C

we say that morphism

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

is an extension of f if

fηη=ηff’ \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,α),(B,β),(C,γ)(A,\alpha), (B, \beta), (C,\gamma)

we say

g:ABCg : A \otimes B \rightarrow C

is bilinear if

hαβ=γ𝕋(h)𝖽𝗌𝗍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:𝕋(X)𝕋(Y)𝕋(Z)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

(𝕋(X),μX),(𝕋(Y),μY),(𝕋(Z),μZ)(\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

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

To confirm this is an extension:

𝕋(f)𝖽𝗌𝗍ηη=𝕋(f)η=ηf\mathbb{T}(f) \cdot \mathsf{dst} \cdot \eta \otimes \eta = \mathbb{T}(f) \cdot \eta = \eta \cdot f

For bilinearity

𝕋(f)𝖽𝗌𝗍μμ=𝕋(f)μ𝕋(𝖽𝗌𝗍)𝖽𝗌𝗍=μ𝕋(f)𝕋(𝖽𝗌𝗍)𝖽𝗌𝗍\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ηη=kηηh \cdot \eta \otimes \eta = k \cdot \eta \otimes \eta

This implies

μ𝕋(h)𝕋(ηη)𝖽𝗌𝗍=μ𝕋(k)𝕋(ηη)𝖽𝗌𝗍\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

μ𝕋(h)𝖽𝗌𝗍𝕋(η)𝕋(η)=μ𝕋(k)𝕋(η)𝕋(η)\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μμ𝕋(η)𝕋(η)=kμμ𝕋(η)𝕋(η)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=kh = 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:

𝖠𝗅𝗀(Σ,E)\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:

(𝕊,η,μ)and(𝕋,η,μ)(\mathbb{S}, \eta, \mu)\quad\text{and}\quad(\mathbb{T}, \eta, \mu)

there is a bijection between:

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(x1y)=h(x)2h(y)andh(11)=12h(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𝒫^=𝒫UU \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:

𝒫^(h)=𝒫(h)\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:

𝒫(h)(U1^V)={h(u1v)|uU,vV}={h(u)2h(v)|uU,vV}=𝒫(h)(U)2^𝒫(h)(V)\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:

𝒫(h)(11^)={h(11)}={12}=12^\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η^=ηUandUμ^=μUU \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:

η^(u1v)={u1v}={u}1^{v}=η(u)1^η(v)\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:

𝐔^^𝐕={U^V|U𝐔,V𝐕}={uv|u𝐔,v𝐕}=μ(𝐔)^μ(𝐕)\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^(A)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:

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

We will move onto these questions in subsequent posts.

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.

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:

  1. The unit and multiplication of the monad, and the axioms they satisfy.
  2. 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:

  1. \eta_A : A \rightarrow \mathbb{T}(A).
  2. \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.