stringdiagram

Quotients of Commutative, Affine and Relevant Monads

We have seen that nice properties such as being commutative, affine, or relevant can be transferred to strong submonads. A natural question to ask is whether something similar applies to quotients? In fact, we can apply the tricks we’ve already seen to get straight to some answers.

Commutative Monads

As strong monad morphisms commute with double strengths, if

\varphi : (\mathbb{T}, \mathsf{st}) \Rightarrow (\mathbb{Q}, \mathsf{st})

is a strong monad morphism, and $\mathbb{T}$ is commutative, we can immediately show

\mathsf{dst}^{\mathbb{Q}} \cdot \varphi \otimes \varphi = \mathsf{dst}^{\mathbb{Q}’} \cdot \varphi \otimes \varphi

If $\varphi \otimes \varphi$ is component-wise epimorphic, then

\mathsf{dst}^{\mathbb{Q}} = \mathsf{dst}^{\mathbb{Q}’}

and $\mathbb{Q}$ is commutative. Even if we restrict attention to where the monoidal structure is products, this condition is not as straightforward as that for monomorphisms. Fortunately there are many special cases where $\varphi$ being a component-wise epimorphism implies $\varphi \times \varphi$ is. In particular, this works nicely for $\mathsf{Set}$ -monads. As all natural transformation are strong in that case, we have

Quotients of commutative monads are commutative.

Affine, Relevant and Cartesian Monads

\varphi : (\mathbb{T}, \mathsf{st}) \Rightarrow (\mathbb{Q}, \mathsf{st})

is a strong monad morphism, and $\mathbb{T}$ is affine, then using the same calculational properties as we did for submonads, but in reverse, we can conclude

\langle \mathbb{Q}\pi_1, \mathbb{Q}\pi_2 \rangle \cdot \mathsf{dst}^{\mathbb{Q}} \cdot \varphi \times \varphi = \varphi \times \varphi

and so if $\varphi \times \varphi$ is component-wise epimorphic

\langle \mathbb{Q}\pi_1, \mathbb{Q}\pi_2 \rangle \cdot \mathsf{dst}^{\mathbb{Q}} = \mathsf{id}

If we restrict attention to $\mathsf{Set}$ -monads, using the result of the previous section, we can conclude

Quotients of affine monads are affine.

A very similar argument allows us to conclude that for $\mathsf{Set}$ -monads

Quotients of relevant monads are relevant.

Combining both these observations gives

Quotients of Cartesian monads are Cartesian.

Algebraic Interpretation

As usual, it pays to see if we use algebraic intuition to justify our conclusions. If we consider $\mathsf{Set}$ -monads presented by operations and equations, being commutative, affine, relevant or Cartesian requires that certain equations between terms hold. We can think of quotient monads as imposing extra equations between terms, so it is unsurprising quotient monads continue to have these nice properties.

Summary

The conclusions above are less general than for submonads. This is because epimorphisms do not interact as nicely with products as monomorphisms do. In the case of $\mathsf{Set}$ -monads everything was about as well-behaved as we could possibly hope.

Affine and Relevant Strong Submonads

We have seen that we can transfer commutativity to strong submonads. Can we transfer other good properties, such as being an affine or relevant monad as well?

Another Commutativity Property

As we are now interested in affine and relevant monads, this post will assume we are working in a category with finite products. We have seen that strong natural transformations commute with double strength. This property will be crucial again today, but we will also need another simple equation.

For a natural transformation

\varphi : F \Rightarrow G

the following equation holds

\varphi \times \varphi \cdot \langle F \pi_1, F \pi_1 \rangle = \langle G \pi_2, G \pi_2 \rangle \cdot \varphi

The proof is a straightforward combination of properties of products and naturality.

Affine Monads

Assume that $\mathbb{T}$ is a affine monad. That is, it is a commutative monad such that the following equation holds

\langle \mathbb{T} \pi_1, \mathbb{T} \pi_2 \rangle \cdot \mathsf{dst}^{\mathbb{T}} = \mathsf{id}

\varphi : (\mathbb{S}, \mathsf{st}) \Rightarrow (\mathbb{T}, \mathsf{st})

a strong monad morphism, then

