Let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation from $A$ to $B$.
The conditions below are row-wise equivalent:
|
Condition |
Inclusion |
|
$R$ is functional |
$R\mathbin {\diamond }R^{\dagger }\subset \Delta _{B}$ |
|
$R$ is total |
$\Delta _{A} \subset R^{\dagger }\mathbin {\diamond }R$ |
|
$R$ is injective |
$R^{\dagger }\mathbin {\diamond }R\subset \Delta _{A}$ |
|
$R$ is surjective |
$\Delta _{B} \subset R\mathbin {\diamond }R^{\dagger }$ |
Since $b\sim _{R^{\dagger }}a$ is the same as $a\sim _{R}b$, the condition says that $a\sim _{R}b$ and $a\sim _{R}b'$ imply $b=b'$. This is precisely the condition for $R$ to be functional.
Since $b\sim _{R^{\dagger }}a'$ is the same as $a'\sim _{R}b$, the condition says that for each $a\in A$, there is some $b\in B$ with $b\in R(a)$, so $R(a)\neq \text{Ø}$. This is precisely the condition for $R$ to be total.
Since $b\sim _{R^{\dagger }}a'$ is the same as $a'\sim _{R}b$, the condition says that for each $b\in B$, if $a\sim _{R}b$ and $a'\sim _{R}b$, then $a=a'$. This is precisely the condition for $R$ to be injective.
Since $b\sim _{R^{\dagger }}a$ is the same as $a\sim _{R}b$, the condition says that for each $b\in B$, there is some $a\in A$ with $b\in R(a)$, so $R^{-1}(b)\neq \text{Ø}$. This is precisely the condition for $R$ to be surjective.
The following conditions are equivalent:
The relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ is an equivalence in $\boldsymbol {\mathsf{Rel}}$, i.e.:
The relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ is an isomorphism in $\mathrm{Rel}$, i.e.:
There exists a bijection $f\colon A\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }B$ with $R=\operatorname {\mathrm{Gr}}(f)$.
We claim that Item 1, Item 2, and Item 3 are indeed equivalent:
Item 1$\iff $Item 2: This follows from the fact that $\boldsymbol {\mathsf{Rel}}$ is locally posetal, so that natural isomorphisms and equalities of $1$-morphisms in $\boldsymbol {\mathsf{Rel}}$ coincide.
Item 2$\implies $Item 3: We proceed in a few steps:
First, note that the equalities in Item 2 imply $R\dashv R^{-1}$ and thus, by Proposition 8.5.3.1.1, there exists a function $f_{R}\colon A\to B$ associated to $R$.
By Lemma 8.5.2.1.1, $f_{R}$ is a bijection.
Item 3$\implies $Item 2: By Item 4 of Proposition 8.2.2.1.2, we have an adjunction $\operatorname {\mathrm{Gr}}(f)\dashv f^{-1}$, giving inclusions
If $f$ is bijective, then the reverse inclusions are also true by Lemma 8.5.2.1.1.
This finishes the proof.
