Krull dimension under integral extensions

The theorem of Cohen–Seidenberg [Fre17, VII 5.7]: "if A ⊂ B is an integral ring extension of noetherian rings then dim A = dim B" — the fact behind the uniqueness of the d of Noether normalization [Fre17, I 7.2] ("the number d is unique (it is the Krull dimension)"). Mathlib has lying over and going up (Ideal.exists_ideal_over_prime_of_isIntegral) and incomparability (Ideal.IsIntegral.comap_lt_comap) but no statement about ringKrullDim; this module assembles the two inequalities on PrimeSpectrum:

• ringKrullDim_le_of_isIntegral: an integral ring homomorphism f : A →+* B (no injectivity) gives dim B ≤ dim A — comap f is strictly monotone on primes by incomparability.
• exists_ltSeries_comap_eq: along an injective integral f, every chain of primes of A lifts to a chain of primes of B with the same preimages (lying over for the first prime, going up for each step; induction on the length with RelSeries.snoc).
• ringKrullDim_eq_of_isIntegral_of_injective, ringKrullDim_eq_of_finite_of_injective: the equality; the finite case through RingHom.Finite.to_isIntegral.

No Noetherian hypothesis is needed for either inequality. The second section reads the Krull dimension of a quotient R ⧸ I on the zero locus of I in Spec R (Ideal.primeSpectrumQuotientOrderIsoZeroLocus): dim R ⧸ √I = dim R ⧸ I (ringKrullDim_quotient_radical) and dim R ⧸ I = max over the minimal primes P of I of dim R ⧸ P (ringKrullDim_quotient_eq_iSup_minimalPrimes; this is the argument of [Fre17, II 5.12]: chains of prime ideals in 𝒪_{X,a} correspond to chains a ⊂ p₀ ⊂ … ⊂ p_m of primes of 𝒪_n, and p₀ contains one of the minimal primes over a).

The third section is Krull's height theorem in the form of a system of parameters (Fre17, VII 5.6: a local noetherian ring whose maximal ideal can be generated by n elements has dimension at most n, applied to R ⧸ I): d elements s of the maximal ideal with 𝔪 ≤ √(I ⊔ (s)) give dim R ⧸ I ≤ d (ringKrullDim_quotient_le_of_maximalIdeal_le_radical_sup, from Mathlib's ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank) — the tool for the upper semicontinuity of the dimension of an analytic germ at the points near a Noether normalization.

Standard commutative algebra, assembled from Mathlib's Cohen–Seidenberg lemmas, prime-spectrum order isomorphisms and Krull's height theorem; used in the dimension theory of analytic germs (Rückert's Noether normalization, the dimension of a germ through its minimal primes).

theorem IsLocalRing.ringKrullDim_le_of_isIntegral {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) (hf : f.IsIntegral) : ringKrullDim B ≤ ringKrullDim A

Incomparability: an integral ring homomorphism does not raise the Krull dimension.

theorem IsLocalRing.exists_comap_eq_of_le {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) (hf : f.IsIntegral) (P : PrimeSpectrum A) (Q₀ : Ideal B) (hle : Ideal.comap f Q₀ ≤ P.asIdeal) : ∃ (Q : PrimeSpectrum B), Q₀ ≤ Q.asIdeal ∧ PrimeSpectrum.comap f Q = P

Lying over: for an injective integral homomorphism every prime of A is the preimage of a prime of B containing a given prime Q₀ whose preimage lies below it (going up; Q₀ = ⊥ gives lying over).

theorem IsLocalRing.exists_ltSeries_comap_eq {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) (hf : f.IsIntegral) (hinj : Function.Injective ⇑f) (n : ℕ) (l : LTSeries (PrimeSpectrum A)) (hl : l.length = n) : ∃ (m : LTSeries (PrimeSpectrum B)) (hm : m.length = n), ∀ (i : Fin (n + 1)), PrimeSpectrum.comap f (m.toFun (Fin.cast ⋯ i)) = l.toFun (Fin.cast ⋯ i)

Lying over and going up: a chain of primes of A lifts along an injective integral f to a chain of primes of B of the same length with the given preimages (the proof of [Fre17, VII 5.7]).

theorem IsLocalRing.ringKrullDim_eq_of_isIntegral_of_injective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) (hf : f.IsIntegral) (hinj : Function.Injective ⇑f) : ringKrullDim B = ringKrullDim A

