diff --git a/chow.tex b/chow.tex
index 26d20627a..da9c9754e 100644
--- a/chow.tex
+++ b/chow.tex
@@ -3545,7 +3545,8 @@ \section{Proper pushforward}
 \end{enumerate}
 Note that the statement makes sense since $f_*\mathcal{F}$ and
 $f_*\mathcal{O}_Z$ are coherent $\mathcal{O}_Y$-modules by
-Cohomology of Schemes, Lemma \ref{coherent-lemma-proper-pushforward-coherent}.
+Cohomology of Schemes, Proposition
+\ref{coherent-proposition-proper-pushforward-coherent}.
 \end{lemma}
 
 \begin{proof}
diff --git a/coherent.tex b/coherent.tex
index 55a5f2330..b8afc074d 100644
--- a/coherent.tex
+++ b/coherent.tex
@@ -3802,14 +3802,14 @@ \section{Higher direct images of coherent sheaves}
 \noindent
 Here is the general statement.
 
-\begin{lemma}
-\label{lemma-proper-pushforward-coherent}
+\begin{proposition}
+\label{proposition-proper-pushforward-coherent}
 Let $S$ be a locally Noetherian scheme.
 Let $f : X \to S$ be a proper morphism.
 Let $\mathcal{F}$ be a coherent $\mathcal{O}_X$-module.
 Then $R^if_*\mathcal{F}$ is a coherent $\mathcal{O}_S$-module
 for all $i \geq 0$.
-\end{lemma}
+\end{proposition}
 
 \begin{proof}
 Since the problem is local on $S$ we may assume that $S$ is
@@ -3883,10 +3883,10 @@ \section{Higher direct images of coherent sheaves}
 as in the statement of Chow's lemma. Also, let $U \subset Z$ be
 the dense open subscheme such that $\pi^{-1}(U) \to U$ is an isomorphism.
 By the discussion in Remark \ref{remark-chow-Noetherian} we see that
-$i' = (i, \pi) : \mathbf{P}^n_S \times_S Z' = \mathbf{P}^n_Z$ is
+$i' = (i, \pi) : Z' \to \mathbf{P}^n_Z$ is
 a closed immersion. Hence
 $$
