Subsection 6.4.1 (00R8): Direct Images

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`

6.4.1 Direct Images

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

The direct image function associated to $R$ is the function

\[ R_{*}\colon \mathcal{P}\webleft (A\webright )\to \mathcal{P}\webleft (B\webright ) \]

\begin{align*} R_{*}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}R\webleft (U\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{a\in U}R\webleft (a\webright )\\ & = \webleft\{ b\in B\ \middle |\ \begin{aligned} & \text{there exists some $a\in U$}\\ & \text{such that $b\in R\webleft (a\webright )$} \end{aligned} \webright\} \end{align*}

for each $U\in \mathcal{P}\webleft (A\webright )$.

Remark 6.4.1.1.2 ▶ Unwinding Definition 6.4.1.1.1

Identifying subsets of $A$ with relations from $\text{pt}$ to $A$ via Chapter 2: Constructions With Sets, Item 3 of Proposition 2.4.3.1.6, we see that the direct image function associated to $R$ is equivalently the function

\[ R_{*}\colon \underbrace{\mathcal{P}\webleft (A\webright )}_{\cong \mathrm{Rel}\webleft (\text{pt},A\webright )} \to \underbrace{\mathcal{P}\webleft (B\webright )}_{\cong \mathrm{Rel}\webleft (\text{pt},B\webright )} \]

defined by

\[ R_{*}\webleft (U\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}R\mathbin {\diamond }U \]

for each $U\in \mathcal{P}\webleft (A\webright )$, where $R\mathbin {\diamond }U$ is the composition

\[ \text{pt}\mathbin {\overset {U}{\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}}}A\mathbin {\overset {R}{\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}}}B. \]

Proposition 6.4.1.1.3 ▶ Properties of Direct Image Functions

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

Functoriality. The assignment $U\mapsto R_{*}\webleft (U\webright )$ defines a functor
\[ R_{*}\colon \webleft (\mathcal{P}\webleft (A\webright ),\subset \webright )\to \webleft (\mathcal{P}\webleft (B\webright ),\subset \webright ) \]

where
- Action on Objects. For each $U\in \mathcal{P}\webleft (A\webright )$, we have
  
  \[ \webleft [R_{*}\webright ]\webleft (U\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}R_{*}\webleft (U\webright ). \]
- Action on Morphisms. For each $U,V\in \mathcal{P}\webleft (A\webright )$:
  - If $U\subset V$, then $R_{*}\webleft (U\webright )\subset R_{*}\webleft (V\webright )$.
Adjointness. We have an adjunction
witnessed by a bijections of sets
\[ \textup{Hom}_{\mathcal{P}\webleft (A\webright )}\webleft (R_{*}\webleft (U\webright ),V\webright )\cong \textup{Hom}_{\mathcal{P}\webleft (A\webright )}\webleft (U,R_{-1}\webleft (V\webright )\webright ), \]

natural in $U\in \mathcal{P}\webleft (A\webright )$ and $V\in \mathcal{P}\webleft (B\webright )$, i.e. such that:
- The following conditions are equivalent:
  - We have $R_{*}\webleft (U\webright )\subset V$.
  - We have $U\subset R_{-1}\webleft (V\webright )$.
Preservation of Colimits. We have an equality of sets
\[ R_{*}\webleft (\bigcup _{i\in I}U_{i}\webright )=\bigcup _{i\in I}R_{*}\webleft (U_{i}\webright ), \]

natural in $\webleft\{ U_{i}\webright\} _{i\in I}\in \mathcal{P}\webleft (A\webright )^{\times I}$. In particular, we have equalities

\[ \begin{gathered} R_{*}\webleft (U\webright )\cup R_{*}\webleft (V\webright ) = R_{*}\webleft (U\cup V\webright ),\\ R_{*}\webleft (\emptyset \webright ) = \emptyset , \end{gathered} \]

natural in $U,V\in \mathcal{P}\webleft (A\webright )$.
Oplax Preservation of Limits. We have an inclusion of sets
\[ R_{*}\webleft (\bigcap _{i\in I}U_{i}\webright )\subset \bigcap _{i\in I}R_{*}\webleft (U_{i}\webright ), \]

natural in $\webleft\{ U_{i}\webright\} _{i\in I}\in \mathcal{P}\webleft (A\webright )^{\times I}$. In particular, we have inclusions

\[ \begin{gathered} R_{*}\webleft (U\cap V\webright ) \subset R_{*}\webleft (U\webright )\cap R_{*}\webleft (V\webright ),\\ R_{*}\webleft (A\webright ) \subset B, \end{gathered} \]

natural in $U,V\in \mathcal{P}\webleft (A\webright )$.
Symmetric Strict Monoidality With Respect to Unions. The direct image function of Item 1 has a symmetric strict monoidal structure
\[ \webleft (R_{*},R^{\otimes }_{*},R^{\otimes }_{*|\mathbb {1}}\webright ) \colon \webleft (\mathcal{P}\webleft (A\webright ),\cup ,\emptyset \webright ) \to \webleft (\mathcal{P}\webleft (B\webright ),\cup ,\emptyset \webright ), \]

being equipped with equalities

\[ \begin{gathered} R^{\otimes }_{*|U,V} \colon R_{*}\webleft (U\webright )\cup R_{*}\webleft (V\webright ) \mathbin {\overset {=}{\rightarrow }}R_{*}\webleft (U\cup V\webright ),\\ R^{\otimes }_{*|\mathbb {1}} \colon \emptyset \mathbin {\overset {=}{\rightarrow }}\emptyset , \end{gathered} \]

natural in $U,V\in \mathcal{P}\webleft (A\webright )$.
Symmetric Oplax Monoidality With Respect to Intersections. The direct image function of Item 1 has a symmetric oplax monoidal structure
\[ \webleft (R_{*},R^{\otimes }_{*},R^{\otimes }_{*|\mathbb {1}}\webright ) \colon \webleft (\mathcal{P}\webleft (A\webright ),\cap ,A\webright ) \to \webleft (\mathcal{P}\webleft (B\webright ),\cap ,B\webright ), \]

being equipped with inclusions

\[ \begin{gathered} R^{\otimes }_{*|U,V} \colon R_{*}\webleft (U\cap V\webright ) \subset R_{*}\webleft (U\webright )\cap R_{*}\webleft (V\webright ),\\ R^{\otimes }_{*|\mathbb {1}} \colon R_{*}\webleft (A\webright ) \subset B, \end{gathered} \]

natural in $U,V\in \mathcal{P}\webleft (A\webright )$.
Relation to Direct Images With Compact Support. We have
\[ R_{*}\webleft (U\webright )=B\setminus R_{!}\webleft (A\setminus U\webright ) \]

for each $U\in \mathcal{P}\webleft (A\webright )$.

Proof of Proposition 6.4.1.1.3.

Item 1: Functoriality

Clear.

Item 2: Adjointness

This follows from

Item 3: Preservation of Colimits

This follows from Item 2 and

Item 4: Oplax Preservation of Limits

Omitted.

Item 5: Symmetric Strict Monoidality With Respect to Unions

This follows from Item 3.

Item 6: Symmetric Oplax Monoidality With Respect to Intersections

This follows from Item 4.

Item 7: Relation to Direct Images With Compact Support

The proof proceeds in the same way as in the case of functions (Chapter 2: Constructions With Sets, Item 9 of Proposition 2.4.4.1.4): applying Item 7 of Proposition 6.4.4.1.3 to $A\setminus U$, we have

\begin{align*} R_{!}\webleft (A\setminus U\webright ) & = B\setminus R_{*}\webleft (A\setminus \webleft (A\setminus U\webright )\webright )\\ & = B\setminus R_{*}\webleft (U\webright ). \end{align*}

Taking complements, we then obtain

\begin{align*} R_{*}\webleft (U\webright ) & = B\setminus \webleft (B\setminus R_{*}\webleft (U\webright )\webright ),\\ & = B\setminus R_{!}\webleft (A\setminus U\webright ), \end{align*}

which finishes the proof.

Proposition 6.4.1.1.4 ▶ Properties of the Direct Image Function Operation

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 \mathrm{Rel}\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 \mathrm{Rel}\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 ^[3]
\[ \webleft (\chi _{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 ^[4]

Proof of Proposition 6.4.1.1.4.

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}}}=}}\bigcup _{a\in U}\chi _{A}\webleft (a\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{a\in U}\webleft\{ a\webright\} \\ & = U\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\text{id}_{\mathcal{P}\webleft (A\webright )}\webleft (U\webright ) \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}}}=}}\bigcup _{a\in U}\webleft [S\mathbin {\diamond }R\webright ]\webleft (a\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{a\in U}S\webleft (R\webleft (a\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{a\in U}S_{*}\webleft (R\webleft (a\webright )\webright )\\ & = S_{*}\webleft (\bigcup _{a\in U}R\webleft (a\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}S_{*}\webleft (R_{*}\webleft (U\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [S_{*}\circ R_{*}\webright ]\webleft (U\webright ) \end{align*}

for each $U\in \mathcal{P}\webleft (A\webright )$, where we used Item 3 of Proposition 6.4.1.1.3. Thus $\webleft (S\mathbin {\diamond }R\webright )_{*}=S_{*}\circ R_{*}$.