The Clowder Project

We proceed step by step:

1. From Adjunctions in $\textbf{Rel}$ to Functions. An adjunction in $\textbf{Rel}$ from $A$ to $B$ consists of a pair of relations
   \begin{align*} R & \colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B,\\ S & \colon B\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}A, \end{align*}

   together with inclusions

   \begin{align*} \chi _{A} & \subset S\mathbin {\diamond }R,\\ R\mathbin {\diamond }S & \subset \chi _{B}. \end{align*}

   We claim that these conditions imply that $R$ is total and functional, i.e. that $R\webleft (a\webright )$ is a singleton for each $a\in A$:

   1. $R\webleft (a\webright )$ Has an Element. Given $a\in A$, since $\chi _{A}\subset S\mathbin {\diamond }R$, we must have $\webleft\{ a\webright\} \subset S\webleft (R\webleft (a\webright )\webright )$, implying that there exists some $b\in B$ such that $a\sim _{R}b$ and $b\sim _{S}a$, and thus $R\webleft (a\webright )\neq \text{Ø}$, as $b\in R\webleft (a\webright )$.
   2. $R\webleft (a\webright )$ Has No More Than One Element. 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 $\chi _{A}\subset S\mathbin {\diamond }R$, there exists some $k\in B$ such that $a\sim _{R}k$ and $k\sim _{S}a$.
      2. Since $R\mathbin {\diamond }S\subset \chi _{B}$, if $b''\sim _{S}a'$ and $a'\sim _{R}b'''$, then $b''=b'''$.
      3. Applying the above to $b''=k$, $b'''=b$, and $a'=a$, since $k\sim _{S}a$ and $a\sim _{R}b'$, we have $k=b$.
      4. Similarly $k=b'$.
      5. Thus $b=b'$.
   Together, the above two items show $R\webleft (a\webright )$ to be a singleton, being thus given by $\text{Gr}\webleft (f\webright )$ for some function $f\colon A\to B$, which gives a map
   \[ \webleft\{ \begin{gathered} \text{Adjunctions in $\textbf{Rel}$}\\ \text{from $A$ to $B$} \end{gathered} \webright\} \to \webleft\{ \begin{gathered} \text{Functions}\\ \text{from $A$ to $B$} \end{gathered} \webright\} . \]

   Moreover, by uniqueness of adjoints (, of ), this implies also that $S=f^{-1}$.

2. From Functions to Adjunctions in $\textbf{Rel}$. By Chapter 7: Constructions With Relations, Item 2 of Proposition 7.3.1.1.2, every function $f\colon A\to B$ gives rise to an adjunction $\text{Gr}\webleft (f\webright )\dashv f^{-1}$ in $\mathrm{Rel}$, giving a map
   \[ \webleft\{ \begin{gathered} \text{Functions}\\ \text{from $A$ to $B$} \end{gathered} \webright\} \to \webleft\{ \begin{gathered} \text{Adjunctions in $\textbf{Rel}$}\\ \text{from $A$ to $B$} \end{gathered} \webright\} . \]

3. Invertibility: From Functions to Adjunctions Back to Functions. We need to show that starting with a function $f\colon A\to B$, passing to $\text{Gr}\webleft (f\webright )\dashv f^{-1}$, and then passing again to a function gives $f$ again. This is clear however, since we have $a\sim _{\text{Gr}\webleft (f\webright )}b$ iff $f\webleft (a\webright )=b$.
4. Invertibility: From Adjunctions to Functions Back to Adjunctions. We need to show that, given an adjunction $R\dashv S$ in $\textbf{Rel}$ giving rise to a function $f_{R,S}\colon A\to B$, we have
   \begin{align*} \text{Gr}\webleft (f_{R,S}\webright ) & = R,\\ f^{-1}_{R,S} & = S. \end{align*}

   We check these explicitly:

   • $\text{Gr}\webleft (f_{R,S}\webright )=R$. We have
     \begin{align*} \text{Gr}\webleft (f_{R,S}\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ \webleft (a,f_{R,S}\webleft (a\webright )\webright )\in A\times B\ \middle |\ a\in A\webright\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ \webleft (a,R\webleft (a\webright )\webright )\in A\times B\ \middle |\ a\in A\webright\} \\ & = R. \end{align*}

   • $f^{-1}_{R,S}=S$. We first claim that, given $a\in A$ and $b\in B$, the following conditions are equivalent:
     • We have $a\sim _{R}b$.
     • We have $b\sim _{S}a$.
     Indeed:
     • If $a\sim _{R}b$, then $b\sim _{S}a$: Since $\chi _{A}\subset S\mathbin {\diamond }R$, there exists $k\in B$ such that $a\sim _{R}k$ and $k\sim _{S}a$, but since $a\sim _{R}b$ and $R$ is functional, we have $k=b$ and thus $b\sim _{S}a$.
     • If $b\sim _{S}a$, then $a\sim _{R}b$: First note that since $R$ is total we have $a\sim _{R}b'$ for some $b'\in B$. Now, since $R\mathbin {\diamond }S\subset \chi _{B}$, $b\sim _{S}a$, and $a\sim _{R}b'$, we have $b=b'$, and thus $a\sim _{R}b$.
     Having show this, we now have
     \begin{align*} f^{-1}_{R,S}\webleft (b\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ a\in A\ \middle |\ f_{R,S}\webleft (a\webright )=b\webright\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ a\in A\ \middle |\ a\sim _{R}b\webright\} \\ & = \webleft\{ a\in A\ \middle |\ b\sim _{S}a\webright\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}S\webleft (b\webright ). \end{align*}

     for each $b\in B$, showing $f^{-1}_{R,S}=S$.