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:
-
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 )$.
-
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:
-
Units and counits of the form
-
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 )$.
