Krull's Height Theorem

In this file, we prove Krull's principal ideal theorem (also known as Krullscher Hauptidealsatz), and Krull's height theorem (also known as Krullscher Höhensatz).

Main Results

• Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes : This theorem is the Krull's principal ideal theorem (also known as Krullscher Hauptidealsatz), which states that: In a commutative Noetherian ring R, any prime ideal that is minimal over a principal ideal has height at most 1.

• Ideal.height_le_spanRank_toENat_of_mem_minimal_primes : This theorem is the Krull's height theorem (also known as Krullscher Höhensatz), which states that: In a commutative Noetherian ring R, any prime ideal that is minimal over an ideal generated by n elements has height at most n.

• Ideal.height_le_spanRank_toENat : This theorem is a corollary of the Krull's height theorem (also known as Krullscher Höhensatz). In a commutative Noetherian ring R, the height of a (finitely-generated) ideal is smaller than or equal to the minimum number of generators for this ideal.

• Ideal.height_le_iff_exists_minimal_primes : In a commutative Noetherian ring R, a prime ideal p has height no greater than n if and only if it is a minimal ideal over some ideal generated by no more than n elements.

theorem IsLocalRing.quotient_artinian_of_mem_minimalPrimes_of_isLocalRing {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] (I : Ideal R) (hp : maximalIdeal R ∈ I.minimalPrimes) : IsArtinianRing (R ⧸ I)

theorem Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] (I : Ideal R) [Submodule.IsPrincipal I] (hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes) : (IsLocalRing.maximalIdeal R).height ≤ 1

theorem Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes {R : Type u_1} [CommRing R] [IsNoetherianRing R] (I : Ideal R) [Submodule.IsPrincipal I] (p : Ideal R) (hp : p ∈ I.minimalPrimes) : p.height ≤ 1

Krull's principal ideal theorem (also known as Krullscher Hauptidealsatz) : In a commutative Noetherian ring R, any prime ideal that is minimal over a principal ideal has height at most 1.

theorem Ideal.map_height_le_one_of_mem_minimalPrimes {R : Type u_1} [CommRing R] [IsNoetherianRing R] {I p : Ideal R} {x : R} (hp : p ∈ (I ⊔ span {x}).minimalPrimes) : (map (Quotient.mk I) p).height ≤ 1

theorem Ideal.mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert {R : Type u_1} [CommRing R] [IsNoetherianRing R] {q p : Ideal R} [q.IsPrime] (hqp : q < p) (x : R) (s : Set R) (hp : p ∈ (span (insert x s)).minimalPrimes) (t : Set R) (htq : t ⊆ ↑q) (hsp : s ⊆ ↑(span (insert x t)).radical) : q ∈ (span t).minimalPrimes

If q < p are prime ideals such that p is minimal over span (s ∪ {x}) and t is a set contained in q such that s ⊆ √span (t ∪ {x}), then q is minimal over span t. This is used in the induction step for the proof of Krull's height theorem.

theorem Ideal.height_le_spanRank_toENat_of_mem_minimal_primes {R : Type u_1} [CommRing R] [IsNoetherianRing R] (I p : Ideal R) (hp : p ∈ I.minimalPrimes) : p.height ≤ Cardinal.toENat (Submodule.spanRank I)

Krull's height theorem (also known as Krullscher Höhensatz) : In a commutative Noetherian ring R, any prime ideal that is minimal over an ideal generated by n elements has height at most n.

theorem Ideal.height_le_spanRank_toENat {R : Type u_1} [CommRing R] [IsNoetherianRing R] (I : Ideal R) (hI : I ≠ ⊤) : I.height ≤ Cardinal.toENat (Submodule.spanRank I)

In a commutative Noetherian ring R, the height of a (finitely-generated) ideal is smaller than or equal to the minimum number of generators for this ideal.

theorem Ideal.height_le_spanFinrank {R : Type u_1} [CommRing R] [IsNoetherianRing R] (I : Ideal R) (hI : I ≠ ⊤) : I.height ≤ ↑(Submodule.spanFinrank I)

theorem Ideal.height_le_spanRank {R : Type u_1} [CommRing R] [IsNoetherianRing R] (I : Ideal R) (hI : I ≠ ⊤) : ↑I.height ≤ Submodule.spanRank I

instance Ideal.finiteHeight_of_isNoetherianRing {R : Type u_1} [CommRing R] [IsNoetherianRing R] (I : Ideal R) : I.FiniteHeight

instance instFiniteRingKrullDimOfIsNoetherianRingOfIsLocalRing {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] : FiniteRingKrullDim R

theorem Ideal.exists_spanRank_eq_and_height_eq {R : Type u_1} [CommRing R] [IsNoetherianRing R] (I : Ideal R) (hI : I ≠ ⊤) : ∃ J ≤ I, Submodule.spanRank J = ↑I.height ∧ J.height = I.height

theorem Ideal.height_le_iff_exists_minimalPrimes {R : Type u_1} [CommRing R] [IsNoetherianRing R] (p : Ideal R) [p.IsPrime] (n : ℕ∞) : p.height ≤ n ↔ ∃ (I : Ideal R), p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ ↑n

In a commutative Noetherian ring R, a prime ideal p has height no greater than n if and only if it is a minimal ideal over some ideal generated by no more than n elements.

theorem Ideal.exists_finset_card_eq_height_of_isNoetherianRing {R : Type u_1} [CommRing R] [IsNoetherianRing R] (p : Ideal R) [p.IsPrime] : ∃ (s : Finset R), p ∈ (span ↑s).minimalPrimes ∧ ↑s.card = p.height

If p is a prime in a Noetherian ring R, there exists a p-primary ideal I spanned by p.height elements.