Proposition 4.6.3.1.7 (008R): Properties of Codirect Images I

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}(X)\to \mathcal{P}(Y) \]

defined by^1,2

\begin{align*} f_{*}(U) & \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(x)=y$, then $x\in U$}\end{aligned} \right\} \\ & = \left\{ y\in Y\ \middle |\ \text{we have $f^{-1}(y)\subset U$}\right\} \end{align*}

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

¹Further Terminology: The set $f_{*}(U)$ is called the codirect image of $U$ by $f$.
²We also have
\begin{align*} f_{*}(U) & = f_{!}(U^{\textsf{c}})^{\textsf{c}}\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}Y\setminus f_{!}(X\setminus U);\end{align*}
see Item 16 of Proposition 4.6.3.1.7.

Sometimes one finds the notation

\[ \forall _{f}\colon \mathcal{P}(X)\to \mathcal{P}(Y) \]

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

•
We have $y\in \forall _{f}(U)$.
•
For each $x\in X$, if $y=f(x)$, 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}(X)$ with $\mathsf{Sets}(X,\{ \mathsf{t},\mathsf{f}\} )$ 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}(X)\to \mathcal{P}(Y) \]

defined by

\begin{align*} f_{*}(\chi _{U}) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\operatorname {\mathrm{Ran}}_{f}(\chi _{U})\\ & = \operatorname*{\operatorname {\mathrm{lim}}}((\underline{(-_{1})}\mathbin {\overset {\to }{\times }}f)\overset {\operatorname {\mathrm{\mathrm{pr}}}}{\twoheadrightarrow }X\overset {\chi _{U}}{\to }\{ \mathsf{true},\mathsf{false}\} )\\ & = \operatorname*{\operatorname {\mathrm{lim}}}_{\substack {x\in X\\ \begin{bgroup} f(x)=-_{1} \end{bgroup}}}(\chi _{U}(x))\\ & = \bigwedge _{\substack {x\in X\\ \begin{bgroup} f(x)=-_{1} \end{bgroup}}}(\chi _{U}(x)).\end{align*}

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

\begin{align*} [f_{*}(\chi _{U})](y) & = \bigwedge _{\substack {x\in X\\ \begin{bgroup} f(x)=y \end{bgroup}}}(\chi _{U}(x))\\ & = \begin{cases} \mathsf{true}& \text{if, for each $x\in X$ such that}\\ & \text{$f(x)=y$, we have $x\in U,$}\\ \mathsf{false}& \text{otherwise} \end{cases}\\ & = \begin{cases} \mathsf{true}& \text{if $f^{-1}(y)\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_{*}(U)$ of $U$ is the set $f^{\mathrm{im}}_{*}(U)$ defined by

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

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

¹Note that we have
\[ f_{*}(U)=f^{\mathrm{im}}_{*}(U)\cup f^{\mathrm{cp}}_{*}(U), \]
as
\begin{align*} f_{*}(U) & = f_{*}(U)\cap Y\\ & = f_{*}(U)\cap (\mathrm{Im}(f)\cup (Y\setminus \mathrm{Im}(f)))\\ & = (f_{*}(U)\cap \mathrm{Im}(f))\cup (f_{*}(U)\cap (Y\setminus \mathrm{Im}(f)))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f^{\mathrm{im}}_{*}(U)\cup f^{\mathrm{cp}}_{*}(U). \end{align*}
for each $U\in \mathcal{P}(X)$.
²In terms of the meet computation of $f_{*}(U)$ of Remark 4.6.3.1.4, namely
\[ f_{*}(\chi _{U}) =\bigwedge _{\substack {x\in X\\ f(x)=-_{1}}}(\chi _{U}(x)), \]
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(n) \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}}_{*}(U) & = f_{!}(U)\\ f^{\mathrm{cp}}_{*}(U) & = \left\{ \text{odd natural numbers}\right\} \end{align*}

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

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

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

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

\[ f^{\mathrm{cp}}_{*}(U)=\mathbb {R}_{<0} \]

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

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

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

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

\[ f^{\mathrm{cp}}_{*}(U)=\mathbb {R}_{<0} \]

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

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

we have e.g.:

\begin{gather*} f^{\mathrm{im}}_{*}([-1,1]\times [-1,1]) = [0,1],\\ f^{\mathrm{im}}_{*}(([-1,1]\times [-1,1])\setminus [-1,1]\times \left\{ 0\right\} ) = \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_{*}(U)$ defines a functor

\[ f_{*}\colon (\mathcal{P}(X),\subset )\to (\mathcal{P}(Y),\subset ). \]

