The Stacks project

Proof. Let $F_{\bullet }$ be a finite resolution of $\kappa $ by finite free $R$-modules (Lemma 10.109.7). By Lemma 10.102.2 we may assume all the maps in the complex $F_{\bullet }$ have to property that $\mathop{\mathrm{Im}}(F_ i \to F_{i-1}) \subset \mathfrak m F_{i-1}$, because removing a trivial summand from the resolution can at worst shorten the resolution. Say $F_ n \not= 0$ and $F_ i = 0$ for $i > n$, so that the projective dimension of $\kappa $ is $n$. By Proposition 10.102.9 we see that $\text{depth}_{I(\varphi _ n)}(R) \geq n$ since $I(\varphi _ n)$ cannot equal $R$ by our choice of the complex. Thus by Lemma 10.72.3 also $\dim (R) \geq n$. $\square$