\varphi \times \varphi \cdot \langle \mathbb{S}\pi_1, \mathbb{S}\pi2 \rangle \cdot \mathsf{dst}^{\mathbb{S}} = \langle \mathbb{T}\pi_1, \mathbb{T}\pi2 \rangle \cdot \varphi \cdot \mathsf{dst}^{\mathbb{S}} = \langle \mathbb{T} \pi_1, \mathbb{T} \pi_2 \rangle \cdot \mathsf{dst}^{\mathbb{T}} \cdot \varphi \times \varphi = \varphi \times \varphi

If $\varphi$ is component-wise a monomorphism, then so is $\varphi \times \varphi$ , and so

\langle \mathbb{S} \pi_1, \mathbb{S} \pi_2 \rangle \cdot \mathsf{dst}^{\mathbb{S}} = \mathsf{id}

Combining this with the results of the previous post, $\mathbb{S}$ is then an affine monad. In categories with pullbacks, we can strengthen this to

Strong submonads of affine monads are affine.

When the base category is set we can go further, to the slogan

Submonads of affine monads are affine.

Relevant Monads

The argument for relevant monads is even easier. Assume $\mathbb{T}$ is a relevant monad, so the following equation holds:

\mathsf{dst}^{\mathbb{T}} \cdot \langle \mathbb{T} \pi_1, \mathbb{T} \pi_2 \rangle = \mathsf{id}

\varphi : (\mathbb{S}, \mathsf{st}) \Rightarrow (\mathbb{T}, \mathsf{st})

is a strong monad morphism, then:

\varphi \cdot \mathsf{dst}^{\mathbb{S}} \cdot \langle \mathbb{S} \pi_1, \mathbb{S} \pi_2 \rangle = \mathsf{dst}^{\mathbb{T}} \cdot \varphi \times \varphi \cdot \langle \mathbb{S} \pi_1, \mathbb{S} \pi_2 \rangle = \mathsf{dst}^{\mathbb{T}} \cdot \langle \mathbb{T} \pi_1, \mathbb{T} \pi_2 \rangle \cdot \varphi = \varphi

and so if $\varphi$ is component-wise a monomorphism

\mathsf{dst}^{\mathbb{S}} \cdot \langle \mathbb{S} \pi_1, \mathbb{S} \pi_2 \rangle = \mathsf{id}

and from the results of the previous post, $\mathbb{S}$ is relevant. For categories with pullbacks, we have the slogan

Strong submonads of relevant monads are relevant.

and in the case of set monads we get the punchier

Submonads of relevant monads are relevant.

Cartesian Monads

As Cartesian monads are simply monads which are both affine and relevant, we can combine the previous two results to deduce that:

Strong submonads of Cartesian monads are Cartesian.

Algebraic Intuitions

For set monads, being affine or relevant requires that certain equations hold between terms. If we think of a submonad as dropping some of the algebraic structure whilst retaining all applicable equations, intuitively we would expect being affine or relevant to still hold.

Summary

Commutative, affine, relevant and Cartesian monads were important when we discussed both well-known and more recent sufficient conditions for the existence of distributive laws. These results allow us to extract new such monads from those we already understand.

Commutativity of Strong Submonads

In this post we begin to explore transferring nice properties of monads to their submonads. A key tool will be strong monad morphisms. These are monad morphisms which are also strong natural transformations.

Strong Natural Transformations and Right-Strength

In a symmetric monoidal category $\mathcal{C}$ , given a strong endofunctor

