The Stacks project

Lemma 29.28.3. Let

be a fibre product diagram of schemes. Assume $f$ locally of finite type. Suppose that $x' \in X'$, $x = g'(x')$, $s' = f'(x')$ and $s = g(s') = f(x)$. Then

1. $\dim _ x(X_ s) = \dim _{x'}(X'_{s'})$,

2. if $F$ is the fibre of the morphism $X'_{s'} \to X_ s$ over $x$, then

   $$\dim (\mathcal{O}_{F, x'}) = \dim (\mathcal{O}_{X'_{s'}, x'}) - \dim (\mathcal{O}_{X_ s, x}) = \text{trdeg}_{\kappa (s)}(\kappa (x)) - \text{trdeg}_{\kappa (s')}(\kappa (x'))$$

   In particular $\dim (\mathcal{O}_{X'_{s'}, x'}) \geq \dim (\mathcal{O}_{X_ s, x})$ and $\text{trdeg}_{\kappa (s)}(\kappa (x)) \geq \text{trdeg}_{\kappa (s')}(\kappa (x'))$.

3. given $s', s, x$ there exists a choice of $x'$ such that $\dim (\mathcal{O}_{X'_{s'}, x'}) = \dim (\mathcal{O}_{X_ s, x})$ and $\text{trdeg}_{\kappa (s)}(\kappa (x)) = \text{trdeg}_{\kappa (s')}(\kappa (x'))$.