8.5.5 Internal Comonads

    Let $X$ be a set.

    We have a natural identification

    \[ \left\{ \begin{gathered} \text{Comonads in}\\ \text{$\boldsymbol {\mathsf{Rel}}$ on $X$} \end{gathered} \right\} \cong \left\{ \text{Subsets of $X$}\right\} . \]

    A comonad in $\boldsymbol {\mathsf{Rel}}$ on $X$ consists of a relation $R\colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}X$ together with maps

    \begin{align*} \Delta _{R} & \colon R \subset R\mathbin {\diamond }R,\\ \epsilon _{R} & \colon R \subset \Delta _{X} \end{align*}

    making the diagrams

    commute. However, since all morphisms involved are inclusions, the commutativity of the above diagrams is automatic (Chapter 11: Categories, Item 4 of Proposition 11.2.7.1.2), and hence all that is left is the data of the two maps $\Delta _{R}$ and $\epsilon _{R}$, which correspond respectively to the following conditions:

    1. 1.

      For each $x,y\in X$, if $x\sim _{R}y$, then there exists some $k\in X$ such that $x\sim _{R}k$ and $k\sim _{R}y$.

    2. 2.

      For each $x,y\in X$, if $x\sim _{R}y$, then $x=y$.

    The second condition implies that $R\subset \Delta _{X}$, so $R$ must be a subset of $X$. Taking $k=y$ in the first condition above then shows it to be trivially satisfied. Conversely, any subset $U$ of $X$ satisfies $U\subset \Delta _{X}$, defining a comonad as above.

    Let $f\colon A\to B$ be a function.

  • 1.

    The density comonad $\operatorname {\mathrm{Lan}}_{f}(f)\colon B\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ is given by

    for each $b\in B$. Thus, it corresponds to the image $\mathrm{Im}(f)$ of $f$ as a subset of $B$.

  • 2.

    The dual density comonad $\operatorname {\mathrm{Lift}}_{f^{\dagger }}(f^{\dagger })\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}A$ is given by

    for each $b\in B$. Thus, it also corresponds to the image $\mathrm{Im}(f)$ of $f$ as a subset of $B$.


Noticed something off, or have any comments? Feel free to reach out!


You can also use the contact form below: