Differentials of a regular system of parameters at a closed point #
f : X ⟶ Spec k smooth of relative dimension n over a perfect field, x ∈ X a closed point,
𝒪 = 𝒪_{X,x}, κ = κ(x). The main theorem: for a regular system of parameters y_0, …, y_{n-1}
of 𝒪, the classes 1 ⊗ d y_i form a basis of κ ⊗_𝒪 Ω[𝒪⁄k]
(exists_basis_tensor_kaehlerDifferential_of_span_eq_maximalIdeal), the differentials of Kollár's
local coordinates at a point of a smooth variety ([Kol07, Definition 24]). The argument assembles
the comparison of regular and smooth points of Hironaka/Algebra/RegularSmooth/: the conormal map
𝔪/𝔪² → κ ⊗ Ω[𝒪⁄k], ȳ ↦ 1 ⊗ d y, is injective because κ is formally smooth over the perfect
k ([TSPA, Tag 00TU]; injective_cotangentSpaceToTensor); the classes of the y_i form a basis
of 𝔪/𝔪² (Nakayama, Hironaka/Algebra/Local/RegularSystem.lean); and
dim_κ κ ⊗ Ω[𝒪⁄k] = dim_κ 𝔪/𝔪² + dim_κ Ω[κ⁄k] = n + 0 (the conormal sequence of [TSPA, Tag 00TV];
𝔪/𝔪² has dimension dim 𝒪 = n at a closed point by regularity, and Ω[κ⁄k] = 0 because
trdeg_k κ = 0 there). An injective map from an n-dimensional space to an n-dimensional
space carries a basis to a basis.
Used to spread adapted parameters out to étale coordinates on an affine neighbourhood
(Hironaka/Scheme/Smooth/EtaleLocal.lean, EtaleCoordinatesAdapted.lean,
CoordinateSystemPair.lean).
The stalk of a scheme locally of finite type over k is essentially of finite type over
k.
The residue field of the stalk is essentially of finite type over k.
Ω[𝒪_{X,x}⁄k] is a finite 𝒪_{X,x}-module (the localization of the finite module
Ω[Γ(U)⁄k] of a standard smooth affine chart).
At a closed point the residue field is algebraic over k: trdeg_k κ(x) = 0 (the dimension
formula dim 𝒪_{X,x} + trdeg_k κ(x) = n with dim 𝒪_{X,x} = n).
At a closed point dim_κ 𝔪_x/𝔪_x² = n (regularity of the stalk and dim 𝒪_{X,x} = n).
At a closed point dim_κ κ(x) ⊗ Ω[𝒪_{X,x}⁄k] = n (the short exact conormal sequence, with
Ω[κ(x)⁄k] = 0).
The differentials of a regular system of parameters at a closed point form a basis of
κ(x) ⊗ Ω[𝒪_{X,x}⁄k] ([TSPA, Tag 00TU]; the local coordinates of [Kol07, Definition 24] at a
closed point).