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,𝗌𝗍:X⊗F(Y)⇒F(X⊗Y)(F, \mathsf{st} : X \otimes F(Y) \Rightarrow F(X \otimes Y)

we can define a right-strength natural transformation

𝗌𝗍′:F(X)⊗Y⇒F(X⊗Y)\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,𝗌𝗍)and(G,𝗌𝗍)(F,\mathsf{st})\quad\text{and}\quad (G, \mathsf{st})

requiring that an ordinary natural transformation

φ:F⇒G\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:

𝖽𝗌𝗍,𝖽𝗌𝗍′:𝕋(X)⊗𝕋(Y)⇒𝕋(X⊗Y)\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:

𝖽𝗌𝗍𝕋⋅φ⊗φ=φ⋅𝖽𝗌𝗍𝕊and𝖽𝗌𝗍𝕋′⋅φ⊗φ=φ⋅𝖽𝗌𝗍𝕊′\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.

One thought on “Commutativity of Strong Submonads”

  1. Pingback: Affine and Relevant Strong Submonads – Dan Marsden

Leave a comment