Documentation

TauCeti.RingTheory.KrullDimension.Quotient

Krull dimension and heights under quotients #

For an ideal I of a commutative ring R, the quotient map R → R ⧸ I identifies Spec (R ⧸ I) homeomorphically with the closed subset V(I) of Spec R. So the topological Krull dimension of V(I) is the Krull dimension of R ⧸ I. Quotienting by the nilradical preserves the entire prime spectrum, hence its Krull dimension and the height of each prime ideal.

The spectrum of a ring is pure-dimensional of dimension d exactly when every quotient by a minimal prime has Krull dimension d: the irreducible components are the closed subsets V(P) for minimal primes P. This gives a componentwise criterion using only quotient dimensions.

Main results #

source
@[simp]
theorem Ideal.topologicalKrullDim_zeroLocus {R : Type u_1} [CommRing R] (I : Ideal R) :
topologicalKrullDim ↑(PrimeSpectrum.zeroLocus ↑I) = ringKrullDim (R ⧸ I)

The closed subset V(I) of Spec R has the Krull dimension of R ⧸ I.

source
theorem TauCeti.isPureDimensional_primeSpectrum_iff {R : Type u_1} [CommRing R] {d : ℕ} :
IsPureDimensional d (PrimeSpectrum R) ↔ ∀ P ∈ minimalPrimes R, ringKrullDim (R ⧸ P) = ↑d

The spectrum of a ring R is pure-dimensional of dimension d if and only if R ⧸ P has Krull dimension d for every minimal prime P of R.

source
@[simp]
theorem TauCeti.ringKrullDim_quotient_nilradical (R : Type u_1) [CommRing R] :
ringKrullDim (R ⧸ nilradical R) = ringKrullDim R

Passing to the quotient by the nilradical preserves Krull dimension.

source
@[simp]
theorem Ideal.height_map_quotientMk_nilradical {R : Type u_1} [CommRing R] (p : Ideal R) [p.IsPrime] :
(map (Quotient.mk (nilradical R)) p).height = p.height

Passing to the quotient by the nilradical preserves the height of a prime ideal.