A relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ from $A$ to $B$1,2 is equivalently:
-
1.
A subset $R$ of $A\times B$.
-
2.
A function from $A\times B$ to $\{ \mathsf{true},\mathsf{false}\} $.
-
3.
A function from $A$ to $\mathcal{P}(B)$.
-
4.
A function from $B$ to $\mathcal{P}(A)$.
-
5.
A cocontinuous morphism of posets from $(\mathcal{P}(A),\subset )$ to $(\mathcal{P}(B),\subset )$.
-
6.
A continuous morphism of posets from $(\mathcal{P}(B),\supset )$ to $(\mathcal{P}(A),\supset )$.
- 1Further Terminology: Also called a multivalued function from $A$ to $B$.
- 2Further Terminology: When $A=B$, we also call $R\subset A\times A$ a relation on $A$.
-
•
Item 1$\iff $Item 2: This is a special case of Chapter 4: Constructions With Sets, Item 2 and Item 3 of Proposition 4.5.1.1.4.
-
•
Item 2$\iff $Item 3: This follows from the bijections
\begin{align*} \mathsf{Sets}(A\times B,\{ \mathsf{true},\mathsf{false}\} ) & \cong \mathsf{Sets}(A,\mathsf{Sets}(B,\{ \mathsf{true},\mathsf{false}\} ))\\ & \cong \mathsf{Sets}(A,\mathcal{P}(B)), \end{align*}where the last bijection is from Chapter 4: Constructions With Sets, Item 2 and Item 3 of Proposition 4.5.1.1.4.
-
•
Item 2$\iff $Item 4: This follows from the bijections
\begin{align*} \mathsf{Sets}(A\times B,\{ \mathsf{true},\mathsf{false}\} ) & \cong \mathsf{Sets}(B,\mathsf{Sets}(B,\{ \mathsf{true},\mathsf{false}\} ))\\ & \cong \mathsf{Sets}(B,\mathcal{P}(A)), \end{align*}where again the last bijection is from Chapter 4: Constructions With Sets, Item 2 and Item 3 of Proposition 4.5.1.1.4.
-
•
Item 2$\iff $Item 5: This follows from the universal property of the powerset $\mathcal{P}(X)$ of a set $X$ as the free cocompletion of $X$ via the characteristic embedding
\[ \chi _{X} \colon X \hookrightarrow \mathcal{P}(X) \]of $X$ into $\mathcal{P}(X)$, as in Chapter 4: Constructions With Sets, Proposition 4.4.5.1.1. In particular, the bijection
\[ \mathsf{Sets}(A,\mathcal{P}(B))\cong \mathsf{Pos}^{\style {display: inline-block; transform: rotate(180deg)}{\mathcal{C}}\mkern -2.5mu}(\mathcal{P}(A),\mathcal{P}(B)) \]is given by extending each $f\colon A\to \mathcal{P}(B)$ in $\mathsf{Sets}(A,\mathcal{P}(B))$ from $A$ to all of $\mathcal{P}(A)$ by taking its left Kan extension along $\chi _{X}$, recovering the direct image function $f_{!}\colon \mathcal{P}(A)\to \mathcal{P}(B)$ of $f$ of Chapter 4: Constructions With Sets, Definition 4.6.1.1.1.
- •
-
1.
We write $\mathrm{Rel}(A,B)$ for the set of relations from $A$ to $B$.
-
2.
We write $\mathbf{Rel}(A,B)$ for the sub-poset of $(\mathcal{P}(A\times B),\subset )$ spanned by the relations from $A$ to $B$.
-
3.
Given $a\in A$ and $b\in B$, we write $a\sim _{R}b$ to mean $(a,b)\in R$.
-
4.
When viewing $R$ as a function
\[ R\colon A\times B\to \{ \mathsf{t},\mathsf{f}\} , \]we write $R^{b}_{a}$ for the value of $R$ at $(a,b)$.1
-
1The choice to write $R^{b}_{a}$ in place of $R^{a}_{b}$ is to keep the notation consistent with the notation we will later employ for profunctors in
. -
1.
End Formula for the Set of Inclusions of Relations. We have
\[ \operatorname {\mathrm{Hom}}_{\mathbf{Rel}(A,B)}(R,S)\cong \int _{a\in A}\int _{b\in B}\operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }(R^{b}_{a},S^{b}_{a}). \]
8.1.1 Foundations
Let $A$ and $B$ be sets.
Proof of the Equivalences in Definition 8.1.1.1.1.
(We will prove that Item 1, Item 2, Item 3, Item 4, Item 5, and Item 6 are indeed equivalent in a bit.)
We may think of a relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ as a function from $A$ to $B$ that is multivalued, assigning to each element $a$ in $A$ a set $R(a)$ of elements of $B$, thought of as the set of values of $R$ at $a$.
Note that this includes also the possibility of $R$ having no value at all on a given $a\in A$ when $R(a)=\text{Ø}$.
Another way of stating the equivalence between Item 1, Item 2, Item 3, Item 4, and Item 5 of Definition 8.1.1.1.1 is by saying that we have bijections of sets
\begin{align*} \left\{ \text{relations from $A$ to $B$}\right\} & \cong \mathcal{P}(A\times B)\\ & \cong \mathsf{Sets}(A\times B,\{ \mathsf{true},\mathsf{false}\} )\\ & \cong \mathsf{Sets}(A,\mathcal{P}(B))\\ & \cong \mathsf{Sets}(B,\mathcal{P}(A))\\ & \cong \mathsf{Pos}^{\style {display: inline-block; transform: rotate(180deg)}{\mathcal{C}}\mkern -2.5mu}(\mathcal{P}(A),\mathcal{P}(B))\\ & \cong \mathsf{Pos}^{\mathcal{C}}(\mathcal{P}(B),\mathcal{P}(A)) \end{align*}
natural in $A,B\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$, where $\mathcal{P}(A)$ and $\mathcal{P}(B)$ are endowed with the poset structure given by inclusion.
Proof of the Equivalences in Definition 8.1.1.1.1.
We claim that Item 1, Item 2, Item 3, Item 4, and Item 5 are indeed equivalent:
This finishes the proof.
Let $A$ and $B$ be sets and let $R\colon \mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation from $A$ to $B$.
Let $A$ and $B$ be sets and let $R,S\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be relations.
Proof of Proposition 8.1.1.1.5.
Item 1: End Formula for the Set of Inclusions of Relations
Unwinding the expression inside the end on the right hand side, we have
\[ \int _{a\in A}\int _{b\in B}\operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }(R^{b}_{a},S^{b}_{a})\cong \begin{cases} \mathrm{pt}& \text{if, for each $a\in A$ and each $b\in B$,}\\ & \text{we have $\operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }(R^{b}_{a},S^{b}_{a})\cong \mathrm{pt}$}\\ \text{Ø}& \text{otherwise.}\end{cases} \]
Since we have $\operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }(R^{b}_{a},S^{b}_{a})=\left\{ \mathsf{true}\right\} \cong \mathrm{pt}$ exactly when $R^{b}_{a}=\mathsf{false}$ or $R^{b}_{a}=S^{b}_{a}=\mathsf{true}$, we get
\[ \int _{a\in A}\int _{b\in B}\operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }(R^{b}_{a},S^{b}_{a})\cong \begin{cases} \mathrm{pt}& \text{if, for each $a\in A$ and each $b\in B$,}\\ & \text{if $a\sim _{R}b$, then $a\sim _{S}b$,}\\ \text{Ø}& \text{otherwise.}\end{cases} \]
On the left hand-side, we have
\[ \operatorname {\mathrm{Hom}}_{\mathbf{Rel}(A,B)}(R,S)\cong \begin{cases} \mathrm{pt}& \text{if $R\subset S$,}\\ \text{Ø}& \text{otherwise.}\end{cases} \]
Since $(a\sim _{R}b\implies a\sim _{S}b)$ iff $R\subset S$, the two sets above are isomorphic. This finishes the proof.
