symmetric monoidal (∞,1)-category of spectra
category with duals (list of them)
dualizable object (what they have)
ribbon category, a.k.a. tortile category
monoidal dagger-category?
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.
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 $V$-actegories instead of just the canonical action of $V$ on itself (see below).
For $V$ a monoidal category, a strong monad over $V$ is a monad in the $2$-category $V\text{-}Act$ of left $V$-actegories on categories.
The classical definition of 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 strong monad has as opposed to the underlying monad on Cat is called strength.
Dually, a costrength is the analogous concept where $V$ is instead acting on the right.
If we write $\mathbf{B}V$ for the one-object bicategory obtained by delooping $V$ once, we have
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 strong monad, being a monad in this lax functor bicategory is given by
a lax natural transformation $T : \hat V \to \hat V$;
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.
A strong monad over a monoidal category $(C,\otimes,1)$ is a monad $(T, \eta, \mu)$ together with a natural transformation $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 $V$ acts on a category $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.
A costrength 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 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\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 $C$ is symmetric monoidal, the braiding $b$ 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 $(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 strength (hence also a costrength) such that the two induced maps $T X \otimes T Y \to T(X\otimes Y)$ agree.
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 $X$ and $Y$, the strength is the map
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 costrength is inherited by the associator as follows (see Brandenburg ‘14, Example 6.3.4),
On a symmetric monoidal category, a 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 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 strength creates “slices”, or probability distributions which are deterministic in one variable. For the Giry monad, for example, the strength for measurable spaces $X$ and $Y$ is the map
for all $x\in X$ and $y\in P Y$. This 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 strong - see Sato ‘16.)
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
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 strong. Then we define
This preserves
This is
The coherence laws will be satisfied.
Conversely, assume $\odot$ is given. Then we define
This is natural and
If the category $C$ is monoidal closed, strength and costrength 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\otimes [X,Y]\to Y$.
The unit is the unit of $- \otimes Y \dashv [Y, -]$ applied to $X$. The co-unit is the co-unit of $X \otimes - \dashv [X, -]$ applied to $Y$. 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.
The original reference for this part is Kock ‘72. Note that in there the terminology is a little different:
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 $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
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
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 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.
Every monad on Set is Set-enriched. In particular, it is strong.
Given a monad $T$ on Set, the assignment
is just the action of $T$ on the morphisms,
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.)
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
such that the following diagrams commute.
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 costrength $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 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).
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
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 $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 (Moggi ‘89) proposed the following typing rules for a sequence operator:
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
With the subscripts:
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,
is a strength map.
(Moggi)
Let $C$ be a category with finite products and let $T$ be a strong monad on $C$. For any points $x:1\to X$, $y:1\to T(Y)$, we have
Hence if $1$ is a generator, i.e. $C(1,-):C\to Set$ is faithful, then there is at most one strength for any ordinary monad on $C$.
In other words, a monad being strong is a property-like structure in a category with enough points.
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
Strong monads are important in Moggi’s theory of notions of computation (see monad (in computer science)):
More in-text references:
Last revised on October 4, 2021 at 09:38:17. See the history of this page for a list of all contributions to it.