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\} . \] - (★) For each $b\in B$, if $b\sim _{R}a$, then there exists some $a'\in A$ such that $b\sim _{R}a'$ and $a'\sim _{U}a$.
- (★) For each $a\in A$, if $a\sim _{R}b$, then there exists some $x\in A$ such that $a\sim _{U}x$ and $x\sim _{R}b$.
8.5.7 Comodules Over Internal Comonads
Let $A$ be a set.
Proof of Proposition 8.5.7.1.1.
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 \]
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}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.
