Difference between revisions of "Public:Comonads"

m (Comonad morphism)
m (Different representations)
Line 20: Line 20:


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


\[
\[
\begin{array}{rcl}
\begin{array}{rcl}
C & \overset{\delta}\Rightarrow & C^2 \\
C & \overset{\delta}\rightarrow & C^2 \\


{}_\delta\Downarrow & & \Downarrow {}_{\delta_C} \\
{}_\delta\downarrow & & \downarrow {}_{\delta_C} \\


C^2 & \overset{C\delta}\Rightarrow & C^3
C^2 & \overset{C\delta}\rightarrow & C^3
\end{array}
\end{array}
\qquad
\qquad
\qquad
\qquad
\begin{array}{rrl}
\begin{array}{rrl}
C & \overset{\delta}\Rightarrow & C^2 \\
C & \overset{\delta}\rightarrow & C^2 \\


& {}_{\id}\seArrow & \Downarrow {}_{\epsilon_C} \\
& {}_{\id}\searrow & \downarrow {}_{\epsilon_C} \\


& & C
& & C
Line 44: Line 44:
\qquad
\qquad
\begin{array}{rrl}
\begin{array}{rrl}
C & \overset{\delta}\Rightarrow & C^2 \\
C & \overset{\delta}\rightarrow & C^2 \\


& {}_{\mathrm{id}}\seArrow & \Downarrow {}_{C\epsilon} \\
& {}_{\mathrm{id}}\searrow & \downarrow {}_{C\epsilon} \\


& & C
& & C
Line 67: Line 67:
And conversely:
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)}}\).
* \((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)}}\).



== Relative comonads ==
== Relative comonads ==

Revision as of 10:07, 9 April 2021

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

Relative comonads

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 ...

\[ \array{ x & \stackrel{\eta^s x}{\to} & s x \\ x \eta^t \downarrow & & \downarrow \lambda \\ x t & \stackrel{1}{\to} & x t }\qquad \qquad \array{ s s x & \stackrel{s \lambda}{\to} & s x t & \stackrel{\lambda t}{\to} & x t t \\ \mu^s x \downarrow & & & & \downarrow x \mu^t \\ s x & & \stackrel{\lambda}{\to} & & x t } \]

In particular, if the two comonads \(C,D\) are on the same category \(\mathcal A\) a comonad morphism \(t\colon C\to D\) is required to satisfy the two following diagrams \begin{align} \begin{array}{rcl} C & \overset{t}\to & D \\ & {}_{\epsilon^C}\searrow & \downarrow_{\epsilon^D} \\ & & \Id \end{array} \qquad \qquad \begin{array}{rcl} C & --- & -\overset{t}-- & \to & D \\ {}_{\delta^C}\downarrow & & & & \downarrow {}_{\delta^D} \\ C^2 & \overset{C(t)}\to & C\circ D & \overset{t_D}\to & D^2 \end{array} \label{eq:com-morph} \end{align}

Distributive laws

Distributive laws with monads

References

TODO add more