The Clowder Project

We proceed step by step:

1. 1.

   From Adjunctions in $\boldsymbol {\mathsf{Rel}}$ to Functions. An adjunction in $\boldsymbol {\mathsf{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*} \Delta _{A} & \subset S\mathbin {\diamond }R,\\ R\mathbin {\diamond }S & \subset \Delta _{B}. \end{align*}

   By Lemma 8.5.2.1.1, $R$ is total and functional. In particular, $R(a)$ is a singleton for all $a\in A$. Defining $f_{R}$ such that $f_{R}(a)$ is the unique element of $R(a)$ then gives us our desired function, forming a map

   \[ \left\{ \begin{gathered} \text{Adjunctions in $\boldsymbol {\mathsf{Rel}}$}\\ \text{from $A$ to $B$} \end{gathered} \right\} \to \left\{ \begin{gathered} \text{Functions}\\ \text{from $A$ to $B$} \end{gathered} \right\} . \]

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

2. 2.

   From Functions to Adjunctions in $\boldsymbol {\mathsf{Rel}}$. By Item 4 of Proposition 8.2.2.1.2, every function $f\colon A\to B$ gives rise to an adjunction $\operatorname {\mathrm{Gr}}(f)\dashv f^{-1}$ in $\mathrm{Rel}$, giving a map

   \[ \left\{ \begin{gathered} \text{Functions}\\ \text{from $A$ to $B$} \end{gathered} \right\} \to \left\{ \begin{gathered} \text{Adjunctions in $\boldsymbol {\mathsf{Rel}}$}\\ \text{from $A$ to $B$} \end{gathered} \right\} . \]
3. 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 $\operatorname {\mathrm{Gr}}(f)\dashv f^{-1}$, and then passing again to a function gives $f$ again. This follows form the fact that we have $a\sim _{\operatorname {\mathrm{Gr}}(f)}b$ iff $f(a)=b$.

4. 4.

   Invertibility: From Adjunctions to Functions Back to Adjunctions. We need to show that, given an adjunction $R\dashv S$ in $\boldsymbol {\mathsf{Rel}}$ giving rise to a function $f_{R,S}\colon A\to B$, we have

   \begin{align*} \operatorname {\mathrm{Gr}}(f_{R,S}) & = R,\\ f^{-1}_{R,S} & = S. \end{align*}

   We check these explicitly:

   • •

     $\operatorname {\mathrm{Gr}}(f_{R,S})=R$. We have

     \begin{align*} \operatorname {\mathrm{Gr}}(f_{R,S}) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (a,f_{R,S}(a))\in A\times B\ \middle |\ a\in A\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (a,R(a))\in A\times B\ \middle |\ a\in A\right\} \\ & = 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$: We proceed in a few steps.

       • •

         Since $\Delta _{A}\subset S\mathbin {\diamond }R$, there exists $k\in B$ such that $a\sim _{R}k$ and $k\sim _{S}a$.

       • •

         Since $a\sim _{R}b$ and $R$ is functional, we have $k=b$.

       • •

         Thus $b\sim _{S}a$.

     • •

       If $b\sim _{S}a$, then $a\sim _{R}b$: We proceed in a few steps.

       • •

         First note that, since $R$ is total, we have $a\sim _{R}b'$ for some $b'\in B$.

       • •

         Since $R\mathbin {\diamond }S\subset \Delta _{B}$, $b\sim _{S}a$, and $a\sim _{R}b'$, we have $b=b'$.

       • •

         Thus $a\sim _{R}b$.

     Having show this, we now have

     \begin{align*} f^{-1}_{R,S}(b) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ a\in A\ \middle |\ f_{R,S}(a)=b\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ a\in A\ \middle |\ a\sim _{R}b\right\} \\ & = \left\{ a\in A\ \middle |\ b\sim _{S}a\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}S(b). \end{align*}

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

This finishes the proof.