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} \)

UNDER CONSTRUCTION

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)}}\).

Comonad morphism

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

\[ \begin{array}{rcl} CF & \stackrel{\lambda}{\to} & FD \\ & {}_{\epsilon^C_F}\searrow & \downarrow_{F\epsilon^D} \\ & & F \end{array} \qquad \qquad \begin{array}{rcl} CF & --- & -\stackrel{\lambda}{--} & \to & FD \\ {}_{\delta^C_F}\downarrow & & & & \downarrow {}_{F\delta^D} \\ C^2F & \stackrel{C(\lambda)}{\to} & CFD & \stackrel{\lambda_D}{\to} & FD^2 \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} \]

A morphism of comonad morphisms \(\gamma\colon (F,\lambda) \Rightarrow (F',\lambda')\) is given by ...

References

• Gabriella Böhm, Tomasz Brzeziński, Robert Wisbauer. Monads and comonads on module categories. Journal of Algebra 322.5 (2009): 1719-1747.
• Aura Bârdeş. Bimonads in a 2-category.

TODO add more