Proposition 7.4.2.1.4 (00S5): Properties of the Strong Inverse Image Function Operation

Style	Class	Font	Theorem Environments
Style 1	`book`	Alegreya Sans	`tcbthm`
Style 2	`book`	Alegreya Sans	`amsthm`
Style 3	`book`	Arno*	`amsthm`
Style 4	`book`	Computer Modern	`amsthm`

Let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation.

Functionality I. The assignment $R\mapsto R_{-1}$ defines a function
\[ \webleft (-\webright )_{-1}\colon \mathsf{Sets}\webleft (A,B\webright ) \to \mathsf{Sets}\webleft (\mathcal{P}\webleft (A\webright ),\mathcal{P}\webleft (B\webright )\webright ). \]
Functionality II. The assignment $R\mapsto R_{-1}$ defines a function
\[ \webleft (-\webright )_{-1}\colon \mathsf{Sets}\webleft (A,B\webright ) \to \mathsf{Pos}\webleft (\webleft (\mathcal{P}\webleft (A\webright ),\subset \webright ),\webleft (\mathcal{P}\webleft (B\webright ),\subset \webright )\webright ). \]
Interaction With Identities. For each $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, we have
\[ \webleft (\text{id}_{A}\webright )_{-1}=\text{id}_{\mathcal{P}\webleft (A\webright )}; \]
Interaction With Composition. For each pair of composable relations $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ and $S\colon B\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}C$, we have

Item 1: Functionality I

Clear.

Item 2: Functionality II

Clear.

Item 3: Interaction With Identities

Indeed, we have

\begin{align*} \webleft (\chi _{A}\webright )_{-1}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ a\in A\ \middle |\ \chi _{A}\webleft (a\webright )\subset U\webright\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ a\in A\ \middle |\ \webleft\{ a\webright\} \subset U\webright\} \\ & = U \end{align*}

for each $U\in \mathcal{P}\webleft (A\webright )$. Thus $\webleft (\chi _{A}\webright )_{-1}=\text{id}_{\mathcal{P}\webleft (A\webright )}$.

Item 4: Interaction With Composition

Indeed, we have

\begin{align*} \webleft (S\mathbin {\diamond }R\webright )_{-1}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ a\in A\ \middle |\ \webleft [S\mathbin {\diamond }R\webright ]\webleft (a\webright )\subset U\webright\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ a\in A\ \middle |\ S\webleft (R\webleft (a\webright )\webright )\subset U\webright\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ a\in A\ \middle |\ S_{*}\webleft (R\webleft (a\webright )\webright )\subset U\webright\} \\ & = \webleft\{ a\in A\ \middle |\ R\webleft (a\webright )\subset S_{-1}\webleft (U\webright )\webright\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}R_{-1}\webleft (S_{-1}\webleft (U\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [R_{-1}\circ S_{-1}\webright ]\webleft (U\webright ) \end{align*}

for each $U\in \mathcal{P}\webleft (C\webright )$, where we used Item 2 of Proposition 7.4.2.1.3, which implies that the conditions

We have $S_{*}\webleft (R\webleft (a\webright )\webright )\subset U$;
We have $R\webleft (a\webright )\subset S_{-1}\webleft (U\webright )$;

are equivalent. Thus $\webleft (S\mathbin {\diamond }R\webright )_{-1}=R_{-1}\circ S_{-1}$.