Proposition 2.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}}}=}}\text{pr}^{-1}_{1}\webleft (U\webright )\cap \text{pr}^{-1}_{2}\webleft (V\webright )\\ & = \webleft\{ \webleft (u,v\webright )\in X\times Y\ \middle |\ \text{$u\in U$ and $v\in V$}\webright\} . \end{align*}

    This is the same map as the one in Item 5 of Proposition 2.4.1.1.4. Moreover, the following conditions are satisfied:

    1. 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. 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. Interaction With Direct Images With Compact Support. 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. 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 2.4.7.1.3, satisfying the following conditions:

    1. Duality. We have
    2. 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. 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. 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. Interaction With Direct Images With Compact Support. 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 2.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}}}=}}\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:

  1. Item 2 of Proposition 2.6.1.1.4 for the inclusion.
  2. 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:

  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 )$.
  4. 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$.
  5. 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$.
  6. But $y=f\webleft (x\webright )$, so $y\in f_{*}\webleft (U\webright )\cap V$.
  7. 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 2.6.3.1.6 for the inclusion.
  2. 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:

  1. Proof of Item (a): This is a repetition of Item 16 of Proposition 2.6.1.1.4 and is proved there.
  2. Proof of Item (b): This is a repetition of Item 16 of Proposition 2.6.2.1.3 and is proved there.
  3. Proof of Item (c): This is a repetition of Item 15 of Proposition 2.6.3.1.6 and is proved there.
  4. 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.

Previous

View Proposition 2.6.4.1.2 as PDF

Statistics Cite
1 tag refers to this tag

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

You can also use the contact form below: