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_{!}(U\cap f^{-1}(V))=f_{!}(U)\cap V \]

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

3. 3.

   The Projection Formula II. We have a natural transformation

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

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

4. 4.

   Strong Closed Monoidality. The diagram

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

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

5. 5.

   The External Tensor Product. We have an external tensor product

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

   given by

   \begin{align*} U\boxtimes _{X\times Y}V & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\operatorname {\mathrm{\mathrm{pr}}}^{-1}_{1}(U)\cap \operatorname {\mathrm{\mathrm{pr}}}^{-1}_{2}(V)\\ & = \left\{ (u,v)\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
      \[ [f_{!}\times g_{!}](U\boxtimes _{X\times Y}V)=f_{!}(U)\boxtimes _{X'\times Y'}g_{!}(V) \]

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

   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
      \[ [f^{-1}\times g^{-1}](U\boxtimes _{X'\times Y'}V)=f^{-1}(U)\boxtimes _{X\times Y}g^{-1}(V) \]

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

   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
      \[ [f_{*}\times g_{*}](U\boxtimes _{X\times Y}V)=f_{*}(U)\boxtimes _{X'\times Y'}g_{*}(V) \]

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

   4. (d)

      Interaction With Diagonals. The diagram

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

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

6. 6.

   The Dualisation Functor. We have a functor

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

   given by

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

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

   1. (a)

      Duality. We have

      

   2. (b)

      Interaction With Internal Homs. The diagram

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

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

   3. (c)

      Interaction With Direct Images. The diagram

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

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

   4. (d)

      Interaction With Inverse Images. The diagram

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

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

   5. (e)

      Interaction With Codirect Images. The diagram

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

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