Remark 6.1.1.1.3 (01R0) — The Clowder Project

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`

Another way of stating the equivalence between Item 1, Item 2, Item 3, Item 4, and Item 5 of Definition 6.1.1.1.1 is by saying that we have bijections of sets

\begin{align*} \webleft\{ \text{relations from $A$ to $B$}\webright\} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\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{PosFun}^{\style {display: inline-block; transform: rotate(180deg)}{\mathcal{C}}\mkern -2.5mu}\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 )$, where $\mathcal{P}\webleft (A\webright )$ and $\mathcal{P}\webleft (B\webright )$ are endowed with the poset structure given by inclusion.

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, and of .
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 2: Constructions With Sets, and of .
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 2: Constructions With Sets, and of .
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, of .

In particular, the bijection

\[ \mathsf{Sets}\webleft (A,\mathcal{P}\webleft (B\webright )\webright )\cong \textup{Hom}^{\mathrm{cocont}}_{\mathsf{Pos}}\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 )$ 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.6.1.1.1.

This finishes the proof.

¹Note that by Chapter 2: Constructions With Sets, Remark 2.6.1.1.3, we have $\text{Lan}_{\chi }\webleft (f\webright )=f_{*}$, the direct image of $f$.