Derivations dual to a regular system of parameters at any point

The input for [Hau14, Proposition 5.4 (6)] at a non-closed point (Hironaka.Scheme.Snc.InducedCoordinates): at a point x of a scheme X smooth over a perfect field k, a regular system of parameters z_1, …, z_n of 𝒪_{X,x} admits dual derivations D_1, …, D_n : 𝒪_{X,x} → 𝒪_{X,x} over k with D_i z_j = δ_{ij} (exists_derivation_dual). At a closed point this is the route of Hironaka.Scheme.Snc.EtaleParameters through étale coordinates; at a general point it needs the injectivity of the conormal map (Hironaka.Algebra.RegularSmooth.Cotangent):

• Ω[𝒪_{X,x}⁄k] is free of finite rank — the base change of Ω[Γ(V)⁄k] for a standard smooth affine neighbourhood V of x (exists_affineOpen_isStandardSmooth of Hironaka.Scheme.Snc.RelativeDimension; free_finite_kaehlerDifferential_stalk);
• the conormal map 𝔪_x/𝔪_x² → κ(x) ⊗ Ω[𝒪_{X,x}⁄k] is injective because κ(x) is formally smooth over the perfect field k ([TSPA, Tag 00TU]; injective_cotangentSpaceToTensor, with Mathlib's Algebra.FormallySmooth.of_perfectField), so the classes of dz_1, …, dz_n are linearly independent in κ(x) ⊗ Ω (the z_i are a basis of 𝔪_x/𝔪_x²);
• a linear map 𝒪^n → Ω into a finite free module over a local ring which is injective modulo the maximal ideal is a split injection (Mathlib's IsLocalRing.split_injective_iff_lTensor_residueField_injective); the retraction composed with the universal derivation d and the coordinate projections gives the D_i.

Sources: [Hau14, Proposition 5.4 (6)]; [Hau03, Appendix C (7)]; [TSPA, Tag 00TU].

theorem AlgebraicGeometry.free_finite_kaehlerDifferential_stalk {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [Smooth f] (x : ↥X) : Module.Free ↑(X.presheaf.stalk x) Ω[↑(X.presheaf.stalk x)⁄k] ∧ Module.Finite ↑(X.presheaf.stalk x) Ω[↑(X.presheaf.stalk x)⁄k]

Ω[𝒪_{X,x}⁄k] is a finite free module at every point of a scheme smooth over k: the base change of Ω[Γ(V)⁄k], free and finite on a standard smooth affine neighbourhood V ∋ x.

theorem AlgebraicGeometry.essFiniteType_stalk_of_smooth {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [Smooth f] (x : ↥X) : Algebra.EssFiniteType k ↑(X.presheaf.stalk x)

The stalk of a scheme smooth over k is essentially of finite type over k (the form of essFiniteType_stalk without a relative dimension).

theorem AlgebraicGeometry.essFiniteType_residueField_stalk_of_smooth {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [Smooth f] (x : ↥X) : Algebra.EssFiniteType k (IsLocalRing.ResidueField ↑(X.presheaf.stalk x))

The residue field of the stalk is essentially of finite type over k.

theorem AlgebraicGeometry.exists_derivation_dual {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [PerfectField k] [Smooth f] (x : ↥X) {n : ℕ} (z : Fin n → ↑(X.presheaf.stalk x)) (hz : IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) = Ideal.span (Set.range z)) (hn : ↑n = ringKrullDim ↑(X.presheaf.stalk x)) : ∃ (D : Fin n → Derivation k ↑(X.presheaf.stalk x) ↑(X.presheaf.stalk x)), ∀ (i j : Fin n), (D i) (z j) = if i = j then 1 else 0

At any point x of X smooth over the perfect field k, a regular system of parameters z of 𝒪_{X,x} has dual derivations over k: D_i z_j = δ_{ij} ([TSPA, Tag 00TU] for the injectivity of the conormal map).