The Stacks project

Proof. Part (1) is essentially true by definition. Namely, if $y \in Z$, then we can take $k = 0$ and $V_0 = W_0 = \overline{\{ y\} }$.

Proof of (2). Let $y \leadsto y'$ be a nontrivial specialization and let $V_0 \subset W_0 \supset V_1 \subset W_1 \supset \ldots \subset W_ k$ is a system for $y$. Here there are two cases. Case I: $V_ k = W_ k$, i.e., $c_ k = 0$. In this case we can set $V'_ k = W'_ k = \overline{\{ y'\} }$. An easy computation shows that $\delta (V_0, W_0, \ldots , V'_ k, W'_ k) \leq \delta (V_0, W_0, \ldots , V_ k, W_ k)$ because only $b_{k - 1}$ is changed into a bigger integer. Case II: $V_ k \not= W_ k$, i.e., $c_ k > 0$. Observe that in this case $\max _{i = 0, 1, \ldots , k} (c_ i + c_{i + 1} + \ldots + c_ k - b_ i - b_{i + 1} - \ldots - b_{k - 1}) > 0$. Hence if we set $V'_{k + 1} = W_{k + 1} = \overline{\{ y'\} }$, then although $k$ is replaced by $k + 1$, the maximum now looks like

with $c_{k + 1} = 0$ and $b_ k = \text{codim}(V_{k + 1}, W_ k) > 0$. This is strictly smaller than $\max _{i = 0, 1, \ldots , k} (c_ i + c_{i + 1} + \ldots + c_ k - b_ i - b_{i + 1} - \ldots - b_{k - 1})$ and hence $\delta (V_0, W_0, \ldots , V'_{k + 1}, W'_{k + 1}) \leq \delta (V_0, W_0, \ldots , V_ k, W_ k)$ as desired.

Proof of (3). Given $y \in Y$ and $z \in \overline{\{ y\} } \cap Z$ we get the system

and $c_0 = \text{codim}(V_0, W_0) = \dim (\mathcal{O}_{\overline{\{ y\} }, z})$ by Properties, Lemma 28.10.3. Thus we see that $\delta (V_0, W_0) = 0 + c_0 = c_0$ which proves what we want.

Proof of (4). Let $\delta$ be a dimension function on $Y$. Let $V_0 \subset W_0 \supset V_1 \subset W_1 \supset \ldots \subset W_ k$ be a system for $y$. Let $y'_ i \in W_ i$ and $y_ i \in V_ i$ be the generic points, so $y_0 \in Z$ and $y_ k = y$. Then we see that

Finally, we have $\delta (y'_ k) - \delta (y_{k - 1}) = c_ k$. Thus we see that

We conclude $\delta (V_0, W_0, \ldots , W_ k) \geq k + \delta (y) - \delta (y_0)$ which proves what we want.

Proof of (5). The function $\delta (y) = \dim (\overline{\{ y\} })$ is a dimension function. Hence $\delta (y) \leq \delta _ Z(y)$ by part (4). By part (3) we have $\delta _ Z(y) \leq \delta (y)$ and we are done.

Proof of (6). Given such a sequence of points, we may assume all the specializations $y'_ i \leadsto y_{i + 1}$ are nontrivial (otherwise we can shorten the chain of specializations). Then we set $V_ i = \overline{\{ y_ i\} }$ and $W_ i = \overline{\{ y'_ i\} }$ and we compute $\delta (V_0, W_1, V_1, \ldots , W_{k - 1}) = k$ because all the codimensions $c_ i$ of $V_ i \subset W_ i$ are $1$ and all $b_ i > 0$. This implies $\delta _ Z(y'_{k - 1}) \leq k$ as $y'_{k - 1}$ is the generic point of $W_ k$. Then $\delta _ Z(y) \leq k$ by part (2) as $y$ is a specialization of $y_{k - 1}$.

Proof of (7). This is clear as their are fewer systems to consider in the computation of $\delta ^{Y'}_{Y' \cap Z}$. $\square$

Proof. If $\delta _{Z'}(y') = \infty$, then there is nothing to prove. If $\delta _{Z'}(y') < \infty$, then we choose a system of integral closed subschemes

of $Y'$ with $V'_0 \subset Z'$ and $y'$ the generic point of $W'_ k$ such that $\delta _{Z'}(y') = \delta (V'_0, W'_0, \ldots , W'_ k)$. Denote

the scheme theoretic images of the above schemes in $Y$. Observe that $y$ is the generic point of $W_ k$ and that $V_0 \subset Z$. For each $i$ we look at the diagram

Denote $n_ i$ the relative dimension of $V'_ i/V_ i$ and $m_ i$ the relative dimension of $W'_ i/W_ i$; more precisely these are the transcendence degrees of the corresponding extensions of the function fields. Set $c_ i = \text{codim}(V_ i, W_ i)$, $c'_ i = \text{codim}(V'_ i, W'_ i)$, $b_ i = \text{codim}(V_{i + 1}, W_ i)$, and $b'_ i = \text{codim}(V'_{i + 1}, W'_ i)$. By the dimension formula we have

See Morphisms, Lemma 29.52.1. Hence $c_ i - b_ i = c'_ i - b'_ i + n_ i - n_{i + 1}$. Thus we see that

Thus we see that

Since $m_ k = \text{trdeg}_{\kappa (y)}(\kappa (y'))$ we conclude that

as desired. $\square$