The Clowder Project

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:

   • If $U\subset V$, then $f_{!}\webleft (U\webright )\subset f_{!}\webleft (V\webright )$.

2. Triple Adjointness. We have a triple adjunction
   
   witnessed by:
   1. 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 )$.

   2. 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:

      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. 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_{!}\webleft(\bigcup _{i\in I}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\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_{!}\webleft(\bigcap _{i\in I}U_{i}\webright)=\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 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 direct image with compact support 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_{!,\text{im}}\webleft (U\webright ) = f_{*}\webleft (U\webright ),\\ f_{!,\text{cp}}\webleft (U\webright ) = Y\setminus \mathrm{Im}\webleft (f\webright ),\\ \begin{aligned} f_{!}\webleft (U\webright ) & = f_{!,\text{im}}\webleft (U\webright )\cup f_{!,\text{cp}}\webleft (U\webright )\\ & = f_{*}\webleft (U\webright )\cup \webleft (Y\setminus \mathrm{Im}\webleft (f\webright )\webright ) \end{aligned}\end{gather*}

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

18. Interaction With Surjections. If $f$ is surjective, then we have
    \begin{align*} f_{!,\text{im}}\webleft (U\webright ) & \subset f_{*}\webleft (U\webright ),\\ f_{!,\text{cp}}\webleft (U\webright ) & = \text{Ø},\\ f_{!}\webleft (U\webright ) & \subset f_{*}\webleft (U\webright ) \end{align*}

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