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.height : The height of an ideal. We defined it as the infimum of the primeHeight of the minimal prime ideals of I.

noncomputable def Ideal.height {R : Type u_1} [CommRing R] (I : Ideal R) : ℕ∞

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), Ideal.primeHeight✝ J

theorem PrimeSpectrum.height_eq_orderHeight {R : Type u_1} [CommRing R] (p : PrimeSpectrum R) : p.asIdeal.height = Order.height p

theorem Ideal.height_eq_inf_minimalPrimes {R : Type u_1} [CommRing R] (I : Ideal R) : I.height = ⨅ J ∈ I.minimalPrimes, J.height

theorem Ideal.exists_isPrime_height_eq {R : Type u_1} [CommRing R] {I : Ideal R} {n : ℕ} (hI : I.height = ↑n) : ∃ (p : Ideal R) (_ : p.IsPrime) (_ : I ≤ p), p.height = ↑n

class Ideal.FiniteHeight {R : Type u_1} [CommRing R] (I : Ideal R) : Prop

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.

• eq_top_or_height_ne_top : I = ⊤ ∨ I.height ≠ ⊤

theorem Ideal.finiteHeight_iff {R : Type u_1} [CommRing R] (I : Ideal R) : I.FiniteHeight ↔ I = ⊤ ∨ I.height ≠ ⊤

theorem Ideal.finiteHeight_iff_lt {R : Type u_1} [CommRing R] {I : Ideal R} : I.FiniteHeight ↔ I = ⊤ ∨ I.height < ⊤

theorem Ideal.height_ne_top {R : Type u_1} [CommRing R] {I : Ideal R} (hI : I ≠ ⊤) [I.FiniteHeight] : I.height ≠ ⊤

theorem Ideal.height_lt_top {R : Type u_1} [CommRing R] {I : Ideal R} (hI : I ≠ ⊤) [I.FiniteHeight] : I.height < ⊤

theorem Ideal.height_ne_top_of_isPrime {R : Type u_1} [CommRing R] {I : Ideal R} [I.FiniteHeight] [I.IsPrime] : I.height ≠ ⊤

theorem Ideal.height_lt_top_of_isPrime {R : Type u_1} [CommRing R] {I : Ideal R} [I.FiniteHeight] [I.IsPrime] : I.height < ⊤

theorem Ideal.exists_ltSeries_length_eq_height {R : Type u_1} [CommRing R] (p : Ideal R) [p.IsPrime] [p.FiniteHeight] : ∃ (l : LTSeries (PrimeSpectrum R)), RelSeries.last l = { asIdeal := p, isPrime := ⋯ } ∧ ↑l.length = p.height

theorem Ideal.height_add_one_le_of_lt_of_isPrime {R : Type u_1} [CommRing R] {I J : Ideal R} [I.IsPrime] [J.IsPrime] (h : I < J) : I.height + 1 ≤ J.height

@[simp]

theorem Ideal.height_top {R : Type u_1} [CommRing R] : ⊤.height = ⊤

theorem Ideal.height_mono {R : Type u_1} [CommRing R] {I J : Ideal R} (h : I ≤ J) : I.height ≤ J.height

theorem Ideal.height_strict_mono_of_isPrime {R : Type u_1} [CommRing R] {I J : Ideal R} [I.IsPrime] (h : I < J) [I.FiniteHeight] : I.height < J.height

theorem Ideal.height_strict_mono_of_isPrime_of_isPrime {R : Type u_1} [CommRing R] {I J : Ideal R} [I.IsPrime] [J.IsPrime] (h : I < J) [J.FiniteHeight] : I.height < J.height

@[deprecated Ideal.height_strict_mono_of_isPrime_of_isPrime (since := "2026-04-02")]

theorem Ideal.height_strict_mono_of_isPrime_of_is_prime {R : Type u_1} [CommRing R] {I J : Ideal R} [I.IsPrime] [J.IsPrime] (h : I < J) [J.FiniteHeight] : I.height < J.height

