Scheme forms of "smooth implies regular" and of the dimension of a smooth stalk #
The affine reduction of Hironaka/Algebra/RegularSmooth/SmoothAt.lean and Regular.lean turns the
ring statements of this directory into statements about a scheme X locally of finite type over a
field k, f : X ⟶ Spec k. Regularity (the last sentence of [TSPA, Tag 00TT]): a point x of
the smooth locus of f is a regular point, because on an affine open U ∋ x with prime 𝔮 of
x, x ∈ f.smoothLocus means Γ(X, U) is smooth at 𝔮 over k
(mem_smoothLocus_iff_isSmoothAt), Γ(X, U) is of finite type over k, so Γ(X, U)_𝔮 is
regular (SmoothImpliesRegular.lean), and Γ(X, U)_𝔮 ≅ 𝒪_{X,x}
(isRegularAt_iff_isRegularLocalRing_localization). Dimension ([TSPA, Tag 0A21, (10)]): if f
is smooth of relative dimension n, every x has an affine open V ∋ x on which Γ(X, V) is
standard smooth of relative dimension n over k (Mathlib's SmoothOfRelativeDimension, with
Spec k a single point so the affine open of the target is ⊤, and the base ring Γ(Spec k, ⊤)
replaced by k along Scheme.ΓSpecIso); the stalk 𝒪_{X,x} ≅ Γ(X, V)_𝔮 as k-algebras
(Scheme.Hom.stalkAlgebra, the scalar tower of Stalk.lean), so dim 𝒪_{X,x} + trdeg_k κ(x) = n
and, at a closed point (where 𝔮 is maximal), dim 𝒪_{X,x} = n follow from the affine statements
of Dimension.lean. The closed-point form gives the dimension of the local rings of a smooth
variety, used for étale coordinates and normal crossings (Hironaka/Smooth/, Hironaka/Snc/).
For X locally of finite type over a field k, a point of the smooth locus of X → Spec k is
a regular point (the last sentence of [TSPA, Tag 00TT]).
For f : X ⟶ Spec k smooth of relative dimension n, every point has an affine open
neighbourhood V on which Γ(X, V) is standard smooth of relative dimension n over k
(Mathlib's SmoothOfRelativeDimension, with the affine open of Spec k necessarily ⊤ and the
base ring Γ(Spec k, ⊤) replaced by k along Scheme.ΓSpecIso).
The scheme form of [TSPA, Tag 0A21, (10)]: for k perfect and f : X ⟶ Spec k smooth of
relative dimension n, at every point x, with κ(x) the residue field of the stalk as a
k-algebra through f, dim 𝒪_{X,x} + trdeg_k κ(x) = n.
For k perfect and f : X ⟶ Spec k smooth of relative dimension n, the stalk at a closed
point has dimension n (its residue field is finite over k by Zariski's lemma).