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:𝒞→𝒞F : \mathcal{C} \rightarrow \mathcal{C}

on a monoidal category is a natural transformation

𝗌𝗍:X⊗F(Y)⇒F(X⊗Y)\mathsf{st} : X \otimes F(Y) \Rightarrow F (X \otimes Y)

compatible with the monoidal left unitor and associator, in that

Fλ⋅𝗌𝗍=λF \lambda \cdot \mathsf{st} = \lambda

and

Fα⋅𝗌𝗍=𝗌𝗍⋅𝗂𝖽⊗𝗌𝗍⋅αF \alpha \cdot \mathsf{st} = \mathsf{st} \cdot \mathsf{id} \otimes \mathsf{st} \cdot \alpha

A strong functor is a pair

(F,𝗌𝗍:X⊗F(Y)⇒F(X⊗Y))(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

φ:(F,𝗌𝗍)→(G,𝗌𝗍)\varphi : (F,\mathsf{st}) \rightarrow (G,\mathsf{st})

is an ordinary natural transformation

φ:F⇒G\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,𝗌𝗍)∘(F,𝗌𝗍)=(G∘F,X⊗GF(Y)→𝗌𝗍G(X⊗F(Y))→G𝗌𝗍GF(X⊗Y))(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

φ:(F1,𝗌𝗍)⇒(F2,𝗌𝗍)andγ:(G1,𝗌𝗍)⇒(G2,𝗌𝗍)\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

γ∘φ:G1∘F1⇒G2∘F2\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:

𝕊(𝗌𝗍)⋅𝗌𝗍⋅1⊗λ=λ⋅𝕋(𝗌𝗍)⋅𝗌𝗍\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.

One thought on “A Strong Monad is Monoid in the Category of Strong Endofunctors”

  1. Pingback: Commutativity of Strong Submonads – Dan Marsden

Leave a comment