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:X→Xh : 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×X→Xh \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×X→Xh : 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:X→Xh \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.

One thought on “Distributive Laws and General Equations”

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

Leave a comment