The Clowder Project

Let $X$ be a set.

1. 1.

   The Projection Formula I. The diagram

   
   commutes, i.e. we have
   \[ R_{!}(U\cap R_{-1}(V))=R_{!}(U)\cap V \]

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

2. 2.

   The Projection Formula II. We have a natural transformation

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

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

3. 3.

   Interaction Between Co/Direct Images and Internal Homs of Powersets. The diagram

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

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

4. 4.

   Interaction Between Co/Inverse Images and Internal Homs of Powersets. The diagram

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

   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 Chapter 4: Constructions With Sets, Item 5 of Proposition 4.4.1.1.4. Moreover, the following conditions are satisfied:

   1. (a)

      Interaction With Direct Images. Let $R\colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}X'$ and $S\colon Y\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}Y'$ be relations. The diagram

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

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

   2. (b)

      Interaction With Coinverse Images. Let $R\colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}X'$ and $S\colon Y\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}Y'$ be relations. The diagram

      
      commutes, i.e. we have
      \[ [R_{-1}\times S_{-1}](U\boxtimes _{X'\times Y'}V)=R_{-1}(U)\boxtimes _{X\times Y}S_{-1}(V) \]

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

   3. (c)

      Interaction With Inverse Images. Let $R\colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}X'$ and $S\colon Y\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}Y'$ be relations. The diagram

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

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

   4. (d)

      Interaction With Codirect Images. Let $R\colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}X'$ and $S\colon Y\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}Y'$ be relations. The diagram

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

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

   5. (e)

      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 Chapter 4: Constructions With Sets, 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
      \[ R_{!}(D_{X}(U))=D_{Y}(R_{*}(U)) \]

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

   4. (d)

      Interaction With Coinverse Images. The diagram

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

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