The Clowder Project

Let $X$ be a set.

1. 1.

   The Beck–Chevalley Condition. Let

   
   be a pullback diagram in $\mathsf{Sets}$. We have
   

2. 2.

   The Projection Formula I. The diagram

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

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

3. 3.

   The Projection Formula II. We have a natural transformation

   
   with components
   \[ f_{*}\webleft (U\webright )\cap V\subset f_{*}\webleft (U\cap f^{-1}\webleft (V\webright )\webright ) \]

   indexed by $U\in \mathcal{P}\webleft (X\webright )$ and $V\in \mathcal{P}\webleft (Y\webright )$.

4. 4.

   Strong Closed Monoidality. The diagram

   
   commutes, i.e. we have an equality of sets
   \[ f^{-1}\webleft (\webleft [U,V\webright ]_{Y}\webright )=\webleft [f^{-1}\webleft (U\webright ),f^{-1}\webleft (V\webright )\webright ]_{X}, \]

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

5. 5.

   The External Tensor Product. We have an external tensor product

   \[ -_{1}\boxtimes _{X\times Y}-_{2}\colon \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright )\to \mathcal{P}\webleft (X\times Y\webright ) \]

   given by

   \begin{align*} U\boxtimes _{X\times Y}V & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\operatorname {\mathrm{\mathrm{pr}}}^{-1}_{1}\webleft (U\webright )\cap \operatorname {\mathrm{\mathrm{pr}}}^{-1}_{2}\webleft (V\webright )\\ & = \left\{ \webleft (u,v\webright )\in X\times Y\ \middle |\ \text{$u\in U$ and $v\in V$}\right\} . \end{align*}

   This is the same map as the one in Item 5 of Proposition 4.4.1.1.4. Moreover, the following conditions are satisfied:

   1. (a)

      Interaction With Direct Images. Let $f\colon X\to X'$ and $g\colon Y\to Y'$ be functions. The diagram

      
      commutes, i.e. we have
      \[ \webleft [f_{!}\times g_{!}\webright ]\webleft (U\boxtimes _{X\times Y}V\webright )=f_{!}\webleft (U\webright )\boxtimes _{X'\times Y'}g_{!}\webleft (V\webright ) \]

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

   2. (b)

      Interaction With Inverse Images. Let $f\colon X\to X'$ and $g\colon Y\to Y'$ be functions. The diagram

      
      commutes, i.e. we have
      \[ \webleft [f^{-1}\times g^{-1}\webright ]\webleft (U\boxtimes _{X'\times Y'}V\webright )=f^{-1}\webleft (U\webright )\boxtimes _{X\times Y}g^{-1}\webleft (V\webright ) \]

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

   3. (c)

      Interaction With Codirect Images. Let $f\colon X\to X'$ and $g\colon Y\to Y'$ be functions. The diagram

      
      commutes, i.e. we have
      \[ \webleft [f_{*}\times g_{*}\webright ]\webleft (U\boxtimes _{X\times Y}V\webright )=f_{*}\webleft (U\webright )\boxtimes _{X'\times Y'}g_{*}\webleft (V\webright ) \]

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

   4. (d)

      Interaction With Diagonals. The diagram

      
      i.e. we have
      \[ U\cap V=\Delta ^{-1}_{X}\webleft (U\boxtimes _{X\times X}V\webright ) \]

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

6. 6.

   The Dualisation Functor. We have a functor

   \[ D_{X}\colon \mathcal{P}\webleft (X\webright )^{\mathsf{op}}\to \mathcal{P}\webleft (X\webright ) \]

   given by

   \begin{align*} D_{X}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [U,\text{Ø}\webright ]_{X}\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}U^{\textsf{c}} \end{align*}

   for each $U\in \mathcal{P}\webleft (X\webright )$, as in Item 5 of Proposition 4.4.7.1.3, satisfying the following conditions:

   1. (a)

      Duality. We have

      

   2. (b)

      Duality. The diagram

      
      commutes, i.e. we have
      \[ \underbrace{D_{X}\webleft (U\cap D_{X}\webleft (V\webright )\webright )}_{\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [U\cap \webleft [V,\text{Ø}\webright ]_{X},\text{Ø}\webright ]_{X}}=\webleft [U,V\webright ]_{X} \]

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

   3. (c)

      Interaction With Direct Images. The diagram

      
      commutes, i.e. we have
      \[ f_{!}\webleft (D_{X}\webleft (U\webright )\webright )=D_{Y}\webleft (f_{*}\webleft (U\webright )\webright ) \]

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

   4. (d)

      Interaction With Inverse Images. The diagram

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

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

   5. (e)

      Interaction With Codirect Images. The diagram

      
      commutes, i.e. we have
      \[ f_{*}\webleft (D_{X}\webleft (U\webright )\webright )=D_{Y}\webleft (f_{!}\webleft (U\webright )\webright ) \]

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