In particular, for each $U,V\in \mathcal{P}(X)$, 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}(X)} & \hookrightarrow f^{-1}\circ f_{!},\\ f_{!}\circ f^{-1} & \hookrightarrow \operatorname {\mathrm{id}}_{\mathcal{P}(Y)},\\ \end{aligned} \qquad \begin{aligned} \operatorname {\mathrm{id}}_{\mathcal{P}(Y)} & \hookrightarrow f_{*}\circ f^{-1},\\ f^{-1}\circ f_{*} & \hookrightarrow \operatorname {\mathrm{id}}_{\mathcal{P}(X)}. \end{aligned} \]
  
  In particular:
  - •
    For each $U\in \mathcal{P}(X)$, we have $U\subset f^{-1}(f_{!}(U))$.
  - •
    For each $U\in \mathcal{P}(X)$, we have $f^{-1}(f_{*}(U))\subset U$.
  - •
    For each $V\in \mathcal{P}(Y)$, we have $f_{!}(f^{-1}(V))\subset V$.
  - •
    For each $V\in \mathcal{P}(Y)$, we have $V\subset f_{*}(f^{-1}(V))$.
2. (b)
  Bijections of sets
  
  \begin{align*} \operatorname {\mathrm{Hom}}_{\mathcal{P}(Y)}(f_{!}(U),V) & \cong \operatorname {\mathrm{Hom}}_{\mathcal{P}(X)}(U,f^{-1}(V)),\\ \operatorname {\mathrm{Hom}}_{\mathcal{P}(X)}(f^{-1}(U),V) & \cong \operatorname {\mathrm{Hom}}_{\mathcal{P}(X)}(U,f_{*}(V)), \end{align*}
  
  natural in $U\in \mathcal{P}(X)$ and $V\in \mathcal{P}(Y)$ and (respectively) $V\in \mathcal{P}(X)$ and $U\in \mathcal{P}(Y)$. In particular:
  1. (i)
    The following conditions are equivalent:
    
    (I)
    We have $f_{!}(U)\subset V$.
    
    (II)
    We have $U\subset f^{-1}(V)$.
  2. (ii)
    The following conditions are equivalent:
    
    (I)
    We have $f^{-1}(U)\subset V$.
    
    (II)
    We have $U\subset f_{*}(V)$.
3.
Interaction With Unions of Families of Subsets. The diagram
commutes, i.e. we have

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

for each $\mathcal{U}\in \mathcal{P}(X)$, where $f_{*}(\mathcal{U})\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(f_{*})_{!}(\mathcal{U})$.
4.
Interaction With Intersections of Families of Subsets. The diagram
commutes, i.e. we have

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

for each $\mathcal{U}\in \mathcal{P}(X)$, where $f_{*}(\mathcal{U})\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(f_{*})_{!}(\mathcal{U})$.
5.
Interaction With Binary Unions. Let $f\colon X\to Y$ be a function. We have a natural transformation
with components

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

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

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

for each $U,V\in \mathcal{P}(X)$.
7.
Interaction With Complements. The diagram
commutes, i.e. we have

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

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

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

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

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

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

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

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

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

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

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

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

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

natural in $U,V\in \mathcal{P}(X)$.
12.
Symmetric Lax Monoidality With Respect to Unions. The codirect image function of Item 1 has a symmetric lax monoidal structure

\[ (f_{*},f^{\otimes }_{*},f^{\otimes }_{*|\mathbb {1}}) \colon (\mathcal{P}(X),\cup ,\text{Ø}) \to (\mathcal{P}(Y),\cup ,\text{Ø}), \]

being equipped with inclusions

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

natural in $U,V\in \mathcal{P}(X)$.
13.
Symmetric Strict Monoidality With Respect to Intersections. The direct image function of Item 1 has a symmetric strict monoidal structure

\[ (f_{*},f^{\otimes }_{*},f^{\otimes }_{*|\mathbb {1}}) \colon (\mathcal{P}(X),\cap ,X) \to (\mathcal{P}(Y),\cap ,Y), \]

being equipped with equalities

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

natural in $U,V\in \mathcal{P}(X)$.
14.
Interaction With Coproducts. Let $f\colon X\to X'$ and $g\colon Y\to Y'$ be maps of sets. The diagram
commutes, i.e. we have

\[ (f\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}g)_{*}(U\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}V)=f_{*}(U)\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}g_{*}(V) \]

for each $U\in \mathcal{P}(X)$ and each $V\in \mathcal{P}(Y)$.
15.
Interaction With Products. Let $f\colon X\to X'$ and $g\colon Y\to Y'$ be maps of sets. The diagram
commutes, i.e. we have

\[ (f\boxtimes _{X\times Y} g)_{*}(U\boxtimes _{X\times Y}V)=f_{*}(U)\boxtimes _{X'\times Y'}g_{*}(V) \]

for each $U\in \mathcal{P}(X)$ and each $V\in \mathcal{P}(Y)$.
16.
Relation to Direct Images. We have

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

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

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

so

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

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

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

so

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

