Krull dimension of schemes and extension of the base field

The Krull dimension of a scheme is the topological Krull dimension of its underlying space. This file computes it from an open cover and shows that it is unchanged by extending the base field: if X is locally of finite type over a field K and L / K is a field extension, then X ×_{Spec K} Spec L has the same Krull dimension as X.

The affine case is the commutative-algebra statement dim (A ⊗[K] L) = dim A for a finitely generated K-algebra A (TauCeti.ringKrullDim_tensorProduct_field_of_finiteType); the general case follows by covering X with affine opens, whose base changes cover the fibre product.

This is the input for the stability of fibrewise dimension bounds of morphisms under base change: the fibre of a base change is the base change of a fibre along an extension of residue fields. Likewise X is pure-dimensional of dimension d exactly when X ×_{Spec K} Spec L is: on affine charts, the irreducible components of Spec (L ⊗[K] A) lie over those of Spec A and have the same dimension (TauCeti.isPureDimensional_primeSpectrum_tensorProduct_iff).

On a scheme locally of finite type over a field, a nonempty open part Z ∩ U of an irreducible closed subset Z has the Krull dimension of Z. On an affine chart this is the corresponding statement for spectra of finitely generated algebras (TauCeti.topologicalKrullDim_inter_eq_of_finiteType), and Z is covered by the charts it meets. This is the input for the locality of pure-dimensionality on such schemes.

On an irreducible scheme locally of finite type over a field, the local ring at every closed point has the dimension of the scheme. On an affine chart Spec A this is the statement that every maximal ideal of the finitely generated irreducible algebra A has height dim A (TauCeti.height_eq_ringKrullDim_of_isMaximal), and the chart has the dimension of the scheme.

Main declarations

• TauCeti.AlgebraicGeometry.topologicalKrullDim_eq_iSup_openCover: the Krull dimension of a scheme is the supremum of the Krull dimensions of the members of an open cover.
• TauCeti.AlgebraicGeometry.topologicalKrullDim_pullback_Spec_map_of_field: the Krull dimension of a scheme locally of finite type over a field is invariant under extension of the base field.
• TauCeti.AlgebraicGeometry.topologicalKrullDim_inter_eq_of_locallyOfFiniteType: on a scheme locally of finite type over a field, a nonempty open part of an irreducible closed subset has the dimension of that subset.
• TauCeti.AlgebraicGeometry.topologicalKrullDim_eq_of_isOpenEmbedding_of_locallyOfFiniteType: a nonempty open subspace of an irreducible scheme locally of finite type over a field has the dimension of the scheme.
• TauCeti.AlgebraicGeometry.isPureDimensional_pullback_Spec_map_iff_of_field: pure-dimensionality of a scheme locally of finite type over a field is invariant under extension of the base field.
• TauCeti.AlgebraicGeometry.ringKrullDim_stalk_eq_topologicalKrullDim_of_isClosed: on an irreducible scheme locally of finite type over a field, the local ring at a closed point has the dimension of the scheme.

References

• Stacks Project, Tag 00P4, the pointwise form of the invariance of dimension under extension of the base field

theorem TauCeti.AlgebraicGeometry.topologicalKrullDim_eq_iSup_openCover {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) : topologicalKrullDim ↥X = ⨆ (i : 𝒰.I₀), topologicalKrullDim ↥(𝒰.X i)

The Krull dimension of a scheme is the supremum of the Krull dimensions of the members of an open cover.

theorem TauCeti.AlgebraicGeometry.topologicalKrullDim_pullback_Spec_algebraMap (K L A : Type u) [Field K] [Field L] [CommRing A] [Algebra K L] [Algebra K A] [Algebra.FiniteType K A] : topologicalKrullDim ↥(CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K A))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L)))) = ringKrullDim A

For a finitely generated algebra A over a field K and a field extension L / K, the fibre product Spec A ×_{Spec K} Spec L has the Krull dimension of A.

theorem TauCeti.AlgebraicGeometry.topologicalKrullDim_pullback_Spec_map_of_field {K L : Type u} [Field K] [Field L] [Algebra K L] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧K) [AlgebraicGeometry.LocallyOfFiniteType f] : topologicalKrullDim ↥(CategoryTheory.Limits.pullback f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L)))) = topologicalKrullDim ↥X

The Krull dimension of a scheme locally of finite type over a field K is invariant under extension of the base field.

theorem TauCeti.AlgebraicGeometry.topologicalKrullDim_inter_eq_of_locallyOfFiniteType {K : Type u} [Field K] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧K) [AlgebraicGeometry.LocallyOfFiniteType f] {Z U : Set ↥X} (hZ : IsIrreducible Z) (hZc : IsClosed Z) (hU : IsOpen U) (hZU : (Z ∩ U).Nonempty) : topologicalKrullDim ↑(Z ∩ U) = topologicalKrullDim ↑Z

On a scheme locally of finite type over a field, a nonempty open part Z ∩ U of an irreducible closed subset Z has the Krull dimension of Z.

theorem TauCeti.AlgebraicGeometry.topologicalKrullDim_eq_of_isOpenEmbedding_of_locallyOfFiniteType {K : Type u} [Field K] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧K) [AlgebraicGeometry.LocallyOfFiniteType f] [IrreducibleSpace ↥X] {Y : Type u_1} [TopologicalSpace Y] [Nonempty Y] {g : Y → ↥X} (hg : Topology.IsOpenEmbedding g) : topologicalKrullDim Y = topologicalKrullDim ↥X

A nonempty open subspace of an irreducible scheme locally of finite type over a field has the Krull dimension of the scheme.

theorem TauCeti.AlgebraicGeometry.isPureDimensional_pullback_Spec_map_iff_of_field {K L : Type u} [Field K] [Field L] [Algebra K L] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧K) [AlgebraicGeometry.LocallyOfFiniteType f] {d : ℕ} : IsPureDimensional d ↥(CategoryTheory.Limits.pullback f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L)))) ↔ IsPureDimensional d ↥X

A scheme locally of finite type over a field K is pure-dimensional of dimension d exactly when its base change to a field extension L / K is.

theorem TauCeti.AlgebraicGeometry.ringKrullDim_stalk_eq_topologicalKrullDim_of_isClosed {K : Type u} [Field K] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧K) [AlgebraicGeometry.LocallyOfFiniteType f] [IrreducibleSpace ↥X] {x : ↥X} (hx : IsClosed {x}) : ringKrullDim ↑(X.presheaf.stalk x) = topologicalKrullDim ↥X

On an irreducible scheme X locally of finite type over a field, the local ring at a closed point has the Krull dimension of X.