Item 3 (024F) — The Clowder Project

4.6.4 A Six-Functor Formalism for Sets

Remark 4.6.4.1.1 ▶ A Six-Functor Formalism for Sets

The assignment $X\mapsto \mathcal{P}\webleft (X\webright )$ 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}\webleft (X\webright )\times \mathcal{P}\webleft (X\webright ) \to \mathcal{P}\webleft (X\webright ),\\ \webleft [-_{1},-_{2}\webright ]_{X} & \colon \mathcal{P}\webleft (X\webright )^{\mathsf{op}}\times \mathcal{P}\webleft (X\webright ) \to \mathcal{P}\webleft (X\webright ) \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.¹

¹See also [nLab Authors, Interactions of Images and Pre-images with Unions and Intersections].

Proposition 4.6.4.1.2 ▶ A Six-Functor Formalism for Sets

Let $X$ be a set.

1.
The Beck–Chevalley Condition. Let
be a pullback diagram in $\mathsf{Sets}$. We have
2.
The Projection Formula I. The diagram
commutes, i.e. we have

\[ f_{!}\webleft (U\cap f^{-1}\webleft (V\webright )\webright )=f_{!}\webleft (U\webright )\cap V \]

for each $U\in \mathcal{P}\webleft (X\webright )$ and each $V\in \mathcal{P}\webleft (Y\webright )$.
3.
The Projection Formula II. We have a natural transformation
with components

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

indexed by $U\in \mathcal{P}\webleft (X\webright )$ and $V\in \mathcal{P}\webleft (Y\webright )$.
4.
Strong Closed Monoidality. The diagram
commutes, i.e. we have an equality of sets

\[ f^{-1}\webleft (\webleft [U,V\webright ]_{Y}\webright )=\webleft [f^{-1}\webleft (U\webright ),f^{-1}\webleft (V\webright )\webright ]_{X}, \]

natural in $U,V\in \mathcal{P}\webleft (X\webright )$.
5.
The External Tensor Product. We have an external tensor product

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

given by

\begin{align*} U\boxtimes _{X\times Y}V & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\operatorname {\mathrm{\mathrm{pr}}}^{-1}_{1}\webleft (U\webright )\cap \operatorname {\mathrm{\mathrm{pr}}}^{-1}_{2}\webleft (V\webright )\\ & = \left\{ \webleft (u,v\webright )\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
  
  \[ \webleft [f_{!}\times g_{!}\webright ]\webleft (U\boxtimes _{X\times Y}V\webright )=f_{!}\webleft (U\webright )\boxtimes _{X'\times Y'}g_{!}\webleft (V\webright ) \]
  
  for each $\webleft (U,V\webright )\in \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright )$.
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
  
  \[ \webleft [f^{-1}\times g^{-1}\webright ]\webleft (U\boxtimes _{X'\times Y'}V\webright )=f^{-1}\webleft (U\webright )\boxtimes _{X\times Y}g^{-1}\webleft (V\webright ) \]
  
  for each $\webleft (U,V\webright )\in \mathcal{P}\webleft (X'\webright )\times \mathcal{P}\webleft (Y'\webright )$.
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
  
  \[ \webleft [f_{*}\times g_{*}\webright ]\webleft (U\boxtimes _{X\times Y}V\webright )=f_{*}\webleft (U\webright )\boxtimes _{X'\times Y'}g_{*}\webleft (V\webright ) \]
  
  for each $\webleft (U,V\webright )\in \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright )$.
4. (d)
  Interaction With Diagonals. The diagram
  i.e. we have
  
  \[ U\cap V=\Delta ^{-1}_{X}\webleft (U\boxtimes _{X\times X}V\webright ) \]
  
  for each $U,V\in \mathcal{P}\webleft (X\webright )$.
6.
The Dualisation Functor. We have a functor

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

given by

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

for each $U\in \mathcal{P}\webleft (X\webright )$, as in Item 5 of Proposition 4.4.7.1.3, satisfying the following conditions:
1. (a)
  Duality. We have
2. (b)
  Duality. The diagram
  commutes, i.e. we have
  
  \[ \underbrace{D_{X}\webleft (U\cap D_{X}\webleft (V\webright )\webright )}_{\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [U\cap \webleft [V,\text{Ø}\webright ]_{X},\text{Ø}\webright ]_{X}}=\webleft [U,V\webright ]_{X} \]
  
  for each $U,V\in \mathcal{P}\webleft (X\webright )$.
3. (c)
  Interaction With Direct Images. The diagram
  commutes, i.e. we have
  
  \[ f_{!}\webleft (D_{X}\webleft (U\webright )\webright )=D_{Y}\webleft (f_{*}\webleft (U\webright )\webright ) \]
  
  for each $U\in \mathcal{P}\webleft (X\webright )$.
