Item 3 (0096) — The Clowder Project

4.6.3 Codirect Images

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

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

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

defined by^1,2

\begin{align*} f_{*}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ y\in Y\ \middle |\ \begin{aligned} & \text{for each $x\in X$, if we have}\\ & \text{$f\webleft (x\webright )=y$, then $x\in U$}\end{aligned} \right\} \\ & = \left\{ y\in Y\ \middle |\ \text{we have $f^{-1}\webleft (y\webright )\subset U$}\right\} \end{align*}

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

¹Further Terminology: The set $f_{*}\webleft (U\webright )$ is called the codirect image of $U$ by $f$.
²We also 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*}
see Item 16 of Proposition 4.6.3.1.7.

Sometimes one finds the notation

\[ \forall _{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 \forall _{f}\webleft (U\webright )$.
•
For each $x\in X$, if $y=f\webleft (x\webright )$, then $x\in U$.

We will not make use of this notation elsewhere in Clowder.

ゴ

Warning 4.6.3.1.3 ▶ Notation for Codirect Images Is Confusing

See Warning 4.6.1.1.3.

ゴ

Remark 4.6.3.1.4 ▶ Unwinding Definition 4.6.3.1.1

Identifying $\mathcal{P}\webleft (X\webright )$ with $\mathsf{Sets}\webleft (X,\{ \mathsf{t},\mathsf{f}\} \webright )$ via Item 2 of Proposition 4.5.1.1.4, we see that the codirect 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}}}=}}\operatorname {\mathrm{Ran}}_{f}\webleft (\chi _{U}\webright )\\ & = \operatorname*{\operatorname {\mathrm{lim}}}\webleft (\webleft (\underline{\webleft (-_{1}\webright )}\mathbin {\overset {\to }{\times }}f\webright )\overset {\operatorname {\mathrm{\mathrm{pr}}}}{\twoheadrightarrow }X\overset {\chi _{U}}{\to }\{ \mathsf{true},\mathsf{false}\} \webright )\\ & = \operatorname*{\operatorname {\mathrm{lim}}}_{\substack {x\in X\\ \begin{bgroup} f\webleft (x\webright )=-_{1} \end{bgroup}}}\webleft (\chi _{U}\webleft (x\webright )\webright )\\ & = \bigwedge _{\substack {x\in X\\ \begin{bgroup} f\webleft (x\webright )=-_{1} \end{bgroup}}}\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 ) & = \bigwedge _{\substack {x\in X\\ \begin{bgroup} f\webleft (x\webright )=y \end{bgroup}}}\webleft (\chi _{U}\webleft (x\webright )\webright )\\ & = \begin{cases} \mathsf{true}& \text{if, for each $x\in X$ such that}\\ & \text{$f\webleft (x\webright )=y$, we have $x\in U,$}\\ \mathsf{false}& \text{otherwise} \end{cases}\\ & = \begin{cases} \mathsf{true}& \text{if $f^{-1}\webleft (y\webright )\subset U$}\\ \mathsf{false}& \text{otherwise} \end{cases}\end{align*}

for each $y\in Y$.

Definition 4.6.3.1.5 ▶ The Image and Complement Parts of $f_{*}$

Let $U$ be a subset of $X$.^1,2

1.
The image part of the codirect image $f_{*}\webleft (U\webright )$ of $U$ is the set $f_{*,\mathrm{im}}\webleft (U\webright )$ defined by

\begin{align*} f_{*,\mathrm{im}}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f_{*}\webleft (U\webright )\cap \mathrm{Im}\webleft (f\webright )\\ & = \left\{ y\in Y\ \middle |\ \begin{aligned} & \text{we have $f^{-1}\webleft (y\webright )\subset U$}\\ & \text{and $f^{-1}\webleft (y\webright )\neq \text{Ø}$.} \end{aligned}\right\} .\end{align*}
2.
The complement part of the codirect image $f_{*}\webleft (U\webright )$ of $U$ is the set $f_{*,\mathrm{cp}}\webleft (U\webright )$ defined by

