nLab strong monad

Idea

A left-strength and a right-strength 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 (left/right) strength is called a (left/right) strong monad. For a symmetric monoidal category, the concepts of left-strength and right-strength coincide, and we simply talk about strengths. The notion of strength can be motivated at least in the following ways.

• A strong monad over a monoidal category $V$ is a monad in the bicategory of $V$-actegories, on the category $V$ (acting on itself from the left for a left-strength, and from the right for a right-strength).

• A left-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 right-strength is the analogous notion, where the action is from the right.

• A left-strength for a monad is a way of creating “slices”, expressions over tensor products which are trivial in the first component. (The right-strength 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 $V$ is a monoidal closed category, then a left-strong monad is the same thing as a $V$-enriched monad, and a right-strength is the same thing as a pointwise structure for the monad on the internal homs. In particular, every monad on Set is canonically left-strong.

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

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

Definition

Abstractly

Definition

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

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

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

Dually, a right-strength is the analogous concept where $V$ is instead acting on the right.

Details:

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

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

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

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

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

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

• modifications

  • unit: $\eta : Id_V \Rightarrow T$

  • product: $\mu : T \circ T \Rightarrow T$

• satisfying the usual uniticity and associativity constraints.

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

Then the usual diagrams that specify a strong monad

• unitalness and functoriality of the component functor of $T$;

• naturalness of unit and product modifications.

Concretely

A left-strong monad over a monoidal category $(C,\otimes,1)$ is a monad $(T, \eta, \mu)$ equipped with a natural transformation of the form

(1)$$t_{A,B} \;\colon\; A \otimes T B \longrightarrow T(A\otimes B) \,,$$

called the left-strength, and required to make 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”:

The notion of strong monads for which the (left) strength $t$ (1) is even a natural isomorphism has been called very strong (Ratkovic (2013), Def. 3.1.6) or linear (Berger & Ratkovic (2019), §1.2).

More generally, if a monoidal category $V$ acts on a category $C$

$$\bullet : V\times C\to C$$

then a $V$-strength for a monad $T$ on $C$ is a family of morphisms $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.

Right-strength

A right-strength for the monad $T$ is a natural transformation $s_{A,B}:T A \otimes B \to T(A\otimes B)$ satisfying analogous diagrams to those for the left-strength.

Remark. In some papers, the term “strength” is used for what is here called a “left-strength” and the term “costrength” is used for what is here called a “right-strength”. However, this terminology is confusing, as it is not in line with the usual convention in category theory of prefixing a term by “co-” when it is the same concept in the opposite category: instead, a left-strength is a right-strength with respect to the reversal of the tensor product $A\otimes^{rev} B = B\otimes A$. See tensorial costrength for more details.

A strength (on a monoidal category which is not necessarily symmetric) is a left-strength and a right-strength such that the two induced maps $(X\otimes T Y) \otimes Z \to T(X\otimes (Y\otimes Z))$ agree. If the category is symmetric monoidal, then $T$ is a commutative monad if it is equipped with a left-strength (hence also a right-strength) such that the two induced maps $T X \otimes T Y \to T(X\otimes Y)$ agree.

Examples

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

• The left-strength for the list monad works in the following way. Given sets $X$ and $Y$, the left-strength is the map

  $$(x,[y_1,\dots,y_n]) \; \mapsto \; [(x,y_1),\dots,(x,y_n)] .$$

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

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

• On a symmetric monoidal category, a left-strength for a left action monad can be obtained analogously, using the braiding. (For right actions, the braiding is not needed.) In that case, this left-strength is commutative precisely if $M$ is commutative as a monoid (see Brandenburg ‘14, Example 6.3.12).

• For probability monads on cartesian monoidal categories, the left-strength creates “slices”, or probability distributions which are deterministic in one variable. For the Giry monad, for example, the left-strength for measurable spaces $X$ and $Y$ is the map

  $$(x,p) \;\mapsto\; \delta_x\otimes p$$

  for all $x\in X$ and $y\in P Y$. This left-strength is commutative and it allows to define easily the product of measures?. Most probability monads behave analogously. (Note that the category Meas has another monoidal structure, which is closed, different from the cartesian product. For that monoidal structure, the Giry monad is not left-strong - see Sato ‘16.)

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 : C \to C$ on a monoidal category $(C, \otimes, I)$, let $Kl(M)$ be the Kleisli category of $M$ with $J : C \to Kl(M)$. If $X \in Obj(C)$, write $[X] \in Obj(Kl(M))$ for the corresponding object in the Kleisli category. Moreover, given $f : X \to MY$, write $[f] : [X] \to [Y]$.

Then there is a correspondence between

• left-strengths of $M$,
• functorial operations $\odot : C \times Kl(M) \to Kl(M)$ that are
  • left unital: $I \odot A \cong A$ (naturally),
  • right unital: $X \odot [I] \cong JX$ (naturally),
  • mixed associative: $(X \otimes Y) \odot [Z] \cong X \odot (Y \odot [Z])$ (naturally),
  • subject to coherence laws (see at action of a monoidal category)

Right unitality entails that $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 $M$ is left-strong. Then we define

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

This preserves

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

This is

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

The coherence laws will be satisfied.

Conversely, assume $\odot$ is given. Then we define

$$[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 $C$ is monoidal closed, left-strength and right-strength induce particular structures on the internal homs.

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

Left-strong monads are enriched monads

The original reference for this part is Kock ‘72. For more references see at enriched monad – Relation to strong and monoidal monads.

Beware that Kock ‘72 uses somewhat different terminology:

• The left-strength as defined here is called tensorial strength;

• The enrichment of the monad is called strength.

Since the two notions are equivalent under mild conditions see (there), the different terminology does not lead to confusion (once the equivalence is established).

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

$$[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] \otimes T X \;\to\; T Y.$$

The latter is provided by the strength $t$ as follows,

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

One can verify that these assignments are inverse to each other. Moreover, the strength diagrams for $t$ 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 left-strong.

Given a monad $T$ on Set, the assignment

$$[X,Y] \;\to\; [T X, T Y]$$

is just the action of $T$ on the morphisms,

$$\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 left-strength of the list monad, (Compare with the example above.)

Right-strength 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 $T$ on a closed category $C$ is a natural transformation

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

such that the following diagrams commute.

• Compatibility with the unit of the monad $\eta^T$:

• Compatibility with the multiplication of the monad $\mu^T$:

• Compatibility with the “unitor of the closed structure”, the natural isomorphism $i:X\to [1,X]$ (see closed category#basic_definition):

• Compatibility with the (curried) composition morphism of the closed structure, the morphism $l:[Y,Z]\to [[X,Y],[Y,Z]]$ (see closed category#basic_definition):

Equivalence with the notion of right-strength

Suppose now that $C$ is a monoidal closed category. In this case, a pointwise structure and a costrength coincide. Let’s see how. Given a right-strength $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]\to [X,TY]$ we can obtain a right-strength 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 $T$-algebra $(A,a)$, and any object $X$, we can canonically define an algebra structure on $[X,A]$, given by

The diagrams above assure us that

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

Example in Set

Consider the list monad on Set. The usual right-strength gives the following pointwise structure:

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

If $(A,a)$ is an $L$-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:

$$\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 $X$, an object $T(X)$;

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

• a family of functions $*_{\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 * \eta =f$, $\eta * f=f$, and $h*(g*f)=(h*g)*f$.

With the subscripts:

• $f *_{\Gamma,X} \eta_X = f$ and $\eta *_{I,\Delta} f=f$, and $h *_{\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 $\hat C$-enriched monad on $C$, where $\hat C$ is the category of presheaves on $C$ regarded with the Day convolution monoidal structure. More concretely,

$$\eta_{X\otimes Y}*_{X,T(Y)} id_{T(Y)}:X\otimes T(Y)\to T(X\otimes Y)$$

is a left-strength map.

Uniqueness of left-strength with enough points

Theorem

(Moggi)

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

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

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

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

Related concepts

• tensorial strength

• costrong monad, cotensorial strength

• monoidal monad

• commutative monad

• enriched monad

• monad (in computer science)

References

The notion of strong monads was introduced (as an alternative description of enriched monads and related to monoidal monads and commutative monads) in:

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

• Anders Kock, Closed categories generated by commutative monads, Journal of the Australian Mathematical Society 12 4 (Nov 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]

See also:

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

The notion of strong monads is picked up in the context of monads in computer science:

• Eugenio Moggi, Def. 3.2 in: Notions of computation and monads, Information and Computation, 93 1 (1991) [doi:10.1016/0890-5401(91)90052-4, pdf]

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

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)

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

Usually strong monads are described explicitly in terms of data and coherence conditions. The above repackaging of the definition in terms of a 2-category of actions appears in the comments of the blog post:

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

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)

The terminology of “very strong” monads:

• Kruna S. Ratkovic, Def. 3.1.6 in: Morita theory in enriched context (2013) [arXiv:1302.2774]

• Daniel Schmitter, Def. 8.10 in: On Operations with Binders and Operations with Equations (2020) [web, pdf]

also called “linear monads” in:

• Clemens Berger, Kruna Ratkovic, §1.2 in: Gabriel-Morita theory for excisive model categories, Appl Categor Struct 27 (2019) 23–54 [arXiv:1705.03863, doi;10.1007/s10485-018-9539-x]