Let $f\colon A\to B$ be a function.

  1. Functoriality. The assignment $A\mapsto \text{Gr}\webleft (A\webright )$ defines a functor
    \[ \text{Gr}\colon \mathsf{Sets}\to \mathrm{Rel} \]

    where

    • Action on Objects. For each $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, we have

      \[ \text{Gr}\webleft (A\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}A. \]

    • Action on Morphisms. For each $A,B\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, the action on $\textup{Hom}$-sets

      \[ \text{Gr}_{A,B}\colon \mathsf{Sets}\webleft (A,B\webright ) \to \underbrace{\mathrm{Rel}\webleft (\text{Gr}\webleft (A\webright ),\text{Gr}\webleft (B\webright )\webright )}_{\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathrm{Rel}\webleft (A,B\webright )} \]

      of $\text{Gr}$ at $\webleft (A,B\webright )$ is defined by

      \[ \text{Gr}_{A,B}\webleft (f\webright ) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\text{Gr}\webleft (f\webright ), \]

      where $\text{Gr}\webleft (f\webright )$ is the graph of $f$ as in Definition 6.3.1.1.1.

    In particular:
    • Preservation of Identities. We have

      \[ \text{Gr}\webleft (\text{id}_{A}\webright )=\chi _{A} \]

      for each $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.

    • Preservation of Composition. We have

      \[ \text{Gr}\webleft (g\circ f\webright )=\text{Gr}\webleft (g\webright )\mathbin {\diamond }\text{Gr}\webleft (f\webright ) \]

      for each pair of functions $f\colon A\to B$ and $g\colon B\to C$.

  2. Adjointness Inside $\textbf{Rel}$. We have an adjunction
    in $\textbf{Rel}$, where $f^{-1}$ is the inverse of $f$ of Definition 6.3.2.1.1.
  3. Adjointness. We have an adjunction
    witnessed by a bijection of sets
    \[ \mathrm{Rel}\webleft (\text{Gr}\webleft (A\webright ),B\webright ) \cong \mathsf{Sets}\webleft (A,\mathcal{P}\webleft (B\webright )\webright ) \]

    natural in $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ and $B\in \text{Obj}\webleft (\mathrm{Rel}\webright )$.

  4. Interaction With Inverses. We have
    \begin{align*} \text{Gr}\webleft (f\webright )^{\dagger } & = f^{-1},\\ \webleft (f^{-1}\webright )^{\dagger } & = \text{Gr}\webleft (f\webright ). \end{align*}
  5. Cocontinuity. The functor $\text{Gr}\colon \mathsf{Sets}\to \mathrm{Rel}$ of Item 1 preserves colimits.
  6. Characterisations. Let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation. The following conditions are equivalent:
    1. There exists a function $f\colon A\to B$ such that $R=\text{Gr}\webleft (f\webright )$.
    2. The relation $R$ is total and functional.
    3. The weak and strong inverse images of $R$ agree, i.e. we have $R^{-1}=R_{-1}$.
    4. The relation $R$ has a right adjoint $R^{\dagger }$ in $\mathrm{Rel}$.

Item 1: Functoriality
Clear.
Item 2: Adjointness Inside $\textbf{Rel}$
We need to check that there are inclusions

\begin{align*} \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{align*}

These correspond respectively to the following conditions:

  1. For each $a\in A$, there exists some $b\in B$ such that $a\sim _{\text{Gr}\webleft (f\webright )}b$ and $b\sim _{f^{-1}}a$.
  2. For each $a,b\in A$, if $a\sim _{\text{Gr}\webleft (f\webright )}b$ and $b\sim _{f^{-1}}a$, then $a=b$.
In other words, the first condition states that the image of any $a\in A$ by $f$ is nonempty, whereas the second condition states that $f$ is not multivalued. As $f$ is a function, both of these statements are true, and we are done.
Item 3: Adjointness
The stated bijection follows from Chapter 5: Relations, Remark 5.1.1.1.4, with naturality being clear.
Item 4: Interaction With Inverses
Clear.
Item 5: Cocontinuity
Omitted.
Item 6: Characterisations
We claim that Item (a), Item (b), Item (c), and Item (d) are indeed equivalent:
  • Item (a)$\iff $Item (b). This is shown in the proof of of .
  • Item (b)$\implies $Item (c). If $R$ is total and functional, then, for each $a\in A$, the set $R\webleft (a\webright )$ is a singleton, implying that

    \begin{align*} R^{-1}\webleft (V\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ a\in A \ \middle |\ R\webleft (a\webright )\cap V\neq \emptyset \webright\} ,\\ R_{-1}\webleft (V\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ a\in A\ \middle |\ R\webleft (a\webright )\subset V\webright\} \end{align*}

    are equal for all $V\in \mathcal{P}\webleft (B\webright )$, as the conditions $R\webleft (a\webright )\cap V\neq \emptyset $ and $R\webleft (a\webright )\subset V$ are equivalent when $R\webleft (a\webright )$ is a singleton.

  • Item (c)$\implies $Item (b). We claim that $R$ is indeed total and functional:
    • Totality. If we had $R\webleft (a\webright )=\emptyset $ for some $a\in A$, then we would have $a\in R_{-1}\webleft (\emptyset \webright )$, so that $R_{-1}\webleft (\emptyset \webright )\neq \emptyset $. But since $R^{-1}\webleft (\emptyset \webright )=\emptyset $, this would imply $R_{-1}\webleft (\emptyset \webright )\neq R^{-1}\webleft (\emptyset \webright )$, a contradiction. Thus $R\webleft (a\webright )\neq \emptyset $ for all $a\in A$ and $R$ is total.
    • Functionality. If $R^{-1}=R_{-1}$, then we have

      \begin{align*} \webleft\{ a\webright\} & = R^{-1}\webleft (\webleft\{ b\webright\} \webright )\\ & = R_{-1}\webleft (\webleft\{ b\webright\} \webright ) \end{align*}

      for each $b\in R\webleft (a\webright )$ and each $a\in A$, and thus $R\webleft (a\webright )\subset \webleft\{ b\webright\} $. But since $R$ is total, we must have $R\webleft (a\webright )=\webleft\{ b\webright\} $, and thus we see that $R$ is functional.

  • Item (a)$\iff $Item (d). This follows from Chapter 5: Relations, Proposition 5.3.3.1.1.
This finishes the proof.


Noticed something off, or have any comments? Feel free to reach out!


You can also use the contact form below: