---
tag: SJZW2HN1SC
kind: statement
role: theorem
name: Krull's principal ideal theorem
msc: ["13C15", "13E05"]
uses: [0MVH4Y1CRZ, 06HC6HK0Z8, 9BKCZPMQT6, S2D8823P8B]
about: [87WH65FJB8, 0670T59HGE]
sources:
  - url: https://en.wikipedia.org/wiki/Krull%27s_principal_ideal_theorem
same_as:
  wikidata: Q3527241
  wikipedia: Krull's principal ideal theorem
---

## Statement

Let $R$ be a commutative [[Noetherian ring|0MVH4Y1CRZ]] and let $x \in R$.
Let $P$ be a [[prime ideal|06HC6HK0Z8]] of $R$ that is [[minimal|S2D8823P8B]] among the prime ideals containing $x$.
Then the [[height|9BKCZPMQT6]] of $P$ is at most $1$.

## Remarks

After localizing at $P$, one may assume that $R$ is local with maximal ideal $P$, and then $R/xR$ is Artinian.
If $Q \subsetneq P$ is prime, the chain of ideals $xR + Q^{(n)}$ stabilizes, where $Q^{(n)}$ is the [[symbolic power|7VFPQVCNJ7]]; with Nakayama's lemma this gives $Q^{(n)} = Q^{(n+1)}$ for large $n$.
Then $Q^n R_Q = 0$ in $R_Q$, so $R_Q$ is Artinian, and $Q$ has height $0$.
For example, in $k[x, y]$ the prime $(x)$ is minimal over $x$ and has height $1$.
The Noetherian hypothesis is needed.
In a valuation domain whose value group is $\Z \times \Z$ with the lexicographic order, the maximal ideal has height $2$ but is minimal over a single element.
If $x$ is not a zero divisor and not a unit, every prime minimal over $x$ has height exactly $1$.

## Explanations

### L1 human

Cutting a space by one equation lowers its dimension by at most one.
In algebra: a prime ideal that is minimal over one element sits at most one step above a minimal prime.

### L2 human

The theorem, the Hauptidealsatz, is the base case of [[Krull's height theorem|TBRTZMHFTV]] for ideals generated by $n$ elements.
Through that generalisation, it shows that every prime ideal of a Noetherian ring has finite height.
It also gives the criterion that a Noetherian domain is a unique factorisation domain exactly when every height one prime is principal.
It is a basic tool in dimension theory, for example in the [[dimension theorem for local rings|KW3HY77V6D]].