\begin{align*} f_{*,\mathrm{cp}}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f_{*}\webleft (U\webright )\cap \webleft (Y\setminus \mathrm{Im}\webleft (f\webright )\webright )\\ & = Y\setminus \mathrm{Im}\webleft (f\webright )\\ & = \left\{ y\in Y\ \middle |\ \begin{aligned} & \text{we have $f^{-1}\webleft (y\webright )\subset U$}\\ & \text{and $f^{-1}\webleft (y\webright )=\text{Ø}$.} \end{aligned}\right\} \\ & = \left\{ y\in Y\ \middle |\ f^{-1}\webleft (y\webright )=\text{Ø}\right\} .\end{align*}

¹Note that we have
\[ f_{*}\webleft (U\webright )=f_{*,\mathrm{im}}\webleft (U\webright )\cup f_{*,\mathrm{cp}}\webleft (U\webright ), \]
as
\begin{align*} f_{*}\webleft (U\webright ) & = f_{*}\webleft (U\webright )\cap Y\\ & = f_{*}\webleft (U\webright )\cap \webleft (\mathrm{Im}\webleft (f\webright )\cup \webleft (Y\setminus \mathrm{Im}\webleft (f\webright )\webright )\webright )\\ & = \webleft (f_{*}\webleft (U\webright )\cap \mathrm{Im}\webleft (f\webright )\webright )\cup \webleft (f_{*}\webleft (U\webright )\cap \webleft (Y\setminus \mathrm{Im}\webleft (f\webright )\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f_{*,\mathrm{im}}\webleft (U\webright )\cup f_{*,\mathrm{cp}}\webleft (U\webright ). \end{align*}
²In terms of the meet computation of $f_{*}\webleft (U\webright )$ of Remark 4.6.3.1.4, namely
\[ f_{*}\webleft (\chi _{U}\webright ) =\bigwedge _{\substack {x\in X\\ f\webleft (x\webright )=-_{1}}}\webleft (\chi _{U}\webleft (x\webright )\webright ), \]
we see that $\smash {f_{*,\mathrm{im}}}$ corresponds to meets indexed over nonempty sets, while $\smash {f_{*,\mathrm{cp}}}$ corresponds to meets indexed over the empty set.

Example 4.6.3.1.6 ▶ Examples of Codirect Images

Here are some examples of codirect images.

1.
Multiplication by Two. Consider the function $f\colon \mathbb {N}\to \mathbb {N}$ given by

\[ f\webleft (n\webright ) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}2n \]

for each $n\in \mathbb {N}$. Since $f$ is injective, we have

\begin{align*} f_{*,\mathrm{im}}\webleft (U\webright ) & = f_{!}\webleft (U\webright )\\ f_{*,\mathrm{cp}}\webleft (U\webright ) & = \left\{ \text{odd natural numbers}\right\} \end{align*}

for any $U\subset \mathbb {N}$. In particular, we have

\[ f_{*}\webleft (\left\{ \text{even natural numbers}\right\} \webright )=\mathbb {N}. \]
2.
Parabolas. Consider the function $f\colon \mathbb {R}\to \mathbb {R}$ given by

\[ f\webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}x^{2} \]

for each $x\in \mathbb {R}$. We have

\[ f_{*,\mathrm{cp}}\webleft (U\webright )=\mathbb {R}_{<0} \]

for any $U\subset \mathbb {R}$. Moreover, since $f^{-1}\webleft (x\webright )=\left\{ -\sqrt{x},\sqrt{x}\right\} $, we have e.g.:

\begin{gather*} \begin{aligned} f_{*,\mathrm{im}}\webleft (\webleft [0,1\webright ]\webright ) & = \left\{ 0\right\} ,\\ f_{*,\mathrm{im}}\webleft (\webleft [-1,1\webright ]\webright ) & = \webleft [0,1\webright ],\\ f_{*,\mathrm{im}}\webleft (\webleft [1,2\webright ]\webright ) & = \text{Ø}, \end{aligned}\\ f_{*,\mathrm{im}}\webleft (\webleft [-2,-1\webright ]\cup \webleft [1,2\webright ]\webright ) = \webleft [1,4\webright ]. \end{gather*}
3.
Circles. Consider the function $f\colon \mathbb {R}^{2}\to \mathbb {R}$ given by

