The Stacks project

Proof. Choose a smooth surjective morphism $f:U \to \mathcal{X}$ whose source is a scheme, and consider the function $u \mapsto \dim _{f(u)}(\mathcal{X});$ since the morphism $|U| \to |\mathcal{X}|$ induced by $f$ is open (as $f$ is smooth) as well as surjective (by assumption), and takes finite type points to finite type points (by the very definition of the finite type points of $|\mathcal{X}|$), it suffices to show that for any $u \in U$, and any open neighbourhood of $u$, there is a finite type point $u_0$ in this neighbourhood such that $\dim _{f(u_0)}(\mathcal{X}) = \dim _{f(u)}(\mathcal{X}).$ Since, with this reformulation of the problem, the surjectivity of $f$ is no longer required, we may replace $U$ by the open neighbourhood of the point $u$ in question, and thus reduce to the problem of showing that for each $u \in U$, there is a finite type point $u_0 \in U$ such that $\dim _{f(u_0)}(\mathcal{X}) = \dim _{f(u)}(\mathcal{X}).$ By Lemma 107.5.4 $\dim _{f(u)}(\mathcal{X}) = \dim _ u(U) - \dim _ u(U_{f(u)}),$ while $\dim _{f(u_0)}(\mathcal{X}) = \dim _{u_0}(U) - \dim _{u_0}(U_{f(u_0)}).$ Since $f$ is smooth, the expression $\dim _{u_0}(U_{f(u_0)})$ is locally constant as $u_0$ varies over $U$ (by Lemma 107.5.11 (2)), and so shrinking $U$ further around $u$ if necessary, we may assume it is constant. Thus the problem becomes to show that we may find a finite type point $u_0 \in U$ for which $\dim _{u_0}(U) = \dim _ u(U)$. Since by definition $\dim _ u U$ is the minimum of the dimensions $\dim V$, as $V$ ranges over the open neighbourhoods $V$ of $u$ in $U$, we may shrink $U$ down further around $u$ so that $\dim _ u U = \dim U$. The existence of desired point $u_0$ then follows from Lemma 107.5.12. $\square$