Remark 5.1.1.1.4 (00HQ): Equivalent Definitions of Relations

Style	Class	Font	Theorem Environments
Style 1	`book`	Alegreya Sans	`tcbthm`
Style 2	`book`	Alegreya Sans	`amsthm`
Style 3	`book`	Arno*	`amsthm`
Style 4	`book`	Computer Modern	`amsthm`

A relation from $A$ to $B$ is equivalently:^[1]

A subset of $A\times B$.
A function from $A\times B$ to $\{ \mathsf{true},\mathsf{false}\} $.
A function from $A$ to $\mathcal{P}\webleft (B\webright )$.
A function from $B$ to $\mathcal{P}\webleft (A\webright )$.
A cocontinuous morphism of posets from $\webleft (\mathcal{P}\webleft (A\webright ),\subset \webright )$ to $\webleft (\mathcal{P}\webleft (B\webright ),\subset \webright )$.

That is: we have bijections of sets

\begin{align*} \mathrm{Rel}\webleft (A,B\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathcal{P}\webleft (A\times B\webright ),\\ & \cong \textup{Hom}_{\mathsf{Sets}}\webleft (A\times B,\{ \mathsf{true},\mathsf{false}\} \webright ),\\ & \cong \textup{Hom}_{\mathsf{Sets}}\webleft (A,\mathcal{P}\webleft (B\webright )\webright ),\\ & \cong \textup{Hom}_{\mathsf{Sets}}\webleft (B,\mathcal{P}\webleft (A\webright )\webright ),\\ & \cong \textup{Hom}^{\mathrm{cocont}}_{\mathsf{Pos}}\webleft (\mathcal{P}\webleft (A\webright ),\mathcal{P}\webleft (B\webright )\webright ), \end{align*}

natural in $A,B\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.

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 2: Constructions With Sets, Item 1 and Item 2 of Proposition 2.4.3.1.6.
Item 2$\iff $Item 3: This follows from the bijections

\begin{align*} \textup{Hom}_{\mathsf{Sets}}\webleft (A\times B,\{ \mathsf{true},\mathsf{false}\} \webright ) & \cong \textup{Hom}_{\mathsf{Sets}}\webleft (A,\textup{Hom}_{\mathsf{Sets}}\webleft (B,\{ \mathsf{true},\mathsf{false}\} \webright )\webright )\\ & \cong \textup{Hom}_{\mathsf{Sets}}\webleft (A,\mathcal{P}\webleft (B\webright )\webright ), \end{align*}

where the last bijection is from Chapter 2: Constructions With Sets, Item 1 and Item 2 of Proposition 2.4.3.1.6.
Item 2$\iff $Item 4: This follows from the bijections

\begin{align*} \textup{Hom}_{\mathsf{Sets}}\webleft (A\times B,\{ \mathsf{true},\mathsf{false}\} \webright ) & \cong \textup{Hom}_{\mathsf{Sets}}\webleft (B,\textup{Hom}_{\mathsf{Sets}}\webleft (B,\{ \mathsf{true},\mathsf{false}\} \webright )\webright )\\ & \cong \textup{Hom}_{\mathsf{Sets}}\webleft (B,\mathcal{P}\webleft (A\webright )\webright ), \end{align*}

where again the last bijection is from Chapter 2: Constructions With Sets, Item 1 and Item 2 of Proposition 2.4.3.1.6.
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 )$, Chapter 2: Constructions With Sets, Item 2 of Proposition 2.4.3.1.8.

In particular, the bijection

\[ \mathrm{Rel}\webleft (A,B\webright )\cong \textup{Hom}^{\mathrm{cocont}}_{\mathsf{Pos}}\webleft (\mathcal{P}\webleft (A\webright ),\mathcal{P}\webleft (B\webright )\webright ) \]

is given by taking a relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$, passing to its associated function $f\colon A\to \mathcal{P}\webleft (B\webright )$ from $A$ to $B$ and then extending $f$ from $A$ to all of $\mathcal{P}\webleft (A\webright )$ by taking its left Kan extension along $\chi _{X}$.

This coincides with the direct image function $f_{*}\colon \mathcal{P}\webleft (A\webright )\to \mathcal{P}\webleft (B\webright )$ of Chapter 2: Constructions With Sets, Definition 2.4.4.1.1.

This finishes the proof.

Footnotes

[1] Intuition: In particular, we may think of a relation $R\colon A\to \mathcal{P}\webleft (B\webright )$ from $A$ to $B$ as a multivalued function from $A$ to $B$ (including the possibility of a given $a\in A$ having no value at all).