The Stacks project

Proof. If we show that $\Gamma (S, \mathcal{F}) = \mathcal{F}_{\overline{s}}$ then $\Gamma (S, -)$ is exact as the stalk functor is exact. Let $(U, \overline{u})$ be an étale neighbourhood of $\overline{s}$. Pick an affine open neighborhood $\mathop{\mathrm{Spec}}(A)$ of $\overline{u}$ in $U$. Then $R \to A$ is étale and $\kappa (\overline{s}) = \kappa (\overline{u})$. By Theorem 59.32.4 we see that $A \cong R \times A'$ as an $R$-algebra compatible with maps to $\kappa (\overline{s}) = \kappa (\overline{u})$. Hence we get a section

It follows that in the system of étale neighbourhoods of $\overline{s}$ the identity map $(S, \overline{s}) \to (S, \overline{s})$ is cofinal. Hence $\Gamma (S, \mathcal{F}) = \mathcal{F}_{\overline{s}}$. The final statement of the lemma follows as the higher derived functors of an exact functor are zero, see Derived Categories, Lemma 13.16.9. $\square$

Proof. Let $X_{\overline{y}}^{sh}$ denote the fiber product $X \times _ Y \mathop{\mathrm{Spec}}(\mathcal{O}_{Y, \overline{y}}^{sh})$. By Theorem 59.53.1 the stalk of $R^ qf_*\mathcal{F}$ at $\overline{y}$ is computed by $H_{\acute{e}tale}^ q(X_{\overline{y}}^{sh}, \mathcal{F})$. Since $f$ is finite, $X_{\bar y}^{sh}$ is finite over $\mathop{\mathrm{Spec}}(\mathcal{O}_{Y, \overline{y}}^{sh})$, thus $X_{\bar y}^{sh} = \mathop{\mathrm{Spec}}(A)$ for some ring $A$ finite over $\mathcal{O}_{Y, \bar y}^{sh}$. Since the latter is strictly henselian, Lemma 59.32.5 implies that $A$ is a finite product of henselian local rings $A = A_1 \times \ldots \times A_ r$. Since the residue field of $\mathcal{O}_{Y, \overline{y}}^{sh}$ is separably closed the same is true for each $A_ i$. Hence $A_ i$ is strictly henselian. This implies that $X_{\overline{y}}^{sh} = \coprod _{i = 1}^ r \mathop{\mathrm{Spec}}(A_ i)$. The vanishing of Lemma 59.55.1 implies that $(R^ qf_*\mathcal{F})_{\overline{y}} = 0$ for $q > 0$ which implies (2) by Theorem 59.29.10. Part (1) follows from the corresponding statement of Lemma 59.55.1. $\square$

Proof. In great generality there is a pullback map $g^{-1}f_*\mathcal{F} \to f'_*(g')^{-1}\mathcal{F}$, see Sites, Section 7.45. It suffices to check on stalks (Theorem 59.29.10). Let $\overline{y}' : \mathop{\mathrm{Spec}}(k) \to Y'$ be a geometric point. We have

The first equality by Proposition 59.55.2. The second equality by Lemma 59.36.2. The third equality holds because the diagram is a cartesian square and hence the map

sending $\overline{x}'$ to $g' \circ \overline{x}'$ is a bijection. The fourth equality by Proposition 59.55.2. The fifth equality by Lemma 59.36.2. $\square$

Proof. The question is local on $Y$ and hence we may assume $Y$ is affine. Then we can write $X = \mathop{\mathrm{lim}}\nolimits X_ i$ with $f_ i : X_ i \to Y$ finite (this is easy in the affine case, but see Limits, Lemma 32.7.3 for a reference). Denote $p_{i'i} : X_{i'} \to X_ i$ the transition morphisms and $p_ i : X \to X_ i$ the projections. Setting $\mathcal{F}_ i = p_{i, *}\mathcal{F}$ we obtain from Lemma 59.51.9 a system $(\mathcal{F}_ i, \varphi _{i'i})$ with $\mathcal{F} = \mathop{\mathrm{colim}}\nolimits p_ i^{-1}\mathcal{F}_ i$. We get $f_*\mathcal{F} = \mathop{\mathrm{colim}}\nolimits f_{i, *}\mathcal{F}_ i$ from Lemma 59.51.7. Set $X'_ i = Y' \times _ Y X_ i$ with projections $f'_ i$ and $g'_ i$. Then $X' = \mathop{\mathrm{lim}}\nolimits X'_ i$ as limits commute with limits. Denote $p'_ i : X' \to X'_ i$ the projections. We have

as desired. For the first equality see above. For the second use that pullback commutes with colimits. For the third use the finite case, see Lemma 59.55.3. For the fourth use Lemma 59.51.7. For the fifth use that $g'_ i \circ p'_ i = p_ i \circ g'$. For the sixth use that pullback commutes with colimits. For the seventh use $\mathcal{F} = \mathop{\mathrm{colim}}\nolimits p_ i^{-1}\mathcal{F}_ i$. $\square$

Proof. If we prove the first statement of the lemma, then we obtain a spectral sequence with $E_1^{p, q} = H^ q_{\acute{e}tale}(Y, \mathcal{F})$ converging to $H^{p + q}(Y_{\acute{e}tale}, \mathcal{F})$, see Derived Categories, Lemma 13.21.3. On the other hand, since $R^ if_{p, *}f_ p^{-1}\mathcal{F} = 0$ for $i > 0$ (Proposition 59.55.2) we get

by Proposition 59.54.2 and we get the spectral sequence of the lemma.

To prove the first statement of the lemma, observe that $X_ n$ forms a simplicial scheme over $Y$, see Simplicial, Example 14.3.5. Observe moreover, that for each of the projections $d_ j : X_{n + 1} \to X_ n$ there is a map $d_ j^{-1} f_ n^{-1}\mathcal{F} \to f_{n + 1}^{-1}\mathcal{F}$. These maps induce maps

for $j = 0, \ldots , n + 1$. We use the alternating sum of these maps to define the differentials $\mathcal{F}_ n \to \mathcal{F}_{n + 1}$. Similarly, there is a canonical augmentation $\mathcal{F} \to \mathcal{F}_0$, namely this is just the canonical map $\mathcal{F} \to f_*f^{-1}\mathcal{F}$. To check that this sequence of sheaves is an exact complex it suffices to check on stalks at geometric points (Theorem 59.29.10). Thus we let $\overline{y} : \mathop{\mathrm{Spec}}(k) \to Y$ be a geometric point. Let $E = \{ \overline{x} : \mathop{\mathrm{Spec}}(k) \to X \mid f(\overline{x}) = \overline{y}\} $. Then $E$ is a finite nonempty set and we see that

by Proposition 59.55.2 and Lemma 59.36.2. Thus we have to see that given an abelian group $M$ the sequence

is exact. Here the first map is the diagonal map and the map $\bigoplus _{e \in E^{n + 1}} M \to \bigoplus _{e \in E^{n + 2}} M$ is the alternating sum of the maps induced by the $(n + 2)$ projections $E^{n + 2} \to E^{n + 1}$. This can be shown directly or deduced by applying Simplicial, Lemma 14.26.9 to the map $E \to \{ *\} $. $\square$