-\mathcal{L} = i^*\mathcal{O}_{\mathbf{P}^n_X}(1) \cong
+\mathcal{L} = i^*\mathcal{O}_{\mathbf{P}^n_S}(1) \cong
 (i')^*\mathcal{O}_{\mathbf{P}^n_Z}(1)
 $$
 is $g'$-relatively ample and $\pi$-relatively ample (for example by
@@ -3932,8 +3932,8 @@ \section{Higher direct images of coherent sheaves}
 $\mathcal{F} = i_*\mathcal{G}$ for some coherent module $\mathcal{G}$
 on $Z$ (Lemma \ref{lemma-coherent-support-closed}).
 Denoting $g : Z \to S$ the composition $f \circ i$ we see that
-$R^pg_*\mathcal{G}$
-is coherent on $S$ by Lemma \ref{lemma-proper-pushforward-coherent}.
+$R^pg_*\mathcal{G}$ is coherent on $S$ by
+Proposition \ref{proposition-proper-pushforward-coherent}.
 On the other hand, $R^qi_*\mathcal{G} = 0$ for $q > 0$
 (Lemma \ref{lemma-finite-pushforward-coherent}).
 By Cohomology, Lemma \ref{cohomology-lemma-relative-Leray}
@@ -3950,7 +3950,8 @@ \section{Higher direct images of coherent sheaves}
 \end{lemma}
 
 \begin{proof}
-This is just the affine case of Lemma \ref{lemma-proper-pushforward-coherent}.
+This is just the affine case of
+Proposition \ref{proposition-proper-pushforward-coherent}.
 Namely, by Lemmas \ref{lemma-quasi-coherence-higher-direct-images} and
 \ref{lemma-quasi-coherence-higher-direct-images-application} we know that
 $R^if_*\mathcal{F}$ is the quasi-coherent sheaf associated
@@ -4488,7 +4489,7 @@ \section{The theorem on formal functions}
 $p > 0$. Hence we see that $(R^pf_*\mathcal{F})_y^\wedge = 0$
 by Lemma \ref{lemma-formal-functions-stalk}.
 Note that $R^pf_*\mathcal{F}$ is coherent by
-Lemma \ref{lemma-proper-pushforward-coherent} and
+Proposition \ref{proposition-proper-pushforward-coherent} and
 hence $R^pf_*\mathcal{F}_y$ is a finite
 $\mathcal{O}_{Y, y}$-module.
 By Algebra, Lemma \ref{algebra-lemma-completion-tensor}
@@ -4518,11 +4519,11 @@ \section{The theorem on formal functions}
 Moreover, the underlying topological space of each infinitesimal
 neighbourhood $X_n$ is the same as that of $X_y$.
 Hence $H^p(X_n, \mathcal{F}_n) = 0$ for all $p > d$ by
-Cohomology, Lemma \ref{cohomology-lemma-vanishing-Noetherian}.
+Cohomology, Proposition \ref{cohomology-proposition-vanishing-Noetherian}.
 Hence we see that $(R^pf_*\mathcal{F})_y^\wedge = 0$
 by Lemma \ref{lemma-formal-functions-stalk} for $p > d$.
 Note that $R^pf_*\mathcal{F}$ is coherent by
-Lemma \ref{lemma-proper-pushforward-coherent} and
+Proposition \ref{proposition-proper-pushforward-coherent} and
 hence $R^pf_*\mathcal{F}_y$ is a finite
 $\mathcal{O}_{Y, y}$-module.
 By Algebra, Lemma \ref{algebra-lemma-completion-tensor}
@@ -5363,7 +5364,7 @@ \section{Grothendieck's existence theorem, II}
 \begin{proof}
 Since $f$ is a proper morphism we see that $f_*\mathcal{F}$
 is a coherent $\mathcal{O}_Y$-module
-(Lemma \ref{lemma-proper-pushforward-coherent}).
+(Proposition \ref{proposition-proper-pushforward-coherent}).
 Thus the statement of the lemma makes sense.
 Consider the compositions
 $$
@@ -5503,7 +5504,7 @@ \section{Grothendieck's existence theorem, II}
 (Lemma \ref{lemma-existence-projective})
 there exists a coherent module $\mathcal{F}'$ on $X'$ such
 that $(\mathcal{F}')^\wedge \cong (f^*\mathcal{F}_n)$. By
-Lemma \ref{lemma-proper-pushforward-coherent}
+Proposition \ref{proposition-proper-pushforward-coherent}
 the $\mathcal{O}_X$-module $\mathcal{H} = f_*\mathcal{F}'$ is coherent
 and by Lemma \ref{lemma-inverse-systems-push-pull}
 there exists a morphism $(\mathcal{F}_n) \to \mathcal{H}^\wedge$
@@ -5634,9 +5635,8 @@ \section{Grothendieck's existence theorem, II}
 
 \medskip\noindent
 Let $\mathcal{K}$ be the quasi-coherent sheaf of ideals cutting
-out the reduced complement $X \setminus U$.
-By
-Lemma \ref{lemma-proper-pushforward-coherent}
+out the reduced complement $X \setminus U$. By
+Proposition \ref{proposition-proper-pushforward-coherent}
 the $\mathcal{O}_X$-module $\mathcal{H} = f_*\mathcal{F}'$ is coherent
 and by Lemma \ref{lemma-inverse-systems-push-pull}
 there exists a morphism $\alpha : (\mathcal{F}_n) \to \mathcal{H}^\wedge$
diff --git a/cohomology.tex b/cohomology.tex
index 2f04aed47..cb1191160 100644
--- a/cohomology.tex
+++ b/cohomology.tex
@@ -3172,7 +3172,7 @@ \section{Vanishing on Noetherian topological spaces}
 
 \noindent
 The aim is to prove a theorem of Grothendieck namely
-Lemma \ref{lemma-vanishing-Noetherian}. See \cite{Tohoku}.
+Proposition \ref{proposition-vanishing-Noetherian}. See \cite{Tohoku}.
 
 \begin{lemma}
 \label{lemma-cohomology-and-closed-immersions}
@@ -3397,8 +3397,8 @@ \section{Vanishing on Noetherian topological spaces}
 hence we get the lemma.
 \end{proof}
 
-\begin{lemma}
-\label{lemma-vanishing-Noetherian}
+\begin{proposition}[Grothendieck]
+\label{proposition-vanishing-Noetherian}
 \begin{reference}
 \cite[Theorem 3.6.5]{Tohoku}.
 \end{reference}
@@ -3406,7 +3406,7 @@ \section{Vanishing on Noetherian topological spaces}
 If $\dim(X) \leq d$, then $H^p(X, \mathcal{F}) = 0$
 for all $p > d$ and any abelian sheaf $\mathcal{F}$
 on $X$.
-\end{lemma}
+\end{proposition}
 
 \begin{proof}
 We prove this lemma by induction on $d$.
@@ -3659,7 +3659,8 @@ \section{Cohomology on spectral spaces}
 
 \noindent
 The following result on cohomological vanishing
-improves Grothendieck's result (Lemma \ref{lemma-vanishing-Noetherian})
+improves Grothendieck's result
+(Proposition \ref{proposition-vanishing-Noetherian})
 and can be found in \cite{Scheiderer}.
 
 \begin{proposition}
diff --git a/crystalline.tex b/crystalline.tex
index e29ff208a..62ec4358c 100644
--- a/crystalline.tex
+++ b/crystalline.tex
@@ -4698,7 +4698,8 @@ \section{Some further results}
 of dimension $e$ over $S$
 (see Lemma \ref{lemma-compute-cohomology-crystal-smooth}).
 These de Rham complexes are zero in all degrees $>e$. Hence (1)
-follows from Cohomology, Lemma \ref{cohomology-lemma-vanishing-Noetherian}.
+follows from Cohomology, Proposition
+\ref{cohomology-proposition-vanishing-Noetherian}.
 In case (2) we use the alternating {\v C}ech complex (see
 Remark \ref{remark-alternating-cech-complex}) to reduce to the case
 $X$ affine. In the affine case we prove the result using the de Rham complex
diff --git a/etale-cohomology.tex b/etale-cohomology.tex
index fc910982e..bedc6ce61 100644
--- a/etale-cohomology.tex
+++ b/etale-cohomology.tex
@@ -7551,9 +7551,7 @@ \section{Vanishing of finite higher direct images}
 Algebra, Lemma \ref{algebra-lemma-ring-with-only-minimal-primes}.
 Thus the higher cohomology groups of an abelian sheaf on the topological
 space $S$ (i.e., Zariski cohomology) is trivial, see
-Topology, Lemma \ref{topology-lemma-profinite-refine-open-covering}
-and
-Cohomology on Sites, Lemma \ref{sites-cohomology-lemma-w-contractible}.
+Cohomology, Lemma \ref{cohomology-lemma-vanishing-for-profinite}.
 The local rings are strictly henselian by
 Algebra, Lemma \ref{algebra-lemma-local-dimension-zero-henselian}.
 Thus \'etale cohomology of $S$ is computed by Zariski cohomology
@@ -8930,7 +8928,8 @@ \section{The Artin-Schreier sequence}
 be a coherent sheaf of ideals on $Z$. To finish the proof have to show
 that $H^d(X, i_*\mathcal{I}) = H^d(Z, \mathcal{I})$ is finite dimensional.
 If $\dim(Z) < d$, then the result holds because the cohomology group
-will be zero (Cohomology, Lemma \ref{cohomology-lemma-vanishing-Noetherian}).
+will be zero (Cohomology, Proposition
+\ref{cohomology-proposition-vanishing-Noetherian}).
 In this way we reduce to the situation discussed in the following paragraph.
 
 \medskip\noindent
diff --git a/more-morphisms.tex b/more-morphisms.tex
index 9d1dacc04..ece8558f9 100644
--- a/more-morphisms.tex
+++ b/more-morphisms.tex
@@ -9350,7 +9350,8 @@ \section{Stein factorization}
 and finite type
 (Morphisms, Lemma \ref{morphisms-lemma-permanence-finite-type}).
 Hence $f'$ is proper. By
-Cohomology of Schemes, Lemma \ref{coherent-lemma-proper-pushforward-coherent}
+Cohomology of Schemes, Proposition
+\ref{coherent-proposition-proper-pushforward-coherent}
 we see that $f_*\mathcal{O}_X$ is a coherent $\mathcal{O}_S$-module.
 Hence we see that $\pi$ is finite, i.e., (2) holds.
 
diff --git a/perfect.tex b/perfect.tex
index 7a40ec85b..a64cf8aac 100644
--- a/perfect.tex
+++ b/perfect.tex
@@ -2623,7 +2623,7 @@ \section{Compact and perfect objects}
 
 \noindent
 Let $X$ be a Noetherian scheme of finite dimension. By
-Cohomology, Lemma \ref{cohomology-lemma-vanishing-Noetherian}
+Cohomology, Proposition \ref{cohomology-proposition-vanishing-Noetherian}
 and
 Cohomology on Sites, Lemma \ref{sites-cohomology-lemma-when-jshriek-compact}
 the sheaves of modules $j_!\mathcal{O}_U$ are compact objects
diff --git a/tags/tags b/tags/tags
index 112f19591..23359a3da 100644
--- a/tags/tags
+++ b/tags/tags
@@ -3499,7 +3499,7 @@
 02O2,coherent-section-chows-lemma
 02O3,coherent-section-proper-pushforward
 02O4,coherent-lemma-locally-projective-pushforward
-02O5,coherent-lemma-proper-pushforward-coherent
+02O5,coherent-proposition-proper-pushforward-coherent
 02O6,coherent-lemma-proper-over-affine-cohomology-finite
 02O7,coherent-section-theorem-formal-functions
 02O8,coherent-lemma-cohomology-powers-ideal-times-F
@@ -3745,7 +3745,7 @@
 02UW,cohomology-lemma-irreducible-constant-cohomology-zero
 02UX,cohomology-lemma-vanishing-generated-one-section
 02UY,cohomology-lemma-subsheaf-irreducible
-02UZ,cohomology-lemma-vanishing-Noetherian
+02UZ,cohomology-proposition-vanishing-Noetherian
 02V0,schemes-lemma-composition-immersion
 02V1,morphisms-lemma-composition-universally-injective
 02V2,morphisms-lemma-composition-open
diff --git a/varieties.tex b/varieties.tex
index a476fcfae..3ee9c06cc 100644
--- a/varieties.tex
+++ b/varieties.tex
@@ -2631,8 +2631,8 @@ \section{Types of varieties}
 \end{lemma}
 
 \begin{proof}
-By
-Cohomology of Schemes, Lemma \ref{coherent-lemma-proper-pushforward-coherent}
+By Cohomology of Schemes, Proposition
+\ref{coherent-proposition-proper-pushforward-coherent}
 we see that $\Gamma(X, \mathcal{O}_X)$ is a finite dimensional
 $k$-vector space. It is also a $k$-algebra without zero-divisors.
 Hence it is a field, see
@@ -4351,7 +4351,7 @@ \section{One dimensional Noetherian schemes}
 $$
 of sheaves of abelian groups on $X$. Since $\dim(X) \leq 1$ we see that
 $H^2(X, \mathcal{F}) = 0$ for any abelian sheaf $\mathcal{F}$, see
-Cohomology, Lemma \ref{cohomology-lemma-vanishing-Noetherian}.
+Cohomology, Proposition \ref{cohomology-proposition-vanishing-Noetherian}.
 Hence the map $H^1(X, \mathcal{O}^*_X) \to H^1(Z, \mathcal{O}_Z^*)$
 is surjective. This proves the lemma by
 Cohomology, Lemma \ref{cohomology-lemma-h1-invertible}.