4. (d)
  Interaction With Inverse Images. The diagram
  commutes, i.e. we have
  
  \[ f^{-1}\webleft (D_{Y}\webleft (U\webright )\webright )=D_{X}\webleft (f^{-1}\webleft (U\webright )\webright ) \]
  
  for each $U\in \mathcal{P}\webleft (X\webright )$.
5. (e)
  Interaction With Codirect Images. The diagram
  commutes, i.e. we have
  
  \[ f_{*}\webleft (D_{X}\webleft (U\webright )\webright )=D_{Y}\webleft (f_{!}\webleft (U\webright )\webright ) \]
  
  for each $U\in \mathcal{P}\webleft (X\webright )$.

Proof of Proposition 4.6.4.1.2.

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}}}=}}\left\{ y\in Y\ \middle |\ g\webleft (y\webright )\in f_{!}\webleft (U\webright )\right\} \\ & = \left\{ 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}\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}\webleft (x,y\webright )=y$}\end{aligned}\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\operatorname {\mathrm{\mathrm{pr}}}_{2}\webright )_{!}\webleft (\left\{ \webleft (x,y\webright )\in X\times _{Z}Y\ \middle |\ x\in U\right\} \webright )\\ & = \webleft (\operatorname {\mathrm{\mathrm{pr}}}_{2}\webright )_{!}\webleft (\left\{ \webleft (x,y\webright )\in X\times _{Z}Y\ \middle |\ \operatorname {\mathrm{\mathrm{pr}}}_{1}\webleft (x,y\webright )\in U\right\} \webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\operatorname {\mathrm{\mathrm{pr}}}_{2}\webright )_{!}\webleft (\operatorname {\mathrm{\mathrm{pr}}}^{-1}_{1}\webleft (U\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [\webleft (\operatorname {\mathrm{\mathrm{pr}}}_{2}\webright )_{!}\circ \operatorname {\mathrm{\mathrm{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 (\operatorname {\mathrm{\mathrm{pr}}}_{2}\webright )_{!}\circ \operatorname {\mathrm{\mathrm{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}}}=}}\left\{ x\in X\ \middle |\ f\webleft (x\webright )\in g_{!}\webleft (V\webright )\right\} \\ & = \left\{ 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}\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}\webleft (x,y\webright )=x$}\end{aligned}\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\operatorname {\mathrm{\mathrm{pr}}}_{1}\webright )_{!}\webleft (\left\{ \webleft (x,y\webright )\in X\times _{Z}Y\ \middle |\ y\in V\right\} \webright )\\ & = \webleft (\operatorname {\mathrm{\mathrm{pr}}}_{1}\webright )_{!}\webleft (\left\{ \webleft (x,y\webright )\in X\times _{Z}Y\ \middle |\ \operatorname {\mathrm{\mathrm{pr}}}_{2}\webleft (x,y\webright )\in V\right\} \webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\operatorname {\mathrm{\mathrm{pr}}}_{1}\webright )_{!}\webleft (\operatorname {\mathrm{\mathrm{pr}}}^{-1}_{2}\webleft (V\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [\webleft (\operatorname {\mathrm{\mathrm{pr}}}_{1}\webright )_{!}\circ \operatorname {\mathrm{\mathrm{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 (\operatorname {\mathrm{\mathrm{pr}}}_{1}\webright )_{!}\circ \operatorname {\mathrm{\mathrm{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:

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

Indeed:

1.
Let $y\in f_{!}\webleft (U\cap f^{-1}\webleft (V\webright )\webright )$.
2.
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$.

3.
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:

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}\webleft (Y\webright )$ 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}\webleft (U\webright )\cap \operatorname {\mathrm{\mathrm{pr}}}^{-1}_{2}\webleft (V\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ \webleft (x,y\webright )\in X\times Y\ \middle |\ \operatorname {\mathrm{\mathrm{pr}}}_{1}\webleft (x,y\webright )\in U\right\} \\ & \phantom{={}} \mkern 4mu\cup \left\{ \webleft (x,y\webright )\in X\times Y\ \middle |\ \operatorname {\mathrm{\mathrm{pr}}}_{2}\webleft (x,y\webright )\in V\right\} \\ & = \left\{ \webleft (x,y\webright )\in X\times Y\ \middle |\ x\in U\right\} \\ & \phantom{={}} \mkern 4mu\cup \left\{ \webleft (x,y\webright )\in X\times Y\ \middle |\ y\in V\right\} \\ & = \left\{ \webleft (x,y\webright )\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}\webleft (U\boxtimes _{X\times X}V\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ x\in X\ \middle |\ \webleft (x,x\webright )\in U\boxtimes _{X\times X}V\right\} \\ & = \left\{ x\in X\ \middle |\ \webleft (x,x\webright )\in \left\{ \webleft (u,v\webright )\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.

Statistics Cite

Noticed something off, or have any comments? Feel free to reach out!

•Email
•Discord

You can also use the contact form below: