8.1.1 Foundations
Let $A$ and $B$ be sets.
A relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ from $A$ to $B$ 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 )$.
(We will prove that Item 1, Item 2, Item 3, Item 4, Item 5, and Item 6 are indeed equivalent in a bit.)
We claim that Item 1, Item 2, Item 3, Item 4, and Item 5 are indeed equivalent:
-
•
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.
-
•
Item 5$\iff $Item 6: Omitted.
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$.
-
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)$.
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.