The Stacks project

Remark 37.52.8. We can use Lemma 37.52.6 or its variant Lemma 37.52.7 to give an alternative proof of Lemma 37.52.4 in case $S$ is locally Noetherian. Here is a rough sketch. Namely, first replace $S$ by the spectrum of the local ring at $s'$. Then we may use induction on $\dim (S)$. The case $\dim (S) = 0$ is trivial because then $s' = s$. Replace $X$ by the reduced induced scheme structure on $\overline{\{ x\} }$. Apply Lemma 37.52.7 to $X \to S$ and $x' \mapsto s'$ and any nonempty open $U \subset X$ containing $x$. This gives us a closed subscheme $x' \in Z \subset X$ a point $z \in Z$ such that $Z \to S$ is quasi-finite at $x'$ and such that $f(z) \not= s'$. Then $z$ is a closed point of $X_{f(z)}$, and $z \leadsto x'$. As $f(z) \not= s'$ we see $\dim (\mathcal{O}_{S, f(z)}) < \dim (S)$. Since $x$ is the generic point of $X$ we see $x \leadsto z$, hence $s = f(x) \leadsto f(z)$. Apply the induction hypothesis to $s \leadsto f(z)$ and $z \mapsto f(z)$ to win.