nLab monoidal monad

Definition

Definition

A monoidal monad is a monad in the 2-category of monoidal categories, lax monoidal functors, and monoidal transformations.

This notion originates inside the statement of Kock 1970, Thm. 3.2.

In components, this means (cf. Kock 1970, p. 8, review includes Seal 2012, §1.2):

Monoidal structure on a monad

$\mathcal{E} \,\colon\, \mathbf{C} \to \mathbf{C}$

$c \in \mathbf{C} \;\;\;\; \vdash \;\;\;\; ret^{\mathcal{E}}_c \,\colon\, c \to \mathcal{E}(c)$

$c \in \mathbf{C} \;\;\;\; \vdash \;\;\;\; join^{\mathcal{E}}_{c} \,\colon\, \mathcal{E} \circ \mathcal{E}(c) \to \mathcal{E}(c)$

acting on a monoidal category $(\mathbf{C}, \otimes, \mathbb{1})$ is:

1. lax monoidal functor-structure on $\mathcal{E}$

   $\vdash \;\;\;\; \epsilon^{\mathcal{E}} \,\colon\, 1\!\!1 \to \mathcal{E}(1\!\!1)$

   $c,c' \in \mathbf{C} \;\;\;\; \vdash \;\;\;\; \mu^{\mathcal{E}}_{c,c'} \,\colon\, \mathcal{E}(c) \otimes \mathcal{E}(c') \to \mathcal{E}(c \otimes c')$

2. such that the monad structure transformations $ret^{\mathcal{E}}$ and $join^{\mathcal{E}}$ are monoidal transformations in that together with the lax monoidal structure $\epsilon^{\mathcal{E}}$ and $\mu^{\mathcal{E}}$ they make the following diagrams commute:

First of all, the lax monoidal unit must coincide with the monad unit

(1)

which already implies the unit diagram for the join operation:

and then the two main conditions:

and

Moreover, if $\mathbf{C}$ is even a symmetric monoidal category with braiding $\sigma$, then a monoidal monad on $\mathbf{C}$ as above is a symmetric monoidal monad if the underlying monoidal functor is a symmetric monoidal functor.

Remark

The notion of monoidal monad is equivalent to the notion of commutative monad. To put it another way: to give a commutative strength for a monad $T$ is to give a monoidal monad whose underlying monad is $T$. We explore this connection below.

Properties

Relation to commutative strong monads

We discuss how monoidal monads functorially give rise to strong monads.

Strength

First to recall the notion of a strong monad:

Let $V$ be a monoidal category. We say a functor $T \colon V \to V$ is strong if there are given left and right tensorial strengths, namely natural transformations of the form:

$$\tau_{A, B} \;\colon\; A \otimes T(B) \to T(A \otimes B)$$

$$\,$$

$$\sigma_{A, B} \;\colon\; T(A) \otimes B \to T(A \otimes B) \,,$$

which are suitably compatible with one another: The full set of coherence conditions may be summarized by saying $T$ preserves the two-sided monoidal action of $V$ on itself, in an appropriate 2-categorical sense. More precisely: the two-sided action of $V$ on itself is a lax functor of 2-categories

$$\tilde{V} \colon B V \times (B V)^{op} \to Cat$$

where

• Cat denotes the 2-category of categories, functors and natural transformations,

• $B V$ denotes the delooping one-object 2-category of the monoidal category $V$,

• $(B V)^{op}$ denotes its 1-cell dual, hence the same 2-category except with 1-morphism composition (here: tensor product) in reverse order),

• the two-sided strength means we have a structure of lax natural transformation $\tilde{V} \to \tilde{V}$.

Remark

In the setting where $V$ is symmetric monoidal, we will assume that the left and right strengths $\tau$ and $\sigma$ are related by the symmetry in the obvious way, by a commutative square

$$\array{ A \otimes T(B) & \stackrel {\tau_{A, B}} {\longrightarrow} & T(A \otimes B) \\ \mathllap{^c} \big\downarrow & & \big\downarrow \mathrlap{^{T(c)}} \\ T(B) \otimes A & \underset{ \sigma_{B, A}} {\longrightarrow} & T(B \otimes A) }$$

where the $c$‘s are instances of the symmetry isomorphism.

Definition

There is a category of strong functors $V \to V$, whose morphisms are natural transformations $\lambda \colon S \to T$ which are compatible with the strengths in the obvious sense. Under composition, this is a strict monoidal category.

