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 via Order.height.

• 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.primeHeight {R : Type u_1} [CommRing R] (I : Ideal R) [hI : I.IsPrime] : ℕ∞

The height of a prime ideal is defined as the supremum of the lengths of strictly decreasing chains of prime ideals below it.

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.

theorem Ideal.height_eq_primeHeight {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] : I.height = I.primeHeight

For a prime ideal, its height equals its prime height.

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.primeHeight_ne_top {R : Type u_1} [CommRing R] (I : Ideal R) [I.FiniteHeight] [I.IsPrime] : I.primeHeight ≠ ⊤

theorem Ideal.primeHeight_lt_top {R : Type u_1} [CommRing R] (I : Ideal R) [I.FiniteHeight] [I.IsPrime] : I.primeHeight < ⊤

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.primeHeight_mono {R : Type u_1} [CommRing R] {I J : Ideal R} [I.IsPrime] [J.IsPrime] (h : I ≤ J) : I.primeHeight ≤ J.primeHeight

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

@[simp]

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

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

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_is_prime {R : Type u_1} [CommRing R] {I J : Ideal R} [I.IsPrime] (h : I < J) [I.FiniteHeight] : I.height < J.height

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

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.primeHeight_eq_zero_iff {R : Type u_1} [CommRing R] {I : Ideal R} [I.IsPrime] : I.primeHeight = 0 ↔ I ∈ minimalPrimes R

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

@[simp]

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

@[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_primeHeight_eq_ringKrullDim {R : Type u_1} [CommRing R] {I : Ideal R} [I.IsPrime] [FiniteRingKrullDim R] (e : ↑I.primeHeight = ringKrullDim R) : I.IsMaximal

@[simp]

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

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

@[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.primeHeight_eq_ringKrullDim_iff {R : Type u_1} [CommRing R] [FiniteRingKrullDim R] [IsLocalRing R] {I : Ideal R} [I.IsPrime] : ↑I.primeHeight = 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.primeHeight_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) [J.IsPrime] : (Ideal.comap (algebraMap R A) J).primeHeight = J.primeHeight

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.comap (algebraMap R A) J).height = J.height

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 mem_minimalPrimes_of_primeHeight_eq_height {R : Type u_1} [CommRing R] {I J : Ideal R} [J.IsPrime] (e : I ≤ J) (e' : J.primeHeight = I.height) [J.FiniteHeight] : J ∈ I.minimalPrimes

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_primeHeight_eq_ringKrullDim {R : Type u_1} [CommRing R] [Nontrivial R] : ↑(⨆ (I : Ideal R), ⨆ (x : I.IsPrime), I.primeHeight) = ringKrullDim R

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

theorem Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim {R : Type u_1} [CommRing R] [Nontrivial R] : ↑(⨆ (I : Ideal R), ⨆ (x : I.IsMaximal), I.primeHeight) = ringKrullDim R

In a nontrivial commutative ring R, the supremum of prime 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