Krull dimension of finitely generated algebras over a field

Let A be a nontrivial finitely generated algebra over a field k. Noether normalization gives an injective finite map k[X₁, …, Xₛ] → A, so A has Krull dimension s. Extending scalars along any Noetherian k-algebra K keeps the map K[X₁, …, Xₛ] → K ⊗[k] A injective (every k-module is flat) and finite, so K ⊗[k] A has the dimension of K[X₁, …, Xₛ], namely dim K + s. The tensor-product theorem handles the subsingleton case separately.

In particular the Krull dimension of a finitely generated algebra over a field does not change under extension of the base field. This is the affine form of the invariance of the dimension of a scheme locally of finite type over a field under field extension, which is what makes fibrewise dimension bounds on morphisms stable under base change.

For a domain A, the same Noether normalization identifies s with the transcendence degree of A over k: the variables form a transcendence basis because A is integral over them. The transcendence degree only sees the fraction field, so an algebraic extension of finitely generated domains, such as a localization A[1/f] with f ≠ 0, does not change the Krull dimension.

Every maximal ideal of a finitely generated algebra A with irreducible spectrum over k has height dim A. For the polynomial ring k[X₁, …, Xₛ] this follows by induction on s: a maximal ideal of R[X], for R a Jacobson ring, contracts to a maximal ideal of R, and its height is one more than the height of that contraction. For a domain A, Noether normalization makes A integral over the normal domain k[X₁, …, Xₛ], so going down gives the lower height bound. The general case follows by quotienting by the nilradical, which preserves dimension and prime heights. Geometrically, all closed points of an irreducible variety have local dimension the dimension of the variety.

Geometrically, a nonempty open part of an irreducible closed subset of Spec A has the dimension of the whole closed subset; this is what makes pure-dimensionality of schemes locally of finite type over a field a local property.

Main results

• TauCeti.ringKrullDim_eq_of_injective_of_isIntegral_mvPolynomial: an injective integral map k[X₁, …, Xₛ] → A forces dim A = s, the number of variables.
• TauCeti.finiteRingKrullDim_of_finiteType: a nontrivial finitely generated algebra over a field has finite Krull dimension.
• TauCeti.ringKrullDim_tensorProduct_of_isNoetherianRing_of_finiteType: dim (K ⊗[k] A) = dim K + dim A for a Noetherian k-algebra K.
• TauCeti.ringKrullDim_tensorProduct_field_of_finiteType: dim (K ⊗[k] A) = dim A for a field extension K / k.
• TauCeti.ringKrullDim_eq_toNat_trdeg: a finitely generated domain over k has Krull dimension its transcendence degree over k.
• TauCeti.ringKrullDim_eq_of_isAlgebraic: an algebraic extension of finitely generated domains over k preserves the Krull dimension; TauCeti.ringKrullDim_localization_away is the case of A[1/f] with f ≠ 0.
• MvPolynomial.height_eq_natCard_of_isMaximal: every maximal ideal of k[Xᵢ | i ∈ ι], for ι finite, has height the number of variables.
• TauCeti.height_eq_ringKrullDim_of_isMaximal: every maximal ideal of a finitely generated algebra A with irreducible spectrum over k has height dim A.
• Ideal.isMaximal_under_of_finiteType: along a homomorphism of k-algebras A → B with B finitely generated, maximal ideals of B contract to maximal ideals of A.
• TauCeti.topologicalKrullDim_inter_eq_of_finiteType: in Spec A, a nonempty open part of an irreducible closed subset has the dimension of that subset.

References

• Stacks Project, Tag 00OW (Noether normalization)
• Stacks Project, Tag 00P0 (dimension and transcendence degree)
• R. Hartshorne, Algebraic Geometry (1977), Chapter I, Theorem 1.8A (heights of primes in finitely generated domains over a field)

theorem TauCeti.ringKrullDim_eq_of_injective_of_isIntegral_mvPolynomial {k : Type u_1} [Field k] {ι : Type u_2} {A : Type u_3} [Finite ι] [CommRing A] [Algebra k A] (g : MvPolynomial ι k →ₐ[k] A) (hinj : Function.Injective ⇑g) (hint : g.IsIntegral) : ringKrullDim A = ↑(Nat.card ι)

If a k-algebra A is integral over a polynomial ring k[Xᵢ | i ∈ ι] in finitely many variables embedded in it, then A has Krull dimension the number of variables.