The theorem of Cohen–Seidenberg [Fre17, VII 5.7]: an injective integral ring homomorphism preserves the Krull dimension.

theorem IsLocalRing.ringKrullDim_eq_of_finite_of_injective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) (hf : f.Finite) (hinj : Function.Injective ⇑f) : ringKrullDim B = ringKrullDim A

Cohen–Seidenberg for a finite injective ring homomorphism (f.Finite gives f.IsIntegral).

theorem IsLocalRing.ringKrullDim_le_of_finite {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) (hf : f.Finite) : ringKrullDim B ≤ ringKrullDim A

A finite ring homomorphism does not raise the Krull dimension.

Krull dimension of quotients: the radical, the minimal primes

theorem IsLocalRing.ringKrullDim_quotient_eq_krullDim_zeroLocus {R : Type u_3} [CommRing R] (I : Ideal R) : ringKrullDim (R ⧸ I) = Order.krullDim ↑(PrimeSpectrum.zeroLocus ↑I)

The Krull dimension of R ⧸ I is that of the zero locus of I in Spec R.

theorem IsLocalRing.ringKrullDim_quotient_radical {R : Type u_3} [CommRing R] (I : Ideal R) : ringKrullDim (R ⧸ I.radical) = ringKrullDim (R ⧸ I)

R ⧸ I and R ⧸ √I have the same Krull dimension (same zero locus).

theorem IsLocalRing.ringKrullDim_quotient_le_quotient_of_le {R : Type u_3} [CommRing R] {I J : Ideal R} (h : I ≤ J) : ringKrullDim (R ⧸ J) ≤ ringKrullDim (R ⧸ I)

A quotient by a larger ideal has smaller dimension.

theorem IsLocalRing.ringKrullDim_quotient_eq_iSup_minimalPrimes {R : Type u_3} [CommRing R] (I : Ideal R) : ringKrullDim (R ⧸ I) = ⨆ P ∈ I.minimalPrimes, ringKrullDim (R ⧸ P)

The dimension of R ⧸ I is the maximum of the dimensions of R ⧸ P over the minimal primes P of I [Fre17, II 5.12] — a chain of primes over I starts at a prime containing a minimal prime of I, hence lies over it.

Systems of parameters: Krull's height theorem in a local Noetherian ring

theorem IsLocalRing.ringKrullDim_quotient_le_zero_of_maximalIdeal_le_radical {R : Type u_4} [CommRing R] [IsLocalRing R] (J : Ideal R) (hm : maximalIdeal R ≤ J.radical) : ringKrullDim (R ⧸ J) ≤ 0

A quotient of a local ring by an ideal whose radical contains the maximal ideal has Krull dimension ≤ 0.

theorem IsLocalRing.map_quotientMk_le_jacobson_of_le_maximalIdeal {R : Type u_4} [CommRing R] [IsLocalRing R] (I B : Ideal R) (hBm : B ≤ maximalIdeal R) : Ideal.map (Ideal.Quotient.mk I) B ≤ Ring.jacobson (R ⧸ I)

An ideal inside the maximal ideal maps into the Jacobson radical of any quotient.

theorem IsLocalRing.spanFinrank_map_span_range_le {R : Type u_4} [CommRing R] {d : ℕ} (I : Ideal R) (g : Fin d → R) : Submodule.spanFinrank (Ideal.map (Ideal.Quotient.mk I) (Ideal.span (Set.range g))) ≤ d

The image of an ideal generated by d elements has span rank ≤ d.

theorem IsLocalRing.ringKrullDim_quotient_le_of_maximalIdeal_le_radical_sup {R : Type u_4} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {d : ℕ} (I : Ideal R) (s : Fin d → R) (hs : ∀ (j : Fin d), s j ∈ maximalIdeal R) (hm : maximalIdeal R ≤ (I ⊔ Ideal.span (Set.range s)).radical) : ringKrullDim (R ⧸ I) ≤ ↑d

Krull's height theorem, in the form of a system of parameters: if d elements s j of the maximal ideal of the local Noetherian ring R satisfy 𝔪 ≤ √(I ⊔ (s)), then dim R ⧸ I ≤ d ([Fre17, VII 5.6], a local noetherian ring whose maximal ideal can be generated by n elements has dimension at most n, applied to R ⧸ I, whose maximal ideal is the radical of (s)).