The differential basis at an arbitrary point #
Kollár's local coordinates at non-closed points: at any x ∈ X (smooth of relative dimension n
over the perfect field k), with t = trdeg_k κ(x), a regular system of parameters
y_0, …, y_{m-1} of 𝒪_{X,x} (m = dim 𝒪_{X,x} = n − t) together with lifts
z_0, …, z_{t-1} ∈ 𝒪_{X,x} of a separating transcendence basis of κ(x)/k has differentials
1 ⊗ d y_i, 1 ⊗ d z_j forming a basis of κ(x) ⊗ Ω[𝒪_{X,x}⁄k]
(exists_basis_tensor_kaehlerDifferential_sum). Not in the sources in this form.
The argument: the conormal sequence 0 → 𝔪/𝔪² → κ ⊗ Ω[𝒪⁄k] → Ω[κ⁄k] → 0 is exact
([TSPA, Tag 00TV]; κ is formally smooth over the perfect k, see
Hironaka/Algebra/RegularSmooth/Cotangent.lean); the d s_j of a separating transcendence basis
s form a basis of Ω[κ⁄k]
(exists_basis_kaehlerDifferential_of_isTranscendenceBasis, the construction of
Hironaka/Algebra/RegularSmooth/Trdeg.lean: Ω[k[s]⁄k] is free on the d s_j, and k(s)/k[s] and
κ/k(s) are formally étale, [TSPA, Tags 00RX, 030O]); the classes ȳ_i form a basis of 𝔪/𝔪²
(Nakayama). Hence the family 1 ⊗ d y_i (in the image of 𝔪/𝔪²) and 1 ⊗ d z_j (mapping to the
basis d s_j) is linearly independent of size m + t, and
dim_κ κ ⊗ Ω = dim 𝔪/𝔪² + dim Ω[κ⁄k] = m + t, so it is a basis. Used in
Hironaka/Scheme/IdealSheaf/Derivative/StalkCoords.lean.
For a separating transcendence basis v of K/k, the differentials d (v i) form a basis of
Ω[K⁄k] ([TSPA, Tags 00RX, 030O]; the construction of Hironaka/Algebra/RegularSmooth/Trdeg.lean).
At any point x, the differentials of a regular system of parameters y of 𝒪_{X,x} and of
lifts z of a separating transcendence basis of κ(x)/k form a basis of κ(x) ⊗ Ω[𝒪_{X,x}⁄k]
([TSPA, Tag 00TV] for the conormal sequence, [TSPA, Tag 00RX] for the differentials of the basis).