nLab
strong monad

Strong monads

Context

Higher algebra

Monoidal categories

monoidal categories

With symmetry

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

Enriched category theory

Strong monads

Idea

A strength and a costrength for a monad on a monoidal category are structures relating the monad with the tensor product of the category “in one direction”. A monad equipped with a strength is called a strong monad. The notion of strength can be motivated at least in the following ways.

  • A strong monad over a monoidal category VV is a monad in the bicategory of VV-actegories, on the category VV (acting on itself on the left for a strength, on the right for a costrength).
  • A strength for a monad is a compatibility condition between the monad and the tensor product “from the left”, less symmetric than being a monoidal monad, as it lacks the commutativity property. A costrength is a similar notion, where the action is on the right.
  • A strength for a monad is a way of creating “slices”, expressions over tensor products which are trivial in the first component. (The costrength gives expressions which are trivial in the second component.)
  • A strong monad is a strong endofunctor with a monad structure which is compatible with the strength.
  • If VV is a monoidal closed category, then a strong monad is the same thing as a VV-enriched monad, and a costrength is the same thing as a pointwise structure for the monad on the internal homs. In particular, every monad on Set is canonically strong.

On a symmetric monoidal category, strength and costrength, if they exist, can be obtained from one another.

Under some conditions, the strength is a property-like structure.

A more general notion of strength allows for general VV-actegories instead of just the canonical action of VV on itself (see below).

Abstract definition

Definition

For VV a monoidal category, a strong monad over VV is a monad in the 22-category V-ActV\text{-}Act of left VV-actegories on categories.

The classical definition of strength is on the category VV itself, regarded as equipped with the canonical VV-action on itself. The definition is useful in the general case too.

The extra structure that a strong monad has as opposed to the underlying monad on Cat is called strength.

Dually, a costrength is the analogous concept where VV is instead acting on the right.

Details

If we write BV\mathbf{B}V for the one-object bicategory obtained by delooping VV once, we have

V-ActLax2Funct(BV,Cat), V\text{-}Act \simeq Lax2Funct(\mathbf{B}V, Cat) \,,

where on the right we have the 22-category of lax 2-functors from BV\mathbf{B}V to Cat, lax natural transformations of and modifications.

The category VV defines a canonical functor V^:BVCat\hat V : \mathbf{B}V \to Cat.

The strong monad, being a monad in this lax functor bicategory is given by

  • a lax natural transformation T:V^V^T : \hat V \to \hat V;

  • modifications

    • unit: η:Id VT\eta : Id_V \Rightarrow T

    • product: μ:TTT\mu : T \circ T \Rightarrow T

  • satisfying the usual uniticity and associativity constraints.

By the general logic of (2,1)(2,1)-transformations the components of TT are themselves a certain functor.

Then the usual diagrams that specify a strong monad

  • unitalness and functoriality of the component functor of TT;

  • naturalness of unit and product modifications.

Concrete definition

A strong monad over a monoidal category (C,,1)(C,\otimes,1) is a monad (T,η,μ)(T, \eta, \mu) together with a natural transformation t A,B:ATBT(AB)t_{A,B}:A \otimes T B \to T(A\otimes B), called the strength, such that the following diagrams commute.

“Strengthening with 1 is irrelevant” (and plays well with the unitors):

I think it only plays well with the left unitor?

“Consecutive applications of strength commute” (and play well with the associators):

“Strength commutes with the monad unit”:

“Strength commutes with the monad multiplication”:

More generally, if a monoidal category VV acts on a category CC

:V×CC \bullet : V\times C\to C

then a VV-strength for a monad TT on CC is a family of morphisms t A,B:AT(B)T(AB)t_{A,B}:A\bullet T(B)\to T(A\bullet B) satisfying similar commutative diagrams.

In particular, the underlying endofunctor of a strong monad is a strong functor.

Costrength

A costrength for the monad TT is a natural transformation s A,B:TABT(AB)s_{A,B}:T A \otimes B \to T(A\otimes B) satisfying analogous diagrams to those for the strength.

Note that the “co-” in “costrength” does not refer to the opposite category; instead it refers to the reversal of the tensor product, A revB=BAA\otimes^{rev} B = B\otimes A. The terminology also makes sense in the context of closed monoidal categories, where strength and costrength appear on the two sides of the internal hom. See the dedicated section for the details.

When the category CC is symmetric monoidal, the braiding bb allows to obtain a strength from a costrength and vice versa,