The monoid objects in this monoidal category are called strong monads.

Definition

A strong monad $(T \colon V \to V, m \colon T T \to T, u: 1 \to T)$ (def. ) is a commutative monad if there is an equality of natural transformations $\alpha = \beta$ where

• $\alpha$ is the composite

  $$T A \otimes T B \stackrel{\sigma_{A, T B}}{\to} T(A \otimes T B) \stackrel{T(\tau_{A, B})}{\to} T T(A \otimes B) \stackrel{m(A \otimes B)}{\to} T(A \otimes B).$$

• $\beta$ is the composite

  $$T A \otimes T B \stackrel{\tau_{T A, B}}{\to} T(T A \otimes B) \stackrel{T(\sigma_{A, B})}{\to} T T(A \otimes B) \stackrel{m(A \otimes B)}{\to} T(A \otimes B).$$

From monoidal to commutative strong monads

Definition

(strength from monoidalness)
For $(T \colon V \to V, u \colon id \to T, m \colon T T \to T)$ a monoidal monad (Def. ), with the monoidal monad-structure on the underlying functor denoted by

$$\alpha_{A, B} \,\colon\, T(A) \otimes T(B) \to T(A \otimes B), \qquad \iota = u(I) \,:\, I \to T(I) \,,$$

Define strengths on both the left and the right by:

$$\tau_{A, B} \;\coloneqq\; \big( A \otimes T(B) \overset{u_A \otimes id}{\to} T(A) \otimes T(B) \overset{\alpha_{A, B}}{\to} T(A \otimes B) \big) \,,$$

$$\,$$

$$\sigma_{A, B} \;\coloneqq\; \big( T(A) \otimes B \overset{id \otimes u_B}{\to} T(A) \otimes T(B) \overset{\alpha_{A, B}}{\to} T(A \otimes B) \big) \,.$$

Proposition

The strong monad structures obtained from monoidal monads via Def. are commutative monads (Def. ).

Proof

In fact, the two composites

$$T A \otimes T B \stackrel{\sigma_{A, T B}}{\to} T(A \otimes T B) \stackrel{T(\tau_{A, B})}{\to} T T(A \otimes B) \stackrel{m(A \otimes B)}{\to} T(A \otimes B)$$

$$\,$$

$$T A \otimes T B \stackrel{\tau_{T A, B}}{\to} T(T A \otimes B) \stackrel{T(\sigma_{A, B})}{\to} T T(A \otimes B) \stackrel{m(A \otimes B)}{\to} T(A \otimes B)$$

are both equal to $\alpha_{A, B}$. We show this for the second composite; the proof is similar for the first. If $\alpha_T$ denotes the monoidal constraint for $T$ and $\alpha_{T T}$ the constraint for the composite $T T$, then by definition $\alpha_{T T}$ is the composite given by

$$T T X \otimes T T Y \stackrel{\alpha_T T}{\to} T(T X \otimes T Y) \stackrel{T\alpha_T}{\to} T T(X \otimes Y)$$

and so, using the properties of monoidal monads, we have a commutative diagram

$$\array{ & & T T X \otimes T Y & \stackrel{\alpha_T}{\to} & T(T X \otimes Y) \\ & ^\mathllap{u \otimes 1} \nearrow & \downarrow^\mathrlap{1 \otimes T u} & & \downarrow^\mathrlap{T(1 \otimes u)} \\ T X \otimes T Y & \stackrel{u \otimes T u}{\to} & T T X \otimes T T Y & \stackrel{\alpha_T T}{\to} & T(T X \otimes T Y) \\ & ^\mathllap{1} \searrow & \downarrow^\mathrlap{m \otimes m} & \searrow^\mathrlap{\alpha_{T T}} & \downarrow^\mathrlap{T\alpha_T} \\ & & T X \otimes T Y & & T T(X \otimes Y) \\ & & & ^\mathllap{\alpha_T} \searrow & \downarrow^\mathrlap{m} \\ & & & & T(X \otimes Y) }$$

which completes the proof.

This construction is functorial:

Proposition

Given monoidal monads $S$ and $T$ on a monoidal category $C$, a morphism of monads $\alpha \colon S\Rightarrow T$ is a morphism of the induced strong monad structures (Def. ) if and only if it is a monoidal natural transformation.

