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.
-
2.
Item 6 of Proposition 4.6.3.1.7 for the equality.
Since $\mathcal{P}(Y)$ is posetal, naturality is automatic (Chapter 11: Categories, Item 4 of Proposition 11.2.7.1.2).
Item 4: Strong Closed Monoidality
This is a repetition of Item 19 of Proposition 4.4.7.1.3 and is proved there.
Item 5: The External Tensor Product
We have
\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)\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (x,y)\in X\times Y\ \middle |\ \operatorname {\mathrm{\mathrm{pr}}}_{1}(x,y)\in U\right\} \\ & \phantom{={}} \mkern 4mu\cup \left\{ (x,y)\in X\times Y\ \middle |\ \operatorname {\mathrm{\mathrm{pr}}}_{2}(x,y)\in V\right\} \\ & = \left\{ (x,y)\in X\times Y\ \middle |\ x\in U\right\} \\ & \phantom{={}} \mkern 4mu\cup \left\{ (x,y)\in X\times Y\ \middle |\ y\in V\right\} \\ & = \left\{ (x,y)\in X\times Y\ \middle |\ \text{$x\in U$ and $y\in V$}\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}U\times V. \end{align*}
Next, we claim that Item 5a, Item 5b, Item 5c, and Item 5d are indeed true:
-
1.
Proof of Item 5a: This is a repetition of Item 16 of Proposition 4.6.1.1.5 and is proved there.
-
2.
Proof of Item 5b: This is a repetition of Item 16 of Proposition 4.6.2.1.3 and is proved there.
-
3.
Proof of Item 5c: This is a repetition of Item 15 of Proposition 4.6.3.1.7 and is proved there.
-
4.
Proof of Item 5d: We have
\begin{align*} \Delta ^{-1}_{X}(U\boxtimes _{X\times X}V) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ x\in X\ \middle |\ (x,x)\in U\boxtimes _{X\times X}V\right\} \\ & = \left\{ x\in X\ \middle |\ (x,x)\in \left\{ (u,v)\in X\times X\ \middle |\ \text{$u\in U$ and $v\in V$}\right\} \right\} \\ & = U\cap V.\end{align*}
This finishes the proof.
Item 6: The Dualisation Functor
This is a repetition of Item 5 and Item 6 of Proposition 4.4.7.1.3 and is proved there.
. 