theorem TauCeti.finiteRingKrullDim_of_finiteType (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Nontrivial A] [Algebra k A] [Algebra.FiniteType k A] : FiniteRingKrullDim A

A nontrivial finitely generated algebra over a field has finite Krull dimension.

@[simp]

theorem TauCeti.ringKrullDim_tensorProduct_of_isNoetherianRing_of_finiteType {k : Type u_1} [Field k] (K : Type u_2) (A : Type u_3) [CommRing K] [IsNoetherianRing K] [Algebra k K] [CommRing A] [Algebra k A] [Algebra.FiniteType k A] : ringKrullDim (TensorProduct k K A) = ringKrullDim K + ringKrullDim A

The Krull dimension of K ⊗[k] A, for a Noetherian k-algebra K and a finitely generated k-algebra A, is the sum of the Krull dimensions of K and A.

theorem TauCeti.ringKrullDim_tensorProduct_field_of_finiteType {k : Type u_1} [Field k] (K : Type u_2) (A : Type u_3) [Field K] [Algebra k K] [CommRing A] [Algebra k A] [Algebra.FiniteType k A] : ringKrullDim (TensorProduct k K A) = ringKrullDim A

The Krull dimension of a finitely generated algebra over a field is unchanged by extending the base field.

theorem TauCeti.ringKrullDim_eq_toNat_trdeg (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [Algebra k A] [Algebra.FiniteType k A] : ringKrullDim A = ↑(Cardinal.toNat (Algebra.trdeg k A))

A finitely generated domain over a field k has Krull dimension its transcendence degree over k. The transcendence degree is finite by Algebra.trdeg_lt_aleph0_of_finiteType.

theorem TauCeti.ringKrullDim_eq_of_isAlgebraic (k : Type u_1) [Field k] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [IsDomain B] [Algebra k A] [Algebra k B] [Algebra A B] [IsScalarTower k A B] [FaithfulSMul A B] [Algebra.IsAlgebraic A B] [Algebra.FiniteType k A] [Algebra.FiniteType k B] : ringKrullDim A = ringKrullDim B

An algebraic extension B / A of finitely generated domains over a field k does not change the Krull dimension: both have the transcendence degree of B over k.

theorem TauCeti.ringKrullDim_localization_away (k : Type u_1) [Field k] {A : Type u_2} [CommRing A] [IsDomain A] [Algebra k A] [Algebra.FiniteType k A] {f : A} (hf : f ≠ 0) : ringKrullDim (Localization.Away f) = ringKrullDim A

Inverting a nonzero element of a finitely generated domain over a field does not change its Krull dimension.

@[simp]

theorem MvPolynomial.height_eq_natCard_of_isMaximal {k : Type u_1} [Field k] {ι : Type u_2} [Finite ι] (M : Ideal (MvPolynomial ι k)) [M.IsMaximal] : M.height = ↑(Nat.card ι)

Every maximal ideal of the polynomial ring k[Xᵢ | i ∈ ι] over a field k in finitely many variables has height the number of variables.

theorem TauCeti.height_eq_ringKrullDim_of_isMaximal (k : Type u_1) [Field k] {A : Type u_2} [CommRing A] [Algebra k A] [Algebra.FiniteType k A] [IrreducibleSpace (PrimeSpectrum A)] (m : Ideal A) [m.IsMaximal] : ↑m.height = ringKrullDim A

Every maximal ideal of a finitely generated algebra with irreducible spectrum over a field has height the Krull dimension of the algebra.

theorem Ideal.isMaximal_under_of_finiteType (k : Type u_1) [Field k] {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Algebra A B] [IsScalarTower k A B] [Algebra.FiniteType k B] (q : Ideal B) [q.IsMaximal] : (under A q).IsMaximal

Let A → B be a homomorphism of algebras over a field k, with B finitely generated over k. Then every maximal ideal of B contracts to a maximal ideal of A.

theorem TauCeti.topologicalKrullDim_inter_eq_of_finiteType (k : Type u_1) [Field k] {A : Type u_2} [CommRing A] [Algebra k A] [Algebra.FiniteType k A] {Z U : Set (PrimeSpectrum A)} (hZ : IsIrreducible Z) (hZc : IsClosed Z) (hU : IsOpen U) (hZU : (Z ∩ U).Nonempty) : topologicalKrullDim ↑(Z ∩ U) = topologicalKrullDim ↑Z

In the spectrum of a finitely generated algebra over a field, a nonempty open part Z ∩ U of an irreducible closed subset Z has the Krull dimension of Z.