(e.g. FPR (2019), Prop. C.5)

This relation has a converse:

Proposition

For a monad $T$ on (the underlying category of) a monoidal category, there is a bijection between the structure on $T$ of:

1. a commutative strong monad

2. a monoidal monad,

and furthermore, in a symmetric monoidal category, under this equivalence, there is a logical equivalence between the properties of:

1. being a symmetric strength in the sense of remark

2. being a symmetric monoidal monad (def. ).

This is due to Kock (1972), Thm. 2.3), a detailed review is in GLLN08, §7.3, §A.4 and an Agda formalisation is in 1Lab.

Note that being a symmetric monoidal monad is a non-trivial property: see (McDermott & Uustalu 2022, appendix A.2) or math.SE.a/4877915 for an explicit example of a non-symmetric monoidal monad.

Tensor product of algebras and multimorphisms

See here.

Monoidal structure on the Kleisli category

The Kleisli category of a monoidal monad $T$ on $C$ inherits the monoidal structure from $C$. In particular, the tensor product is given

• On objects, by the tensor product $\otimes$ of $C$;
• On morphisms, given $k:X\to TA$ and $h:Y\to TB$, their product is the map $X\otimes Y \to T(A\otimes B)$ obtained by the composition

where $\nabla$ is the monoidal multiplication of $T$.

• The associator and unitor are induced by those of $C$.

Examples

See examples of commutative monads.

See also

• strong monad, tensorial strength
• monoidal functor
• commutative monad, commutative algebraic theory

References

The definition originally appears inside statement and proof of Thm. 3.2 in:

• Anders Kock, Monads on symmetric monoidal closed categories, Arch. Math. 21 (1970) 1-10 [doi:10.1007/BF01220868]

establishing right away the relation to commutative strong monads (in the case that the underlying monoidal category is symmetric monoidal closed) which is further expanded on in:

• Anders Kock, Closed categories generated by commutative monads, Journal of the Australian Mathematical Society 12 4 (1971) 405-424 [doi:10.1017/S1446788700010272, pdf]

• Anders Kock, Strong functors and monoidal monads, Arch. Math 23 (1972) 113–120 [doi:10.1007/BF01304852, pdf]

Further discussion:

• H. Lindner, Commutative monads in: Deuxiéme colloque sur l’algébre des catégories Amiens-1975. Résumés des conférences, pages 283-288. Cahiers de topologie et géométrie différentielle catégoriques, tome 16, nr. 3 (1975) [numdam:CTGDC_1975__16_3_217_0, pdf]

• William Keigher, Symmetric monoidal closed categories generated by commutative adjoint monads, Cahiers de Topologie et Géométrie Différentielle Catégoriques, 19 no. 3 (1978) 269-293 [numdam:CTGDC_1978__19_3_269_0, pdf]

• Kosta Dosen, Zoran Petric, Coherence for Monoidal Monads and Comonads, Mathematical Structures in Computer Science , 20 4 (2010) 545-561 [arXiv:0907.2199, doi:10.1017/S0960129510000034]

• Gavin J. Seal, Tensors, monads and actions, Theory and Applications of Categories 28 15 (2013) 403-434. [arXiv:1205.0101, tac:28-15]

  (on the Eilenberg-Moore categories of monoidal monads)

• Martin Brandenburg, Tensor categorical foundations of algebraic geometry (arXiv:1410.1716)

• Dylan McDermott, Tarmo Uustalu, What Makes a Strong Monad?, EPTCS 360 (2022) 113-133 [arXiv:2207.00851, doi:10.4204/EPTCS.360.6]

• Paolo Perrone, Starting Category Theory, World Scientific, 2024, Chapter 6. (website)

Formalisation in cubical Agda:

• 1lab, Monoidal monads

Discussion in the context of monads in computer science:

• Jean Goubault-Larrecq, Slawomir Lasota, David Nowak, Logical Relations for Monadic Types, Mathematical Structures in Computer Science, 18 6 (2008) 1169-1217 [arXiv:cs/0511006, doi:10.1017/S0960129508007172]

A statement in the above text is from

• Tobias Fritz, Paolo Perrone and Sharwin Rezagholi, Appendix C of: Probability, valuations, hyperspace: Three monads on Top and the support as a morphism, 2019 (arXiv:1910.03752)