7.3.2 The Inverse of a Function
Let $f\colon A\to B$ be a function.
The inverse of $f$ is the relation $f^{-1}\colon B\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}A$ defined as follows:
- Viewing relations from $B$ to $A$ as subsets of $B\times A$, we define
\[ f^{-1}\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ \webleft (b,f^{-1}\webleft (b\webright )\webright )\in B\times A\ \middle |\ a\in A\webright\} , \]
where
\[ f^{-1}\webleft (b\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ a\in A\ \middle |\ f\webleft (a\webright )=b\webright\} \]
for each $b\in B$.
- Viewing relations from $B$ to $A$ as functions $B\times A\to \{ \mathsf{true},\mathsf{false}\} $, we define
\[ f^{-1}\webleft (b,a\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} \mathsf{true}& \text{if there exists $a\in A$ with $f\webleft (a\webright )=b$,}\\ \mathsf{false}& \text{otherwise} \end{cases} \]
for each $\webleft (b,a\webright )\in B\times A$;
- Viewing relations from $B$ to $A$ as functions $B\to \mathcal{P}\webleft (A\webright )$, we define
\[ f^{-1}\webleft (b\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ a\in A\ \middle |\ f\webleft (a\webright )=b\webright\} \]
for each $b\in B$.
Let $f\colon A\to B$ be a function.
-
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 \text{Obj}\webleft (\mathsf{Sets}\webright )$, we have
\[ \webleft[\webleft (-\webright )^{-1}\webright]\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
\[ \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}}}=}}\webleft[\webleft (-\webright )^{-1}\webright]\webleft (f\webright ), \]
where $f^{-1}$ is the inverse of $f$ as in Definition 7.3.2.1.1.
In particular: - Preservation of Identities. We have
\[ \text{id}^{-1}_{A}=\chi _{A} \]
for each $A\in \text{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$.
-
Adjointness Inside $\textbf{Rel}$. We have an adjunction in $\textbf{Rel}$.
-
Interaction With Inverses of Relations. We have
\begin{align*} \webleft (f^{-1}\webright )^{\dagger } & = \text{Gr}\webleft (f\webright ),\\ \text{Gr}\webleft (f\webright )^{\dagger } & = f^{-1}. \end{align*}
Clear.
Item 2: Adjointness Inside $\textbf{Rel}$
This is proved in Item 2 of Proposition 7.3.1.1.2.
Item 3: Interaction With Inverses of Relations
Clear.