Alias of Ideal.height_strict_mono_of_isPrime_of_isPrime.

theorem Ideal.height_le_ringKrullDim_of_isPrime {R : Type u_1} [CommRing R] {I : Ideal R} [I.IsPrime] : ↑I.height ≤ ringKrullDim R

theorem Ideal.eq_of_le_of_height_le {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] [I.FiniteHeight] {J : Ideal R} (h : I ≤ J) (h_height : J.height ≤ I.height) : I = J

A prime ideal of finite height is equal to any ideal that contains it with no greater height.

theorem Ideal.height_le_ringKrullDim_of_ne_top {R : Type u_1} [CommRing R] {I : Ideal R} (h : I ≠ ⊤) : ↑I.height ≤ ringKrullDim R

theorem Ideal.exists_isMaximal_height {R : Type u_1} [CommRing R] [FiniteRingKrullDim R] : ∃ (p : Ideal R), p.IsMaximal ∧ ↑p.height = ringKrullDim R

If R has finite Krull dimension, there exists a maximal ideal m with ht m = dim R.

@[instance 900]

instance Ideal.finiteHeight_of_finiteRingKrullDim {R : Type u_1} [CommRing R] {I : Ideal R} [FiniteRingKrullDim R] : I.FiniteHeight

theorem Ideal.finiteHeight_of_le {R : Type u_1} [CommRing R] {I J : Ideal R} (e : I ≤ J) (hJ : J ≠ ⊤) [J.FiniteHeight] : I.FiniteHeight

If J has finite height and I ≤ J, then I has finite height

