Subsection 6.1.4 (00JC): Functional 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 $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ is functional if, for each $a\in A$, the set $R\webleft (a\webright )$ is either empty or a singleton.

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

Characterisations. The following conditions are equivalent:
1. The relation $R$ is functional.
2. We have $R\mathbin {\diamond }R^{\dagger }\subset \chi _{B}$.

Item 1: Characterisations

We claim that Item (a) and Item (b) are indeed equivalent:

Item (a)$\implies $Item (b): Let $\webleft (b,b'\webright )\in B\times B$. We need to show that
\[ \webleft [R\mathbin {\diamond }R^{\dagger }\webright ]\webleft (b,b'\webright )\preceq _{\{ \mathsf{t},\mathsf{f}\} }\chi _{B}\webleft (b,b'\webright ), \]

i.e. that if there exists some $a\in A$ such that $b\sim _{R^{\dagger }}a$ and $a\sim _{R}b'$, then $b=b'$. But since $b\sim _{R^{\dagger }}a$ is the same as $a\sim _{R}b$, we have both $a\sim _{R}b$ and $a\sim _{R}b'$ at the same time, which implies $b=b'$ since $R$ is functional.
Item (b)$\implies $Item (a): Suppose that we have $a\sim _{R}b$ and $a\sim _{R}b'$ for $b,b'\in B$. We claim that $b=b'$:
1. Since $a\sim _{R}b$, we have $b\sim _{R^{\dagger }}a$.
2. Since $R\mathbin {\diamond }R^{\dagger }\subset \chi _{B}$, we have
  
  \[ \webleft [R\mathbin {\diamond }R^{\dagger }\webright ]\webleft (b,b'\webright )\preceq _{\{ \mathsf{t},\mathsf{f}\} }\chi _{B}\webleft (b,b'\webright ), \]
  
  and since $b\sim _{R^{\dagger }}a$ and $a\sim _{R}b'$, it follows that $\webleft [R\mathbin {\diamond }R^{\dagger }\webright ]\webleft (b,b'\webright )=\mathsf{true}$, and thus $\chi _{B}\webleft (b,b'\webright )=\mathsf{true}$ as well, i.e. $b=b'$.

This finishes the proof.

The Clowder Project

6.1.4 Functional Relations