\[ f\webleft (x,y\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}x^{2}+y^{2} \]

for each $\webleft (x,y\webright )\in \mathbb {R}^{2}$. We have

\[ f_{*,\mathrm{cp}}\webleft (U\webright )=\mathbb {R}_{<0} \]

for any $U\subset \mathbb {R}^{2}$, and since

\[ f^{-1}\webleft (r\webright )= \begin{cases} \text{a circle of radius $r$ about the origin} & \text{if $r>0$,}\\ \left\{ \webleft (0,0\webright )\right\} & \text{if $r=0$,}\\ \text{Ø}& \text{if $r<0$,} \end{cases} \]

we have e.g.:

\begin{gather*} f_{*,\mathrm{im}}\webleft (\webleft [-1,1\webright ]\times \webleft [-1,1\webright ]\webright ) = \webleft [0,1\webright ],\\ f_{*,\mathrm{im}}\webleft (\webleft (\webleft [-1,1\webright ]\times \webleft [-1,1\webright ]\webright )\setminus \webleft [-1,1\webright ]\times \left\{ 0\right\} \webright ) = \text{Ø}. \end{gather*}

Proposition 4.6.3.1.7 ▶ Properties of Codirect Images I

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

1.
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:
- (★)
2.
Triple Adjointness. We have a triple adjunction
witnessed by:
1. (a)
  Units and counits of the form
  
  \[ \begin{aligned} \operatorname {\mathrm{id}}_{\mathcal{P}\webleft (X\webright )} & \hookrightarrow f^{-1}\circ f_{!},\\ f_{!}\circ f^{-1} & \hookrightarrow \operatorname {\mathrm{id}}_{\mathcal{P}\webleft (Y\webright )},\\ \end{aligned} \qquad \begin{aligned} \operatorname {\mathrm{id}}_{\mathcal{P}\webleft (Y\webright )} & \hookrightarrow f_{*}\circ f^{-1},\\ f^{-1}\circ f_{*} & \hookrightarrow \operatorname {\mathrm{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. (b)
  Bijections of sets
  
  \begin{align*} \operatorname {\mathrm{Hom}}_{\mathcal{P}\webleft (Y\webright )}\webleft (f_{!}\webleft (U\webright ),V\webright ) & \cong \operatorname {\mathrm{Hom}}_{\mathcal{P}\webleft (X\webright )}\webleft (U,f^{-1}\webleft (V\webright )\webright ),\\ \operatorname {\mathrm{Hom}}_{\mathcal{P}\webleft (X\webright )}\webleft (f^{-1}\webleft (U\webright ),V\webright ) & \cong \operatorname {\mathrm{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. (i)
    The following conditions are equivalent:
    
    (I)
    We have $f_{!}\webleft (U\webright )\subset V$.
    
    (II)
    We have $U\subset f^{-1}\webleft (V\webright )$.
  2. (ii)
    The following conditions are equivalent:
    
    (I)
    We have $f^{-1}\webleft (U\webright )\subset V$.
    
    (II)
    We have $U\subset f_{*}\webleft (V\webright )$.
3.
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 )$.
4.
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 )$.
5.
Interaction With Binary Unions. Let $f\colon X\to Y$ be a function. We have a natural transformation
with components

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

indexed by $U,V\in \mathcal{P}\webleft (X\webright )$.
6.
Interaction With Binary Intersections. The diagram
commutes, i.e. we have

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

for each $U,V\in \mathcal{P}\webleft (X\webright )$.
7.
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 )$.
8.
Interaction With Symmetric Differences. We have a natural transformation
with components

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

indexed by $U,V\in \mathcal{P}\webleft (X\webright )$.
9.
Interaction With Internal Homs of Powersets. We have a natural transformation
with components

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

indexed by $U,V\in \mathcal{P}\webleft (X\webright )$.
10.
Lax Preservation of Colimits. We have an inclusion of sets

\[ \bigcup _{i\in I}f_{*}\webleft (U_{i}\webright )\subset f_{*}\left(\bigcup _{i\in I}U_{i}\right), \]

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

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

natural in $U,V\in \mathcal{P}\webleft (X\webright )$.
11.
Preservation of Limits. We have an equality of sets

\[ f_{*}\left(\bigcap _{i\in I}U_{i}\right)=\bigcap _{i\in I}f_{*}\webleft (U_{i}\webright ), \]

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

\[ \begin{gathered} f^{-1}\webleft (U\cap V\webright ) = f_{*}\webleft (U\webright )\cap f^{-1}\webleft (V\webright ),\\ f_{*}\webleft (X\webright ) = Y, \end{gathered} \]

natural in $U,V\in \mathcal{P}\webleft (X\webright )$.
12.
Symmetric Lax Monoidality With Respect to Unions. The codirect image function of Item 1 has a symmetric lax 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 inclusions

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

natural in $U,V\in \mathcal{P}\webleft (X\webright )$.
13.
Symmetric Strict Monoidality With Respect to Intersections. 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 ),\cap ,X\webright ) \to \webleft (\mathcal{P}\webleft (Y\webright ),\cap ,Y\webright ), \]

