Subsection 2.6.1 (007F): 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`

2.6.1 Direct Images

Let $f\colon X\to Y$ be a function.

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

\[ f_{*}\colon \mathcal{P}\webleft (X\webright )\to \mathcal{P}\webleft (Y\webright ) \]

defined by¹

\begin{align*} f_{*}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f\webleft (U\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ y\in Y\ \middle |\ \begin{aligned} & \text{there exists some $x\in U$}\\ & \text{such that $y=f\webleft (x\webright )$} \end{aligned} \webright\} \\ & = \webleft\{ f\webleft (x\webright )\in Y\ \middle |\ x\in U\webright\} \end{align*}

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

¹Further Terminology: The set $f\webleft (U\webright )$ is called the direct image of $U$ by $f$.

Notation 2.6.1.1.2 ▶ Further Notation for Direct Images

Sometimes one finds the notation

\[ \exists _{f}\colon \mathcal{P}\webleft (X\webright )\to \mathcal{P}\webleft (Y\webright ) \]

for $f_{*}$. This notation comes from the fact that the following statements are equivalent, where $y\in Y$ and $U\in \mathcal{P}\webleft (X\webright )$:

We have $y\in \exists _{f}\webleft (U\webright )$.
There exists some $x\in U$ such that $f\webleft (x\webright )=y$.

We will not make use of this notation in the present work.

Remark 2.6.1.1.3 ▶ Unwinding Definition 2.6.1.1.1

Identifying $\mathcal{P}\webleft (X\webright )$ with $\mathsf{Sets}\webleft (X,\{ \mathsf{t},\mathsf{f}\} \webright )$ via Item 2 of Proposition 2.5.1.1.4, we see that the direct image function associated to $f$ is equivalently the function

\[ f_{*}\colon \mathcal{P}\webleft (X\webright )\to \mathcal{P}\webleft (Y\webright ) \]

defined by

\begin{align*} f_{*}\webleft (\chi _{U}\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\text{Ran}_{f}\webleft (\chi _{U}\webright )\\ & = \operatorname*{\text{colim}}\webleft (\webleft (f\mathbin {\overset {\to }{\times }}\underline{\webleft (-_{1}\webright )}\webright )\overset {\text{pr}}{\twoheadrightarrow }A\overset {\chi _{U}}{\to }\{ \mathsf{t},\mathsf{f}\} \webright )\\ & = \operatorname*{\text{colim}}_{\substack {x\in X\\ f\webleft (x\webright )=-_{1} }}\webleft (\chi _{U}\webleft (x\webright )\webright )\\ & = \bigvee _{\substack {x\in X\\ f\webleft (x\webright )=-_{1} }}\webleft (\chi _{U}\webleft (x\webright )\webright ),\end{align*}

where we have used , for the second equality. In other words, we have

\begin{align*} \webleft [f_{*}\webleft (\chi _{U}\webright )\webright ]\webleft (y\webright )& =\bigvee _{\substack {x\in X\\ f\webleft (x\webright )=y }}\webleft (\chi _{U}\webleft (x\webright )\webright )\\ & =\begin{cases} \mathsf{true}& \text{if there exists some $x\in X$ such}\\ & \text{that $f\webleft (x\webright )=y$ and $x\in U,$}\\ \mathsf{false}& \text{otherwise} \end{cases}\\ & =\begin{cases} \mathsf{true}& \text{if there exists some $x\in U$}\\ & \text{such that $f\webleft (x\webright )=y$,}\\ \mathsf{false}& \text{otherwise} \end{cases}\end{align*}

for each $y\in Y$.

Proposition 2.6.1.1.4 ▶ Properties of Direct Images I

Let $f\colon X\to Y$ be a function.

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

In particular, for each $U,V\in \mathcal{P}\webleft (X\webright )$, the following condition is satisfied:
- If $U\subset V$, then $f_{*}\webleft (U\webright )\subset f_{*}\webleft (V\webright )$.
Triple Adjointness. We have a triple adjunction
witnessed by:
1. Units and counits of the form
  \[ \begin{aligned} \text{id}_{\mathcal{P}\webleft (X\webright )} & \hookrightarrow f^{-1}\circ f_{*},\\ f_{*}\circ f^{-1} & \hookrightarrow \text{id}_{\mathcal{P}\webleft (Y\webright )},\\ \end{aligned} \qquad \begin{aligned} \text{id}_{\mathcal{P}\webleft (Y\webright )} & \hookrightarrow f_{!}\circ f^{-1},\\ f^{-1}\circ f_{!} & \hookrightarrow \text{id}_{\mathcal{P}\webleft (X\webright )}, \end{aligned} \]
  
  having components of the form
  
  \[ \begin{gathered} U \subset f^{-1}\webleft (f_{*}\webleft (U\webright )\webright ),\\ f_{*}\webleft (f^{-1}\webleft (V\webright )\webright ) \subset V, \end{gathered} \qquad \begin{gathered} V \subset f_{!}\webleft (f^{-1}\webleft (V\webright )\webright ),\\ f^{-1}\webleft (f_{!}\webleft (U\webright )\webright ) \subset U \end{gathered} \]
  
  indexed by $U\in \mathcal{P}\webleft (X\webright )$ and $V\in \mathcal{P}\webleft (Y\webright )$.
2. Bijections of sets
  \begin{align*} \textup{Hom}_{\mathcal{P}\webleft (Y\webright )}\webleft (f_{*}\webleft (U\webright ),V\webright ) & \cong \textup{Hom}_{\mathcal{P}\webleft (X\webright )}\webleft (U,f^{-1}\webleft (V\webright )\webright ),\\ \textup{Hom}_{\mathcal{P}\webleft (X\webright )}\webleft (f^{-1}\webleft (U\webright ),V\webright ) & \cong \textup{Hom}_{\mathcal{P}\webleft (X\webright )}\webleft (U,f_{!}\webleft (V\webright )\webright ), \end{align*}
  
  natural in $U\in \mathcal{P}\webleft (X\webright )$ and $V\in \mathcal{P}\webleft (Y\webright )$ and (respectively) $V\in \mathcal{P}\webleft (X\webright )$ and $U\in \mathcal{P}\webleft (Y\webright )$. In particular:
  1. The following conditions are equivalent:
    1. We have $f_{*}\webleft (U\webright )\subset V$.
    2. We have $U\subset f^{-1}\webleft (V\webright )$.
  2. The following conditions are equivalent:
    1. We have $f^{-1}\webleft (U\webright )\subset V$.
    2. We have $U\subset f_{!}\webleft (V\webright )$.
Interaction With Unions of Families of Subsets. The diagram

commutes, i.e. we have

\[ \bigcup _{U\in \mathcal{U}}f_{*}\webleft (U\webright )=\bigcup _{V\in f_{*}\webleft (\mathcal{U}\webright )}V \]

for each $\mathcal{U}\in \mathcal{P}\webleft (X\webright )$, where $f_{*}\webleft (\mathcal{U}\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (f_{*}\webright )_{*}\webleft (\mathcal{U}\webright )$.
Interaction With Intersections of Families of Subsets. The diagram

commutes, i.e. we have

\[ \bigcap _{U\in \mathcal{U}}f_{*}\webleft (U\webright )=\bigcap _{V\in f_{*}\webleft (\mathcal{U}\webright )}V \]

for each $\mathcal{U}\in \mathcal{P}\webleft (X\webright )$, where $f_{*}\webleft (\mathcal{U}\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (f_{*}\webright )_{*}\webleft (\mathcal{U}\webright )$.
Interaction With Binary Unions. The diagram

commutes, i.e. we have

\[ f_{*}\webleft (U\cup V\webright )=f_{*}\webleft (U\webright )\cup f_{*}\webleft (V\webright ) \]

for each $U,V\in \mathcal{P}\webleft (X\webright )$.
Interaction With Binary Intersections. We have a natural transformation

with components

\[ f_{*}\webleft (U\cap V\webright )\subset f_{*}\webleft (U\webright )\cap f_{*}\webleft (V\webright ) \]

indexed by $U,V\in \mathcal{P}\webleft (X\webright )$.
Interaction With Differences. We have a natural transformation

with components

\[ f_{*}\webleft (U\webright )\setminus f_{*}\webleft (V\webright )\subset f_{*}\webleft (U\setminus V\webright ) \]

indexed by $U,V\in \mathcal{P}\webleft (X\webright )$.
Interaction With Complements. The diagram

commutes, i.e. we have

\[ f_{*}\webleft (U^{\textsf{c}}\webright )=f_{!}\webleft (U\webright )^{\textsf{c}} \]

for each $U\in \mathcal{P}\webleft (X\webright )$.
Interaction With Symmetric Differences. We have a natural transformation

with components

\[ f_{*}\webleft (U\webright )\mathbin {\triangle }f_{*}\webleft (V\webright )\subset f_{*}\webleft (U\mathbin {\triangle }V\webright ) \]

indexed by $U,V\in \mathcal{P}\webleft (X\webright )$.
Interaction With Internal Homs of Powersets. The diagram

commutes, i.e. we have an equality of sets

\[ f_{*}\webleft (\webleft [U,V\webright ]_{X}\webright )=\webleft [f_{!}\webleft (U\webright ),f_{*}\webleft (V\webright )\webright ]_{Y}, \]

natural in $U,V\in \mathcal{P}\webleft (X\webright )$.
Preservation of Colimits. We have an equality of sets
\[ f_{*}\webleft(\bigcup _{i\in I}U_{i}\webright)=\bigcup _{i\in I}f_{*}\webleft (U_{i}\webright ), \]

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

\[ \begin{gathered} f_{*}\webleft (U\webright )\cup f_{*}\webleft (V\webright ) = f_{*}\webleft (U\cup V\webright ),\\ f_{*}\webleft (\text{Ø}\webright ) = \text{Ø}, \end{gathered} \]

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

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

\[ \begin{gathered} f_{*}\webleft (U\cap V\webright ) \subset f_{*}\webleft (U\webright )\cap f_{*}\webleft (V\webright ),\\ f_{*}\webleft (X\webright ) \subset Y, \end{gathered} \]

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

being equipped with equalities

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

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

being equipped with inclusions

\[ \begin{gathered} f^{\otimes }_{*|U,V} \colon f_{*}\webleft (U\cap V\webright ) \hookrightarrow f_{*}\webleft (U\webright )\cap f_{*}\webleft (V\webright ),\\ f^{\otimes }_{*|\mathbb {1}} \colon f_{*}\webleft (X\webright ) \hookrightarrow Y, \end{gathered} \]

natural in $U,V\in \mathcal{P}\webleft (X\webright )$.
Interaction With Coproducts. Let $f\colon X\to X'$ and $g\colon Y\to Y'$ be maps of sets. We have
\[ \webleft (f\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}g\webright )_{*}\webleft (U\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}V\webright )=f_{*}\webleft (U\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}g_{*}\webleft (V\webright ) \]

for each $U\in \mathcal{P}\webleft (X\webright )$ and each $V\in \mathcal{P}\webleft (Y\webright )$.
Interaction With Products. Let $f\colon X\to X'$ and $g\colon Y\to Y'$ be maps of sets. We have
\[ \webleft (f\boxtimes _{X\times Y} g\webright )_{*}\webleft (U\boxtimes _{X\times Y}V\webright )=f_{*}\webleft (U\webright )\boxtimes _{X'\times Y'}g_{*}\webleft (V\webright ) \]

for each $U\in \mathcal{P}\webleft (X\webright )$ and each $V\in \mathcal{P}\webleft (Y\webright )$.
Relation to Direct Images With Compact Support. We have
\begin{align*} f_{*}\webleft (U\webright ) & = f_{!}\webleft (U^{\textsf{c}}\webright )^{\textsf{c}}\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}Y\setminus f_{!}\webleft (X\setminus U\webright )\end{align*}

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

Proof of Proposition 2.6.1.1.4.

Item 1: Functoriality

Omitted.

Item 2: Triple Adjointness

This follows from Remark 2.6.1.1.3, Remark 2.6.2.1.2, Remark 2.6.3.1.3, and

Item 3: Interaction With Unions of Families of Subsets

We have

\begin{align*} \bigcup _{V\in f_{*}\webleft (\mathcal{U}\webright )}V & = \bigcup _{V\in \webleft\{ f_{*}\webleft (U\webright )\in \mathcal{P}\webleft (X\webright )\ \middle |\ U\in \mathcal{U}\webright\} }V\\ & = \bigcup _{U\in \mathcal{U}}f_{*}\webleft (U\webright ).\end{align*}

This finishes the proof.

Item 4: Interaction With Intersections of Families of Subsets

We have

\begin{align*} \bigcap _{V\in f_{*}\webleft (\mathcal{U}\webright )}V & = \bigcap _{V\in \webleft\{ f_{*}\webleft (U\webright )\in \mathcal{P}\webleft (X\webright )\ \middle |\ U\in \mathcal{U}\webright\} }V\\ & = \bigcap _{U\in \mathcal{U}}f_{*}\webleft (U\webright ).\end{align*}

This finishes the proof.

Item 5: Interaction With Binary Unions

See [Proof Wiki, Image of Union Under Mapping].

Item 6: Interaction With Binary Intersections

See [Proof Wiki, Image of Intersection Under Mapping].

Item 7: Interaction With Differences

See [Proof Wiki, Image of Set Difference Under Mapping].

Item 8: Interaction With Complements

Applying Item 17 to $X\setminus U$, we have

\begin{align*} f_{*}\webleft (U^{\textsf{c}}\webright ) & = f_{*}\webleft (X\setminus U\webright )\\ & = Y\setminus f_{!}\webleft (X\setminus \webleft (X\setminus U\webright )\webright )\\ & = Y\setminus f_{!}\webleft (U\webright )\\ & = f_{!}\webleft (U\webright )^{\textsf{c}}. \end{align*}

This finishes the proof.

Item 9: Interaction With Symmetric Differences

We have

\begin{align*} f_{*}\webleft (U\webright )\mathbin {\triangle }f_{*}\webleft (V\webright ) & = \webleft (f_{*}\webleft (U\webright )\cup f_{*}\webleft (V\webright )\webright )\setminus \webleft (f_{*}\webleft (U\webright )\cap f_{*}\webleft (V\webright )\webright )\\ & \subset \webleft (f_{*}\webleft (U\webright )\cup f_{*}\webleft (V\webright )\webright )\setminus \webleft (f_{*}\webleft (U\cap V\webright )\webright )\\ & = \webleft (f_{*}\webleft (U\cup V\webright )\webright )\setminus \webleft (f_{*}\webleft (U\cap V\webright )\webright )\\ & \subset f_{*}\webleft (\webleft (U\cup V\webright )\setminus \webleft (U\cap V\webright )\webright )\\ & = f_{*}\webleft (U\mathbin {\triangle }V\webright ), \end{align*}

where we have used:

Item 2 of Proposition 2.3.12.1.2 for the first equality.
Item 6 of this proposition together with Item 1 of Proposition 2.3.10.1.2 for the first inclusion.
Item 5 for the second equality.
Item 7 for the second inclusion.
Item 2 of Proposition 2.3.12.1.2 for the tchird equality.

Since $\mathcal{P}\webleft (Y\webright )$ is posetal, naturality is automatic (). This finishes the proof.

Item 10: Interaction With Internal Homs of Powersets

We have

\begin{align*} f_{*}\webleft (\webleft [U,V\webright ]_{X}\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f_{*}\webleft (U^{\textsf{c}}\cup V\webright )\\ & = f_{*}\webleft (U^{\textsf{c}}\webright )\cup f_{*}\webleft (V\webright )\\ & = f_{!}\webleft (U\webright )^{\textsf{c}}\cup f_{*}\webleft (V\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [f_{!}\webleft (U\webright ),f_{*}\webleft (V\webright )\webright ]_{Y},\end{align*}

where we have used:

Item 5 for the second equality.
Item 17 for the third equality.

Since $\mathcal{P}\webleft (Y\webright )$ is posetal, naturality is automatic (). This finishes the proof.

Item 11: Preservation of Colimits

This follows from Item 2 and

.¹

Item 12: Oplax Preservation of Limits

The inclusion $f_{*}\webleft (X\webright )\subset Y$ is automatic. See [Proof Wiki, Image of Intersection Under Mapping] for the other inclusions.

Item 13: Symmetric Strict Monoidality With Respect to Unions

This follows from Item 11.

Item 14: Symmetric Oplax Monoidality With Respect to Intersections

The inclusions in the statement follow from Item 12. Since $\mathcal{P}\webleft (Y\webright )$ is posetal, the commutativity of the diagrams in the definition of a symmetric oplax monoidal functor is automatic (

Item 15: Interaction With Coproducts

Omitted.

Item 16: Interaction With Products

Omitted.

Item 17: Relation to Direct Images With Compact Support

Applying Item 16 of Proposition 2.6.3.1.6 to $X\setminus U$, we have

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

Taking complements, we then obtain

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

which finishes the proof.

¹Reference: [Proof Wiki, Image of Union Under Mapping].

Proposition 2.6.1.1.5 ▶ Properties of Direct Images II

Let $f\colon X\to Y$ be a function.

Functionality I. The assignment $f\mapsto f_{*}$ defines a function
\[ \webleft (-\webright )_{*|X,Y}\colon \mathsf{Sets}\webleft (X,Y\webright ) \to \mathsf{Sets}\webleft (\mathcal{P}\webleft (X\webright ),\mathcal{P}\webleft (Y\webright )\webright ). \]
Functionality II. The assignment $f\mapsto f_{*}$ defines a function
\[ \webleft (-\webright )_{*|X,Y}\colon \mathsf{Sets}\webleft (X,Y\webright ) \to \mathsf{Pos}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (\mathcal{P}\webleft (Y\webright ),\subset \webright )\webright ). \]
Interaction With Identities. For each $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, we have
\[ \webleft (\text{id}_{X}\webright )_{*}=\text{id}_{\mathcal{P}\webleft (X\webright )}. \]
Interaction With Composition. For each pair of composable functions $f\colon X\to Y$ and $g\colon Y\to Z$, we have