Coordinates at a point of an étale chart

Hauser's chart computation ([Hau14, Proposition 5.4 (6)]; [Hau03, Appendix C (7)]) reads the total transform of an snc divisor in the chart of a smooth blow-up at a rational point, where the chart functions y_i vanishing at the point are, by construction, local coordinates. At a general point x' of the exceptional divisor — a prime q of the chart ring A — the vanishing chart functions need not be a full system of parameters; this module says what survives. For a k-algebra A with étale coordinates y : Fin n → A (the k-algebra map k[t_0, …, t_{n-1}] → A, t_i ↦ y_i, is étale; the chart functions of Hironaka.Scheme.Smooth.ChartEtale) and any prime q of A:

• A_q is a regular local ring (A is smooth over k, being étale over k[t]);
• the coordinates vanishing at q are part of a regular system of parameters of A_q (exists_span_eq_maximalIdeal_of_etale_coordinates).

Why the lemma holds. The second clause is the regular-sequence criterion [TSPA, Tag 00NR] with [TSPA, Tag 00UW]; the argument here is the classical one through coordinate derivations. The partial derivative ∂/∂t_c of k[t] extends to a k-derivation D_c of A because A is formally smooth over k[t] (Derivation.exists_extension_of_formallySmooth), with D_c (y_{c'}) = δ_{c c'}, and D_c localizes to A_q (Derivation.localization). A derivation maps 𝔪² = 𝔪 · 𝔪 into 𝔪 by the Leibniz rule; so if a combination ∑ a_c y_c of vanishing coordinates lies in 𝔪_q², applying D_c shows a_c ∈ 𝔪_q: the classes of the vanishing y_c in 𝔪_q/𝔪_q² are linearly independent over κ(q) (linearIndependent_toCotangent_of_derivations). In a regular local ring a linearly independent family of 𝔪/𝔪² extends to a basis (Mathlib's Basis.extend), the basis lifts to generators of 𝔪 (Nakayama, span_eq_maximalIdeal_and_card_eq_spanFinrank_iff) whose number is dim_κ 𝔪/𝔪² = dim R: a regular system of parameters containing the given elements (exists_span_eq_maximalIdeal_of_linearIndependent).

theorem Derivation.map_mem_maximalIdeal_of_mem_sq {R : Type u} [CommRing R] [IsLocalRing R] {k : Type v} [CommRing k] [Algebra k R] (D : Derivation k R R) {a : R} (ha : a ∈ IsLocalRing.maximalIdeal R ^ 2) : D a ∈ IsLocalRing.maximalIdeal R

A derivation maps 𝔪² into 𝔪: D (m n) = m D n + n D m (Leibniz).

theorem AlgebraicGeometry.linearIndependent_toCotangent_of_derivations {R : Type u} [CommRing R] [IsLocalRing R] {k : Type v} [CommRing k] [Algebra k R] {ι : Type u_1} [Finite ι] [DecidableEq ι] (w : ι → R) (hw : ∀ (i : ι), w i ∈ IsLocalRing.maximalIdeal R) (D : ι → Derivation k R R) (hD : ∀ (i j : ι), (D i) (w j) = if i = j then 1 else 0) : LinearIndependent (IsLocalRing.ResidueField R) fun (i : ι) => (IsLocalRing.maximalIdeal R).toCotangent ⟨w i, ⋯⟩

The independence step (the classical criterion by coordinate derivations): elements w_i ∈ 𝔪 admitting "dual" derivations D_i with D_i (w_j) = δ_{ij} have linearly independent classes in 𝔪/𝔪² — if ∑ a_j w_j ∈ 𝔪² then a_i = D_i (∑ a_j w_j) − ∑ w_j D_i (a_j) ∈ 𝔪.

theorem AlgebraicGeometry.exists_span_eq_maximalIdeal_of_linearIndependent {R : Type u} [CommRing R] [IsRegularLocalRing R] {ι : Type u_1} (w : ι → R) (hw : ∀ (i : ι), w i ∈ IsLocalRing.maximalIdeal R) (hli : LinearIndependent (IsLocalRing.ResidueField R) fun (i : ι) => (IsLocalRing.maximalIdeal R).toCotangent ⟨w i, ⋯⟩) : ∃ (m : ℕ) (z : Fin m → R), (Ideal.span (Set.range z) = IsLocalRing.maximalIdeal R ∧ ↑m = ringKrullDim R) ∧ ∃ (σ : ι → Fin m), Function.Injective σ ∧ ∀ (i : ι), z (σ i) = w i

The extension step ([TSPA, Tag 00NR] in cotangent form): in a regular local ring, elements w_i ∈ 𝔪 whose classes in 𝔪/𝔪² are linearly independent are part of a regular system of parameters — extend the classes to a basis, lift the new basis vectors to 𝔪, and count.

theorem AlgebraicGeometry.exists_span_eq_maximalIdeal_of_etale_coordinates {k : Type u} [Field k] {A : Type u} [CommRing A] [Algebra k A] {n : ℕ} (y : Fin n → A) (hy : (MvPolynomial.aeval y).Etale) (q : Ideal A) [q.IsPrime] : IsRegularLocalRing (Localization.AtPrime q) ∧ ∃ (m : ℕ) (z : Fin m → Localization.AtPrime q), (Ideal.span (Set.range z) = IsLocalRing.maximalIdeal (Localization.AtPrime q) ∧ ↑m = ringKrullDim (Localization.AtPrime q)) ∧ ∃ (σ : { c : Fin n // y c ∈ q } → Fin m), Function.Injective σ ∧ ∀ (c : { c : Fin n // y c ∈ q }), z (σ c) = (algebraMap A (Localization.AtPrime q)) (y ↑c)

Coordinates at a point of an étale chart ([Hau14, Proposition 5.4 (6)] and [Hau03, Appendix C (7)] at a rational point): for a k-algebra A with étale coordinates y : Fin n → A — k[t] → A, t_i ↦ y_i, étale — and any prime q of A, the local ring A_q is regular and the coordinates vanishing at q are part of a regular system of parameters of A_q. Regularity: A is smooth over k (étale over the polynomial ring), so A_q is regular; the parameters: the coordinate derivations ∂/∂t_c extend to A, localize to A_q and detect independence mod 𝔪_q².