Public:Comonads

\( \require{HTML} \newcommand\seArrow{\style{display: inline-block; transform: rotate(45deg)}{\Rightarrow}} \newcommand\searrow{\style{display: inline-block; transform: rotate(45deg)}{\to}} \newcommand\seEq{\style{display: inline-block; transform: rotate(45deg)}{=}} \newcommand\Id{\mathrm{Id}} \newcommand\id{\mathrm{id}} \newcommand\fcmp{\mathbin{;}} \renewcommand\epsilon{\varepsilon} \)

Different representations

Recall that a comonad on a category \(\mathcal{A}\) is a triple \((C,\epsilon,\delta)\) such that

1. \(C\colon \mathcal{A} \to \mathcal{A}\) is a functor,
2. \(\epsilon\colon C \to \mathrm{Id}_\mathcal{A}\) is a natural transformation,
3. \(\delta\colon C \to C^2\) is a natural transformation, and
4. the following diagrams commute

\[ \begin{array}{rcl} C & \overset{\delta}\rightarrow & C^2 \\ {}_\delta\downarrow & & \downarrow {}_{\delta_C} \\ C^2 & \overset{C\delta}\rightarrow & C^3 \end{array} \qquad \qquad \begin{array}{rrl} C & \overset{\delta}\rightarrow & C^2 \\ & {}_{\id}\searrow & \downarrow {}_{\epsilon_C} \\ & & C \end{array} \qquad \qquad \begin{array}{rrl} C & \overset{\delta}\rightarrow & C^2 \\ & {}_{\mathrm{id}}\searrow & \downarrow {}_{C\epsilon} \\ & & C \end{array} \]

Equivalently, it can be represented as a Kleisli-Manes triple \((C, \epsilon, \overline{(-)})\) such that

1. \(C\) is a mapping \(\mathrm{obj}(\mathcal{A}) \to \mathrm{obj}(\mathcal{A})\)
2. \(\epsilon\) is a collection of morphisms \(\epsilon_A\colon C(A) \to A\), for every object \(A\in \mathcal A\)
3. for every morphism \(f\colon C(A)\to B\) in \(\mathcal A\) we have a morphism \(\overline f\colon C(A)\to C(B)\) such that
   • (C1) \(\ \overline{\epsilon_A} = \id_{C(A)}\) for all objects \(A\in \mathcal{A}\)
   • (C2) \(\ \overline f \fcmp \epsilon_B = f\) for all morphisms \(f\colon C(A) \to B\)
   • (C3) \(\ \overline{\overline f \fcmp g} = \overline f \fcmp \overline g\) for all morphisms \(f\colon C(A) \to B\) and \(g\colon C(B) \to E\)

Here \(f \fcmp g\) is the diagramatic composition of arrows, equivalent to the more standard \(g \circ f\).

To transfer from the standard representation to the Kleisli-Manes we assign:

• \((C,\epsilon,\delta) \mapsto (C, \epsilon, \overline{(-)}) \) where \(\overline f = \delta_A \fcmp C(f)\) for every \(f\colon C(A) \to B\)

And conversely:

• \((C, \epsilon, \overline{(-)}) \mapsto (C,\epsilon,\delta)\) where, for a morphism \(f\colon A \to B\), the morphism \(C(f)\colon C(A) \to C(B)\) is \(\overline{\epsilon_A \fcmp f}\) and \(\delta_A\) is equal to \(\overline{\id_{C(A)}}\).

In fact, this is a bijective correspondence, cf. Proposition 1.6 in .

Every comonad \(C\) gives rise to two categories: the category of Eilenberg-Moore coalgebras \(EM(C)\) and the co-Kleisli category \(Klei(C)\).

Relative comonads

TODO

Comonad morphism

Given comonads \(C\) and \(D\) on categories \(\mathcal A\) and \(\mathcal B\), respectively, a comonad morphism \((F,\lambda)\colon C \to D\) is given by a functor \(F\colon \mathcal A\to \mathcal B\) and a natural transformation \(\lambda\colon FC \to DF\) such that

\[ \begin{array}{rcl} FC & \stackrel{\lambda}{\to} & DF \\ & {}_{F\epsilon^C}\searrow & \downarrow_{\epsilon^D_F} \\ & & F \end{array} \qquad \qquad \begin{array}{rcl} FC & --- & -\stackrel{\lambda}{--} & \to & DF \\ {}_{F\delta^C}\downarrow & & & & \downarrow {}_{F\delta^D} \\ FC^2 & \stackrel{\lambda_C}{\to} & DFC & \stackrel{D\lambda}{\to} & D^2F \end{array} \]

