The Clowder Project

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

1. 1.

   Functoriality. The assignment $A\mapsto A$, $f\mapsto f^{-1}$ defines a functor

   \[ \webleft (-\webright )^{-1}\colon \mathsf{Sets}\to \mathrm{Rel} \]

   where

   • •

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

     \[ \left[\webleft (-\webright )^{-1}\right]\webleft (A\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}A. \]
   • •

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

     \[ \webleft (-\webright )^{-1}_{A,B}\colon \mathsf{Sets}\webleft (A,B\webright ) \to \mathrm{Rel}\webleft (A,B\webright ) \]

     of $\webleft (-\webright )^{-1}$ at $\webleft (A,B\webright )$ is defined by

     \[ \webleft (-\webright )^{-1}_{A,B}\webleft (f\webright ) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left[\webleft (-\webright )^{-1}\right]\webleft (f\webright ), \]

     where $f^{-1}$ is the inverse of $f$ as in Definition 8.2.3.1.1.

   In particular:

   • •

     Preservation of Identities. We have

     \[ \operatorname {\mathrm{id}}^{-1}_{A}=\chi _{A} \]

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

   • •

     Preservation of Composition. We have

     \[ \webleft (g\circ f\webright )^{-1}=g^{-1}\mathbin {\diamond }f^{-1} \]

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

2. 2.

   Adjointness Inside $\boldsymbol {\mathsf{Rel}}$. We have an adjunction

   
   in $\boldsymbol {\mathsf{Rel}}$.

3. 3.

   Interaction With Converses of Relations. We have

   \begin{align*} \webleft (f^{-1}\webright )^{\dagger } & = \operatorname {\mathrm{Gr}}\webleft (f\webright ),\\ \operatorname {\mathrm{Gr}}\webleft (f\webright )^{\dagger } & = f^{-1}. \end{align*}