Lemma 7.31.3. Let $f : \mathop{\mathit{Sh}}\nolimits (\mathcal{C}) \to \mathop{\mathit{Sh}}\nolimits (\mathcal{D})$ be a morphism of topoi. Let $\mathcal{G} \in \mathop{\mathit{Sh}}\nolimits (\mathcal{D})$, $\mathcal{F} \in \mathop{\mathit{Sh}}\nolimits (\mathcal{C})$ and $s : \mathcal{F} \to f^{-1}\mathcal{G}$ a morphism of sheaves. There exists a commutative diagram of topoi
\[ \xymatrix{ \mathop{\mathit{Sh}}\nolimits (\mathcal{C})/\mathcal{F} \ar[r]_{j_\mathcal {F}} \ar[d]_{f_ s} & \mathop{\mathit{Sh}}\nolimits (\mathcal{C}) \ar[d]^ f \\ \mathop{\mathit{Sh}}\nolimits (\mathcal{D})/\mathcal{G} \ar[r]^{j_\mathcal {G}} & \mathop{\mathit{Sh}}\nolimits (\mathcal{D}). } \]
We have $f_ s = f' \circ j_{\mathcal{F}/f^{-1}\mathcal{G}}$ where $f' : \mathop{\mathit{Sh}}\nolimits (\mathcal{C})/f^{-1}\mathcal{G} \to \mathop{\mathit{Sh}}\nolimits (\mathcal{D})/\mathcal{F}$ is as in Lemma 7.31.1 and $j_{\mathcal{F}/f^{-1}\mathcal{G}} : \mathop{\mathit{Sh}}\nolimits (\mathcal{C})/\mathcal{F} \to \mathop{\mathit{Sh}}\nolimits (\mathcal{C})/f^{-1}\mathcal{G}$ is as in Lemma 7.30.6. The functor $(f_ s)^{-1}$ is described by the rule
\[ (f_ s)^{-1}(\mathcal{H} \xrightarrow {\varphi } \mathcal{G}) = (f^{-1}\mathcal{H} \times _{f^{-1}\varphi , f^{-1}\mathcal{G}, s} \mathcal{F} \rightarrow \mathcal{F}). \]
Finally, given any morphisms $b : \mathcal{G}' \to \mathcal{G}$, $a : \mathcal{F}' \to \mathcal{F}$ and $s' : \mathcal{F}' \to f^{-1}\mathcal{G}'$ such that
\[ \xymatrix{ \mathcal{F}' \ar[r]_-{s'} \ar[d]_ a & f^{-1}\mathcal{G}' \ar[d]^{f^{-1}b} \\ \mathcal{F} \ar[r]^-s & f^{-1}\mathcal{G} } \]
commutes, then the diagram
\[ \xymatrix{ \mathop{\mathit{Sh}}\nolimits (\mathcal{C})/\mathcal{F}' \ar[r]_{j_{\mathcal{F}'/\mathcal{F}}} \ar[d]_{f_{s'}} & \mathop{\mathit{Sh}}\nolimits (\mathcal{C})/\mathcal{F} \ar[d]^{f_ s} \\ \mathop{\mathit{Sh}}\nolimits (\mathcal{D})/\mathcal{G}' \ar[r]^{j_{\mathcal{G}'/\mathcal{G}}} & \mathop{\mathit{Sh}}\nolimits (\mathcal{D})/\mathcal{G}. } \]
commutes.
Proof.
The commutativity of the first square follows from the commutativity of the diagram in Lemma 7.30.6 and the commutativity of the diagram in Lemma 7.31.1. The description of $f_ s^{-1}$ follows on combining the descriptions of $(f')^{-1}$ in Lemma 7.31.1 with the description of $(j_{\mathcal{F}/f^{-1}\mathcal{G}})^{-1}$ in Lemma 7.30.6. The commutativity of the last square then follows from the equality
\[ f^{-1}\mathcal{H} \times _{f^{-1}\mathcal{G}, s} \mathcal{F} \times _\mathcal {F} \mathcal{F}' = f^{-1}(\mathcal{H} \times _\mathcal {G} \mathcal{G}') \times _{f^{-1}\mathcal{G}', s'} \mathcal{F}' \]
which is formal.
$\square$
Comments (0)