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

φ:F⇒G\varphi : F \Rightarrow G

the following equation holds

φ×φ⋅⟨Fπ1,Fπ1⟩=⟨Gπ2,Gπ2⟩⋅φ\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

⟨𝕋π1,𝕋π2⟩⋅𝖽𝗌𝗍𝕋=𝗂𝖽\langle \mathbb{T} \pi_1, \mathbb{T} \pi_2 \rangle \cdot \mathsf{dst}^{\mathbb{T}} = \mathsf{id}

If

φ:(𝕊,𝗌𝗍)⇒(𝕋,𝗌𝗍)\varphi : (\mathbb{S}, \mathsf{st}) \Rightarrow (\mathbb{T}, \mathsf{st})

a strong monad morphism, then

φ×φ⋅⟨𝕊π1,𝕊π2⟩⋅𝖽𝗌𝗍𝕊=⟨𝕋π1,𝕋π2⟩⋅φ⋅𝖽𝗌𝗍𝕊=⟨𝕋π1,𝕋π2⟩⋅𝖽𝗌𝗍𝕋⋅φ×φ=φ×φ\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

⟨𝕊π1,𝕊π2⟩⋅𝖽𝗌𝗍𝕊=𝗂𝖽\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:

𝖽𝗌𝗍𝕋⋅⟨𝕋π1,𝕋π2⟩=𝗂𝖽\mathsf{dst}^{\mathbb{T}} \cdot \langle \mathbb{T} \pi_1, \mathbb{T} \pi_2 \rangle = \mathsf{id}

If

φ:(𝕊,𝗌𝗍)⇒(𝕋,𝗌𝗍)\varphi : (\mathbb{S}, \mathsf{st}) \Rightarrow (\mathbb{T}, \mathsf{st})

is a strong monad morphism, then:

φ⋅𝖽𝗌𝗍𝕊⋅⟨𝕊π1,𝕊π2⟩=𝖽𝗌𝗍𝕋⋅φ×φ⋅⟨𝕊π1,𝕊π2⟩=𝖽𝗌𝗍𝕋⋅⟨𝕋π1,𝕋π2⟩⋅φ=φ\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

𝖽𝗌𝗍𝕊⋅⟨𝕊π1,𝕊π2⟩=𝗂𝖽\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.

Leave a comment