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_card_of_mem_minimalPrimes_span_finset {R : Type u_1} [CommRing R] [IsNoetherianRing R] {p : Ideal R} {s : Finset R} (hI : p ∈ (span ↑s).minimalPrimes) : p.height ≤ ↑s.card

theorem Ideal.height_le_card_of_mem_minimalPrimes_span {R : Type u_1} [CommRing R] [IsNoetherianRing R] {p : Ideal R} {s : Set R} (hs : s.Finite) (hI : p ∈ (span s).minimalPrimes) : p.height ≤ ↑s.ncard

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.

theorem Ideal.height_le_height_add_of_liesOver {R : Type u_1} [CommRing R] [IsNoetherianRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsNoetherianRing S] (p : Ideal R) [p.IsPrime] (P : Ideal S) [P.IsPrime] [P.LiesOver p] : P.height ≤ p.height + (map (Quotient.mk (map (algebraMap R S) p)) P).height

If P lies over p, the height of P is bounded by the height of p plus the height of the image of P in S ⧸ p S. Equality holds if S satisfies going-down as an R-algebra (see Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown).

theorem Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown {R : Type u_1} [CommRing R] [IsNoetherianRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsNoetherianRing S] [Algebra.HasGoingDown R S] (p : Ideal R) [p.IsPrime] (P : Ideal S) [P.IsPrime] [P.LiesOver p] : P.height = p.height + (map (Quotient.mk (map (algebraMap R S) p)) P).height

If S satisfies going-down as an R-algebra and P lies over p, the height of P is equal to the height of p plus the height of the image of P in S ⧸ p S (Matsumura 13.B Th. 19 (2)).