ncatlab.org

monoidal monad in nLab

Contents

Context

Higher algebra

higher algebra

universal algebra

Algebraic theories

Algebras and modules

Higher algebras

Model category presentations

Geometry on formal duals of algebras

Theorems

Monoidal categories

monoidal categories

With braiding

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products

Semisimplicity

Morphisms

Internal monoids

Examples

Theorems

In higher category theory

2-Category theory

2-category theory

Definitions

Transfors between 2-categories

Morphisms in 2-categories

Structures in 2-categories

Limits in 2-categories

Structures on 2-categories

Contents

Definition

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

ℰ:C→C \mathcal{E} \,\colon\, \mathbf{C} \to \mathbf{C}

c∈C⊢ret c ℰ:c→ℰ(c) c \in \mathbf{C} \;\;\;\; \vdash \;\;\;\; ret^{\mathcal{E}}_c \,\colon\, c \to \mathcal{E}(c)

c∈C⊢join c ℰ:ℰ∘ℰ(c)→ℰ(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 (C,⊗,𝟙)(\mathbf{C}, \otimes, \mathbb{1}) is:

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

    ⊢ϵ ℰ:11→ℰ(11) \vdash \;\;\;\; \epsilon^{\mathcal{E}} \,\colon\, 1\!\!1 \to \mathcal{E}(1\!\!1)

    c,c′∈C⊢μ c,c′ ℰ:ℰ(c)⊗ℰ(c′)→ℰ(c⊗c′) 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 ℰret^{\mathcal{E}} and join ℰ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 C\mathbf{C} is even a symmetric monoidal category with braiding σ\sigma, then a monoidal monad on C\mathbf{C} as above is a symmetric monoidal monad if the underlying monoidal functor is a symmetric monoidal functor.

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 VV be a monoidal category. We say a functor T:V→VT \colon V \to V is strong if there are given left and right tensorial strengths, namely natural transformations of the form:

τ A,B:A⊗T(B)→T(A⊗B) \tau_{A, B} \;\colon\; A \otimes T(B) \to T(A \otimes B)

\,

σ A,B:T(A)⊗B→T(A⊗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 TT preserves the two-sided monoidal action of VV on itself, in an appropriate 2-categorical sense. More precisely: the two-sided action of VV on itself is a lax functor of 2-categories

V˜:BV×(BV) op→Cat \tilde{V} \colon B V \times (B V)^{op} \to Cat

where

Definition

A strong monad (T:V→V,m:TT→T,u:1→T)(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

    TA⊗TB→σ A,TBT(A⊗TB)→T(τ A,B)TT(A⊗B)→m(A⊗B)T(A⊗B).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

    TA⊗TB→τ TA,BT(TA⊗B)→T(σ A,B)TT(A⊗B)→m(A⊗B)T(A⊗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).

From monoidal to commutative strong monads

Definition

(strength from monoidalness)
For (T:V→V,u:id→T,m:TT→T)(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

α A,B:T(A)⊗T(B)→T(A⊗B),ι=u(I):I→T(I), \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:

τ A,B≔(A⊗T(B)→u A⊗idT(A)⊗T(B)→α A,BT(A⊗B)), \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) \,,

\,

σ A,B≔(T(A)⊗B→id⊗u BT(A)⊗T(B)→α A,BT(A⊗B)). \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

TA⊗TB→σ A,TBT(A⊗TB)→T(τ A,B)TT(A⊗B)→m(A⊗B)T(A⊗B)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)

\,

TA⊗TB→τ TA,BT(TA⊗B)→T(σ A,B)TT(A⊗B)→m(A⊗B)T(A⊗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 α A,B\alpha_{A, B}. We show this for the second composite; the proof is similar for the first. If α T\alpha_T denotes the monoidal constraint for TT and α TT\alpha_{T T} the constraint for the composite TTT T, then by definition α TT\alpha_{T T} is the composite given by

TTX⊗TTY→α TTT(TX⊗TY)→Tα TTT(X⊗Y)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

TTX⊗TY →α T T(TX⊗Y) u⊗1↗ ↓ 1⊗Tu ↓ T(1⊗u) TX⊗TY →u⊗Tu TTX⊗TTY →α TT T(TX⊗TY) 1↘ ↓ m⊗m ↘ α TT ↓ Tα T TX⊗TY TT(X⊗Y) α T↘ ↓ m T(X⊗Y)\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:

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

This relation has a converse:

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 TT on CC inherits the monoidal structure from CC. In particular, the tensor product is given

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

where ∇\nabla is the monoidal multiplication of TT.

  • The associator and unitor are induced by those of CC.

Examples

See examples of commutative monads.

See also

References

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

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:

Further discussion:

Formalisation in cubical Agda:

Discussion in the context of monads in computer science:

A statement in the above text is from

Last revised on July 8, 2024 at 11:06:15. See the history of this page for a list of all contributions to it.