The Stacks project

Proof. If $R_{\mathfrak p}$ is Noetherian (and hence $S_{\mathfrak q}$ Noetherian since it is essentially of finite type over $R_{\mathfrak p}$) then this follows immediately from Lemma 10.112.6 and the definitions. In the general case, let $S'$ be the integral closure of $R_\mathfrak p$ in $S_\mathfrak p$. By Zariski's Main Theorem 10.123.12 we have $S_{\mathfrak q} = S'_{\mathfrak q'}$ for some $\mathfrak q' \subset S'$ lying over $\mathfrak q$. By Lemma 10.112.3 we have $\dim (S') \leq \dim (R_\mathfrak p)$ and hence a fortiori $\dim (S_\mathfrak q) = \dim (S'_{\mathfrak q'}) \leq \dim (R_\mathfrak p)$. $\square$