Let $f\colon A\to B$ be a function.
-
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 7.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$.
-
Adjointness Inside $\textbf{Rel}$. We have an adjunction in $\textbf{Rel}$, where $f^{-1}$ is the inverse of $f$ of Definition 7.3.2.1.1.
-
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 )$.
-
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*}
-
Cocontinuity. The functor $\text{Gr}\colon \mathsf{Sets}\to \mathrm{Rel}$ of Item 1 preserves colimits.
-
Characterisations. Let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation. The following conditions are equivalent:
-
There exists a function $f\colon A\to B$ such that $R=\text{Gr}\webleft (f\webright )$.
-
The relation $R$ is total and functional.
-
The weak and strong inverse images of $R$ agree, i.e. we have $R^{-1}=R_{-1}$.
-
The relation $R$ has a right adjoint $R^{\dagger }$ in $\mathrm{Rel}$.