nLab relative monad

Contents

Contents

Idea

A relative monad is what is to a relative adjunction as a monad is to an adjunction.

In ACU14, the authors proved that a relative monad on a functor J:JCJ:\mathbf J \to \mathbf C are ‘skew-monoids in the skew-monoidal category [J,C][\mathbf J, \mathbf C]’ (see below).

Definition

Let J,C\mathbf J, \mathbf C be categories and J:JCJ: \mathbf J \to \mathbf C be a functor.

Definition

A relative monad TT on JJ is a functor T:JCT:\mathbf J \to \mathbf C equipped with

  • a unit η X:JXTX\eta_X : J X \to T X natural in X:JX : \mathbf J,
  • a Kleisli extension () *:C(JX,TY)C(TX,TY)(-)^* : \mathbf C(J X, T Y) \to \mathbf C(T X, T Y) in both X,Y:JX,Y:\mathbf J

such that for every X,Y,Z:JX,Y,Z:\mathbf J and k:JXTYk:J X \to T Y,

  • (left unital law) k=k *η Xk = k^* \circ \eta_X,
  • (right unital law) η X *=1 TX\eta_X^* = 1_{T X},
  • (associativity law) ( *k) *= *k *(\ell^* \circ k)^* = \ell^* \circ k^* for every :JYTZ\ell : J Y \to T Z.

Notice that for any f:XYf:X \to Y in J\mathbf J, one has

Tf=(η JYJf) *. Tf = (\eta_{J Y} \circ J f)^*.

In computer science, monads are usually defined by a unit and an extension operator, as above, so that relative monads are very close to plain monads in that regard. Since [J,C][\mathbf J, \mathbf C] lacks a monoidal structure (unlike [C,C][\mathbf C, \mathbf C]), to define relative monads like mathematicians define monads (as monoids in a category of endofunctors) we need to be more clever.

As skew-monoids

A skew-monoidal category is like a monoidal category except its unitors and associators are not necessarily invertible. A monoid in a skew-monoidal category is called a ‘skew-monoid’.

Composition of functors F,G:JCF,G:\mathbf J \to \mathbf C can be defined by first extending FF along JJ and then composing with GG. The resulting composition product on [J,C][\mathbf J, \mathbf C] is coherent but only laxly so, hence the need to appeal to skew-monoidal categories.

Theorem

[Theorem 3.4] Suppose J:JCJ:\mathbf J \to \mathbf C is such that Lan J:[J,C][C,C]\mathrm{Lan}_J : [\mathbf J, \mathbf C] \to [\mathbf C, \mathbf C] exists (e.g. if J\mathbf J is small and C\mathbf C cocomplete). Then [J,C][\mathbf J, \mathbf C] is skew-monoidal, with unit JJ and product F JG=(Lan JF)GF \circ^J G = (\mathrm{Lan}_J F) \circ G, and a relative monad is a monoid in ([J,C],J, J)([\mathbf J, \mathbf C], J, \circ^J).

When J:JCJ:\mathbf J \to \mathbf C is a free completion of J\mathbf{J} under colimits from some set \mathcal{F} of indexing types, then this skew-monoidal structure on [J,C][\mathbf J, \mathbf C] is properly monoidal, since it is equivalent to the \mathcal{F}-colimit preserving functors CC\mathbf C\to\mathbf C, and the monoidal structure is just functor composition.

Examples

  • A relative monad on the embedding J:FinSetSetJ:\mathbf{FinSet} \to \mathbf {Set} is the same thing as an abstract clone. These are equivalent to finitary monads and single-sorted algebraic theories.

  • Any monad TT on C\mathbf{C} induces a relative monad TJTJ on JJ, for any J:JCJ:\mathbf{J}\to \mathbf{C}.

  • Fixing a category 𝕍\mathbb{V} with finite products, to give a Freyd category is to give a strong relative monad on the Yoneda embedding 𝕍[𝕍 op,Set]\mathbb{V}\to [\mathbb{V}^{\mathrm{op}},\mathbf{Set}].

  • The presheaf construction ([ op,Set])(\mathbb{C}\mapsto [{\mathbb{C}}^{\mathrm{op}},\mathbf{Set}]) can be regarded as a relative pseudomonad on the inclusion CatCAT\mathbf{Cat}\to \mathbf{CAT}. (See also Yoneda structures.)

  • A monad on C \mathbf C with arities in J C \mathbf{J}\subseteq \mathbf C is the same thing as a relative monad for the embedding JC\mathbf{J}\to \mathbf C. (Here JC\mathbf{J}\subseteq \mathbf{C} is required to be a dense subcategory, so that to give a functor JC\mathbf{J}\subseteq \mathbf{C} is to give a functor CC\mathbf{C}\to\mathbf{C} preserving JJ-absolute colimits.)

References

Discussion with an eye towards monads in computer science is in

  • Thorsten Altenkirch, James Chapman, Tarmo Uustalu, Monads need not be endofunctors, Logical methods in computer science (arxiv)

Last revised on September 28, 2022 at 11:18:58. See the history of this page for a list of all contributions to it.