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}\webleft (B\webright )$.
-
4.
A function from $B$ to $\mathcal{P}\webleft (A\webright )$.
-
5.
A cocontinuous morphism of posets from $\webleft (\mathcal{P}\webleft (A\webright ),\subset \webright )$ to $\webleft (\mathcal{P}\webleft (B\webright ),\subset \webright )$.
-
6.
A continuous morphism of posets from $\webleft (\mathcal{P}\webleft (B\webright ),\supset \webright )$ to $\webleft (\mathcal{P}\webleft (A\webright ),\supset \webright )$.
(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}\webleft (A\times B,\{ \mathsf{true},\mathsf{false}\} \webright ) & \cong \mathsf{Sets}\webleft (A,\mathsf{Sets}\webleft (B,\{ \mathsf{true},\mathsf{false}\} \webright )\webright )\\ & \cong \mathsf{Sets}\webleft (A,\mathcal{P}\webleft (B\webright )\webright ), \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}\webleft (A\times B,\{ \mathsf{true},\mathsf{false}\} \webright ) & \cong \mathsf{Sets}\webleft (B,\mathsf{Sets}\webleft (B,\{ \mathsf{true},\mathsf{false}\} \webright )\webright )\\ & \cong \mathsf{Sets}\webleft (B,\mathcal{P}\webleft (A\webright )\webright ), \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}\webleft (X\webright )$ of a set $X$ as the free cocompletion of $X$ via the characteristic embedding
\[ \chi _{X} \colon X \hookrightarrow \mathcal{P}\webleft (X\webright ) \]
of $X$ into $\mathcal{P}\webleft (X\webright )$, as in Chapter 4: Constructions With Sets, Proposition 4.4.5.1.1. In particular, the bijection
\[ \mathsf{Sets}\webleft (A,\mathcal{P}\webleft (B\webright )\webright )\cong \mathsf{Pos}^{\style {display: inline-block; transform: rotate(180deg)}{\mathcal{C}}\mkern -2.5mu}\webleft (\mathcal{P}\webleft (A\webright ),\mathcal{P}\webleft (B\webright )\webright ) \]
is given by extending each $f\colon A\to \mathcal{P}\webleft (B\webright )$ in $\mathsf{Sets}\webleft (A,\mathcal{P}\webleft (B\webright )\webright )$ from $A$ to all of $\mathcal{P}\webleft (A\webright )$ by taking its left Kan extension along $\chi _{X}$, recovering the direct image function $f_{!}\colon \mathcal{P}\webleft (A\webright )\to \mathcal{P}\webleft (B\webright )$ 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}\webleft (A,B\webright )$ for the set of relations from $A$ to $B$.
-
2.
We write $\mathbf{Rel}\webleft (A,B\webright )$ for the sub-poset of $\webleft (\mathcal{P}\webleft (A\times B\webright ),\subset \webright )$ 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 $\webleft (a,b\webright )\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 $\webleft (a,b\webright )$.
The trivial relation on $A$ and $B$ is the relation $\mathord {\sim }_{\mathrm{triv}}$ defined equivalently as follows:
-
1.
As a subset of $A\times B$, we have
\[ \mathord {\sim }_{\mathrm{triv}}\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}A\times B. \]
-
2.
As a function from $A\times B$ to $\{ \mathsf{true},\mathsf{false}\} $, the relation $\mathord {\sim }_{\mathrm{triv}}$ is the constant function
\[ \Delta _{\mathsf{true}}\colon A\times B\to \{ \mathsf{true},\mathsf{false}\} \]
from $A\times B$ to $\{ \mathsf{true},\mathsf{false}\} $ taking the value $\mathsf{true}$.
-
3.
As a function from $A$ to $\mathcal{P}\webleft (B\webright )$, the relation $\mathord {\sim }_{\mathrm{triv}}$ is the function
\[ \Delta _{\mathsf{true}}\colon A\to \mathcal{P}\webleft (B\webright ) \]
defined by
\[ \Delta _{\mathsf{true}}\webleft (a\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}B \]
for each $a\in A$.
-
4.
Lastly, it is the unique relation $R$ on $A$ and $B$ such that we have $a\sim _{R}b$ for each $a\in A$ and each $b\in B$.
The cotrivial relation on $A$ and $B$ is the relation $\mathord {\sim }_{\mathrm{cotriv}}$ defined equivalently as follows:
-
1.
As a subset of $A\times B$, we have
\[ \mathord {\sim }_{\mathrm{cotriv}}\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\text{Ø}. \]
-
2.
As a function from $A\times B$ to $\{ \mathsf{true},\mathsf{false}\} $, the relation $\mathord {\sim }_{\mathrm{cotriv}}$ is the constant function
\[ \Delta _{\mathsf{false}}\colon A\times B\to \{ \mathsf{true},\mathsf{false}\} \]
from $A\times B$ to $\{ \mathsf{true},\mathsf{false}\} $ taking the value $\mathsf{false}$.
-
3.
As a function from $A$ to $\mathcal{P}\webleft (B\webright )$, the relation $\mathord {\sim }_{\mathrm{cotriv}}$ is the function
\[ \Delta _{\mathsf{false}}\colon A\to \mathcal{P}\webleft (B\webright ) \]
defined by
\[ \Delta _{\mathsf{false}}\webleft (a\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\text{Ø} \]
for each $a\in A$.
-
4.
Lastly, it is the unique relation $R$ on $A$ and $B$ such that we have $a\nsim _{R}b$ for each $a\in A$ and each $b\in B$.
The characteristic relation
\[ \chi _{X}\webleft (-_{1},-_{2}\webright )\colon X\times X\to \{ \mathsf{t},\mathsf{f}\} \]
on $X$ of Chapter 4: Constructions With Sets, Definition 4.5.3.1.1, defined by
\[ \chi _{X}\webleft (x,y\webright ) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} \mathsf{true}& \text{if $x=y$,}\\ \mathsf{false}& \text{if $x\neq y$} \end{cases} \]
for each $x,y\in X$, is another example of a relation.
Let $A$ and $B$ be sets and let $R,S\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be relations.
-
1.
End Formula for the Set of Inclusions of Relations. We have
\[ \operatorname {\mathrm{Hom}}_{\mathbf{Rel}\webleft (A,B\webright )}\webleft (R,S\webright )\cong \int _{a\in A}\int _{b\in B}\operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright ). \]
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}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright )\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}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright )\cong \mathrm{pt}$}\\ \text{Ø}& \text{otherwise.}\end{cases} \]
Since we have $\operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright )=\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}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright )\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}\webleft (A,B\webright )}\webleft (R,S\webright )\cong \begin{cases} \mathrm{pt}& \text{if $R\subset S$,}\\ \text{Ø}& \text{otherwise.}\end{cases} \]
Since $\webleft (a\sim _{R}b\implies a\sim _{S}b\webright )$ iff $R\subset S$, the two sets above are isomorphic. This finishes the proof.
