A smooth scheme with preconnected underlying space has one relative dimension

[Kol07, Notation 64 (1)] asks the ambient scheme to be smooth of one relative dimension; the smooth locus X^{ns} of an integral scheme is irreducible, hence preconnected, and so is smooth of a single relative dimension d — the codimension n − d of X^{ns} in a smooth ambient of relative dimension n is then the same at every closed point, which is what the étale equivalence of two smooth points of X in the proof of [Kol07, Theorem 27] ("any two smooth points of X are étale equivalent", [Kol07, 4.2]) needs. Hironaka.Resolution.Algebraic.Kol07.Thm36.IsoOverSmoothLocus and Hironaka.Resolution.Algebraic.Hir64.SingleCenter use it to speak of the relative dimension of the smooth locus.

• ringKrullDim_stalk_add_trdeg_of_isStandardSmoothOfRelativeDimension: on an affine open V whose section ring is standard smooth of relative dimension m over k, every point x ∈ V has dim 𝒪_{X,x} + trdeg_k κ(x) = m (the body of Scheme.ringKrullDim_stalk_add_trdeg_residueField_of_smoothOfRelativeDimension, with the chart given instead of chosen).
• isLocallyConstant_dimCount: for f smooth, x ↦ dim 𝒪_{X,x} + trdeg_k κ(x) is locally constant — each point has a standard smooth affine chart, of some relative dimension (exists_affineOpen_isStandardSmoothOfRelativeDimension').
• exists_smoothOfRelativeDimension_of_preconnectedSpace: a smooth f : X ⟶ Spec k with X preconnected and nonempty is smooth of one relative dimension (a locally constant function on a preconnected space is constant; smoothOfRelativeDimension_of_forall_exists_affineOpen).

Sources: [Kol07, Notation 64; Theorem 27; 4.2]; [TSPA, Tag 0A21].

theorem AlgebraicGeometry.ringKrullDim_stalk_add_trdeg_of_isStandardSmoothOfRelativeDimension {k : Type u} [Field k] {X : Scheme} [PerfectField k] (f : X ⟶ Spec ↧k) (m : ℕ) {V : X.Opens} (hV : IsAffineOpen V) {x : ↥X} (hxV : x ∈ V) (hstd : Algebra.IsStandardSmoothOfRelativeDimension m k ↑(X.presheaf.obj (Opposite.op V))) : ringKrullDim ↑(X.presheaf.stalk x) + ↑(Cardinal.toENat (Algebra.trdeg k (IsLocalRing.ResidueField ↑(X.presheaf.stalk x)))) = ↑m

On an affine open V whose section ring is standard smooth of relative dimension m over k through f, every point x ∈ V satisfies dim 𝒪_{X,x} + trdeg_k κ(x) = m ([TSPA, Tag 0A21]; the body of Scheme.ringKrullDim_stalk_add_trdeg_residueField_of_smoothOfRelativeDimension with the chart given).

noncomputable def AlgebraicGeometry.dimCount {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (x : ↥X) : WithBot ℕ∞

The dimension count x ↦ dim 𝒪_{X,x} + trdeg_k κ(x) of a scheme over k, as a function to WithBot ℕ∞.

Equations

• AlgebraicGeometry.dimCount f x = ringKrullDim ↑(X.presheaf.stalk x) + ↑(Cardinal.toENat (Algebra.trdeg k (IsLocalRing.ResidueField ↑(X.presheaf.stalk x))))

theorem AlgebraicGeometry.exists_affineOpen_isStandardSmoothOfRelativeDimension' {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [Smooth f] (x : ↥X) : ∃ (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (m : ℕ), Algebra.IsStandardSmoothOfRelativeDimension m k ↑(X.presheaf.obj (Opposite.op V))

Every point of a scheme smooth over k has an affine neighbourhood whose section ring is standard smooth of SOME relative dimension over k.

theorem AlgebraicGeometry.isLocallyConstant_dimCount {k : Type u} [Field k] {X : Scheme} [PerfectField k] (f : X ⟶ Spec ↧k) [Smooth f] : IsLocallyConstant (dimCount f)

For f smooth over a perfect field the dimension count is locally constant.

theorem AlgebraicGeometry.exists_smoothOfRelativeDimension_of_preconnectedSpace {k : Type u} [Field k] {X : Scheme} [PerfectField k] (f : X ⟶ Spec ↧k) [Smooth f] [PreconnectedSpace ↥X] [Nonempty ↥X] : ∃ (m : ℕ), SmoothOfRelativeDimension m f

A scheme smooth over a perfect field whose underlying space is preconnected and nonempty is smooth of ONE relative dimension — the dimension count is locally constant, hence constant, and each chart's relative dimension is that constant ([Kol07, Notation 64 (1)] for the smooth locus of an integral scheme).