A bistrength is a strength and a costrength such that the two induced maps (XTY)ZT((XY)Z(X\otimes T Y) \otimes Z \to T((X\otimes Y)\otimes Z agree. If the category is symmetric monoidal, then TT is a commutative monad if it is equipped with a strength (hence also a costrength) such that the two induced maps TXTYT(XY)T X \otimes T Y \to T(X\otimes Y) agree.

Examples

Every monad on Set with its cartesian product is canonically strong (see below for why).

  • The strength for the list monad works in the following way. Given sets XX and YY, the strength is the map

    (x,[y 1,,y n])[(x,y 1),,(x,y n)]. (x,[y_1,\dots,y_n]) \; \mapsto \; [(x,y_1),\dots,(x,y_n)] .

    In other words, it turns an element of XX and a list of elements of YY into a list of elements of X×YX\times Y, canonically.

  • For the left action monad (on Set or on any other monoidal category) relative to a monoid or monoid object MM, the costrength is inherited by the associator as follows (see Brandenburg ‘14, Example 6.3.4),

Interaction with the Kleisli category

Is what’s written here somehow the same as the abstract definition? Can we be more general than the Kleisli category and pick an arbitrary adjunction?

Given a monad M:CCM : C \to C on a monoidal category (C,,I)(C, \otimes, I), let Kl(M)Kl(M) be the Kleisli category of MM with J:CKl(M)J : C \to Kl(M). If XObj(C)X \in Obj(C), write [X]Obj(Kl(M))[X] \in Obj(Kl(M)) for the corresponding object in the Kleisli category. Moreover, given f:XMYf : X \to MY, write [f]:[X][Y][f] : [X] \to [Y].

Then there is a correspondence between

  • strengths of MM,
  • functorial operations :C×Kl(M)Kl(M)\odot : C \times Kl(M) \to Kl(M) that are
    • left unital: IAAI \odot A \cong A (naturally),
    • right unital: X[I]JXX \odot [I] \cong JX (naturally),
    • mixed associative: (XY)[Z]X(Y[Z])(X \otimes Y) \odot [Z] \cong X \otimes (Y \odot [Z]) (naturally),
    • subject to coherence laws.

Right unitality entails that X[Y]XY[I][XY]X \odot [Y] \cong X \otimes Y \odot [I] \cong [X \otimes Y] so basically \odot is fixed on objects. Is it better to fix this on the nose? Does this violate the principle of equivalence?

This correspondence is used in the formulation of call-by-push-value as an adjoint logic.

Indeed, assume that MM is strong. Then we define

  • X[Y]:=[XY]X \odot [Y] := [X \otimes Y]
  • f XX[g] [Y][Y]:=[t X,Y(fg)]f^{X \to X'} \odot [g]^{[Y] \to [Y']} := [t_{X', Y'} \circ (f \otimes g)]

This preserves

  • identity because the strength commutes with the unit,
  • composition because the strength commutes with monad multiplication.

This is

  • left unital on objects (by mapping the left unitor into the Kleisli category),
  • naturally so because the strength is compatible with the left unitor,
  • right unital on objects (by mapping the right unitor into the Kleisli category),
  • naturally so because the strength commutes with the unit (!),
  • mixed associative on objects (by mapping the assiciator into the Kleisli category),
  • naturally so because the strength is compatible with the associator.

The coherence laws will be satisfied.

Conversely, assume \odot is given. Then we define

[t X,y]:J(XMY)XMY[I]XJMY1 X[1 MY]XJYXY[I]J(XY). [t_{X, y}] : J(X \otimes MY) \cong X \otimes MY \odot [I] \cong X \odot JMY \xrightarrow{1_X \odot [1_{MY}]} X \odot JY \cong X \otimes Y \odot [I] \cong J(X \otimes Y).

This is natural and

  • commutes with the unit because \odot preserves identity:
  • commutes with multiplication because \odot preserves composition (similar reasoning),
  • is compatible with the left unitor by naturality and the coherence laws,
  • is compatible with the associator by naturality and the coherence laws.

On closed and monoidal closed categories

If the category CC is monoidal closed, strength and costrength induce particular structures on the internal homs.

In this section, let (C,1)(C,\otimes 1) be monoidal closed, with internal hom denoted by [,][-,-]. Denote the unit of the hom-tensor adjunction by η X:X[Y,XY]\eta_X:X \to [Y,X\otimes Y] and the counit (or evaluation map, see internal hom - evaluation map) by ϵ Y:X[X,Y]Y\epsilon_Y:X\otimes [X,Y]\to Y.

The unit is the unit of Y[Y,]- \otimes Y \dashv [Y, -] applied to XX. The co-unit is the co-unit of X[X,]X \otimes - \dashv [X, -] applied to YY. The swapping of the variable names is already confusing, but more importantly, we’re tensoring on the other side. Either we’re assuming that the category is symmetric monoidal (then we should mention so), or we’re not but then we should be consistent.

Strong monads are enriched monads

The original reference for this part is Kock ‘72. Note that in there the terminology is a little different:

  • The strength as defined here is called tensorial strength;
  • The enrichment of the monad is called strength.

Since the two notions are equivalent, the different terminology does not lead to confusion (once the equivalence is established). For more on this see also the treatment at the related discussion for strong endofunctors.

First of all, a strong endofunctor TT on a closed monoidal category CC is “the same thing” as a CC-enriched endofunctor. To see this, note that an enriched endofunctor amounts to a natural transformation

[X,Y][TX,TY] [X,Y] \;\to\; [T X, T Y]

which satisfies the usual identity and composition rules (see enriched functor). Notice also that a map as above, by the hom-tensor adjunction (or currying) is equivalently specified by a map

[X,Y]TXTY. [X,Y] \otimes T X \;\to\; T Y.

The latter is provided by the strength tt as follows,

Conversely, given a map t:[X,Y]TXTYt':[X,Y] \otimes T X \to T Y natural in YY and extranatural in XX, one can define a strength as

One can verify that these assignments are inverse to each other. Moreover, the strength diagrams for tt commute if and only the resulting assigment is indeed an enriched monad, and vice versa.

Example in Set

Every monad on Set is Set-enriched. In particular, it is strong.

Given a monad TT on Set, the assignment

[X,Y][TX,TY] [X,Y] \;\to\; [T X, T Y]

is just the action of TT on the morphisms,

Hom(X,Y)Hom(TX,TY). \mathrm{Hom}(X,Y) \;\to\; \mathrm{Hom}(T X, T Y) .

Under currying, this corresponds to the map

For example, for the list monad, the map is given by

The strength obtained this way is the usual strength of the list monad,

(Compare with the example above.)

Costrength and pointwise structure

The reference for this part can be found in Kock ‘71, Section 1.

Let’s give a preliminary definition. A pointwise structure or cotensorial strength (Kock ‘72) of a monad TT on a closed category CC is a natural transformation

s X,Y:T[X,Y][X,TY] s' _{X,Y}: T[X,Y] \to [X, T Y]

such that the following diagrams commute.

  • Compatibility with the unit of the monad η T\eta^T:
  • Compatibility with the multiplication of the monad μ T\mu^T:
  • Compatibility with the (curried) composition morphism of the closed structure, the morphism l:[Y,Z][[X,Y],[Y,Z]]l:[Y,Z]\to [[X,Y],[Y,Z]] (see closed category#basic_definition):

Equivalence with the notion of costrength

Suppose now that CC is a monoidal closed category. In this case, a pointwise structure and a costrength coincide. Let’s see how. Given a costrength s:TXYT(XY)s:T X\otimes Y \to T(X\otimes Y) we can obtain a pointwise structure as follows,

Conversely, given a pointwise structure s:T[X,Y][X,TY]s':T[X,Y]\to [X,TY] we can obtain a costrength as

By currying it can be shown that the respective diagrams of costrength and pointwise structure are equivalent (the unit condition corresponds to the unit condition, and so on).

Algebra structure on the internal homs

A pointwise structure allows in particular to form pointwise algebra structures, in the following sense. Given a TT-algebra (A,a)(A,a), and any object XX, we can canonically define an algebra structure on [X,A][X,A], given by

The diagrams above assure us that

  • This map gives indeed a TT-algebra;
  • AA and [1,A][1,A] are canonically isomorphic as TT-algebras too;
  • The internal precomposition with a morphism f:WXf:W\to X gives a morphism of TT-algebras [X,A][W,A][X,A]\to [W,A].

Example in Set

Consider the list monad on Set. The usual costrength gives the following pointwise structure:

Indeed, this turns a list of functions into a function into lists, that maps xXx\in X to the list of the results.

If (A,a)(A,a) is an LL-algebra, i.e. a monoid, this allows to equip function spaces with a monoid structure as follows:

In other words, functions into a monoid form canonically a monoid under pointwise addition (or multiplication).

Moggi’s typing rules and parameterized definition

Moggi (Moggi ‘89) proposed the following typing rules for a sequence operator:

Γt:XΓη(t):T(X)Γ,x:Xu:T(Y)Δt:T(X)Γ,Δletx=tinu:T(Y) \frac{\Gamma \vdash t:X}{\Gamma\vdash \eta(t):T(X)} \qquad \frac{\Gamma,x:X \vdash u: T(Y)\quad \Delta\vdash t:T(X)} {\Gamma,\Delta\vdash let\,x=t\,in\,u:T(Y)}

To interpret these rules in a category, where types are interpreted as objects and judgements are interpreted as morphisms, we require

  • For each object XX, an object T(X)T(X);

  • a morphism η X:XT(X) \eta_X:X\to T(X) for each XX (equivalently, a natural family of functions C(Γ,X)C(Γ,T(X))C(\Gamma,X)\to C(\Gamma, T(X)));

  • a family of functions * Γ,Δ:C(ΓX,T(Y))×C(Δ,T(X))C(ΓΔ,T(Y))*_{\Gamma,\Delta}:C(\Gamma\otimes X, T(Y))\times C(\Delta,T(X))\to C(\Gamma\otimes \Delta,T(Y)) natural in Γ\Gamma and Δ\Delta,

such that

  • f*η=ff * \eta =f, η*f=f\eta * f=f, and h*(g*f)=(h*g)*fh*(g*f)=(h*g)*f.

With the subscripts:

  • f* Γ,Xη X=ff *_{\Gamma,X} \eta_X = f and η* I,Δf=f\eta *_{I,\Delta} f=f, and h* Γ,ΔΞ(g* Δ,Ξf)=(h* Γ,ΔXg)* ΓΔ,Ξfh *_{\Gamma,\Delta\otimes \Xi} (g *_{\Delta,\Xi} f) = (h *_{\Gamma,\Delta\otimes X} g) *_{\Gamma\otimes\Delta,\Xi} f.

Such a structure is the same thing as a strong monad. One way to see this is to notice that it is essentially the same as the Kleisli triple form of an C^\hat C-enriched monad on CC, where C^\hat C is the category of presheaves on CC regarded with the Day convolution monoidal structure. More concretely,

η XY* X,T(Y)id T(Y):XT(Y)T(XY)\eta_{X\otimes Y}*_{X,T(Y)} id_{T(Y)}:X\otimes T(Y)\to T(X\otimes Y)

is a strength map.

Uniqueness of strength with enough points

Theorem

(Moggi)

Let CC be a category with finite products and let TT be a strong monad on CC. For any points x:1Xx:1\to X, y:1T(Y)y:1\to T(Y), we have

t(x,y)=T((x! Y),id Y)y:1T(X×Y) t\circ(x,y)\ = \ T((x\circ !_Y),id_Y)\circ y\ : 1 \to T(X\times Y)

Hence if 11 is a generator, i.e. C(1,):CSetC(1,-):C\to Set is faithful, then there is at most one strength for any ordinary monad on CC.

In other words, a monad being strong is a property-like structure in a category with enough points.

References

Strong monads were defined by Kock, as an alternative description of enriched monads.

  • Anders Kock, Strong functors and monoidal monads, Arch. Math. (Basel) 23 (1972), 113–120 (pdf)

  • Anders Kock, Monads on symmetric monoidal closed categories, Arch. Math. 21 (1970), 1–10 (pdf)

  • Anders Kock, Closed categories generated by commutative monads, 1971 (pdf)

  • 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.

  • 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), p. 269-293 (NUMDAM, pdf)

More resources and surveys:

  • Gavin J. Seal, Tensors, monads and actions (arXiv:1205.0101)

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

    Usually strong monads are described explicitly in terms of the components of the above structure. The above repackaging of that definition appears in the blog post

  • John Baez, The Monads Hurt My Head – But Not Anymore (blog)

Strong monads are important in Moggi’s theory of notions of computation (see monad (in computer science)):

  • Eugenio Moggi. Notions Of Computation And Monads. Information And Computation. 1991;93:55–92.
  • Eugenio Moggi. Computational Lambda-Calculus and Monads. Proceedings of the Fourth Annual Symposium on Logic in Computer Science. 1989. p. 14–23.

More in-text references:

  • Tetsuya Sato, The Giry monad is not strong for the canonical symmetric monoidal closed structure on Meas, Journal of Pure and Applied Algebra, Volume 222, Issue 10, October 2018, Pages 2888-2896. (arXiv:1612.05939)

Last revised on October 4, 2021 at 09:38:17. See the history of this page for a list of all contributions to it.