Lemma 61.31.3. Suppose given big sites \mathit{Sch}_{pro\text{-}\acute{e}tale} and \mathit{Sch}'_{pro\text{-}\acute{e}tale} as in Definition 61.12.7. Assume that \mathit{Sch}_{pro\text{-}\acute{e}tale} is contained in \mathit{Sch}'_{pro\text{-}\acute{e}tale}. The inclusion functor \mathit{Sch}_{pro\text{-}\acute{e}tale}\to \mathit{Sch}'_{pro\text{-}\acute{e}tale} satisfies the assumptions of Sites, Lemma 7.21.8. There are morphisms of topoi
\begin{eqnarray*} g : \mathop{\mathit{Sh}}\nolimits (\mathit{Sch}_{pro\text{-}\acute{e}tale}) & \longrightarrow & \mathop{\mathit{Sh}}\nolimits (\mathit{Sch}'_{pro\text{-}\acute{e}tale}) \\ f : \mathop{\mathit{Sh}}\nolimits (\mathit{Sch}'_{pro\text{-}\acute{e}tale}) & \longrightarrow & \mathop{\mathit{Sh}}\nolimits (\mathit{Sch}_{pro\text{-}\acute{e}tale}) \end{eqnarray*}
such that f \circ g \cong \text{id}. For any object S of \mathit{Sch}_{pro\text{-}\acute{e}tale} the inclusion functor (\mathit{Sch}/S)_{pro\text{-}\acute{e}tale}\to (\mathit{Sch}'/S)_{pro\text{-}\acute{e}tale} satisfies the assumptions of Sites, Lemma 7.21.8 also. Hence similarly we obtain morphisms
\begin{eqnarray*} g : \mathop{\mathit{Sh}}\nolimits ((\mathit{Sch}/S)_{pro\text{-}\acute{e}tale}) & \longrightarrow & \mathop{\mathit{Sh}}\nolimits ((\mathit{Sch}'/S)_{pro\text{-}\acute{e}tale}) \\ f : \mathop{\mathit{Sh}}\nolimits ((\mathit{Sch}'/S)_{pro\text{-}\acute{e}tale}) & \longrightarrow & \mathop{\mathit{Sh}}\nolimits ((\mathit{Sch}/S)_{pro\text{-}\acute{e}tale}) \end{eqnarray*}
with f \circ g \cong \text{id}.
Proof.
Assumptions (b), (c), and (e) of Sites, Lemma 7.21.8 are immediate for the functors \mathit{Sch}_{pro\text{-}\acute{e}tale}\to \mathit{Sch}'_{pro\text{-}\acute{e}tale} and (\mathit{Sch}/S)_{pro\text{-}\acute{e}tale}\to (\mathit{Sch}'/S)_{pro\text{-}\acute{e}tale}. Property (a) holds by Lemma 61.31.1. Property (d) holds because fibre products in the categories \mathit{Sch}_{pro\text{-}\acute{e}tale}, \mathit{Sch}'_{pro\text{-}\acute{e}tale} exist and are compatible with fibre products in the category of schemes.
\square
Comments (0)