Item 3 (02GM) — The Clowder Project

Let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation from $A$ to $B$, and recall that $R^{\textsf{c}}\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}B\times A\setminus R$.

The conditions below are row-wise equivalent:

Condition	Inclusion
$R^{\textsf{c}}$ is functional	$\nabla _{B} \subset R\mathbin {\square }R^{\dagger }$
$R^{\textsf{c}}$ is total	$R\mathbin {\square }R^{\dagger }\subset \nabla _{A}$
$R^{\textsf{c}}$ is injective	$\nabla _{A} \subset R^{\dagger }\mathbin {\square }R$
$R^{\textsf{c}}$ is surjective	$R^{\dagger }\mathbin {\square }R\subset \nabla _{B}$

This follows from Lemma 8.5.2.1.1 and Item 4 of Proposition 8.1.4.1.3. For instance:

•
Suppose we have $R\mathbin {\square }R^{\dagger }\subset \nabla _{B}$.
•
Taking complements, we obtain $\nabla ^{\textsf{c}}_{B}\subset (R\mathbin {\square }R^{\dagger })^{\textsf{c}}$.
•
Applying Item 4 of Proposition 8.1.4.1.3, this becomes $\Delta _{B}\subset R^{\textsf{c}}\mathbin {\diamond }(R^{\dagger })^{\textsf{c}}$.
•
Then, by Lemma 8.5.2.1.1, this is equivalent to $R^{\textsf{c}}$ being total.

The proof of the other equivalences is similar, and thus omitted.

The statements in Lemma 8.6.2.1.1 unwind to the following:

Inclusion	Quantifier	Condition
$\nabla _{B} \subset R\mathbin {\square }R^{\dagger }$	For each $b_{1},b_{2}\in B$	If $b_{1}\neq b_{2}$, then, for each $a\in A$, we have $a\sim _{R}b_{1}$ or $a\sim _{R}b_{2}$.
$R\mathbin {\square }R^{\dagger }\subset \nabla _{B}$	For each $b_{1},b_{2}\in B$	If, for each $a\in A$, $a\sim _{R}b_{1}$ or $a\sim _{R}b_{2}$, then $b_{1}\neq b_{2}$.
$\nabla _{A} \subset R^{\dagger }\mathbin {\square }R$	For each $a_{1},a_{2}\in A$	If $a_{1}\neq a_{2}$, then, for each $b\in B$, we have $a_{1}\sim _{R}b$ or $a_{2}\sim _{R}b$.
$R^{\dagger }\mathbin {\square }R\subset \nabla _{A}$	For each $a_{1},a_{2}\in A$	If, for each $b\in B$, $a_{1}\sim _{R}b$ or $a_{2}\sim _{R}b$, then $a_{1}\neq a_{2}$.

Equivalently:

Inclusion	Quantifier	If	Then
$\nabla _{B} \subset R\mathbin {\square }R^{\dagger }$	For each $b_{1},b_{2}\in B$	$b_{1}\neq b_{2}$	$R^{-1}(b_{1})\cup R^{-1}(b_{2})=A$
$R\mathbin {\square }R^{\dagger }\subset \nabla _{B}$	For each $b_{1},b_{2}\in B$	$R^{-1}(b_{1})\cup R^{-1}(b_{2})=A$	$b_{1}\neq b_{2}$
$\nabla _{A} \subset R^{\dagger }\mathbin {\square }R$	For each $a_{1},a_{2}\in A$	$a_{1}\neq a_{2}$	$R(a_{1})\cup R(a_{2})=B$
$R^{\dagger }\mathbin {\square }R\subset \nabla _{A}$	For each $a_{1},a_{2}\in A$	$R(a_{1})\cup R(a_{2})=B$	$a_{1}\neq a_{2}$

The following conditions are equivalent:

1.
The relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ is an equivalence in $\boldsymbol {\mathsf{Rel}}^{\mathord {\mathbin {\square }}}$, i.e.:
- (★)
2.
The relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ is an isomorphism in $\mathrm{Rel}$, i.e.:
- (★)

8.6.2 Isomorphisms and Equivalences