Rerducedness lemma generalized

Thanks to Laurent Moret-Bailly
https://stacks.math.columbia.edu/tag/0C0D#comment-8088

flat.tex

@@ -5813,6 +5813,48 @@ \section{How purity is used}
 Algebra, Lemma \ref{algebra-lemma-minimal-contains}.
 \end{proof}
 
+\noindent
+An application is the following.
+
+\begin{lemma}
+\label{lemma-proper-flat-over-dvr-reduced-fibre}
+Let $X \to \Spec(R)$ be a proper flat morphism where $R$ is a valuation ring.
+If the special fibre is reduced, then $X$ and every fibre of $X \to \Spec(R)$
+is reduced.
+\end{lemma}
+
+\begin{proof}
+Assume the special fibre $X_s$ is reduced.
+Let $x \in X$ be any point, and let us show that $\mathcal{O}_{X, x}$
+is reduced; this will prove that $X$ is reduced.
+Let $x \leadsto x'$ be a specialization with $x'$
+in the special fibre; such a specialization exists
+as a proper morphism is closed. Consider the local
+ring $A = \mathcal{O}_{X, x'}$. Then $\mathcal{O}_{X, x}$
+is a localization of $A$, so it suffices to show that
+$A$ is reduced. Let $a \in A$ and let $I = (\pi) \subset R$ be its
+content ideal, see
+Lemma \ref{lemma-flat-finite-type-local-valuation-ring-has-content}.
+Then $a = \pi a'$ and $a'$ maps to a nonzero element of
+$A/\mathfrak mA$ where $\mathfrak m \subset R$ is the maximal ideal.
+If $a$ is nilpotent, so is $a'$, because $\pi$ is a nonzerodivisor
+by flatness of $A$ over $R$.
+But $a'$ maps to a nonzero element of the reduced ring
+$A/\mathfrak m A = \mathcal{O}_{X_s, x'}$.
+This is a contradiction unless $A$ is reduced, which
+is what we wanted to show.
+
+\medskip\noindent
+Of course, if $X$ is reduced, so is the generic fibre of $X$ over $R$.
+If $\mathfrak p \subset R$ is a
+prime ideal, then $R/\mathfrak p$ is a valuation ring by
+Algebra, Lemma \ref{algebra-lemma-make-valuation-rings}.
+Hence redoing the argument with the base change of $X$
+to $R/\mathfrak p$ proves the fibre over $\mathfrak p$
+is reduced.
+\end{proof}
+
+
 
 
 

more-morphisms.tex

@@ -7199,7 +7199,7 @@ \section{Reduced fibres}
 \end{lemma}
 
 \begin{proof}
-Assume the special fibre is reduced.
+Assume the special fibre $X_s$ is reduced.
 Let $x \in X$ be any point, and let us show that $\mathcal{O}_{X, x}$
 is reduced; this will prove that $X$ and $X_\eta$ are reduced.
 Let $x \leadsto x'$ be a specialization with $x'$