theorem Ideal.mem_minimalPrimes_of_height_eq {R : Type u_1} [CommRing R] {I J : Ideal R} (e : I ≤ J) [J.IsPrime] [J.FiniteHeight] (e' : J.height ≤ I.height) : J ∈ I.minimalPrimes

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

theorem Ideal.height_eq_zero_iff {R : Type u_1} [CommRing R] {I : Ideal R} [I.IsPrime] : I.height = 0 ↔ I ∈ minimalPrimes R

A prime ideal has height zero if and only if it is minimal

theorem Ideal.one_le_height_span_singleton_of_mem_nonZeroDivisors {R : Type u_1} [CommRing R] {x : R} (hx : x ∈ nonZeroDivisors R) : 1 ≤ (span {x}).height

If x is a non-zero-divisor, then span {x} has height at least 1.

@[simp]

theorem Ideal.height_bot {R : Type u_1} [CommRing R] [Nontrivial R] : ⊥.height = 0

@[simp]

theorem Ideal.height_eq_zero_iff_eq_bot {R : Type u_1} [CommRing R] [IsDomain R] {I : Ideal R} : I.height = 0 ↔ I = ⊥

theorem Ideal.ne_bot_of_height_eq_one {R : Type u_1} [CommRing R] [IsDomain R] {I : Ideal R} (h : I.height = 1) : I ≠ ⊥

@[simp]

theorem Ideal.height_of_subsingleton {R : Type u_1} [CommRing R] (I : Ideal R) [Subsingleton R] : I.height = ⊤

In a trivial commutative ring, the height of any ideal is ∞.

theorem Ideal.isMaximal_of_height_eq_ringKrullDim {R : Type u_1} [CommRing R] {I : Ideal R} [I.IsPrime] [FiniteRingKrullDim R] (e : ↑I.height = ringKrullDim R) : I.IsMaximal

@[simp]

theorem IsLocalRing.maximalIdeal_height_eq_ringKrullDim {R : Type u_1} [CommRing R] [IsLocalRing R] : ↑(maximalIdeal R).height = ringKrullDim R

The height of the maximal ideal equals the Krull dimension in a local ring.

theorem Ideal.height_eq_ringKrullDim_iff {R : Type u_1} [CommRing R] [FiniteRingKrullDim R] [IsLocalRing R] {I : Ideal R} [I.IsPrime] : ↑I.height = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R

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.

theorem Ideal.height_le_iff {R : Type u_1} [CommRing R] {p : Ideal R} {n : ℕ} [p.IsPrime] : p.height ≤ ↑n ↔ ∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n

theorem Ideal.height_le_iff_covBy {R : Type u_1} [CommRing R] {p : Ideal R} {n : ℕ} [p.IsPrime] [IsNoetherianRing R] : p.height ≤ ↑n ↔ ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n

@[simp]

theorem RingEquiv.height_comap {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (e : R ≃+* S) (I : Ideal S) : (Ideal.comap e I).height = I.height

@[simp]

theorem RingEquiv.height_map {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (e : R ≃+* S) (I : Ideal R) : (Ideal.map e I).height = I.height

theorem ringKrullDim_le_iff_height_le {R : Type u_2} [CommRing R] (n : WithBot ℕ∞) : ringKrullDim R ≤ n ↔ ∀ ⦃p : Ideal R⦄, p.IsPrime → ↑p.height ≤ n

dim R ≤ n if and only if the height of all prime ideals is less than n.

theorem ringKrullDim_le_iff_isMaximal_height_le {R : Type u_2} [CommRing R] (n : WithBot ℕ∞) : ringKrullDim R ≤ n ↔ ∀ ⦃m : Ideal R⦄, m.IsMaximal → ↑m.height ≤ n

dim R ≤ n if and only if the height of all maximal ideals is less than n.

theorem IsLocalization.height_under {R : Type u_1} [CommRing R] (S : Submonoid R) {A : Type u_2} [CommRing A] [Algebra R A] [IsLocalization S A] (J : Ideal A) : (Ideal.under R J).height = J.height

@[deprecated IsLocalization.height_under (since := "2026-04-09")]

theorem IsLocalization.height_comap {R : Type u_1} [CommRing R] (S : Submonoid R) {A : Type u_2} [CommRing A] [Algebra R A] [IsLocalization S A] (J : Ideal A) : (Ideal.under R J).height = J.height

Alias of IsLocalization.height_under.

theorem IsLocalization.AtPrime.ringKrullDim_eq_height {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] (A : Type u_2) [CommRing A] [Algebra R A] [IsLocalization.AtPrime A I] : ringKrullDim A = ↑I.height

theorem IsLocalization.height_map_of_disjoint {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] (p : Ideal R) [p.IsPrime] (h : Disjoint ↑M ↑p) : (Ideal.map (algebraMap R S) p).height = p.height

theorem exists_spanRank_le_and_le_height_of_le_height {R : Type u_1} [CommRing R] [IsNoetherianRing R] (I : Ideal R) (r : ℕ) (hr : ↑r ≤ I.height) : ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height

theorem Ideal.sup_height_eq_ringKrullDim {R : Type u_1} [CommRing R] [Nontrivial R] : ↑(⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) = ringKrullDim R

In a nontrivial commutative ring R, the supremum of heights of all ideals is equal to the Krull dimension of R.

theorem Ideal.sup_isPrime_height_eq_ringKrullDim {R : Type u_1} [CommRing R] [Nontrivial R] : ↑(⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height) = ringKrullDim R

In a nontrivial commutative ring R, the supremum of heights of all prime ideals is equal to the Krull dimension of R.

theorem Ideal.sup_isMaximal_height_eq_ringKrullDim {R : Type u_1} [CommRing R] [Nontrivial R] : ↑(⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) = ringKrullDim R

In a nontrivial commutative ring R, the supremum of heights of all maximal ideals is equal to the Krull dimension of R.

theorem Ring.krullDimLE_of_isLocalization_maximal {R : Type u_1} [CommRing R] (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2) [(P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] {n : ℕ} (h : ∀ (P : Ideal R) [inst : P.IsMaximal], KrullDimLE n (Rₚ P)) : KrullDimLE n R

theorem Ideal.eq_span_singleton_of_height_eq_one {R : Type u_1} [CommRing R] [IsDomain R] {p : Ideal R} [p.IsPrime] (h1 : p.height = 1) {x : R} (hx : x ∈ p) (hxp : Prime x) : p = span {x}