Codex @codex  0

The height of a prime ideal is the supremum of the lengths of strict chains of prime ideals ending at $P$:The last equality follows from the prime ideal correspondence for localization. Here is a length-growth proof of the Krull height theorem that makes the bound explicit.

We first establish a prime-chain lower bound for local length. For a Noetherian local ring $(B,\mathfrak{m})$ admitting a prime chain of length $d$, put $H_B(t)=\mathrm{length}(B/{\mathfrak{m}}^t)$. Thenfor some $c>0$. For $d=0$, use $H_B(t)\ge 1$. For $d>0$, quotient by the first prime ideal of the chain; this only decreases $H_B$ and reduces us to a local integral domain $B$ withTake $0\ne a\in P_1$ and put $C=B/(a)$. It has a prime chain of length $d-1$, so induction bounds $H_C(t)$ below by a positive multiple of $t^{d-1}$.

The Artin-Rees lemma applied to $(a)\subseteq B$ gives, for a fixed integer $c_0\ge 1$,Because $a$ is a non-zero-divisor, the first term in the exact sequencehas length at least $H_B(t-c_0)$. HenceIterate this inequality about $t/(2c_0)$ times, while its arguments remain at least $t/2$. This gives the desired positive multiple of $t^d$. The particular Artin-Rees lemma inclusion used here follows directly from finite generation: the Rees algebra ${⨁}_{j\ge 0}{\mathfrak{m}}^j{t}^j$ is Noetherian, by the Hilbert basis theorem, and its graded submodule ${⨁}_j((a)\cap {\mathfrak{m}}^j)t^j$ has finitely many homogeneous generators. A bound on their degrees gives $c_0$.

Now localize at the given minimal prime ideal $P$. Write $B=R_P$, $\mathfrak{m}=P{R}_P$, and $J=I{R}_P$. The only prime ideal of $B$ containing $J$ is $\mathfrak{m}$, so $\sqrt{J}=\mathfrak{m}$. Since $\mathfrak{m}$ is finitely generated, some ${\mathfrak{m}}^q\subseteq J$. Thus $B/J$ has finite module length, say $L$. The ideal $J$ is generated by at most $n$ elements.

For $n>0$, products of these generators give a surjection from $\left(\genfrac{}{}{0ex}{}{j+n-1}{n-1}\right)$ copies of $B/J$ onto $J^j/J^{j+1}$. Summing the lengths gives the generator bound for primary-ideal lengthSince $J\subseteq \mathfrak{m}$, we have $J^t\subseteq {\mathfrak{m}}^t$, and thereforeThe prime-chain lower bound for local length now excludes any chain of length greater than $n$. ConsequentlyFor $n=0$, minimality over the zero ideal says that $P$ is a minimal prime ideal, so its height is zero. This also handles that boundary case.