Proposition 7.4.4.1.4 (00T7): Properties of the Direct Image With Compact Support 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_{!}$ defines a function
\[ \webleft (-\webright )_{!}\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_{!}$ defines a function
\[ \webleft (-\webright )_{!}\colon \mathsf{Sets}\webleft (A,B\webright ) \to \textup{Hom}_{\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 )_{!}=\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 )_{!}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ a\in A\ \middle |\ \chi ^{-1}_{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 )_{!}=\text{id}_{\mathcal{P}\webleft (A\webright )}$.

Item 4: Interaction With Composition

Indeed, we have

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

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

We have $S^{-1}\webleft (R^{-1}\webleft (c\webright )\webright )\subset U$;
We have $R^{-1}\webleft (c\webright )\subset S_{!}\webleft (U\webright )$;

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