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_spanFinrank_of_le {R : Type u_1} [CommRing R] [IsNoetherianRing R] {I p : Ideal R} [p.IsPrime] (hrp : I ≤ p) : p.height ≤ (map (Quotient.mk I) p).height + ↑(Submodule.spanFinrank I)

If I ≤ p and p is prime, the height of p is bounded by the height of p ⧸ I R plus the span rank of I.

theorem height_le_ringKrullDim_quotient_add_spanFinrank {R : Type u_1} [CommRing R] [IsNoetherianRing R] {p I : Ideal R} [p.IsPrime] (h : I ≤ p) : ↑p.height ≤ ringKrullDim (R ⧸ I) + ↑(Submodule.spanFinrank I)

theorem ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank {R : Type u_1} [CommRing R] [IsNoetherianRing R] (I : Ideal R) (h : I ≤ Ring.jacobson R) : ringKrullDim R ≤ ringKrullDim (R ⧸ I) + ↑(Submodule.spanFinrank I)

theorem Ideal.height_le_height_add_encard_of_subset {R : Type u_1} [CommRing R] [IsNoetherianRing R] (s : Set R) {p : Ideal R} [p.IsPrime] (hrm : s ⊆ ↑p) : p.height ≤ (map (Quotient.mk (span s)) p).height + s.encard

If p is a prime ideal containing s, the height of p is bounded by the sum of the height of the image of p in R ⧸ (s) and the cardinality of s.

theorem Ideal.height_le_ringKrullDim_quotient_add_encard {R : Type u_1} [CommRing R] [IsNoetherianRing R] {p : Ideal R} [p.IsPrime] (s : Set R) (hs : s ⊆ ↑p) : ↑p.height ≤ ringKrullDim (R ⧸ span s) + ↑s.encard

theorem Ideal.height_le_height_add_one_of_mem {R : Type u_1} [CommRing R] [IsNoetherianRing R] {r : R} {p : Ideal R} [p.IsPrime] (hrm : r ∈ p) : p.height ≤ (map (Quotient.mk (span {r})) p).height + 1

theorem Ideal.height_le_ringKrullDim_quotient_add_one {R : Type u_1} [CommRing R] [IsNoetherianRing R] {r : R} {p : Ideal R} [p.IsPrime] (hrp : r ∈ p) : ↑p.height ≤ ringKrullDim (R ⧸ span {r}) + 1

theorem ringKrullDim_le_ringKrullDim_quotient_add_encard {R : Type u_1} [CommRing R] [IsNoetherianRing R] (s : Set R) (hs : s ⊆ ↑(Ring.jacobson R)) : ringKrullDim R ≤ ringKrullDim (R ⧸ Ideal.span s) + ↑s.encard

theorem ringKrullDim_le_ringKrullDim_quotient_add_card {R : Type u_1} [CommRing R] [IsNoetherianRing R] (s : Finset R) (hs : ↑s ⊆ ↑(Ring.jacobson R)) : ringKrullDim R ≤ ringKrullDim (R ⧸ Ideal.span ↑s) + ↑s.card

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

theorem ringKrullDim_le_spanFinrank_maximalIdeal (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] : ringKrullDim R ≤ ↑(Submodule.spanFinrank (IsLocalRing.maximalIdeal R))