The Clowder Project

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

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

   • (★)
   If $U\subset V$, then $f_{!}(U)\subset f_{!}(V)$.
2. 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:

         1. (I)

            We have $f_{!}(U)\subset V$.

         2. (II)

            We have $U\subset f^{-1}(V)$.

      2. (ii)

         The following conditions are equivalent:

         1. (I)

            We have $f^{-1}(U)\subset V$.

         2. (II)

            We have $U\subset f_{*}(V)$.

3. 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. 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. 5.

   Interaction With Binary Unions. The diagram

   
   commutes, i.e. we have
   \[ f_{!}(U\cup V)=f_{!}(U)\cup f_{!}(V) \]

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

6. 6.

   Interaction With Binary Intersections. We have a natural transformation

   
   with components
   \[ f_{!}(U\cap V)\subset f_{!}(U)\cap f_{!}(V) \]

   indexed by $U,V\in \mathcal{P}(X)$.

7. 7.

   Interaction With Differences. We have a natural transformation

   
   with components
   \[ f_{!}(U)\setminus f_{!}(V)\subset f_{!}(U\setminus V) \]

   indexed by $U,V\in \mathcal{P}(X)$.

8. 8.

   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)$.

9. 9.

   Interaction With Symmetric Differences. We have a natural transformation

   
   with components
   \[ f_{!}(U)\mathbin {\triangle }f_{!}(V)\subset f_{!}(U\mathbin {\triangle }V) \]

   indexed by $U,V\in \mathcal{P}(X)$.

10. 10.

    Interaction With Internal Homs of Powersets. The diagram

    
    commutes, i.e. we have an equality of sets
    \[ f_{!}([U,V]_{X})=[f_{*}(U),f_{!}(V)]_{Y}, \]

    natural in $U,V\in \mathcal{P}(X)$.

11. 11.

    Preservation of Colimits. We have an equality of sets

    \[ f_{!}\left(\bigcup _{i\in I}U_{i}\right)=\bigcup _{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_{!}(U)\cup f_{!}(V) = f_{!}(U\cup V),\\ f_{!}(\text{Ø}) = \text{Ø}, \end{gathered} \]

    natural in $U,V\in \mathcal{P}(X)$.

12. 12.

    Oplax Preservation of Limits. We have an inclusion of sets

    \[ f_{!}\left(\bigcap _{i\in I}U_{i}\right)\subset \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 inclusions

    \[ \begin{gathered} f_{!}(U\cap V) \subset f_{!}(U)\cap f_{!}(V),\\ f_{!}(X) \subset Y, \end{gathered} \]

    natural in $U,V\in \mathcal{P}(X)$.

13. 13.

    Symmetric Strict Monoidality With Respect to Unions. The direct image function of Item 1 has a symmetric strict monoidal structure

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

    being equipped with equalities

    \[ \begin{gathered} f^{\otimes }_{!|U,V} \colon f_{!}(U)\cup f_{!}(V) \mathbin {\overset {=}{\rightarrow }}f_{!}(U\cup V),\\ f^{\otimes }_{!|\mathbb {1}} \colon \text{Ø}\mathbin {\overset {=}{\rightarrow }}\text{Ø}, \end{gathered} \]

    natural in $U,V\in \mathcal{P}(X)$.

14. 14.

    Symmetric Oplax Monoidality With Respect to Intersections. The direct image function of Item 1 has a symmetric oplax monoidal structure

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

    being equipped with inclusions

    \[ \begin{gathered} f^{\otimes }_{!|U,V} \colon f_{!}(U\cap V) \hookrightarrow f_{!}(U)\cap f_{!}(V),\\ f^{\otimes }_{!|\mathbb {1}} \colon f_{!}(X) \hookrightarrow Y, \end{gathered} \]

    natural in $U,V\in \mathcal{P}(X)$.

15. 15.

    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)$.

16. 16.

    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)$.

17. 17.

    Relation to Codirect Images. We 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*}

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

Let $f\colon X\to Y$ and $g\colon Y\to Z$ be functions.

1. 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. 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. 3.

   Interaction With Identities. We have

   \[ (\operatorname {\mathrm{id}}_{X})_{!}=\operatorname {\mathrm{id}}_{\mathcal{P}(X)}. \]
4. 4.

   Interaction With Composition. We have