The notion of enriched monads is that of monads in the context of enriched category theory: For a base of enrichment, a -enriched monad is a monad internal to the 2-category VCat of -enriched categories.
Generally (except in the base case Set) the structure of a -enriched monad on a -enriched category is stronger than that of the underlying monad on the underlying Set-category , whence one also speaks of strong monads (a priori a different notion, which however coincides with that of enriched monads under mild conditions, such as when is closed, see there).
The concept of enriched monads is key for the application of monads in computer science, since a monad coded verbatim in a functional programming language — where function types are to be interpreted not as external hom-sets but as internal homs in the ambient closed monoidal category of data types — is really a -enriched monad (hence typicall a strong monad).
Let
be a symmetric monoidal category which serves as the base of enrichment,
with denoting its unit object.
be a -enriched category
with underlying Set-category denoted , and
with hom-objects between any pais of objects denoted .
A -enriched monad on is, in Kleisli triple-presentation (eg. McDermott & Uustalu 2022, Def. 5.8):
for every object , an object ;
for every object , a morphism in of the form
(the monad unit)
for all pairs of objects of , a morphism in of the form
(the Kleisli extension or bind-operation)
such that the structural equations on a Kleisli triple
,
hold for generalized elements , of the hom-objects , , which means that the following diagrams commute in for all objects of :
(equivalence between -strength and -enrichment) For
, a pair of -enriched categories
then there is a bijection between the structures of
on the underlying functors,
and for any pair , of such a bijection between
It follows in particular that there is a bijection between
on such .
For a closed monoidal category the further assumptions in Prop. apply to being the canonical self-enrichment of .
Moreover:
For a symmetric monoidal closed category, there is a bijection between the structures of
on underlying monads on .
Hence from combining Prop. with Prop. we get:
For a symmetric closed monoidal category with denoting its self-enriched category, every symmetric monoidal monad on gives the structure of a -enriched monad on .
In the case in of enrichment by truth values, a monad is a closure operator on a poset.
In the application of monads in computer science, is typically the base of enrichment itself, canonically enriched over itself. For classical computing this is typically a cartesian closed category.
Since declaring a monad in a functional programming language means to define it in the internal language of , such monads in computer science are actually enriched, see the discussion there.
For example, if is the syntactic category of a programming language, then all the definable monads in the language are -enriched.
Kruna S. Ratkovic, Strength and Enrichment, Section 3.2 of: Morita theory in enriched context (2012) [arXiv:1302.2774, hal:tel-00785301]
Dylan McDermott, Tarmo Uustalu, Def. 5.6 in: What Makes a Strong Monad?, EPTCS 360 (2022) 113-133 [arXiv:2207.00851, doi:10.4204/EPTCS.360.6]
See also:
Max Kelly, John Power, Adjunctions whose counits are coequalizers and presentations of finitary enriched monads, Journal of Pure and Applied Algebra 89 (1993) [doi:10.1016/0022-4049(93)90092-8]
John Power, Enriched Lawvere theories, Theory and Applications of Categories 6 7 (1999) 83-93 [tac:6-07, pdf]
Eduardo Dubuc, Kan Extensions in Enriched Category Theory, Lecture Notes in Mathematics 145, Springer (1970) [doi:10.1007/BFb0060485]
Last revised on August 23, 2023 at 11:09:32. See the history of this page for a list of all contributions to it.