being equipped with equalities

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

natural in $U,V\in \mathcal{P}\webleft (X\webright )$.
14.
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 )$.
15.
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 )$.
16.
Relation to Direct Images. We have

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

for each $U\in \mathcal{P}\webleft (X\webright )$.
17.
Interaction With Injections. If $f$ is injective, then we have

\begin{gather*} f_{*,\mathrm{im}}\webleft (U\webright ) = f_{!}\webleft (U\webright ),\\ f_{*,\mathrm{cp}}\webleft (U\webright ) = Y\setminus \mathrm{Im}\webleft (f\webright ),\\ \end{gather*}

and so

\begin{align*} f_{*}\webleft (U\webright ) & = f_{*,\mathrm{im}}\webleft (U\webright )\cup f_{*,\mathrm{cp}}\webleft (U\webright )\\ & = f_{!}\webleft (U\webright )\cup \webleft (Y\setminus \mathrm{Im}\webleft (f\webright )\webright ) \end{align*}

for each $U\in \mathcal{P}\webleft (X\webright )$.
18.
Interaction With Surjections. If $f$ is surjective, then we have

\begin{align*} f_{*,\mathrm{im}}\webleft (U\webright ) & \subset f_{!}\webleft (U\webright ),\\ f_{*,\mathrm{cp}}\webleft (U\webright ) & = \text{Ø},\\ \end{align*}

and so

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

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

Proof of Proposition 4.6.3.1.7.

Item 1: Functoriality

Omitted.

Item 2: Triple Adjointness

This follows from Remark 4.6.1.1.4, Remark 4.6.2.1.2, Remark 4.6.3.1.4, 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 \left\{ f_{*}\webleft (U\webright )\in \mathcal{P}\webleft (X\webright )\ \middle |\ U\in \mathcal{U}\right\} }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 \left\{ f_{*}\webleft (U\webright )\in \mathcal{P}\webleft (X\webright )\ \middle |\ U\in \mathcal{U}\right\} }V\\ & = \bigcap _{U\in \mathcal{U}}f_{*}\webleft (U\webright ).\end{align*}

This finishes the proof.

Item 5: Interaction With Binary Unions

We have

