Subsection 5.1.1 (00HF): Foundations

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`

5.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$^[1]^[2] is a subset $R$ of $A\times B$.

Notation 5.1.1.1.2 ▶ Further Notation for Relations

Let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation.

Given elements $a\in A$ and $b\in B$ and a relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$, we write $a\sim _{R}b$ to mean $\webleft (a,b\webright )\in R$.
Viewing $R$ as a function
\[ R\colon A\times B\to \{ \mathsf{t},\mathsf{f}\} \]

via Remark 5.1.1.1.4, we write $R^{b}_{a}$ for the value of $R$ at $\webleft (a,b\webright )$.^[3]

Definition 5.1.1.1.3 ▶ The Po/Set of Relations Over Two Sets

Let $A$ and $B$ be sets.

The set of relations from $A$ to $B$ is the set $\mathrm{Rel}\webleft (A,B\webright )$ defined by
\[ \mathrm{Rel}\webleft (A,B\webright ) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ \text{Relations from $A$ to $B$}\webright\} . \]
The poset of relations from $A$ to $B$ is the poset
\[ \mathbf{Rel}\webleft (A,B\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\mathrm{Rel}\webleft (A,B\webright ),\subset \webright ) \]

consisting of:
- The Underlying Set. The set $\mathrm{Rel}\webleft (A,B\webright )$ of Item 1.
- The Partial Order. The partial order
  
  \[ \subset \colon \mathrm{Rel}\webleft (A,B\webright )\times \mathrm{Rel}\webleft (A,B\webright )\to \{ \mathsf{true},\mathsf{false}\} \]
  
  on $\mathrm{Rel}\webleft (A,B\webright )$ given by inclusion of relations.
The category of relations from $A$ to $B$ is the posetal category $\mathbf{Rel}\webleft (A,B\webright )$^[4] associated to the poset $\mathbf{Rel}\webleft (A,B\webright )$ of Item 2 via Chapter 8: Categories, Definition 8.1.3.1.1.

Remark 5.1.1.1.4 ▶ Equivalent Definitions of Relations

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

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 )$.

Proof of Remark 5.1.1.1.4.

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.

Proposition 5.1.1.1.5 ▶ Properties of Relations

Let $A$ and $B$ be sets and let $R,S\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be relations.

End Formula for the Set of Inclusions of Relations. We have
\[ \textup{Hom}_{\mathbf{Rel}\webleft (A,B\webright )}\webleft (R,S\webright )\cong \int _{a\in A}\int _{b\in B}\textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright ). \]

Proof of Proposition 5.1.1.1.5.

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}\textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright )\cong \begin{cases} \text{pt}& \text{if, for each $a\in A$ and each $b\in B$,}\\ & \text{we have $\textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright )\cong \text{pt}$}\\ \emptyset & \text{otherwise.}\end{cases} \]

Since we have $\textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright )=\webleft\{ \mathsf{true}\webright\} \cong \text{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}\textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright )\cong \begin{cases} \text{pt}& \text{if, for each $a\in A$ and each $b\in B$,}\\ & \text{if $a\sim _{R}b$, then $a\sim _{S}b$,}\\ \emptyset & \text{otherwise.}\end{cases} \]

On the left hand-side, we have

\[ \textup{Hom}_{\mathbf{Rel}\webleft (A,B\webright )}\webleft (R,S\webright )\cong \begin{cases} \text{pt}& \text{if $R\subset S$,}\\ \emptyset & \text{otherwise.}\end{cases} \]

It is then clear that the conditions for each set to evaluate to $\text{pt}$ (up to isomorphism) are equivalent, implying that those two sets are isomorphic.

Footnotes

[1] Further Terminology: Also called a multivalued function from $A$ to $B$, a relation over $A$ and $B$, relation on $A$ and $B$, a binary relation over $A$ and $B$, or a binary relation on $A$ and $B$.

[2] Further Terminology: When $A=B$, we also call $R\subset A\times A$ a relation on $A$.

[3] The choice $R^{b}_{a}$ in place of $R^{a}_{b}$ is to keep the notation consistent with the notation we will later employ for profunctors.

[4] Here we choose to slightly abuse notation by writing $\mathbf{Rel}\webleft (A,B\webright )$ (instead of e.g. $\mathbf{Rel}\webleft (A,B\webright )_{\mathsf{pos}}$) for the posetal category of relations from $A$ to $B$, even though the same notation is used for the poset of relations from $A$ to $B$.

[5] 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).

Noticed something off, or have any comments? Feel free to reach out!

You can also use the contact form below: