Krull dimension of standard smooth algebras over a field

Let S be a standard smooth algebra of relative dimension n over a field k. Then every maximal ideal of S has height n, and so S has Krull dimension n when it is nonzero. This is the dimension count behind the relative dimension of a smooth scheme over a field: the local ring at a closed point has dimension equal to the relative dimension.

By Mathlib's Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, S is étale over the polynomial ring P = k[X₁, …, Xₙ]. Étale algebras are flat and quasi-finite, so heights of primes are preserved along P → S (Ideal.height_eq_height_under_of_quasiFinite). A maximal ideal q of S contracts to a maximal ideal of P (Ideal.isMaximal_under_of_finiteType), and every maximal ideal of P has height n (MvPolynomial.height_eq_natCard_of_isMaximal).

Moreover Spec S is pure-dimensional of dimension n: for every minimal prime P of S, the quotient S ⧸ P has dimension n. Choose a maximal ideal m ⊇ P. The local ring S_m is regular, hence a domain, so every prime contained in m contains P; thus a chain of primes below m realizing its height n is a chain in V(P).

Main declarations

• TauCeti.height_eq_of_isStandardSmoothOfRelativeDimension: every maximal ideal of a standard smooth algebra of relative dimension n over a field has height n;
• TauCeti.ringKrullDim_eq_of_isStandardSmoothOfRelativeDimension: a nonzero standard smooth algebra of relative dimension n over a field has Krull dimension n;
• TauCeti.ringKrullDim_quotient_of_isStandardSmoothOfRelativeDimension and TauCeti.isPureDimensional_primeSpectrum_of_isStandardSmoothOfRelativeDimension: every irreducible component of its spectrum has dimension n.

References

• H. Matsumura, Commutative Ring Theory, Theorem 15.1, for the dimension formula along flat local homomorphisms that underlies the preservation of heights.

theorem TauCeti.height_eq_of_isStandardSmoothOfRelativeDimension (k : Type u_1) {S : Type u_2} [Field k] [CommRing S] [Algebra k S] (n : ℕ) [Algebra.IsStandardSmoothOfRelativeDimension n k S] (q : Ideal S) [q.IsMaximal] : q.height = ↑n

Every maximal ideal of a standard smooth algebra of relative dimension n over a field has height n.

theorem TauCeti.ringKrullDim_eq_of_isStandardSmoothOfRelativeDimension (k : Type u_1) {S : Type u_2} [Field k] [CommRing S] [Algebra k S] (n : ℕ) [Algebra.IsStandardSmoothOfRelativeDimension n k S] [Nontrivial S] : ringKrullDim S = ↑n

A nonzero standard smooth algebra of relative dimension n over a field has Krull dimension n.

theorem TauCeti.ringKrullDim_quotient_of_isStandardSmoothOfRelativeDimension (k : Type u_1) {S : Type u_2} [Field k] [CommRing S] [Algebra k S] (n : ℕ) [Algebra.IsStandardSmoothOfRelativeDimension n k S] {P : Ideal S} (hP : P ∈ minimalPrimes S) : ringKrullDim (S ⧸ P) = ↑n

For every minimal prime P of a standard smooth algebra S of relative dimension n over a field, the quotient S ⧸ P has Krull dimension n.

theorem TauCeti.isPureDimensional_primeSpectrum_of_isStandardSmoothOfRelativeDimension (k : Type u_1) {S : Type u_2} [Field k] [CommRing S] [Algebra k S] (n : ℕ) [Algebra.IsStandardSmoothOfRelativeDimension n k S] : IsPureDimensional n (PrimeSpectrum S)

The spectrum of a standard smooth algebra of relative dimension n over a field is pure-dimensional of dimension n: each of its irreducible components has dimension n.