\begin{align*} f_{*}\webleft (U\webright )\cup f_{*}\webleft (V\webright ) & = f_{!}\webleft (U^{\textsf{c}}\webright )^{\textsf{c}}\cup f_{!}\webleft (V^{\textsf{c}}\webright )^{\textsf{c}}\\ & = \webleft (f_{!}\webleft (U^{\textsf{c}}\webright )\cap f_{!}\webleft (V^{\textsf{c}}\webright )\webright )^{\textsf{c}}\\ & \subset \webleft (f_{!}\webleft (U^{\textsf{c}}\cap V^{\textsf{c}}\webright )\webright )^{\textsf{c}}\\ & = f_{!}\webleft (\webleft (U\cup V\webright )^{\textsf{c}}\webright )^{\textsf{c}}\\ & = f_{*}\webleft (U\cup V\webright ), \end{align*}

where:

1.
We have used Item 16 for the first equality.
2.
We have used Item 2 of Proposition 4.3.11.1.2 for the second equality.
3.
We have used Item 6 of Proposition 4.6.1.1.5 for the third equality.
4.
We have used Item 2 of Proposition 4.3.11.1.2 for the fourth equality.
5.
We have used Item 16 for the last equality.

This finishes the proof.

Item 6: Interaction With Binary Intersections

This follows from Item 11.

Item 7: Interaction With Complements

Omitted.

Item 8: Interaction With Symmetric Differences

Omitted.

Item 9: Interaction With Internal Homs of Powersets

We have

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

where we have used:

1.
Item 7 of Proposition 4.6.3.1.7 for the second equality.
2.
Item 5 of Proposition 4.6.3.1.7 for the inclusion.

Since $\mathcal{P}\webleft (X\webright )$ is posetal, naturality is automatic (Chapter 11: Categories, Item 4 of Proposition 11.2.7.1.2). This finishes the proof.

Item 10: Lax Preservation of Colimits

Omitted.

Item 11: Preservation of Limits

This follows from Item 2 and

Item 12: Symmetric Lax Monoidality With Respect to Unions

This follows from Item 10.

Item 13: Symmetric Strict Monoidality With Respect to Intersections

This follows from Item 11.

Item 14: Interaction With Coproducts

Omitted.

Item 15: Interaction With Products

Omitted.

Item 16: Relation to Direct Images

We claim that $f_{*}\webleft (U\webright )=Y\setminus f_{!}\webleft (X\setminus U\webright )$.

•
The First Implication. We claim that

\[ f_{*}\webleft (U\webright )\subset Y\setminus f_{!}\webleft (X\setminus U\webright ). \]

Let $y\in f_{*}\webleft (U\webright )$. We need to show that $y\not\in f_{!}\webleft (X\setminus U\webright )$, i.e. that there is no $x\in X\setminus U$ such that $f\webleft (x\webright )=y$.

This is indeed the case, as otherwise we would have $x\in f^{-1}\webleft (y\webright )$ and $x\not\in U$, contradicting $f^{-1}\webleft (y\webright )\subset U$ (which holds since $y\in f_{*}\webleft (U\webright )$).

Thus $y\in Y\setminus f_{!}\webleft (X\setminus U\webright )$.
•
The Second Implication. We claim that

\[ Y\setminus f_{!}\webleft (X\setminus U\webright )\subset f_{*}\webleft (U\webright ). \]

Let $y\in Y\setminus f_{!}\webleft (X\setminus U\webright )$. We need to show that $y\in f_{*}\webleft (U\webright )$, i.e. that $f^{-1}\webleft (y\webright )\subset U$.

Since $y\not\in f_{!}\webleft (X\setminus U\webright )$, there exists no $x\in X\setminus U$ such that $y=f\webleft (x\webright )$, and hence $f^{-1}\webleft (y\webright )\subset U$.

Thus $y\in f_{*}\webleft (U\webright )$.

This finishes the proof of Item 16.

Item 17: Interaction With Injections

Omitted.

Item 18: Interaction With Surjections

Omitted.

Proposition 4.6.3.1.8 ▶ Properties of Codirect Images II

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

1.
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 ). \]
2.
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 ). \]

3.
Interaction With Identities. For each $X\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$, we have

\[ \webleft (\operatorname {\mathrm{id}}_{X}\webright )_{*}=\operatorname {\mathrm{id}}_{\mathcal{P}\webleft (X\webright )}. \]