2.4.4 Direct Images

Let $A$ and $B$ be sets and let $f\colon A\to B$ be a function.

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

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

defined by[1][2]

\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\{ b\in B\ \middle |\ \begin{aligned} & \text{there exists some $a\in U$}\\ & \text{such that $b=f\webleft (a\webright )$} \end{aligned} \webright\} \\ & = \webleft\{ f\webleft (a\webright )\in B\ \middle |\ a\in U\webright\} \end{align*}

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

Sometimes one finds the notation

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

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

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

Identifying subsets of $A$ with functions from $A$ to $\{ \mathsf{true},\mathsf{false}\} $ via Item 1 and Item 2 of Proposition 2.4.3.1.6, we see that the direct image function associated to $f$ is equivalently the function

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

defined by

\begin{align*} f_{*}\webleft (\chi _{U}\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\text{Lan}_{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 {a\in A\\ f\webleft (a\webright )=-_{1} }}\webleft (\chi _{U}\webleft (a\webright )\webright )\\ & = \bigvee _{\substack {a\in A\\ f\webleft (a\webright )=-_{1} }}\webleft (\chi _{U}\webleft (a\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 (b\webright )& =\bigvee _{\substack {a\in A\\ f\webleft (a\webright )=b }}\webleft (\chi _{U}\webleft (a\webright )\webright )\\ & =\begin{cases} \mathsf{true}& \text{if there exists some $a\in A$ such}\\ & \text{that $f\webleft (a\webright )=b$ and $a\in U,$}\\ \mathsf{false}& \text{otherwise} \end{cases}\\ & =\begin{cases} \mathsf{true}& \text{if there exists some $a\in U$}\\ & \text{such that $f\webleft (a\webright )=b$,}\\ \mathsf{false}& \text{otherwise} \end{cases}\end{align*}

for each $b\in B$.

Let $f\colon A\to B$ be a function.

  1. Functoriality. The assignment $U\mapsto f_{*}\webleft (U\webright )$ defines a functor
    \[ f_{*}\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 [f_{*}\webright ]\webleft (U\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f_{*}\webleft (U\webright ). \]

    • Action on Morphisms. For each $U,V\in \mathcal{P}\webleft (A\webright )$:
      • If $U\subset V$, then $f_{*}\webleft (U\webright )\subset f_{*}\webleft (V\webright )$.

  2. Triple Adjointness. We have a triple adjunction
    witnessed by bijections of sets
    \begin{align*} \textup{Hom}_{\mathcal{P}\webleft (B\webright )}\webleft (f_{*}\webleft (U\webright ),V\webright ) & \cong \textup{Hom}_{\mathcal{P}\webleft (A\webright )}\webleft (U,f^{-1}\webleft (V\webright )\webright ),\\ \textup{Hom}_{\mathcal{P}\webleft (A\webright )}\webleft (f^{-1}\webleft (U\webright ),V\webright ) & \cong \textup{Hom}_{\mathcal{P}\webleft (A\webright )}\webleft (U,f_{!}\webleft (V\webright )\webright ), \end{align*}

    natural in $U\in \mathcal{P}\webleft (A\webright )$ and $V\in \mathcal{P}\webleft (B\webright )$ and (respectively) $V\in \mathcal{P}\webleft (A\webright )$ and $U\in \mathcal{P}\webleft (B\webright )$, i.e. where:

    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 )$.

  3. 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 (A\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 (\emptyset \webright ) = \emptyset , \end{gathered} \]

    natural in $U,V\in \mathcal{P}\webleft (A\webright )$.

  4. 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 (A\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 (A\webright ) \subset B, \end{gathered} \]

    natural in $U,V\in \mathcal{P}\webleft (A\webright )$.

  5. 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 (A\webright ),\cup ,\emptyset \webright ) \to \webleft (\mathcal{P}\webleft (B\webright ),\cup ,\emptyset \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 \emptyset \mathbin {\overset {=}{\rightarrow }}\emptyset , \end{gathered} \]

    natural in $U,V\in \mathcal{P}\webleft (A\webright )$.

  6. 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 (A\webright ),\cap ,A\webright ) \to \webleft (\mathcal{P}\webleft (B\webright ),\cap ,B\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 (A\webright ) \hookrightarrow B, \end{gathered} \]

    natural in $U,V\in \mathcal{P}\webleft (A\webright )$.

  7. Interaction With Coproducts. Let $f\colon A\to A'$ and $g\colon B\to B'$ 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 (A\webright )$ and each $V\in \mathcal{P}\webleft (B\webright )$.

  8. Interaction With Products. Let $f\colon A\to A'$ and $g\colon B\to B'$ be maps of sets. We have
    \[ \webleft (f\times g\webright )_{*}\webleft (U\times V\webright )=f_{*}\webleft (U\webright )\times g_{*}\webleft (V\webright ) \]

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

  9. Relation to Direct Images With Compact Support. We have
    \[ f_{*}\webleft (U\webright )=B\setminus f_{!}\webleft (A\setminus U\webright ) \]

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

Item 1: Functoriality
Clear.
Item 2: Triple Adjointness
This follows from Remark 2.4.4.1.3, Remark 2.4.5.1.2, Remark 2.4.6.1.3, and of .
Item 3: Preservation of Colimits
This follows from Item 2 and of .[3]
Item 4: Oplax Preservation of Limits
The inclusion $f_{*}\webleft (A\webright )\subset B$ is clear. See [Proof Wiki, Image of Intersection Under Mapping] for the other inclusions.
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: Interaction With Coproducts
Clear.
Item 8: Interaction With Products
Clear.
Item 9: Relation to Direct Images With Compact Support
Applying Item 9 of Proposition 2.4.6.1.6 to $A\setminus U$, we have
\begin{align*} f_{!}\webleft (A\setminus U\webright ) & = B\setminus f_{*}\webleft (A\setminus \webleft (A\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 (A\setminus U\webright ), \end{align*}

which finishes the proof.

Let $f\colon A\to B$ be a function.

  1. Functionality I. The assignment $f\mapsto f_{*}$ defines a function
    \[ \webleft (-\webright )_{*|A,B}\colon \mathsf{Sets}\webleft (A,B\webright ) \to \mathsf{Sets}\webleft (\mathcal{P}\webleft (A\webright ),\mathcal{P}\webleft (B\webright )\webright ). \]
  2. Functionality II. The assignment $f\mapsto f_{*}$ defines a function
    \[ \webleft (-\webright )_{*|A,B}\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 ). \]
  3. 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 )}. \]
  4. Interaction With Composition. For each pair of composable functions $f\colon A\to B$ and $g\colon B\to C$, we have


Footnotes

[1] Further Terminology: The set $f\webleft (U\webright )$ is called the direct image of $U$ by $f$.
[2] We also have
\[ f_{*}\webleft (U\webright )=B\setminus f_{!}\webleft (A\setminus U\webright ); \]
see Item 9 of Proposition 2.4.4.1.4.

Noticed something off, or have any comments? Feel free to reach out!


You can also use the contact form below: