The Clowder Project

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

1. 1.

   Functoriality. The assignment $V\mapsto f^{-1}\webleft (V\webright )$ defines a functor

   \[ f^{-1}\colon \webleft (\mathcal{P}\webleft (Y\webright ),\subset \webright )\to \webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ). \]

   In particular, for each $U,V\in \mathcal{P}\webleft (Y\webright )$, the following condition is satisfied:

   • (★)
   If $U\subset V$, then $f^{-1}\webleft (U\webright )\subset f^{-1}\webleft (V\webright )$.
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}\webleft (X\webright )} & \hookrightarrow f^{-1}\circ f_{!},\\ f_{!}\circ f^{-1} & \hookrightarrow \operatorname {\mathrm{id}}_{\mathcal{P}\webleft (Y\webright )},\\ \end{aligned} \qquad \begin{aligned} \operatorname {\mathrm{id}}_{\mathcal{P}\webleft (Y\webright )} & \hookrightarrow f_{*}\circ f^{-1},\\ f^{-1}\circ f_{*} & \hookrightarrow \operatorname {\mathrm{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. (b)

      Bijections of sets

      \begin{align*} \operatorname {\mathrm{Hom}}_{\mathcal{P}\webleft (Y\webright )}\webleft (f_{!}\webleft (U\webright ),V\webright ) & \cong \operatorname {\mathrm{Hom}}_{\mathcal{P}\webleft (X\webright )}\webleft (U,f^{-1}\webleft (V\webright )\webright ),\\ \operatorname {\mathrm{Hom}}_{\mathcal{P}\webleft (X\webright )}\webleft (f^{-1}\webleft (U\webright ),V\webright ) & \cong \operatorname {\mathrm{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. (i)

         The following conditions are equivalent:

         1. (I)

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

         2. (II)

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

      2. (ii)

         The following conditions are equivalent:

         1. (I)

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

         2. (II)

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

3. 3.

   Interaction With Unions of Families of Subsets. The diagram

   
   commutes, i.e. we have
   \[ \bigcup _{V\in \mathcal{V}}f^{-1}\webleft (V\webright )=\bigcup _{U\in f^{-1}\webleft (\mathcal{U}\webright )}U \]

   for each $\mathcal{V}\in \mathcal{P}\webleft (Y\webright )$, where $f^{-1}\webleft (\mathcal{V}\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (f^{-1}\webright )^{-1}\webleft (\mathcal{V}\webright )$.

4. 4.

   Interaction With Intersections of Families of Subsets. The diagram

   
   commutes, i.e. we have
   \[ \bigcap _{V\in \mathcal{V}}f^{-1}\webleft (V\webright )=\bigcap _{U\in f^{-1}\webleft (\mathcal{U}\webright )}U \]

   for each $\mathcal{V}\in \mathcal{P}\webleft (Y\webright )$, where $f^{-1}\webleft (\mathcal{V}\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (f^{-1}\webright )^{-1}\webleft (\mathcal{V}\webright )$.

5. 5.

   Interaction With Binary Unions. The diagram

   
   commutes, i.e. we have
   \[ f^{-1}\webleft (U\cup V\webright )=f^{-1}\webleft (U\webright )\cup f^{-1}\webleft (V\webright ) \]

   for each $U,V\in \mathcal{P}\webleft (Y\webright )$.

6. 6.

   Interaction With Binary Intersections. The diagram

   
   commutes, i.e. we have
   \[ f^{-1}\webleft (U\cap V\webright )=f^{-1}\webleft (U\webright )\cap f^{-1}\webleft (V\webright ) \]

   for each $U,V\in \mathcal{P}\webleft (Y\webright )$.

7. 7.

   Interaction With Differences. The diagram

   
   commutes, i.e. we have
   \[ f^{-1}\webleft (U\setminus V\webright )=f^{-1}\webleft (U\webright )\setminus f^{-1}\webleft (V\webright ) \]

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

8. 8.

   Interaction With Complements. The diagram

   
   commutes, i.e. we have
   \[ f^{-1}\webleft (U^{\textsf{c}}\webright )=f^{-1}\webleft (U\webright )^{\textsf{c}} \]

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

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

1. 1.

   Functionality I. The assignment $f\mapsto f^{-1}$ defines a function

   \[ \webleft (-\webright )^{-1}_{X,Y}\colon \mathsf{Sets}\webleft (X,Y\webright ) \to \mathsf{Sets}\webleft (\mathcal{P}\webleft (Y\webright ),\mathcal{P}\webleft (X\webright )\webright ). \]
2. 2.

   Functionality II. The assignment $f\mapsto f^{-1}$ defines a function

   \[ \webleft (-\webright )^{-1}_{X,Y}\colon \mathsf{Sets}\webleft (X,Y\webright ) \to \mathsf{Pos}\webleft (\webleft (\mathcal{P}\webleft (Y\webright ),\subset \webright ),\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright )\webright ). \]
3. 3.

   Interaction With Identities. For each $X\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$, we have

   \[ \operatorname {\mathrm{id}}^{-1}_{X}=\operatorname {\mathrm{id}}_{\mathcal{P}\webleft (X\webright )}. \]
4. 4.

   Interaction With Composition. For each pair of composable functions $f\colon X\to Y$ and $g\colon Y\to Z$, we have