Krull dimension along integral extensions

For an integral extension R → S the Krull dimensions of R and S are compared by the two Cohen–Seidenberg theorems.

• Incomparability: a strict inclusion of primes of S contracts to a strict inclusion of primes of R, so contraction is strictly monotone on prime spectra and dim S ≤ dim R.
• Lying over and going up: when every prime of R is a contraction and chains of primes of R lift along R → S, every chain of primes of R is the contraction of a chain in S of the same length, so dim R ≤ dim S.

For an injective integral extension both hold, and the two dimensions agree. This is the step that reduces the dimension of a finitely generated algebra over a field to that of a polynomial ring through Noether normalization.

Main results

• TauCeti.ringKrullDim_le_of_isIntegral: dim S ≤ dim R for an integral R-algebra S.
• TauCeti.ringKrullDim_le_of_hasGoingUp_of_surjective: dim R ≤ dim S when R → S has going up and Spec S → Spec R is surjective.
• TauCeti.ringKrullDim_eq_of_isIntegral_of_faithfulSMul: dim S = dim R for an injective integral extension.

References

• Stacks Project, Tag 00GU (going up)
• M. F. Atiyah, I. G. Macdonald, Introduction to Commutative Algebra, Corollary 5.9 and Theorem 5.11.

theorem TauCeti.primeSpectrumComap_strictMono_of_isIntegral {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] : StrictMono (PrimeSpectrum.comap (algebraMap R S))

Contraction of primes along an integral extension is strictly monotone (incomparability).

theorem TauCeti.ringKrullDim_le_of_isIntegral {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] : ringKrullDim S ≤ ringKrullDim R

The Krull dimension of an integral R-algebra is at most that of R.

theorem TauCeti.ringKrullDim_le_of_hasGoingUp_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.HasGoingUp R S] (hsurj : Function.Surjective (PrimeSpectrum.comap (algebraMap R S))) : ringKrullDim R ≤ ringKrullDim S

If R → S has going up and every prime of R is contracted from a prime of S, the Krull dimension of R is at most that of S.

theorem TauCeti.ringKrullDim_eq_of_isIntegral_of_faithfulSMul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [FaithfulSMul R S] : ringKrullDim S = ringKrullDim R

An injective integral extension preserves Krull dimension.