Proposition 6.3.2.1.1 (00L1): Isomorphisms and Equivalences in $\textbf{Rel}$

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`

The following conditions are equivalent:

The relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ is an equivalence in $\textbf{Rel}$, i.e.:
- There exists a relation $R^{-1}\colon B\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}A$ from $B$ to $A$ together with isomorphisms
  \begin{align*} R^{-1}\mathbin {\diamond }R & \cong \chi _{A},\\ R\mathbin {\diamond }R^{-1} & \cong \chi _{B}. \end{align*}
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 relation $R^{-1}\colon B\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}A$ from $B$ to $A$ such that we have
  \begin{align*} R^{-1}\mathbin {\diamond }R & = \chi _{A},\\ R\mathbin {\diamond }R^{-1} & = \chi _{B}. \end{align*}
There exists a bijection $f\colon A\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }B$ with $R=\text{Gr}\webleft (f\webright )$.

We claim that Item 1, Item 2, and Item 3 are indeed equivalent:

Item 1$\iff $Item 2: This follows from the fact that $\textbf{Rel}$ is locally posetal, so that natural isomorphisms and equalities of $1$-morphisms in $\textbf{Rel}$ coincide.
Item 2$\implies $Item 3: The equalities in Item 2 imply $R\dashv R^{-1}$, and thus by Proposition 6.3.3.1.1, there exists a function $f_{R}\colon A\to B$ associated to $R$, where, for each $a\in A$, the image $f_{R}\webleft (a\webright )$ of $a$ by $f_{R}$ is the unique element of $R\webleft (a\webright )$, which implies $R=\text{Gr}\webleft (f_{R}\webright )$ in particular. Furthermore, we have $R^{-1}=f^{-1}_{R}$ (as in Chapter 7: Constructions With Relations, Definition 7.3.2.1.1). The conditions from Item 2 then become the following:

\begin{align*} f^{-1}_{R}\mathbin {\diamond }f_{R} = \chi _{A},\\ f_{R}\mathbin {\diamond }f^{-1}_{R} = \chi _{B}. \end{align*}

All that is left is to show then is that $f_{R}$ is a bijection:
- The Function $f_{R}$ Is Injective. Let $a,b\in A$ and suppose that $f_{R}\webleft (a\webright )=f_{R}\webleft (b\webright )$. Since $a\sim _{R}f_{R}\webleft (a\webright )$ and $f_{R}\webleft (a\webright )=f_{R}\webleft (b\webright )\sim _{R^{-1}}b$, the condition $f^{-1}_{R}\mathbin {\diamond }f_{R}=\chi _{A}$ implies that $a=b$, showing $f_{R}$ to be injective.
- The Function $f_{R}$ Is Surjective. Let $b\in B$. Applying the condition $f_{R}\mathbin {\diamond }f^{-1}_{R}=\chi _{B}$ to $\webleft (b,b\webright )$, it follows that there exists some $a\in A$ such that $f^{-1}_{R}\webleft (b\webright )=a$ and $f_{R}\webleft (a\webright )=b$. This shows $f_{R}$ to be surjective.
Item 3$\implies $Item 2: By Chapter 7: Constructions With Relations, Item 2 of Proposition 7.3.1.1.2, we have an adjunction $\text{Gr}\webleft (f\webright )\dashv f^{-1}$, giving inclusions

\begin{gather*} \chi _{A} \subset f^{-1}\mathbin {\diamond }\text{Gr}\webleft (f\webright ),\\ \text{Gr}\webleft (f\webright )\mathbin {\diamond }f^{-1} \subset \chi _{B}. \end{gather*}

We claim the reverse inclusions are also true:
- $f^{-1}\mathbin {\diamond }\text{Gr}\webleft (f\webright )\subset \chi _{A}$: This is equivalent to the statement that if $f\webleft (a\webright )=b$ and $f^{-1}\webleft (b\webright )=a'$, then $a=a'$, which follows from the injectivity of $f$.
- $\chi _{B}\subset \text{Gr}\webleft (f\webright )\mathbin {\diamond }f^{-1}$: This is equivalent to the statement that given $b\in B$ there exists some $a\in A$ such that $f^{-1}\webleft (b\webright )=a$ and $f\webleft (a\webright )=b$, which follows from the surjectivity of $f$.

This finishes the proof.