Dual derivations at a closed point span the derivations #
At a closed point x of a scheme smooth of relative dimension n over a field k of
characteristic zero, κ(x) ⊗ Ω_{𝒪_{X,x}/k} has dimension n
(finrank_residueField_tensor_kaehler_stalk_of_isClosed,
Hironaka/Scheme/Smooth/DifferentialBasis.lean). Hence for any n elements y₁, …, yₙ of
𝒪_{X,x} with k-derivations ∂₁, …, ∂ₙ dual to them (∂ᵢ yⱼ = δᵢⱼ), with no assumption that the
yᵢ vanish at x or generate 𝔪_x, the dyᵢ form a basis of Ω_{𝒪_{X,x}/k}: their classes in
κ(x) ⊗ Ω are independent, being dual to the ∂ᵢ, hence a basis by the count, and lift by Nakayama
(Mathlib's exists_basis_of_basis_baseChange); so every k-derivation is δ = ∑ᵢ δ(yᵢ) ∂ᵢ
(forall_derivation_eq_sum_of_isClosed).
This is Kollár's "the derivations ∂/∂x₁, …, ∂/∂xₙ are local generators of Der_X"
([Kol07, Definition 73]) at a closed point, for coordinates that need not be centred there. It is
used in the proof of [Kol07, Theorem 88] for one blow-up
(Hironaka/Resolution/Algebraic/Kol07/Theorem88BlowUp.lean) at the closed points q of a chart of
the blow-up: the chart coordinates yᵢ/y_ρ, y_ρ, y_l need not vanish at q, but their duals are
the chart derivations ∂'ⱼ of Hironaka/Algebra/Local/Chart.lean (chartDerivRing_chartYR), so
the ∂'ⱼ generate the k-derivations of 𝒪_{B,q}, and the chart derivative ideal D' computed
with them is the derivative ideal of the stalk. At a non-closed point the parameters are fewer than
n and the spanning by their duals fails
(Hironaka/Scheme/IdealSheaf/Derivative/StalkCoords.lean).
Kollár's local generators of Der_X ([Kol07, Definition 73]) at a closed point: at a closed
point x of a scheme smooth of relative dimension n over k, n elements yᵢ of 𝒪_{X,x}
with dual k-derivations ∂ᵢ (∂ᵢ yⱼ = δᵢⱼ) have δ = ∑ᵢ δ(yᵢ) ∂ᵢ for every k-derivation
δ: the dyᵢ are a basis of Ω_{𝒪_{X,x}/k}, whose rank at a closed point is n.