The Height of an Ideal #
In this file, we define the height of a prime ideal and the height of an ideal.
Main definitions #
Ideal.primeHeight
: The height of a prime ideal $\mathfrak{p}$. We define it as the supremum of the lengths of strictly decreasing chains of prime ideals below it. This definition is implemented viaOrder.height
.Ideal.height
: The height of an ideal. We defined it as the infimum of theprimeHeight
of the minimal prime ideals of I.
The height of a prime ideal is defined as the supremum of the lengths of strictly decreasing chains of prime ideals below it.
Equations
- I.primeHeight = Order.height { asIdeal := I, isPrime := hI }
Instances For
The height of an ideal is defined as the infimum of the heights of its minimal prime ideals.
Equations
- I.height = ⨅ (J : Ideal R), ⨅ (h : J ∈ I.minimalPrimes), J.primeHeight
Instances For
For a prime ideal, its height equals its prime height.
An ideal has finite height if it is either the unit ideal or its height is finite.
We include the unit ideal in order to have the instance IsNoetherianRing R → FiniteHeight I
.
Instances
If R
has finite Krull dimension, there exists a maximal ideal m
with ht m = dim R
.
If J has finite height and I ≤ J, then I has finite height
If J is a prime ideal containing I, and its height is less than or equal to the height of I, then J is a minimal prime over I
A prime ideal has height zero if and only if it is minimal
In a trivial commutative ring, the height of any ideal is ∞
.
The prime height of the maximal ideal equals the Krull dimension in a local ring
The height of the maximal ideal equals the Krull dimension in a local ring.
For a local ring with finite Krull dimension, a prime ideal has height equal to the Krull dimension if and only if it is the maximal ideal.
In a nontrivial commutative ring R
, the supremum of heights of all ideals is equal to the
Krull dimension of R
.
In a nontrivial commutative ring R
, the supremum of prime heights of all prime ideals is
equal to the Krull dimension of R
.
In a nontrivial commutative ring R
, the supremum of prime heights of all maximal ideals is
equal to the Krull dimension of R
.