Strong monad

A strong monad is a mathematical object defined using category theory that is used in theoretical computer science. In technical terms, a strong monad over a monoidal category (C, ⊗, I) is a monad (T, η, μ) together with a natural transformation tA,B : A ⊗ TB → T(A ⊗ B), called (tensorial) strength, such that the diagrams

, ,
, and

commute for every object A, B and C (see Definition 3.2 in [1]).

If the monoidal category (C, ⊗, I) is closed then a strong monad is the same thing as a C-enriched monad.

Commutative strong monads

For every strong monad T on a symmetric monoidal category, a costrength natural transformation can be defined by

t A , B ′ = T ( γ B , A ) ∘ t B , A ∘ γ T A , B : T A ⊗ B → T ( A ⊗ B ) . {\displaystyle t'_{A,B}=T(\gamma _{B,A})\circ t_{B,A}\circ \gamma _{TA,B}:TA\otimes B\to T(A\otimes B).}

A strong monad T is said to be commutative when the diagram

commutes for all objects A {\displaystyle A} and B {\displaystyle B} .[2]

One interesting fact about commutative strong monads is that they are "the same as" symmetric monoidal monads. More explicitly,

  • a commutative strong monad ( T , η , μ , t ) {\displaystyle (T,\eta ,\mu ,t)} defines a symmetric monoidal monad ( T , η , μ , m ) {\displaystyle (T,\eta ,\mu ,m)} by m A , B = μ A ⊗ B ∘ T t A , B ′ ∘ t T A , B : T A ⊗ T B → T ( A ⊗ B ) {\displaystyle m_{A,B}=\mu _{A\otimes B}\circ Tt'_{A,B}\circ t_{TA,B}:TA\otimes TB\to T(A\otimes B)}
  • and conversely a symmetric monoidal monad ( T , η , μ , m ) {\displaystyle (T,\eta ,\mu ,m)} defines a commutative strong monad ( T , η , μ , t ) {\displaystyle (T,\eta ,\mu ,t)} by t A , B = m A , B ∘ ( η A ⊗ 1 T B ) : A ⊗ T B → T ( A ⊗ B ) {\displaystyle t_{A,B}=m_{A,B}\circ (\eta _{A}\otimes 1_{TB}):A\otimes TB\to T(A\otimes B)}

and the conversion between one and the other presentation is bijective.

References

  1. ^ Moggi, Eugenio (July 1991). "Notions of computation and monads" (PDF). Information and Computation. 93 (1): 55–92. doi:10.1016/0890-5401(91)90052-4.
  2. ^ Muscholl, Anca, ed. (2014). Foundations of software science and computation structures : 17th (Aufl. 2014 ed.). [S.l.]: Springer. pp. 426–440. ISBN 978-3-642-54829-1.
  • Anders Kock (1972). "Strong functors and monoidal monads" (PDF). Archiv der Mathematik. 23: 113–120. doi:10.1007/BF01304852. S2CID 13246783.
  • Jean Goubault-Larrecq, Slawomir Lasota and David Nowak (2005). "Logical Relations for Monadic Types". Mathematical Structures in Computer Science. 18 (6): 1169. arXiv:cs/0511006. doi:10.1017/S0960129508007172. S2CID 741758.
  • Strong monad at the nLab