nLab Kleisli category of a comonad

Contents

Context

2-Category theory

Higher algebra

Contents

Idea

Formally dually to how a monad has a Kleisli category so also a comonad P:𝒞𝒞P \colon \mathcal{C}\to\mathcal{C} has a (co-)Kleisli category: its objects are the objects of 𝒞\mathcal{C}, a morphism f:c 1c 2f \colon c_1 \to c_2 in the co-Kleisli category is a morphism

f˜:P(c 1)c 2 \tilde f \colon P(c_1) \longrightarrow c_2

in 𝒞\mathcal{C}, and the composition of two such in the co-Kleisli category is represented by the morphism in 𝒞\mathcal{C} given by

f 2f 1˜:P(c 1)P(P(c 1))P(f˜ 1)P(c 2)f˜ 2c 3. \widetilde{f_2 \circ f_1} \colon P(c_1) \longrightarrow P(P(c_1)) \stackrel{P(\tilde f_1)}{\longrightarrow} P(c_2) \stackrel{\tilde f_2}{\longrightarrow} c_3 \,.

Examples

General

Example

For an idempotent comonad the co-Kleisli category is the coreflective subcategory of its modal types.

Example

In typed functional programming, the Kleisli category of a comonad can be used to model call-by-name? programming languages. Dually, the Kleisli category of a monad may be used to model call-by-value?-programming, see there.

Generally, see at monad (in computer science) for more on this.

Specific

Example

(matrix multiplication as (co-)Kleisli composition)
For

consider the base change adjoint triple of BB-indexed sets of kk-vector spaces (kk-vector bundles over BB):

By the assumption that BB is finite and since Vect has biproducts, the colimit/coproduct

(p B) !𝒱 = b:B𝒱 b (p_B)_! \mathscr{V}_\bullet \;=\; \coprod_{b : B} \mathscr{V}_b

and the limit/product

(p B) *𝒱 = b:B𝒱 b (p_B)_\ast \mathscr{V}_\bullet \;=\; \prod_{b : B} \mathscr{V}_b

agree (we have an ambidextrous adjunction) and are both equivalent to the direct sum:

(p B) !𝒱 (p B) *𝒱 =b:B𝒱 b. (p_B)_! \mathscr{V}_\bullet \;\simeq\; (p_B)_\ast \mathscr{V}_\bullet \;=\; \underset{b \colon B}{\bigoplus} \mathcal{V}_b \,.

Accordingly, the underlying endofunctors of the induced monad and comonad on kVec Bk Vec_B

B(p B) *(p B) * B(p B) *(p B) !:kVec BkVec B \Box_B \;\coloneqq\; (p_B)^\ast (p_B)_\ast \;\;\vdash\;\; \lozenge_B \;\coloneqq\; (p_B)^\ast (p_B)_! \;\;\colon\;\; k Vec_B \longrightarrow k Vec_B

agree, to make a self-adjoint functor

(p B) * B(p B) * B:kVeckVec (p_B)^\ast \bigotimes_B \;\;\vdash\;\; (p_B)^\ast \bigotimes_B \;\;\;\colon\;\;\; k Vec \longrightarrow k Vec

which carries the structure both of a monad and of a comonad.

We claim that

  1. the categories of

    1. free (p B) * B(p_B)^\ast \oplus_B-algebras

    2. co-free (p B) * B(p_B)^\ast \oplus_B-coalgebras

    are both equivalent to the category k Vec k Vec of kk-vector spaces,

  2. where:

    1. the Kleisli category of B\bigoplus_B exhibits such linear maps as BB-tuples of columns of B×BB \times B-block matrices;

    2. the coKleisli category of B\bigoplus_B exhibits such linear maps as BB-tuples of rows of B×BB \times B-block matrices

with (co)Kleisli composition expressing the operation of block-matrix multiplication.

In particular, on the (co)free algebras of the form B(p B) *k\bigotimes_B (p_B)^\ast k this statement holds in the sense of actual B×BB \times B-matrices with entries in kk (as opposed to block matrices).

Since every linear map admits some B×BB \times B-block matrix representation, the second statement implies the first by the Kleisli theorem (see here).

Moreover, the second statement follows by direct inspection of the Kleisli morphisms (and dually for the coKleisli morphisms):

For this, identify a coKleisli morphism (where our notation now borrows from dependent linear type theory in order to express morphisms between BB-indexed sets of vector spaces)

b:B(b:B𝒱 b)F b𝒲 b b \colon B \;\; \vdash \;\; \Big( \underset{b' \colon B}{\bigoplus} \mathscr{V}_{b'} \Big) \xrightarrow{\; F_b \;} \mathscr{W}_b

with the BB-tuple of “block B×1B \times 1” matrices (F b) b:B(F_b)_{b \colon B} that it evidently encodes.

Observe that the comultiplication on the B\bigotimes_B-comonad is given by the diagonal map into the biproduct, coming from the “randomness unit” (terminology from modal quantum logic, following CQTS (2022)):

Using this, one readily sees that the Kleisli construction indeed sends such BB-tuples (F b) b:B(F_b)_{b \colon B} of block-matrix rows to the linear map FF which is given by the corresponding full matrix, and that the Kleisli composite with any other

b:B(b:B𝒲 b)G b𝒵 b b \colon B \;\; \vdash \;\; \Big( \underset{b' \colon B}{\bigoplus} \mathscr{W}_{b'} \Big) \xrightarrow{\; G_b \;} \mathscr{Z}_b

is indeed the row-decomposition of the corresponding matrix product:

The formally dual argument (now using the “definiteness counit”) shows the analogous statement for Kleisli morphisms and column-decomposition of block matrices:

Example

For P=JetP= Jet a jet comonad, then morphisms in its coKleisli category are differential operators (see there).

References

The equivalence of categories between the co-Kleisli category over a given comonad with the Kleisli category of an adjoint monad (if it exists):

Some introductory material on comonads, coalgebras and co-Kleisli morphisms:

  • Paolo Perrone, Notes on Category Theory with examples from basic mathematics, Chapter 5. (arXiv)

Last revised on November 30, 2022 at 16:32:24. See the history of this page for a list of all contributions to it.