Dimension of finitely presented algebras over a field

Let A = k[x₁, …, x_m] ⧸ (f₁, …, f_c) be a finitely presented algebra over a field k. Every maximal ideal of k[x₁, …, x_m] has height m, and by Krull's height theorem cutting by the c relations lowers the height by at most c. So every maximal ideal of A has height at least m - c: each closed point of Spec A has local dimension at least the number of generators minus the number of relations.

If moreover dim A ≤ m - c, so that A is a global complete intersection over k, then every nonzero localization A[1/g] still has dimension m - c. Indeed A is Jacobson, so some maximal ideal avoids g, and its height is preserved by the localization. This is the algebraic input for the stability of relative global complete intersections, and hence of standard syntomic algebras, under localization on the source.

Such an A is moreover equidimensional: for every minimal prime Q, the quotient A ⧸ Q has dimension m - c. Choose g ∉ Q lying in every other minimal prime. Then every prime of A[1/g] contains Q, so dim A[1/g] ≤ dim (A ⧸ Q), while A[1/g] is nonzero and so has dimension m - c.

Main results

• Algebra.Presentation.dimension_le_height_of_isMaximal: every maximal ideal of a finitely presented algebra over a field has height at least the dimension m - c of the presentation.
• Algebra.Presentation.ringKrullDim_eq_of_isLocalization_away: if dim A ≤ m - c, every nonzero localization A[1/g] has Krull dimension m - c.
• Algebra.Presentation.ringKrullDim_quotient_of_mem_minimalPrimes and Algebra.Presentation.isPureDimensional_primeSpectrum: if dim A ≤ m - c, every irreducible component of Spec A has dimension m - c.

References

• The Stacks Project, Commutative Algebra, Section Syntomic morphisms: global complete intersections over a field, and the stability of relative global complete intersections under localization S → S_g.

theorem Algebra.Presentation.dimension_le_height_of_isMaximal {k : Type u_1} {A : Type u_2} [Field k] [CommRing A] [Algebra k A] {ι : Type u_3} {σ : Type u_4} [Finite ι] [Finite σ] (P : Presentation k A ι σ) (m : Ideal A) [m.IsMaximal] : ↑P.dimension ≤ m.height

Every maximal ideal of an algebra over a field with a finite presentation by m generators and c relations has height at least m - c, the dimension of the presentation.

theorem Algebra.Presentation.ringKrullDim_eq_of_isLocalization_away {k : Type u_1} {A : Type u_2} [Field k] [CommRing A] [Algebra k A] {ι : Type u_3} {σ : Type u_4} [Finite ι] [Finite σ] (P : Presentation k A ι σ) (hA : ringKrullDim A ≤ ↑P.dimension) (g : A) (B : Type u_5) [CommRing B] [Algebra A B] [IsLocalization.Away g B] [Nontrivial B] : ringKrullDim B = ↑P.dimension

Let A be an algebra over a field with a finite presentation by m generators and c relations, such that dim A ≤ m - c. Then every nonzero localization A[1/g] has Krull dimension exactly m - c.

theorem Algebra.Presentation.ringKrullDim_quotient_of_mem_minimalPrimes {k : Type u_1} {A : Type u_2} [Field k] [CommRing A] [Algebra k A] {ι : Type u_3} {σ : Type u_4} [Finite ι] [Finite σ] (P : Presentation k A ι σ) (hA : ringKrullDim A ≤ ↑P.dimension) {Q : Ideal A} (hQ : Q ∈ minimalPrimes A) : ringKrullDim (A ⧸ Q) = ↑P.dimension

Let A be an algebra over a field with a finite presentation by m generators and c relations, such that dim A ≤ m - c. Then for every minimal prime Q of A, the quotient A ⧸ Q has Krull dimension exactly m - c.

theorem Algebra.Presentation.isPureDimensional_primeSpectrum {k : Type u_1} {A : Type u_2} [Field k] [CommRing A] [Algebra k A] {ι : Type u_3} {σ : Type u_4} [Finite ι] [Finite σ] (P : Presentation k A ι σ) (hA : ringKrullDim A ≤ ↑P.dimension) : TauCeti.IsPureDimensional P.dimension (PrimeSpectrum A)

Let A be an algebra over a field with a finite presentation by m generators and c relations, such that dim A ≤ m - c. Then Spec A is pure-dimensional of dimension m - c.