The Clowder Project

Let $f\colon A\to B$ be a function.

1. Functoriality. The assignment $V\mapsto f^{-1}\webleft (V\webright )$ defines a functor
   \[ f^{-1}\colon \webleft (\mathcal{P}\webleft (B\webright ),\subset \webright )\to \webleft (\mathcal{P}\webleft (A\webright ),\subset \webright ) \]

   where

   • Action on Objects. For each $V\in \mathcal{P}\webleft (B\webright )$, we have
     \[ \webleft [f^{-1}\webright ]\webleft (V\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f^{-1}\webleft (V\webright ). \]

   • Action on Morphisms. For each $U,V\in \mathcal{P}\webleft (B\webright )$:
     • If $U\subset V$, then $f^{-1}\webleft (U\webright )\subset f^{-1}\webleft (V\webright )$.

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

   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. Preservation of Colimits. We have an equality of sets
   \[ f^{-1}\webleft (\bigcup _{i\in I}U_{i}\webright )=\bigcup _{i\in I}f^{-1}\webleft (U_{i}\webright ), \]

   natural in $\webleft\{ U_{i}\webright\} _{i\in I}\in \mathcal{P}\webleft (B\webright )^{\times I}$. In particular, we have equalities

   \[ \begin{gathered} f^{-1}\webleft (U\webright )\cup f^{-1}\webleft (V\webright ) = f^{-1}\webleft (U\cup V\webright ),\\ f^{-1}\webleft (\emptyset \webright ) = \emptyset , \end{gathered} \]

   natural in $U,V\in \mathcal{P}\webleft (B\webright )$.

4. Preservation of Limits. We have an equality of sets
   \[ f^{-1}\webleft (\bigcap _{i\in I}U_{i}\webright )=\bigcap _{i\in I}f^{-1}\webleft (U_{i}\webright ), \]

   natural in $\webleft\{ U_{i}\webright\} _{i\in I}\in \mathcal{P}\webleft (B\webright )^{\times I}$. In particular, we have equalities

   \[ \begin{gathered} f^{-1}\webleft (U\webright )\cap f^{-1}\webleft (V\webright ) = f^{-1}\webleft (U\cap V\webright ),\\ f^{-1}\webleft (B\webright ) = A, \end{gathered} \]

   natural in $U,V\in \mathcal{P}\webleft (B\webright )$.

5. Symmetric Strict Monoidality With Respect to Unions. The inverse image function of Item 1 has a symmetric strict monoidal structure
   \[ \webleft (f^{-1},f^{-1,\otimes },f^{-1,\otimes }_{\mathbb {1}}\webright ) \colon \webleft (\mathcal{P}\webleft (B\webright ),\cup ,\emptyset \webright ) \to \webleft (\mathcal{P}\webleft (A\webright ),\cup ,\emptyset \webright ), \]

   being equipped with equalities

   \[ \begin{gathered} f^{-1,\otimes }_{U,V} \colon f^{-1}\webleft (U\webright )\cup f^{-1}\webleft (V\webright ) \mathbin {\overset {=}{\rightarrow }}f^{-1}\webleft (U\cup V\webright ),\\ f^{-1,\otimes }_{\mathbb {1}} \colon \emptyset \mathbin {\overset {=}{\rightarrow }}f^{-1}\webleft (\emptyset \webright ), \end{gathered} \]

   natural in $U,V\in \mathcal{P}\webleft (B\webright )$.

6. Symmetric Strict Monoidality With Respect to Intersections. The inverse image function of Item 1 has a symmetric strict monoidal structure
   \[ \webleft (f^{-1},f^{-1,\otimes },f^{-1,\otimes }_{\mathbb {1}}\webright ) \colon \webleft (\mathcal{P}\webleft (B\webright ),\cap ,B\webright ) \to \webleft (\mathcal{P}\webleft (A\webright ),\cap ,A\webright ), \]

   being equipped with equalities

   \[ \begin{gathered} f^{-1,\otimes }_{U,V} \colon f^{-1}\webleft (U\webright )\cap f^{-1}\webleft (V\webright ) \mathbin {\overset {=}{\rightarrow }}f^{-1}\webleft (U\cap V\webright ),\\ f^{-1,\otimes }_{\mathbb {1}} \colon A \mathbin {\overset {=}{\rightarrow }}f^{-1}\webleft (B\webright ), \end{gathered} \]

   natural in $U,V\in \mathcal{P}\webleft (B\webright )$.

7. 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 )^{-1}\webleft (U'\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}V'\webright )=f^{-1}\webleft (U'\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}g^{-1}\webleft (V'\webright ) \]

   for each $U'\in \mathcal{P}\webleft (A'\webright )$ and each $V'\in \mathcal{P}\webleft (B'\webright )$.

8. 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 )^{-1}\webleft (U'\times V'\webright )=f^{-1}\webleft (U'\webright )\times g^{-1}\webleft (V'\webright ) \]

   for each $U'\in \mathcal{P}\webleft (A'\webright )$ and each $V'\in \mathcal{P}\webleft (B'\webright )$.

Let $f\colon A\to B$ be a function.

1. Functionality I. The assignment $f\mapsto f^{-1}$ defines a function
   \[ \webleft (-\webright )^{-1}_{A,B}\colon \mathsf{Sets}\webleft (A,B\webright ) \to \mathsf{Sets}\webleft (\mathcal{P}\webleft (B\webright ),\mathcal{P}\webleft (A\webright )\webright ). \]
2. Functionality II. The assignment $f\mapsto f^{-1}$ defines a function
   \[ \webleft (-\webright )^{-1}_{A,B}\colon \mathsf{Sets}\webleft (A,B\webright ) \to \mathsf{Pos}\webleft (\webleft (\mathcal{P}\webleft (B\webright ),\subset \webright ),\webleft (\mathcal{P}\webleft (A\webright ),\subset \webright )\webright ). \]
3. Interaction With Identities. For each $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, we have
   \[ \text{id}^{-1}_{A}=\text{id}_{\mathcal{P}\webleft (A\webright )}. \]
4. Interaction With Composition. For each pair of composable functions $f\colon A\to B$ and $g\colon B\to C$, we have