Let $f\colon A\to B$ be a function.
-
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
-
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:
- The following conditions are equivalent:
- We have $f_{*}\webleft (U\webright )\subset V$.
- We have $U\subset f^{-1}\webleft (V\webright )$.
- The following conditions are equivalent:
- We have $f^{-1}\webleft (U\webright )\subset V$.
- We have $U\subset f_{!}\webleft (V\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 (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 )$.
-
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 )$.
-
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 )$.
-
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 )$.
-
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 )$.
-
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 )$.
-
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 )$.