A relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ from $A$ to $B$1,2 is equivalently:
-
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 )$.
- 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}\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.
- •
-
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 )$.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.
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$.
-
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$.
-
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 ). \]
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\webleft (a\webright )$ 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\webleft (a\webright )=\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}\webleft (A\times B\webright )\\ & \cong \mathsf{Sets}\webleft (A\times B,\{ \mathsf{true},\mathsf{false}\} \webright )\\ & \cong \mathsf{Sets}\webleft (A,\mathcal{P}\webleft (B\webright )\webright )\\ & \cong \mathsf{Sets}\webleft (B,\mathcal{P}\webleft (A\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 )\\ & \cong \mathsf{Pos}^{\mathcal{C}}\webleft (\mathcal{P}\webleft (B\webright ),\mathcal{P}\webleft (A\webright )\webright ) \end{align*}
natural in $A,B\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$, where $\mathcal{P}\webleft (A\webright )$ and $\mathcal{P}\webleft (B\webright )$ 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$.
The trivial relation on $A$ and $B$ is the relation $\mathord {\sim }_{\mathrm{triv}}$ defined equivalently as follows:
The cotrivial relation on $A$ and $B$ is the relation $\mathord {\sim }_{\mathrm{cotriv}}$ defined equivalently as follows:
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.
Proof of Proposition 8.1.1.1.8.
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.
