Improve statement and clarify proof of lemma in coherent.tex

Thanks to correction_bot
http://stacks.math.columbia.edu/tag/01XL#comment-938

coherent.tex

@@ -888,7 +888,7 @@ \section{Cohomology and base change, II}
 \label{lemma-separated-case-relative-cech}
 Let $f : X \to S$ be a morphism of schemes.
 Let $\mathcal{F}$ be a quasi-coherent $\mathcal{O}_X$-module.
-Assume $X$ and $S$ are quasi-compact and have affine diagonal
+Assume $X$ is quasi-compact and $X$ and $S$ have affine diagonal
 (e.g., if $X$ and $S$ are separated).
 In this case we can compute $Rf_*\mathcal{F}$ as follows:
 \begin{enumerate}
@@ -924,8 +924,8 @@ \section{Cohomology and base change, II}
 
 \begin{proof}
 Consider the resolution
-$\mathcal{F} \to {\mathfrak C}^\bullet(\mathcal{U}, \mathcal{F})$ of
-Cohomology, Lemma \ref{cohomology-lemma-covering-resolution}.
+$\mathcal{F} \to {\mathfrak C}^\bullet(\mathcal{U}, \mathcal{F})$
+of Cohomology, Lemma \ref{cohomology-lemma-covering-resolution}.
 We have an equality of complexes
 $\check{\mathcal{C}}^\bullet(\mathcal{U}, f, \mathcal{F}) =
 f_*{\mathfrak C}^\bullet(\mathcal{U}, \mathcal{F})$
@@ -935,28 +935,22 @@ \section{Cohomology and base change, II}
 are affine by Morphisms, Lemma \ref{morphisms-lemma-affine-permanence}.
 Hence $R^qj_{i_0 \ldots i_p *}\mathcal{F}_{i_0 \ldots i_p}$
 as well as $R^qf_{i_0 \ldots i_p *}\mathcal{F}_{i_0 \ldots i_p}$
-are zero for $q > 0$. By
+are zero for $q > 0$ (Lemma \ref{lemma-relative-affine-vanishing}).
+Using $f \circ j_{i_0 \ldots i_p} = f_{i_0 \ldots i_p}$ and
+the spectral sequence of
 Cohomology, Lemma \ref{cohomology-lemma-relative-Leray}
 we conclude that
-$Rj_{i_0 \ldots i_p *}\mathcal{F}_{i_0 \ldots i_p} =
-j_{i_0 \ldots i_p *}\mathcal{F}_{i_0 \ldots i_p}$ and
-$Rf_{i_0 \ldots i_p *}\mathcal{F}_{i_0 \ldots i_p} =
-f_{i_0 \ldots i_p *}\mathcal{F}_{i_0 \ldots i_p}$.
-Using that $Rf_* \circ Rj_{i_0 \ldots i_p *} = Rf_{i_0 \ldots i_p *}$
-(Cohomology, Lemma \ref{cohomology-lemma-higher-direct-images-compose})
-we find that
-$Rf_*j_{i_0 \ldots i_p *}\mathcal{F}_{i_0 \ldots i_p} =
-f_{i_0 \ldots i_p *}\mathcal{F}_{i_0 \ldots i_p}$.
+$R^qf_*(j_{i_0 \ldots i_p *}\mathcal{F}_{i_0 \ldots i_p}) = 0$
+for $q > 0$.
 Since the terms of the complex
 ${\mathfrak C}^\bullet(\mathcal{U}, \mathcal{F})$ are finite direct
 sums of the sheaves $j_{i_0 \ldots i_p *}\mathcal{F}_{i_0 \ldots i_p}$
 we conclude using Leray's acyclicity lemma
 (Derived Categories, Lemma \ref{derived-lemma-leray-acyclicity})
 that
 $$
-Rf_* \mathcal{F} =
-Rf_*{\mathfrak C}^\bullet(\mathcal{U}, \mathcal{F}) =
-f_*{\mathfrak C}^\bullet(\mathcal{U}, \mathcal{F})
+Rf_* \mathcal{F} = f_*{\mathfrak C}^\bullet(\mathcal{U}, \mathcal{F}) =
+\check{\mathcal{C}}^\bullet(\mathcal{U}, f, \mathcal{F})
 $$
 as desired.
 \end{proof}