(F, \mathsf{st} : X \otimes F(Y) \Rightarrow F(X \otimes Y)

we can define a right-strength natural transformation

\mathsf{st}’ : F(X) \otimes Y \Rightarrow F(X \otimes Y)

by pre and post-composition with the symmetry of $\mathcal{C}$ .

For strong endofunctors

(F,\mathsf{st})\quad\text{and}\quad (G, \mathsf{st})

requiring that an ordinary natural transformation

\varphi : F \Rightarrow G

be a strong natural transformation is equivalent to requiring it commutes with the left-strengths as follows:

\mathsf{st}’ \cdot \varphi \otimes \mathsf{id} = \varphi \cdot \mathsf{st}’

We see that in this case, being a strong natural transformation can equivalently be phrased in terms of commuting with either the left or right strength. This gives us another convenient equation we can apply in calculations.

Strong Monad Morphisms and Double Strengths

Recall for a strong monad on a monoidal category, using the left and right strength, and the monad multiplication, we can define two double strength natural transformations:

\mathsf{dst}, \mathsf{dst}’ : \mathbb{T}(X) \otimes \mathbb{T}(Y) \Rightarrow \mathbb{T}(X \otimes Y)

A monad is commutative when the double strengths are equal.

For a strong monad morphism

\varphi : (\mathbb{S},\mathsf{st}) \Rightarrow (\mathbb{T}, \mathsf{st})

we can apply commutativity with respect to the left and right strength, and the monad morphism assumption to show that $\varphi$ commutes with both double strengths. That is:

\mathsf{dst}^{\mathbb{T}} \cdot \varphi \otimes \varphi = \varphi \cdot \mathsf{dst}^{\mathbb{S}} \quad\text{and}\quad \mathsf{dst}^{\mathbb{T}’} \cdot \varphi \otimes \varphi = \varphi \cdot \mathsf{dst}^{\mathbb{S}’}

We have added explicit superscripts to indicate to which monad each double strength corresponds.

This is a key property of strong monad morphisms that allows us to prove some interesting results.

Strong Submonads of Commutative Monads

If we have a $\varphi$ as above, assuming the monad $\mathbb{T}$ is commutative, we can calculate:

\varphi \cdot \mathsf{dst}^{\mathbb{S}} = \mathsf{dst}^{\mathbb{T}} \cdot \varphi \otimes \varphi = \mathsf{dst}^{\mathbb{T}’} \cdot \varphi \otimes \varphi = \varphi \cdot \mathsf{dst}^{\mathsf{S}’}

where the middle equality uses the commutativity assumption. Now if $\varphi$ is component-wise a monomorphism, we can conclude that:

\mathsf{dst}^{\mathbb{S}} = \mathsf{dst}^{\mathbb{S}’}

and so the monad $\mathbb{S}$ is commutative.

In full generality, we need the component-wise monomorphism assumption, but if the base category has pullbacks, this is equivalent to requiring $\varphi$ be a monomorphism. In this case it seems appropriate to use the following slogan:

A strong submonad of a commutative monad is commutative.

It is not hard to verify that every natural transformation between set endofunctors is strong. We then get the snappier slogan:

A submonad of a commutative monad is commutative.

Algebraic Intuitions

If we present a set monad by algebraic operations and equations, we have seen that commutativity of a monad is equivalent to all the algebraic operations commuting with each other. If we think of a submonad as dropping some of the algebraic structure whilst retaining all the applicable equations, it is perhaps unsurprising that the monad remains commutative.

Summary

Commutativity is a valuable property to identify in a monad. As verifying commutativity can be a bit of a pain, being able to transfer it to strong submonads can be very convenient.

We will see in forthcoming posts that this is not the only nice property we can transfer along strong monad morphisms.

A Strong Monad is Monoid in the Category of Strong Endofunctors

We encountered the notion of strength when we introduced strong monads. Strength has turned out to be an important idea, for example in discussion of commutative monads which underpin a lot of monad theory.

As strength is so important, we are going to back up, and examine it in a bit more detail, eventually arriving at a concise definition of strong monad.

Our ulterior motive is to set up some background on strong natural transformations so we can learn more about commutative, affine, relevant and cartesian monads in future posts.

Strong functors

Recall, a strength for an endofunctor

F : \mathcal{C} \rightarrow \mathcal{C}

on a monoidal category is a natural transformation

\mathsf{st} : X \otimes F(Y) \Rightarrow F (X \otimes Y)

compatible with the monoidal left unitor and associator, in that

F \lambda \cdot \mathsf{st} = \lambda

and

F \alpha \cdot \mathsf{st} = \mathsf{st} \cdot \mathsf{id} \otimes \mathsf{st} \cdot \alpha

A strong functor is a pair

(F, \mathsf{st} : X \otimes F(Y) \Rightarrow F(X \otimes Y))

consisting of an endofunctor and a choice of strength.

Strong natural transformations

We now introduce the key notion of this post. A strong natural transformation

\varphi : (F,\mathsf{st}) \rightarrow (G,\mathsf{st})

is an ordinary natural transformation

\varphi : F \Rightarrow G

which commutes with strengths. That is:

\mathsf{st} \cdot \mathsf{id} \otimes \varphi = \varphi \cdot \mathsf{st}

We will overload the symbol $\mathsf{st}$ for any strength to avoid a proliferation of symbols.

Categorical Structure

For a monoidal category $\mathcal{C}$ there is a category $\mathsf{Strong(\mathcal{C})}$ with:

Objects: Strong endofunctors on $\mathcal{C}$
Morphisms: Strong natural transformations, with composition and identities as for ordinary natural transformations.

Checking the required closure properties of strong natural transformations is a routine exercise.

Monoidal Structure

For a monoidal category $\mathcal{C}$ , there is a strict monoidal structure on $\mathsf{Strong}(\mathcal{C})$ with unit

(\mathsf{Id}_{\mathcal{C}}, \mathsf{id})

The tensor product on objects is:

(G,\mathsf{st}) \circ (F, \mathsf{st}) = (G \circ F, X \otimes GF(Y) \xrightarrow{\mathsf{st}}G(X \otimes F(Y)) \xrightarrow{G \mathsf{st}} GF(X \otimes Y))

For morphisms

\varphi : (F_1, \mathsf{st}) \Rightarrow (F_2, \mathsf{st}) \quad\text{and}\quad \gamma : (G_1, \mathsf{st}) \Rightarrow (G_2, \mathsf{st})

their tensor product is the usual composition of natural transformations

\gamma \circ \varphi : G_1 \circ F_1 \Rightarrow G_2 \circ F_2

Verifying the monoidal structure is routine, if fiddly, exercise in applying the definitions.

Strong Monads

When we previously discussed strong monads, the definition was only sketched, with detailed deferred to other sources. We are now in a position to give a precise definition of what a strong monad is

A strong monad is a monoid in the category of strong endofunctors.

This is easy to remember, as it is a small variation on the internets favourite meme about monads:

A monad is a monoid in the category of endofunctors.

We just sprinkle the term strong over the slogan for monads, and we get the corresponding slogan for strong monads.

It is not hard to see that there is a strict monoidal forgetful functor to the ordinary category of endofunctors

\mathsf{Strong}(\mathcal{C}) \rightarrow [\mathcal{C}, \mathcal{C}]

so every strong monad is an ordinary monad, along with some additional strength data.

Unpacking the Definition

If we unpack the concise definition above, a strong monad is:

A strong endofunctor $(\mathbb{T} : \mathcal{C} \rightarrow \mathcal{C}, \mathsf{st})$
A unit strong natural transformation $(\mathsf{Id}, \mathsf{id}) \Rightarrow (\mathbb{T}, \mathsf{st})$
A multiplication strong natural transformation $(\mathbb{T},\mathsf{st}) \circ (\mathbb{T}, \mathsf{st}) \Rightarrow (\mathbb{T}, \mathsf{st})$

Such that the usual unit and multiplication axioms hold.

Applying the Definition

To show that this is not just an exercise in meme generation, we can apply the definition above to deduce what a distributive law of strong monad $(\mathbb{T}, \mathsf{st})$ over strong monad $(\mathbb{S}, \mathsf{st})$ should be. We require a strong natural transformation:

\lambda : (\mathbb{T}, \mathsf{st}) \circ (\mathbb{S}, \mathsf{st}) \Rightarrow (\mathbb{S}, \mathsf{st}) \circ (\mathbb{T}, \mathsf{st})

satisfying formally identical equations to those of an ordinary distributive law. Unpacking this, $\lambda$ must be an ordinary distributive law, also satisfying:

\mathbb{S}(\mathsf{st}) \cdot \mathsf{st} \cdot 1 \otimes \lambda = \lambda \cdot \mathbb{T}(\mathsf{st}) \cdot \mathsf{st}

This yields the same definition given in Jacobs “Semantics of Weakening and Contraction” for example.

Summary

By identifying the correct mathematical structure, we have arrived at a concise definition of strong monad paralleling one of the familiar definitions for monads.

Inquisitive readers may wonder if any of the other definitions transfer over cleanly. For example, can we define a strong monad as a monad in a different 2-category? The answer is not yet (except in a rather degenerate way)! As with most things, there is a more general definition of strength, which amongst other things allows us to move away from the restriction to endofunctors that has been conspicuous in this post. Our current level of generality will be sufficient for some forthcoming posts. We may return to this topic on a later occasion. Details can be found on the NLab for example.

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.