Flag coordinates at a point of a smooth centre inside a smooth hypersurface

The proof of [Kol07, Theorem 88] chooses, at a point of the centre Z ⊆ S, "coordinates x₁, …, xₙ such that S = (x₁ = 0)" and the centre is (x₁ = ⋯ = x_r = 0). This module produces such coordinates on the stalk, in two steps.

• The flag of parameters (exists_span_eq_and_chartCenter_eq). Adapted parameters give a regular system of parameters y of 𝒪_{X,z} with Z_z = (y₀, …, y_{c−1}) (exists_adaptedParameters_of_smooth, Hironaka/Scheme/BlowUpSequence/SmoothCenter.lean). The local equation a of the smooth divisor S (S_z = (a), a ∈ 𝔪 ∖ 𝔪², IsSmoothDivisor of Hironaka/Scheme/Snc/SmoothDivisor.lean) lies in Z_z, so a = ∑_{l < c} u_l y_l; not every u_l lies in 𝔪, else a ∈ 𝔪 Z_z ⊆ 𝔪². For a unit u_j, replacing y_j by a changes neither (y₀, …, y_{c−1}) nor (y₀, …, y_{m−1}) (exists_span_update of Hironaka/Algebra/Local/MaximalContact.lean, the exchange of a parameter behind Kollár's local construction of a hypersurface of maximal contact, [Kol07, 51.2], here with the index kept below c), and the transposition (0 j) moves a to index 0: 𝔪 = (x₀, …, x_{m−1}) with x₀ = a and Z_z = (x₀, …, x_r) = chartCenter x r, r = c − 1 (or n − 1 when c ≥ n).
• The derivations (exists_flagCoords, exists_flagCoords_of_isAlgebraic). The construction of the coordinate derivations of Hironaka/Scheme/IdealSheaf/Derivative/StalkCoords.lean runs for any prescribed regular system of parameters (exists_regularCoords_stalk_of_span_eq): the ∂ᵢ dual to the dxᵢ are k-linear, and at a point with residue field algebraic over k (every closed point) they span the k-derivations, because the transcendence basis is empty.

Used in the proof of [Kol07, Theorem 88] for one blow-up (Hironaka/Resolution/Algebraic/Kol07/Theorem88BlowUp.lean).

theorem AlgebraicGeometry.exists_span_eq_and_chartCenter_eq {R : Type u_1} [CommRing R] [IsLocalRing R] {n : ℕ} (x : Fin n → R) (hx : IsLocalRing.maximalIdeal R = Ideal.span (Set.range x)) {c : ℕ} {a : R} (ha : a ∈ Ideal.span (x '' {j : Fin n | ↑j < c})) (ha2 : a ∉ IsLocalRing.maximalIdeal R ^ 2) : ∃ (h0 : 0 < n) (r : Fin n) (x' : Fin n → R), x' ⟨0, h0⟩ = a ∧ IsLocalRing.maximalIdeal R = Ideal.span (Set.range x') ∧ IsLocalRing.chartCenter x' r = Ideal.span (x '' {j : Fin n | ↑j < c})

The flag of parameters: if x generates 𝔪 and a ∈ (x₀, …, x_{c−1}) ∖ 𝔪², some x_j with j < c may be replaced by a and moved to index 0: a family x' with x'₀ = a generating 𝔪 and with chartCenter x' r = (x'₀, …, x'_r) = (x₀, …, x_{c−1}), r = min (c − 1) (n − 1).

theorem AlgebraicGeometry.exists_flagCoords_aux {k : Type u} [Field k] [CharZero k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (Z S : X.IdealSheafData) [Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (hS : IsSmoothDivisor S) (hZS : S ≤ Z) {z : ↥X} (hz : z ∈ Z.support) : ∃ (n' : ℕ) (t : ℕ) (c : IsLocalRing.RegularCoords (↑(X.presheaf.stalk z)) n') (h0 : 0 < n') (r : Fin n') (w : Fin t → ↑(X.presheaf.stalk z)) (der' : Fin t → Derivation k ↑(X.presheaf.stalk z) ↑(X.presheaf.stalk z)), c.IsLinearOver k ∧ S.stalkIdeal z = Ideal.span {c.x ⟨0, h0⟩} ∧ Z.stalkIdeal z = IsLocalRing.chartCenter c.x r ∧ (IsTranscendenceBasis k fun (j : Fin t) => (IsLocalRing.residue ↑(X.presheaf.stalk z)) (w j)) ∧ ∀ (δ : Derivation k ↑(X.presheaf.stalk z) ↑(X.presheaf.stalk z)) (a : ↑(X.presheaf.stalk z)), δ a = ∑ i : Fin n', δ (c.x i) * (c.pderiv i) a + ∑ j : Fin t, δ (w j) * (der' j) a

The construction: flag coordinates at z ∈ Z ⊆ S together with the spanning data of Hironaka/Scheme/IdealSheaf/Derivative/StalkCoords.lean, lifts w of a transcendence basis of κ(z)/k and the derivations ∂'ₗ dual to the dwₗ, with δ = ∑ᵢ δ(xᵢ) ∂ᵢ + ∑ₗ δ(wₗ) ∂'ₗ for every k-derivation δ.

theorem AlgebraicGeometry.exists_flagCoords {k : Type u} [Field k] [CharZero k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (Z S : X.IdealSheafData) [Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (hS : IsSmoothDivisor S) (hZS : S ≤ Z) {z : ↥X} (hz : z ∈ Z.support) : ∃ (n' : ℕ) (c : IsLocalRing.RegularCoords (↑(X.presheaf.stalk z)) n') (h0 : 0 < n') (r : Fin n'), c.IsLinearOver k ∧ S.stalkIdeal z = Ideal.span {c.x ⟨0, h0⟩} ∧ Z.stalkIdeal z = IsLocalRing.chartCenter c.x r

Flag coordinates (the coordinates of the proof of [Kol07, Theorem 88]): at a point z of the smooth centre Z ⊆ S, S a smooth hypersurface, the stalk has regular coordinates with k-linear derivations, S_z = (x₀) and Z_z = (x₀, …, x_r).

theorem AlgebraicGeometry.exists_flagCoords_of_isAlgebraic {k : Type u} [Field k] [CharZero k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (Z S : X.IdealSheafData) [Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (hS : IsSmoothDivisor S) (hZS : S ≤ Z) {z : ↥X} (hz : z ∈ Z.support) (halg : Algebra.IsAlgebraic k (IsLocalRing.ResidueField ↑(X.presheaf.stalk z))) : ∃ (n' : ℕ) (c : IsLocalRing.RegularCoords (↑(X.presheaf.stalk z)) n') (h0 : 0 < n') (r : Fin n'), c.IsLinearOver k ∧ c.SpansDerivations k ∧ S.stalkIdeal z = Ideal.span {c.x ⟨0, h0⟩} ∧ Z.stalkIdeal z = IsLocalRing.chartCenter c.x r

At a point with residue field algebraic over k (every closed point), the flag coordinates may be taken with derivations spanning the k-derivations (exists_regularCoords_stalk_of_isAlgebraic): the transcendence basis is empty, so the ∂'ₗ-sum of the spanning formula is empty.