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.

Equations

• I.primeHeight = Order.height { asIdeal := I, isPrime := hI }

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

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_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 ≠ ⊤) [h : I.FiniteHeight] : I.height ≠ ⊤

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

theorem Ideal.primeHeight_ne_top {R : Type u_1} [CommRing R] (I : Ideal R) [I.FiniteHeight] [h : I.IsPrime] : I.primeHeight ≠ ⊤

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

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

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