Proposition 8.5.7.1.1 (02EW): Comodules Over Internal Comonads in $\boldsymbol {\mathsf{Rel}}$

Let $U$ be a subset of $A$, viewed also as an internal comonad on $A$ via Proposition 8.5.5.1.1.

1.
Left Comodules. We have a natural identification

\[ \left\{ \text{Left comodules over $U$}\right\} \cong \left\{ \begin{aligned} & \text{Relations $R\colon B\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}A$ such that,}\\ & \text{for each $b\in B$, we have $R(b)\subset U$} \end{aligned} \right\} . \]
2.
Right Comodules. We have a natural identification

\[ \left\{ \text{Right comodules over $U$}\right\} \cong \left\{ \begin{aligned} & \text{Relations $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ such that,}\\ & \text{for each $b\in B$, we have $R^{-1}(b)\subset U$}\end{aligned} \right\} . \]
3.
Bicomodules. We have a natural identification

\[ \left\{ \text{Bicomodules over $U$}\right\} \cong \left\{ \begin{gathered} \text{Quadruples $(B,C,R,S)$ such that:}\\ \begin{aligned} & \text{1. For each $b\in B$, we have $R(b)\subset U$}\\ & \text{2. For each $c\in C$, we have $S^{-1}(c)\subset U$} \end{aligned} \end{gathered} \right\} . \]

Item 1: Left Comodules

A left comodule over $U$ in $\boldsymbol {\mathsf{Rel}}$ consists of a relation $R\colon B\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}A$ together with an inclusion

\[ R \subset U\mathbin {\diamond }R \]

making appropriate diagrams commute. Since $\boldsymbol {\mathsf{Rel}}$ is locally posetal, however, the commutativity of the diagrams in question 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 inclusion. This corresponds to the following condition:

(★)

Since $a'\sim _{U}a$ is true if $a=a'$ and $a\in U$, this condition ends up being equivalent to $R(b)\subset U$.

Item 2: Right Comodules

A right comodule over $U$ in $\boldsymbol {\mathsf{Rel}}$ consists of a relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ together with an inclusion

\[ R \subset R\mathbin {\diamond }U \]

(★)

Since $a\sim _{U}x$ is true if $a=x$ and $a\in U$, this condition ends up being equivalent to $R^{-1}(b)\subset U$.

Item 3: Bicomodules

Since $\boldsymbol {\mathsf{Rel}}$ is locally posetal, the diagram encoding the compatibility conditions for a bimodule commutes automatically (Chapter 11: Categories, Item 4 of Proposition 11.2.7.1.2), and hence a bicomodule is just a left comodule along with a right comodule.

The Clowder Project

8.5.7 Comodules Over Internal Comonads