The assignment $X\mapsto \mathcal{P}(X)$ together with the functors $f_{!}$, $f^{-1}$, and $f_{*}$ of Item 1 of Proposition 4.6.1.1.5, Item 1 of Proposition 4.6.2.1.3, and Item 1 of Proposition 4.6.3.1.7, and the functors
\begin{align*} -_{1}\cap -_{2} & \colon \mathcal{P}(X)\times \mathcal{P}(X) \to \mathcal{P}(X),\\ [-_{1},-_{2}]_{X} & \colon \mathcal{P}(X)^{\mathsf{op}}\times \mathcal{P}(X) \to \mathcal{P}(X) \end{align*}
of Item 1 of Proposition 4.3.9.1.2 and Item 1 of Proposition 4.4.7.1.3 satisfy several properties reminiscent of a six functor formalism in the sense of 
.
We collect these properties in Proposition 4.6.4.1.2 below.
Item 1: The Beck–Chevalley Condition
We have
\begin{align*} [g^{-1}\circ f_{!}](U) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}g^{-1}(f_{!}(U))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ y\in Y\ \middle |\ g(y)\in f_{!}(U)\right\} \\ & = \left\{ y\in Y\ \middle |\ \begin{aligned} & \text{there exists some $x\in U$}\\ & \text{such that $f(x)=g(y)$}\end{aligned}\right\} \\ & = \left\{ y\in Y\ \middle |\ \begin{aligned} & \text{there exists some}\\ & \text{$(x,y)\in \left\{ (x,y)\in X\times _{Z}Y\ \middle |\ x\in U\right\} $}\end{aligned}\right\} \\ & = \left\{ y\in Y\ \middle |\ \begin{aligned} & \text{there exists some}\\ & \text{$(x,y)\in \left\{ (x,y)\in X\times _{Z}Y\ \middle |\ x\in U\right\} $}\\ & \text{such that $y=y$}\end{aligned}\right\} \\ & = \left\{ y\in Y\ \middle |\ \begin{aligned} & \text{there exists some}\\ & \text{$(x,y)\in \left\{ (x,y)\in X\times _{Z}Y\ \middle |\ x\in U\right\} $}\\ & \text{such that $\operatorname {\mathrm{\mathrm{pr}}}_{2}(x,y)=y$}\end{aligned}\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(\operatorname {\mathrm{\mathrm{pr}}}_{2})_{!}(\left\{ (x,y)\in X\times _{Z}Y\ \middle |\ x\in U\right\} )\\ & = (\operatorname {\mathrm{\mathrm{pr}}}_{2})_{!}(\left\{ (x,y)\in X\times _{Z}Y\ \middle |\ \operatorname {\mathrm{\mathrm{pr}}}_{1}(x,y)\in U\right\} )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(\operatorname {\mathrm{\mathrm{pr}}}_{2})_{!}(\operatorname {\mathrm{\mathrm{pr}}}^{-1}_{1}(U))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[(\operatorname {\mathrm{\mathrm{pr}}}_{2})_{!}\circ \operatorname {\mathrm{\mathrm{pr}}}^{-1}_{1}](U) \end{align*}
for each $U\in \mathcal{P}(X)$. Therefore, we have
\[ g^{-1}\circ f_{!}=(\operatorname {\mathrm{\mathrm{pr}}}_{2})_{!}\circ \operatorname {\mathrm{\mathrm{pr}}}^{-1}_{1}. \]
For the second equality, we have
\begin{align*} [f^{-1}\circ g_{!}](U) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f^{-1}(g_{!}(U))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ x\in X\ \middle |\ f(x)\in g_{!}(V)\right\} \\ & = \left\{ x\in X\ \middle |\ \begin{aligned} & \text{there exists some $y\in V$}\\ & \text{such that $f(x)=g(y)$}\end{aligned}\right\} \\ & = \left\{ x\in X\ \middle |\ \begin{aligned} & \text{there exists some}\\ & \text{$(x,y)\in \left\{ (x,y)\in X\times _{Z}Y\ \middle |\ y\in V\right\} $}\end{aligned}\right\} \\ & = \left\{ x\in X\ \middle |\ \begin{aligned} & \text{there exists some}\\ & \text{$(x,y)\in \left\{ (x,y)\in X\times _{Z}Y\ \middle |\ y\in V\right\} $}\\ & \text{such that $x=x$}\end{aligned}\right\} \\ & = \left\{ x\in X\ \middle |\ \begin{aligned} & \text{there exists some}\\ & \text{$(x,y)\in \left\{ (x,y)\in X\times _{Z}Y\ \middle |\ y\in V\right\} $}\\ & \text{such that $\operatorname {\mathrm{\mathrm{pr}}}_{1}(x,y)=x$}\end{aligned}\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(\operatorname {\mathrm{\mathrm{pr}}}_{1})_{!}(\left\{ (x,y)\in X\times _{Z}Y\ \middle |\ y\in V\right\} )\\ & = (\operatorname {\mathrm{\mathrm{pr}}}_{1})_{!}(\left\{ (x,y)\in X\times _{Z}Y\ \middle |\ \operatorname {\mathrm{\mathrm{pr}}}_{2}(x,y)\in V\right\} )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(\operatorname {\mathrm{\mathrm{pr}}}_{1})_{!}(\operatorname {\mathrm{\mathrm{pr}}}^{-1}_{2}(V))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[(\operatorname {\mathrm{\mathrm{pr}}}_{1})_{!}\circ \operatorname {\mathrm{\mathrm{pr}}}^{-1}_{2}](V) \end{align*}
for each $V\in \mathcal{P}(Y)$. Therefore, we have
\[ f^{-1}\circ g_{!}=(\operatorname {\mathrm{\mathrm{pr}}}_{1})_{!}\circ \operatorname {\mathrm{\mathrm{pr}}}^{-1}_{2}. \]
This finishes the proof.
Item 2: The Projection Formula I
We claim that
\[ f_{!}(U)\cap V\subset f_{!}(U\cap f^{-1}(V)). \]
Indeed, we have
\begin{align*} f_{!}(U)\cap V & \subset f_{!}(U)\cap f_{!}(f^{-1}(V))\\ & = f_{!}(U\cap f^{-1}(V)), \end{align*}
where we have used:
-
1.
Item 2 of Proposition 4.6.1.1.5 for the inclusion.
-
2.
Item 6 of Proposition 4.6.1.1.5 for the equality.
Conversely, we claim that
\[ f_{!}(U\cap f^{-1}(V))\subset f_{!}(U)\cap V. \]
Indeed:
-
1.
Let $y\in f_{!}(U\cap f^{-1}(V))$.
-
2.
Since $y\in f_{!}(U\cap f^{-1}(V))$, there exists some $x\in U\cap f^{-1}(V)$ such that $f(x)=y$.
-
3.
Since $x\in U\cap f^{-1}(V)$, we have $x\in U$, and thus $f(x)\in f_{!}(U)$.
-
4.
Since $x\in U\cap f^{-1}(V)$, we have $x\in f^{-1}(V)$, and thus $f(x)\in V$.
-
5.
Since $f(x)\in f_{!}(U)$ and $f(x)\in V$, we have $f(x)\in f_{!}(U)\cap V$.
-
6.
But $y=f(x)$, so $y\in f_{!}(U)\cap V$.
-
7.
Thus $f_{!}(U\cap f^{-1}(V))\subset f_{!}(U)\cap V$.
This finishes the proof.
Item 3: The Projection Formula II
We have
\begin{align*} f_{*}(U)\cap V & \subset f_{*}(U)\cap f_{*}(f^{-1}(V))\\ & = f_{*}(U\cap f^{-1}(V)), \end{align*}
where we have used:
-
1.
Item 2 of Proposition 4.6.3.1.7 for the inclusion.
