Regular coordinates on the stalks of a smooth scheme #
[Kol07, Definition 73]: for local coordinates x₁, …, xₙ at a point p ∈ X, the derivations
∂/∂x₁, …, ∂/∂xₙ are "local generators of Der_X". For the stalk 𝒪_{X,x} of a scheme
smooth of relative dimension n over a field k of characteristic zero, this module produces the
coordinate structure RegularCoords 𝒪_{X,x} m of Hironaka/Algebra/Local/Coords.lean with
k-linear derivations: a regular system of parameters y₁, …, y_m (m = dim 𝒪_{X,x}) and
k-derivations ∂ᵢ with ∂ᵢ yⱼ = δᵢⱼ (exists_regularCoords_stalk; with a prescribed regular
system of parameters, exists_regularCoords_stalk_of_span_eq).
The construction reads Kollár's "local coordinates" at an arbitrary point: Ω_{𝒪_{X,x}/k} is
finitely presented and projective (the stalk is essentially of finite type and formally smooth
over k, being a localization of a standard smooth algebra, formallySmooth_stalk), and a
κ(x)-basis of κ(x) ⊗ Ω lifts to a basis of Ω (Mathlib's
Module.exists_basis_of_basis_baseChange); the basis dy₁, …, dy_m, dz₁, …, dz_t of κ(x) ⊗ Ω
is exists_basis_tensor_kaehlerDifferential_sum of
Hironaka/Scheme/Smooth/DifferentialBasisAny.lean, for lifts z of a transcendence basis of
κ(x)/k, separating because k has characteristic zero. The ∂ᵢ are the duals of the dyᵢ under
Ω[A⁄k] →ₗ A ≃ Der_k(A, A) (linearMapEquivDerivation); they commute because their commutator is a
derivation vanishing on every yⱼ and zₗ, hence on the basis of Ω. Every k-derivation is
δ = ∑ᵢ δ(yᵢ) ∂ᵢ + ∑ₗ δ(zₗ) ∂'ₗ (exists_regularCoords_stalk_aux); when κ(x) is algebraic over
k, at every closed point, the transcendence basis is empty and the ∂ᵢ span Der_k(𝒪_{X,x})
(SpansDerivations k, exists_regularCoords_stalk_of_isAlgebraic). At a non-closed point
(t > 0) the ∂ᵢ do not span, the dual of a dzₗ killing every parameter; there only the
inclusion c.D ≤ D is available (D_le_derivative, Hironaka/Algebra/Derivative/Basic.lean).
Used for the cosupport of the derivative ideals
(Hironaka/Scheme/IdealSheaf/Derivative/Cosupport.lean,
Hironaka/Scheme/IdealSheaf/Derivative/Properties.lean,
Hironaka/Scheme/IdealSheaf/Derivative/FlagCoords.lean), for maximal contact and tuning on schemes
(Hironaka/Resolution/Algebraic/MaximalContact/FormalEquivBridge.lean,
Hironaka/Resolution/Algebraic/Tuning/MCTuned.lean,
Hironaka/Resolution/Algebraic/Tuning/Corollary101.lean) and on manifolds
(Hironaka/Manifold/Germ/CoordDerivCoords.lean,
Hironaka/Manifold/BlowUp/Transform/DerivTransform.lean).
The stalk of a smooth k-scheme is formally smooth over k: it is a localization of a
standard smooth k-algebra (exists_affineOpen_isStandardSmoothOfRelativeDimension).
The construction with a prescribed regular system of parameters y of 𝒪_{X,x}
(m = dim 𝒪_{X,x} members generating 𝔪_x): regular coordinates c with c.x = y and k-linear
derivations ∂ᵢ, lifts z of a transcendence basis of κ(x)/k, and k-derivations ∂'ₗ dual to
the dzₗ, such that every k-derivation is δ = ∑ᵢ δ(yᵢ) ∂ᵢ + ∑ₗ δ(zₗ) ∂'ₗ (the ∂ᵢ, ∂'ₗ are
the dual basis of dy₁, …, dy_m, dz₁, …, dz_t lifted to Ω_{𝒪_{X,x}/k}). Used with flag
parameters in Hironaka/Scheme/IdealSheaf/Derivative/FlagCoords.lean.
The construction for a regular system of parameters chosen here: regular coordinates c on
the stalk with k-linear derivations ∂ᵢ, lifts z of a transcendence basis of κ(x)/k, and
k-derivations ∂'ₗ dual to the dzₗ, such that every k-derivation is
δ = ∑ᵢ δ(yᵢ) ∂ᵢ + ∑ₗ δ(zₗ) ∂'ₗ (the ∂ᵢ, ∂'ₗ are the dual basis of dy₁, …, dy_m, dz₁, …, dz_t
lifted to Ω_{𝒪_{X,x}/k}).
Regular coordinates on the stalks (Kollár's local coordinates, [Kol07, Definition 73]):
at every point of a scheme smooth of relative dimension n over a field k of characteristic
zero, the stalk carries regular coordinates (RegularCoords) whose derivations are k-linear.
The spanning of the k-derivations holds at the points with residue field algebraic over k
(exists_regularCoords_stalk_of_isAlgebraic) and fails at the other points, where the dual of a
dzₗ kills every parameter.
At a point whose residue field is algebraic over k, in particular at every closed point, the
stalk carries regular coordinates whose k-linear derivations ∂ᵢ span the k-derivations,
δ = ∑ᵢ δ(yᵢ) ∂ᵢ (Kollár's "the derivations ∂/∂x₁, …, ∂/∂xₙ are local generators of Der_X",
[Kol07, Definition 73]): the transcendence basis of κ(x)/k is empty, so the ∂ᵢ are the whole
dual basis.