Item 1: The Beck–Chevalley Condition
We have
\begin{align*} \webleft [g^{-1}\circ f_{*}\webright ]\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}g^{-1}\webleft (f_{*}\webleft (U\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ y\in Y\ \middle |\ g\webleft (y\webright )\in f_{*}\webleft (U\webright )\webright\} \\ & = \webleft\{ y\in Y\ \middle |\ \begin{aligned} & \text{there exists some $x\in U$}\\ & \text{such that $f\webleft (x\webright )=g\webleft (y\webright )$}\end{aligned}\webright\} \\ & = \webleft\{ y\in Y\ \middle |\ \begin{aligned} & \text{there exists some}\\ & \text{$(x,y)\in \webleft\{ (x,y)\in X\times _{Z}Y\ \middle |\ x\in U\webright\} $}\end{aligned}\webright\} \\ & = \webleft\{ y\in Y\ \middle |\ \begin{aligned} & \text{there exists some}\\ & \text{$(x,y)\in \webleft\{ (x,y)\in X\times _{Z}Y\ \middle |\ x\in U\webright\} $}\\ & \text{such that $y=y$}\end{aligned}\webright\} \\ & = \webleft\{ y\in Y\ \middle |\ \begin{aligned} & \text{there exists some}\\ & \text{$(x,y)\in \webleft\{ (x,y)\in X\times _{Z}Y\ \middle |\ x\in U\webright\} $}\\ & \text{such that $\text{pr}_{2}\webleft (x,y\webright )=y$}\end{aligned}\webright\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\text{pr}_{2}\webright )_{*}\webleft (\webleft\{ \webleft (x,y\webright )\in X\times _{Z}Y\ \middle |\ x\in U\webright\} \webright )\\ & = \webleft (\text{pr}_{2}\webright )_{*}\webleft (\webleft\{ \webleft (x,y\webright )\in X\times _{Z}Y\ \middle |\ \text{pr}_{1}\webleft (x,y\webright )\in U\webright\} \webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\text{pr}_{2}\webright )_{*}\webleft (\text{pr}^{-1}_{1}\webleft (U\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [\webleft (\text{pr}_{2}\webright )_{*}\circ \text{pr}^{-1}_{1}\webright ]\webleft (U\webright ) \end{align*}
for each $U\in \mathcal{P}\webleft (X\webright )$. Therefore, we have
\[ g^{-1}\circ f_{*}=\webleft (\text{pr}_{2}\webright )_{*}\circ \text{pr}^{-1}_{1}. \]
For the second equality, we have
\begin{align*} \webleft [f^{-1}\circ g_{*}\webright ]\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f^{-1}\webleft (g_{*}\webleft (U\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ x\in X\ \middle |\ f\webleft (x\webright )\in g_{*}\webleft (V\webright )\webright\} \\ & = \webleft\{ x\in X\ \middle |\ \begin{aligned} & \text{there exists some $y\in V$}\\ & \text{such that $f\webleft (x\webright )=g\webleft (y\webright )$}\end{aligned}\webright\} \\ & = \webleft\{ x\in X\ \middle |\ \begin{aligned} & \text{there exists some}\\ & \text{$(x,y)\in \webleft\{ (x,y)\in X\times _{Z}Y\ \middle |\ y\in V\webright\} $}\end{aligned}\webright\} \\ & = \webleft\{ x\in X\ \middle |\ \begin{aligned} & \text{there exists some}\\ & \text{$(x,y)\in \webleft\{ (x,y)\in X\times _{Z}Y\ \middle |\ y\in V\webright\} $}\\ & \text{such that $x=x$}\end{aligned}\webright\} \\ & = \webleft\{ x\in X\ \middle |\ \begin{aligned} & \text{there exists some}\\ & \text{$(x,y)\in \webleft\{ (x,y)\in X\times _{Z}Y\ \middle |\ y\in V\webright\} $}\\ & \text{such that $\text{pr}_{1}\webleft (x,y\webright )=x$}\end{aligned}\webright\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\text{pr}_{1}\webright )_{*}\webleft (\webleft\{ \webleft (x,y\webright )\in X\times _{Z}Y\ \middle |\ y\in V\webright\} \webright )\\ & = \webleft (\text{pr}_{1}\webright )_{*}\webleft (\webleft\{ \webleft (x,y\webright )\in X\times _{Z}Y\ \middle |\ \text{pr}_{2}\webleft (x,y\webright )\in V\webright\} \webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\text{pr}_{1}\webright )_{*}\webleft (\text{pr}^{-1}_{2}\webleft (V\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [\webleft (\text{pr}_{1}\webright )_{*}\circ \text{pr}^{-1}_{2}\webright ]\webleft (V\webright ) \end{align*}
for each $V\in \mathcal{P}\webleft (Y\webright )$. Therefore, we have
\[ f^{-1}\circ g_{*}=\webleft (\text{pr}_{1}\webright )_{*}\circ \text{pr}^{-1}_{2}. \]
This finishes the proof.
Item 2: The Projection Formula I
We claim that
\[ f_{*}\webleft (U\webright )\cap V\subset f_{*}\webleft (U\cap f^{-1}\webleft (V\webright )\webright ). \]
Indeed, we have
\begin{align*} f_{*}\webleft (U\webright )\cap V & \subset f_{*}\webleft (U\webright )\cap f_{*}\webleft (f^{-1}\webleft (V\webright )\webright )\\ & = f_{*}\webleft (U\cap f^{-1}\webleft (V\webright )\webright ), \end{align*}
where we have used:
-
Item 2 of Proposition 2.6.1.1.4 for the inclusion.
-
Item 6 of Proposition 2.6.1.1.4 for the equality.
Conversely, we claim that
\[ f_{*}\webleft (U\cap f^{-1}\webleft (V\webright )\webright )\subset f_{*}\webleft (U\webright )\cap V. \]
Indeed:
-
Let $y\in f_{*}\webleft (U\cap f^{-1}\webleft (V\webright )\webright )$.
-
Since $y\in f_{*}\webleft (U\cap f^{-1}\webleft (V\webright )\webright )$, there exists some $x\in U\cap f^{-1}\webleft (V\webright )$ such that $f\webleft (x\webright )=y$.
-
Since $x\in U\cap f^{-1}\webleft (V\webright )$, we have $x\in U$, and thus $f\webleft (x\webright )\in f_{*}\webleft (U\webright )$.
-
Since $x\in U\cap f^{-1}\webleft (V\webright )$, we have $x\in f^{-1}\webleft (V\webright )$, and thus $f\webleft (x\webright )\in V$.
-
Since $f\webleft (x\webright )\in f_{*}\webleft (U\webright )$ and $f\webleft (x\webright )\in V$, we have $f\webleft (x\webright )\in f_{*}\webleft (U\webright )\cap V$.
-
But $y=f\webleft (x\webright )$, so $y\in f_{*}\webleft (U\webright )\cap V$.
-
Thus $f_{*}\webleft (U\cap f^{-1}\webleft (V\webright )\webright )\subset f_{*}\webleft (U\webright )\cap V$.
This finishes the proof.
Item 3: The Projection Formula II
We have
\begin{align*} f_{!}\webleft (U\webright )\cap V & \subset f_{!}\webleft (U\webright )\cap f_{!}\webleft (f^{-1}\webleft (V\webright )\webright )\\ & = f_{!}\webleft (U\cap f^{-1}\webleft (V\webright )\webright ), \end{align*}
where we have used:
-
Item 2 of Proposition 2.6.3.1.6 for the inclusion.
-
Item 6 of Proposition 2.6.3.1.6 for the equality.
Since $\mathcal{P}\webleft (Y\webright )$ is posetal, naturality is automatic (
).
Item 4: Strong Closed Monoidality
This is a repetition of Item 19 of Proposition 2.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}}}=}}\text{pr}^{-1}_{1}\webleft (U\webright )\cap \text{pr}^{-1}_{2}\webleft (V\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ \webleft (x,y\webright )\in X\times Y\ \middle |\ \text{pr}_{1}\webleft (x,y\webright )\in U\webright\} \\ & \phantom{={}} \mkern 4mu\cup \webleft\{ \webleft (x,y\webright )\in X\times Y\ \middle |\ \text{pr}_{2}\webleft (x,y\webright )\in V\webright\} \\ & = \webleft\{ \webleft (x,y\webright )\in X\times Y\ \middle |\ x\in U\webright\} \\ & \phantom{={}} \mkern 4mu\cup \webleft\{ \webleft (x,y\webright )\in X\times Y\ \middle |\ y\in V\webright\} \\ & = \webleft\{ \webleft (x,y\webright )\in X\times Y\ \middle |\ \text{$x\in U$ and $y\in V$}\webright\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}U\times V. \end{align*}
Next, we claim that Item (a), Item (b), Item (c), and Item (d) are indeed true:
-
Proof of Item (a): This is a repetition of Item 16 of Proposition 2.6.1.1.4 and is proved there.
-
Proof of Item (b): This is a repetition of Item 16 of Proposition 2.6.2.1.3 and is proved there.
-
Proof of Item (c): This is a repetition of Item 15 of Proposition 2.6.3.1.6 and is proved there.
-
Proof of Item (d): We have
\begin{align*} \Delta ^{-1}_{X}\webleft (U\boxtimes _{X\times X}V\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ x\in X\ \middle |\ \webleft (x,x\webright )\in U\boxtimes _{X\times X}V\webright\} \\ & = \webleft\{ x\in X\ \middle |\ \webleft (x,x\webright )\in \webleft\{ \webleft (u,v\webright )\in X\times X\ \middle |\ \text{$u\in U$ and $v\in V$}\webright\} \webright\} \\ & = 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 2.4.7.1.3 and is proved there.
