The Stacks project

Proof. Assume the pair $(X, x)$ satisfies the equivalent conditions for Lemma 68.4.2. Let $U$ be a scheme, $U \to X$ étale, and let $u, u' \in |U|$ map to $x$ of $|X|$, and $u' \leadsto u$. We may and do replace $U$ by an affine neighbourhood of $u$. Let $t, s : R = U \times _ X U \to U$ be the étale projection maps.

Pick a point $r \in R$ with $t(r) = u$ and $s(r) = u'$. This is possible by Properties of Spaces, Lemma 66.4.5. Because generalizations lift along the étale morphism $t$ (Remark 68.4.1) we can find a specialization $r' \leadsto r$ with $t(r') = u'$. Set $u'' = s(r')$. Then $u'' \leadsto u'$. Thus we may repeat and find $r'' \leadsto r'$ with $t(r'') = u''$. Set $u''' = s(r'')$, and so on. Here is a picture:

In Remark 68.4.1 we have seen that there are no specializations among points in the fibres of the étale morphism $s$. Hence if $u^{(n + 1)} = u^{(n)}$ for some $n$, then also $r^{(n)} = r^{(n - 1)}$ and hence also (by taking $t$) $u^{(n)} = u^{(n - 1)}$. This then forces the whole tower to collapse, in particular $u = u'$. Thus we see that if $u \not= u'$, then all the specializations are strict and $\{ u, u', u'', \ldots \} $ is an infinite set of points in $U$ which map to the point $x$ in $|X|$. As we chose $U$ affine this contradicts the second part of Lemma 68.4.2, as desired. $\square$

Proof. The discussion in Schemes, Section 26.13 shows that $\mathcal{O}_{U, u'}$ is a localization of the Noetherian local ring $\mathcal{O}_{U, u}$. By Properties of Spaces, Lemma 66.10.1 we have $\dim (\mathcal{O}_{U, u}) = \dim (\mathcal{O}_{U, u'})$. By dimension theory for Noetherian local rings we conclude $u = u'$. $\square$

Proof. We may replace $U$ by an affine open neighbourhood of $u$. Hence we may assume that $U$ is affine. As $x$ is in the image of the open map $|U| \to |X|$, so is $x'$. Thus we may replace $X$ by the Zariski open subspace corresponding to the image of $|U| \to |X|$, see Properties of Spaces, Lemma 66.4.10. In other words we may assume that $U \to X$ is surjective and étale. Let $s, t : R = U \times _ X U \to U$ be the projections. By our assumption that $(X, x')$ satisfies the equivalent conditions of Lemma 68.4.5 we see that the fibres of $|U| \to |X|$ and $|R| \to |X|$ over $x'$ are finite. Say $\{ u'_1, \ldots , u'_ n\} \subset U$ and $\{ r'_1, \ldots , r'_ m\} \subset R$ form the complete inverse image of $\{ x'\} $. Consider the closed sets

Trivially we have $s(T') \subset T$. Because $R$ is an equivalence relation we also have $t(T') = s(T')$ as the set $\{ r_ j'\} $ is invariant under the inverse of $R$ by construction. Let $w \in T$ be any point. Then $u'_ i \leadsto w$ for some $i$. Choose $r \in R$ with $s(r) = w$. Since generalizations lift along $s : R \to U$, see Remark 68.4.1, we can find $r' \leadsto r$ with $s(r') = u_ i'$. Then $r' = r'_ j$ for some $j$ and we conclude that $w \in s(T')$. Hence $T = s(T') = t(T')$ is an $|R|$-invariant closed set in $|U|$. This means $T$ is the inverse image of a closed (!) subset $T'' = \varphi (T)$ of $|X|$, see Properties of Spaces, Lemmas 66.4.5 and 66.4.6. Hence $T'' = \overline{\{ x'\} }$. Thus $T$ contains some point $u_1$ mapping to $x$ as $x \in T''$. I.e., we see that for some $i$ there exists a specialization $u'_ i \leadsto u_1$ which maps to the given specialization $x' \leadsto x$.

To finish the proof, choose a point $r \in R$ such that $s(r) = u$ and $t(r) = u_1$ (using Properties of Spaces, Lemma 66.4.3). As generalizations lift along $t$, and $u'_ i \leadsto u_1$ we can find a specialization $r' \leadsto r$ such that $t(r') = u'_ i$. Set $u' = s(r')$. Then $u' \leadsto u$ and $\varphi (u') = x'$ as desired. $\square$

Proof. (The parenthetical statement holds by the definition of decent spaces and the implications between the different separation conditions mentioned in Section 68.6.) Choose a scheme $V$ and a surjective étale morphism $V \to Y$. Choose $v \in V$ mapping to $y$. Then we see that it suffices to prove the lemma for $V \to X$. Thus we may assume $Y$ is a scheme. Choose a scheme $U$ and a surjective étale morphism $U \to X$. Choose $u \in U$ mapping to $x$. By Lemma 68.7.3 we may choose $u' \leadsto u$ mapping to $x'$. By Properties of Spaces, Lemma 66.4.3 we may choose $z \in U \times _ X Y$ mapping to $y$ and $u$. Thus we reduce to the case of the flat morphism of schemes $U \times _ X Y \to U$ which is Morphisms, Lemma 29.25.9. $\square$