In particular, if the two comonads \(C,D\) are on the same category \(\mathcal A\) a comonad morphism \(\lambda\colon C\to D\) is required to make the two following diagrams commute \[ \begin{array}{rcl} C & \stackrel{\lambda}{\to} & D \\ & {}_{\epsilon^C}\searrow & \downarrow_{\epsilon^D} \\ & & \Id \end{array} \qquad \qquad \begin{array}{rcl} C & --- & -\stackrel{\lambda}{--} & \to & D \\ {}_{\delta^C}\downarrow & & & & \downarrow {}_{\delta^D} \\ C^2 & \stackrel{C(\lambda)}{\to} & C\circ D & \stackrel{\lambda_D}{\to} & D^2 \end{array} \]

Given two morphisms \((F,\lambda),(F',\lambda')\colon D\to C\) of comonads. A morphism of comonad morphisms \(\gamma\colon (F,\lambda) \Rightarrow (F',\lambda')\) is given by a natural transformation \(\gamma\colon F\to F'\) such that \[ \begin{array}{rcl} FC & \stackrel{\gamma_C}{\to} & F'C\\ {}_{\lambda}\downarrow & & {}_{\lambda'}\downarrow \\ DF & \stackrel{D\gamma}{\to} & DF' \end{array} \]

Let's assume we have a functor \(F\colon \mathcal A\to \mathcal B\) and comonads \(C\) and \(D\) on \(\mathcal A\) and \(\mathcal B\), respectively. Then,

1. comonad morphisms \((F,\lambda)\colon C\to D\) are in a bijective correspondence with functors \(\widehat F\colon EM(C) \to EM(D)\) such that \[ \array{ EM(C) & \stackrel{\widehat{F}}{\to} & EM(D) \\ \downarrow & & \downarrow \\ \mathcal A & \stackrel{F}{\to} & \mathcal B } \]
2. If \(EM(C)\) has equalisers of reflexive pairs and \(F\) has a right adjoint, then any lifting \(\widehat F\) has a right adjoint.
3. If \(F\) has a left adjoint and \(\lambda\colon FC \to DF\) is invertible, then the lifting \(\widehat F\) associated with \(\lambda\) has a left adjoint.

For details see Proposition 3.5 in .

Note that monad morphisms can be also defined as natural transformations of the form \(CF \to FD\) satisfying similar conditions to those mentioned above. This probably leads to different characterisations akin to what is in the previous theorem. See, for example .

Distributive laws

These are special kinds of comonad morphisms. Let \(C,D\) be two comonads on the same category \(\mathcal A\) and let \(\lambda\colon CD \to DC\) be a natural transformation which corresponds to a lifting \(\widehat C\) such that \[ \array{ EM(D) & \stackrel{\widehat{C}}{\to} & EM(D) \\ \downarrow & & \downarrow \\ \mathcal A & \stackrel{C}{\to} & \mathcal A } \] Then, \(\lambda\) is said to be a comonad distributive law if and only if \(\widehat{C}\) is a comonad on \(EM(D)\).

There is a bijection between

• comonad distributive laws \(\lambda\colon CD \to DC\),
• liftings \(\widetilde D\colon Klei(C) \to Klei(C)\) such that the following diagram commutes \[ \array{ \mathcal A & \stackrel{D}{\to} & \mathcal A \\ \downarrow & & \downarrow \\ Klei(C) & \stackrel{\widetilde{D}}{\to} & Klei(C) } \] and \(\widetilde D\) has a comonad structure on \(Klei(C)\).
• natural transformations \(\lambda\colon CD \to DC\) making the following four diagrams commute

\begin{align*} \begin{array}{rcl} CD & \stackrel{\lambda}{\to} & DC \\ & {}_{C\epsilon^D}\searrow & \downarrow_{\epsilon^D_C} \\ & & C \end{array} \qquad\qquad \begin{array}{rcl} CD & --- & -\stackrel{\lambda}{--} & \to & DC \\ {}_{C\delta^D}\downarrow & & & & \downarrow {}_{\delta^D_C} \\ CD^2 & \stackrel{\lambda_D}{\to} & DCD & \stackrel{D\lambda}{\to} & D^2C \end{array} \\[1.5em] \begin{array}{rcl} CD & \stackrel{\lambda}{\to} & DC \\ & {}_{\epsilon^C_D}\searrow & \downarrow_{D\epsilon^C} \\ & & D \end{array} \qquad\qquad \begin{array}{rcl} CD & --- & -\stackrel{\lambda}{--} & \to & DC \\ {}_{\delta^C_D}\downarrow & & & & \downarrow {}_{D\delta^C} \\ C^2D & \stackrel{C\lambda}{\to} & CDC & \stackrel{\lambda_C}{\to} & DC^2 \end{array} \end{align*} Also, a distributive law \(\lambda\) (given by any of the equivalent definitions above) introduces a comonad structure on \(CD\) and \(EM(CD) \cong EM(\widehat C)\).

For details see and also .

Distributive laws with monads

See, for example, Section 5 in or .