for each $U\in \mathcal{P}(X)$.
19.
Interaction With Bijections I. If $f$ is bijective, then we have

\begin{align*} f^{\mathrm{im}}_{*}(U) & = f_{!}(U),\\ f^{\mathrm{cp}}_{*}(U) & = \text{Ø}, \end{align*}

so $f_{!}=f_{*}$.
20.
Interaction With Bijections II. If $f_{!}=f_{*}$, then $f$ is bijective.

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_{*}(\mathcal{U})}V & = \bigcup _{V\in \left\{ f_{*}(U)\in \mathcal{P}(X)\ \middle |\ U\in \mathcal{U}\right\} }V\\ & = \bigcup _{U\in \mathcal{U}}f_{*}(U).\end{align*}

This finishes the proof.

Item 4: Interaction With Intersections of Families of Subsets

We have

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

This finishes the proof.

Item 5: Interaction With Binary Unions

We have

\begin{align*} f_{*}(U)\cup f_{*}(V) & = f_{!}(U^{\textsf{c}})^{\textsf{c}}\cup f_{!}(V^{\textsf{c}})^{\textsf{c}}\\ & = (f_{!}(U^{\textsf{c}})\cap f_{!}(V^{\textsf{c}}))^{\textsf{c}}\\ & \subset (f_{!}(U^{\textsf{c}}\cap V^{\textsf{c}}))^{\textsf{c}}\\ & = f_{!}((U\cup V)^{\textsf{c}})^{\textsf{c}}\\ & = f_{*}(U\cup V), \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_{!}(U),f^{!}(V)\big ]_{X} & = f_{!}(U)^{\textsf{c}}\cup f_{*}(V)\\ & = f_{*}(U^{\textsf{c}})\cup f_{*}(V)\\ & \subset f_{*}(U^{\textsf{c}}\cup V)\\ & = f_{*}([U,V]_{X}), \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}(X)$ 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_{*}(U)=Y\setminus f_{!}(X\setminus U)$.

•
The First Implication. We claim that

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

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

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

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

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

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

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

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

This finishes the proof of Item 16.

Item 17: Interaction With Injections

If $f$ is injective, then the condition $f^{-1}(y)\subset U$ is equivalent to $f^{-1}(y)\cap U\neq \text{Ø}$ when $y\in \mathrm{Im}(f)$. Thus $f^{\mathrm{im}}_{*}(U)=f_{!}(U)$.

Item 18: Interaction With Surjections

Indeed, we have

\begin{align*} f^{\mathrm{cp}}_{*}(U) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}Y\setminus \mathrm{Im}(f)\\ & = Y\setminus Y\\ & = \text{Ø}. \end{align*}

Since $f^{-1}(y)\subset U$ is a strictly stronger condition than $f^{-1}(y)\cap U\neq \text{Ø}$ when $f^{-1}(y)$ is nonempty, we have $f^{\mathrm{im}}_{*}(U)\subset f_{!}(U)$. Thus $f_{*}(U)\subset f_{!}(U)$.

Item 19: Interaction With Bijections I

This follows from Item 17 and Item 18.

Item 20: Interaction With Bijections II

First, recall from Item 16 that we have

\[ f_{*}(U)=Y\setminus f_{!}(X\setminus U) \]

for all $U\in \mathcal{P}(A)$. We now claim that $f$ is bijective:

•
Injectivity: We proceed in a few steps:
- •
  Choosing $U=\left\{ a\right\} $, we obtain $\left\{ f(a)\right\} =Y\setminus f(X\setminus \left\{ a\right\} )$.
- •
  This implies $\left\{ f(a)\right\} \cap f(X\setminus \left\{ a\right\} )=\text{Ø}$.
- •
  Thus there can be no $a'\in X$ other than $a$ with $f(a')=f(a)$.
•
Surjectivity: Choosing $U=X$ gives $f_{*}(X)=Y$. But since $f_{!}=f_{*}$, we have $f_{!}(X)=Y$, so $f$ must be surjective.

This finishes the proof.

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

\[ (-)_{!|X,Y}\colon \mathsf{Sets}(X,Y) \to \mathsf{Sets}(\mathcal{P}(X),\mathcal{P}(Y)). \]
2.
Functionality II. The assignment $f\mapsto f_{*}$ defines a function

\[ (-)_{!|X,Y}\colon \mathsf{Sets}(X,Y) \to \mathsf{Pos}((\mathcal{P}(X),\subset ),(\mathcal{P}(Y),\subset )). \]
3.
Interaction With Identities. For each $X\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$, we have

\[ (\operatorname {\mathrm{id}}_{X})_{*}=\operatorname {\mathrm{id}}_{\mathcal{P}(X)}. \]
4.
Interaction With Composition. For each pair of composable functions $f\colon X\to Y$ and $g\colon Y\to Z$, we have