nLab
strong monad

Strong monads

Context

Higher algebra

2-Category theory

Strong monads

Idea

A strong monad over a monoidal category VV is a monad in the bicategory of VV-actegories.

If VV is a monoidal closed category, then a strong monad is the same thing as a VV-enriched monad.

Definition

Definition

For VV a monoidal category a strong monad over VV is a monad

Here we regard VV as equipped with the canonical VV-action on itself.

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 more concrete definition is given in:

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

and later in

  • Eugenio Moggi. Computational Lambda-Calculus and Monads. Proceedings of the Fourth Annual Symposium on Logic in Computer Science. 1989. p. 14–23.

A strong monad over a category CC with finite products is a monad (T,η,μ)(T, \eta, \mu) together with a natural transformation t A,Bt_{A,B} from A×TBA \times T\;B to T(A×B)T(A\times B) subject to three diagrams.

“Strengthening with 1 is irrelevant”:

1×TA TA t 1,At 1,A T(1×A) \begin{array}{ccc} 1\times T\, A & \rightarrow & T\, A\\ \\ & t_{1,A}\searrow\phantom{t_{1,A}} & \downarrow\\ \\ & & T(1\times A) \end{array}

“Consecutive applications of strength commute”:

(A×B)×TC t A×B,C T((A×B)×C) A×(B×TC) A×t B,C A×T(B×C) t A,B×C T(A×(B×C)) \begin{array}{ccccc} (A\times B)\times T\, C & \xrightarrow{t_{A\times B,C}} & T\,((A\times B)\times C)\\ \\ \cong\downarrow\phantom{\cong} & & & \phantom{\cong}\searrow\cong\\ \\ A\times(B\times T\, C) & \xrightarrow[A\times t_{B,C}]{} & A\times T\,(B\times C) & \xrightarrow[t_{A,B\times C}]{} & T(A\times(B\times C)) \end{array}

“Strength commutes with monad unit and multiplication”:

A×B A×η BA×η B η A×Bη A×B A×TB t A,B T(A×B) A×μ BA×μ B μ A×Bμ A×B A×T 2B t A,TB T(A×TB) Tt A,B T 2(A×B) \begin{array}{ccccc} A\times B\\ \\ A\times\eta_{B}\downarrow\phantom{A\times\eta_{B}} & \phantom{\eta_{A\times B}}\searrow\eta_{A\times B}\\ \\ A\times T\, B & \xrightarrow{t_{A,B}} & T(A\times B)\\ \\ A\times\mu_{B}\uparrow\phantom{A\times\mu_{B}} & & & \phantom{\mu_{A\times B}}\nwarrow\mu_{A\times B}\\ \\ A\times T^{2}\, B & \xrightarrow{t_{A,T B}} & T(A\times T B) & \xrightarrow{T\: t_{A,B}} & T^{2}(A\times B) \end{array}

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.

Moggi’s typing rules and parameterized definition

Moggi 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 rather than 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.

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

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

Last revised on August 15, 2019 at 07:49:07. See the history of this page for a list of all contributions to it.