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.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

@[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_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

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 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