Functions critical along a section of étale coordinates, and at a nondegenerate point

Let W be a smooth A-algebra and x : ι → W étale coordinates: finitely many elements whose differentials form a basis of Ω[W⁄A]. Their common zero locus W ⧸ (x) is étale over A, as the base change of the étale map A[Xᵢ] → W, Xᵢ ↦ xᵢ, along Xᵢ ↦ 0 (Module.Basis.etale_quotient_span_range).

Let f ∈ W be critical along this section, in the sense that df ∈ (x) • Ω[W⁄A]. Then, étale locally on the base and on W around any point P of the section, f is a function on the base plus an element of (x) ^ 2: there are an étale A-algebra A', an étale W-algebra W' over A' in which x are again étale coordinates, a prime P' above P with the same residue field, and h ∈ A' with f - h ∈ (x) ^ 2 in W'. With two coordinates p, q this says f = h + a p² + b p q + c q² with a, b, c ∈ W'. This is the second-order normal form of the equation of a plane curve near a point where its partial derivatives cut out the section. Up to sign it is the shape a p² + b p q + c q² - h from which Module.Basis.exists_etale_nodeAlgebra_hom builds étale charts of a node, when the quadratic part is nondegenerate and split at P.

One may take A' = W ⧸ (x). As it is unramified over A, the diagonal of Spec A' ×_A Spec A' is the locus where some t ∈ A' ⊗[A] A' is invertible, with t (1 ⊗ s - s ⊗ 1) = 0 for all s and s₁ ⊗ s₂ ↦ s₁ s₂ sending t to 1 (Algebra.FormallyUnramified.iff_exists_tensorProduct). Let W' be A' ⊗[A] W with a lift of t inverted. There the two images of f in the section agree, so f - h ∈ (x) for h = f mod (x) ∈ A'. As d(f - h) = df ∈ (x) • Ω, this forces f - h ∈ (x) ^ 2 (Module.Basis.mem_span_range_sq_of_D_mem).

A function with a nondegenerate critical point is critical along such a section. Let ∂ᵢ be the partial derivatives dual to a basis bᵢ of Ω[W⁄A], and let f ∈ W have Hessian determinant det (∂ᵢ ∂ⱼ f) invertible. Then the partial derivatives yᵢ = ∂ᵢ f are étale coordinates, as the matrix of their differentials in the basis b is the Hessian; and df = Σ yᵢ bᵢ ∈ (y) • Ω. If f is critical at a point P, that is yᵢ ∈ P, the result above therefore applies along y. In two variables it puts f, étale locally around P, in the form h + a s² + b s t + c t² with s = ∂₀ f, t = ∂₁ f and h ∈ A'. The discriminant b² - 4ac does not vanish at P': modulo P' the Hessian of f along s, t is the transposed inverse of its Hessian along b, and the Hessian of the quadratic form has determinant -(b² - 4ac) (TauCeti.algebraMap_residueField_det_hessian_ne_zero_iff). This is the input shape of Module.Basis.exists_etale_nodeAlgebra_hom, up to the sign of h; that theorem further asks the quadratic form to split over κ(P').

Main results

• Module.Basis.exists_etale_sub_algebraMap_mem_span_range_sq: étale locally, a function critical along the section of étale coordinates is a function on the base plus an element of (x) ^ 2.
• Module.Basis.exists_basis_D_localizationAway_det_hessian: after inverting the Hessian determinant of f, the partial derivatives of f are étale coordinates.
• Module.Basis.exists_etale_eq_algebraMap_add_quadratic: étale locally around a nondegenerate critical point, a function of two coordinates is h + a s² + b s t + c t² with h from the base, s, t its partial derivatives, and b² - 4ac nonvanishing at the point.

References

• B. Iversen, Generic local structure of the morphisms in commutative algebra, Lecture Notes in Mathematics 310, Propositions I.2.3 and I.2.6, for the diagonal of an unramified algebra, as in Mathlib's Algebra.FormallyUnramified.iff_exists_tensorProduct.
• Stacks Project, Section 53.20, Tag 0C58: families of nodal curves and their étale local structure.

theorem Module.Basis.exists_etale_sub_algebraMap_mem_span_range_sq {A W : Type u} [CommRing A] [CommRing W] [Algebra A W] [Algebra.Smooth A W] {ι : Type u_1} {x : ι → W} (b : Basis ι W Ω[W⁄A]) (hb : ∀ (i : ι), b i = (KaehlerDifferential.D A W) (x i)) (P : Ideal W) [P.IsPrime] (hx : ∀ (i : ι), x i ∈ P) {f : W} (hf : (KaehlerDifferential.D A W) f ∈ Ideal.span (Set.range x) • ⊤) : ∃ (A' : Type u) (x_1 : CommRing A') (x_2 : Algebra A A') (_ : Algebra.Etale A A') (W' : Type u) (x_4 : CommRing W') (x_5 : Algebra W W') (_ : Algebra.Etale W W') (x_7 : Algebra A' W') (x_8 : Algebra A W') (_ : IsScalarTower A W W') (_ : IsScalarTower A A' W') (_ : Algebra.Smooth A' W') (b' : Basis ι W' Ω[W'⁄A']) (P' : Ideal W') (x_12 : P'.IsPrime) (hP' : P = Ideal.comap (algebraMap W W') P') (h : A'), (∀ (i : ι), b' i = (KaehlerDifferential.D A' W') ((algebraMap W W') (x i))) ∧ Function.Bijective ⇑(Ideal.ResidueField.map P P' (algebraMap W W') hP') ∧ (algebraMap W W') f - (algebraMap A' W') h ∈ Ideal.span (Set.range (⇑(algebraMap W W') ∘ x)) ^ 2

Étale locally, a function critical along a section of étale coordinates is a function on the base up to second order. Let W be a smooth A-algebra, x : ι → W elements whose differentials form a basis of Ω[W⁄A], all lying in a prime P, and f ∈ W with df ∈ (x) • Ω[W⁄A]. Then there are an étale A-algebra A', an étale W-algebra W' which is a smooth A'-algebra in which the images of x are again étale coordinates, a prime P' of W' above P with the same residue field, and h ∈ A' such that f - h ∈ (x) ^ 2 in W'.

theorem Module.Basis.exists_basis_D_localizationAway_det_hessian {A : Type u_1} {W : Type u_2} [CommRing A] [CommRing W] [Algebra A W] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b : Basis ι W Ω[W⁄A]) (f : W) : ∃ (b' : Basis ι (Localization.Away (TauCeti.hessian (fun (i : ι) => (b.coord i).compDer (KaehlerDifferential.D A W)) f).det) Ω[Localization.Away (TauCeti.hessian (fun (i : ι) => (b.coord i).compDer (KaehlerDifferential.D A W)) f).det⁄A]), ∀ (i : ι), b' i = (KaehlerDifferential.D A (Localization.Away (TauCeti.hessian (fun (i : ι) => (b.coord i).compDer (KaehlerDifferential.D A W)) f).det)) ((algebraMap W (Localization.Away (TauCeti.hessian (fun (i : ι) => (b.coord i).compDer (KaehlerDifferential.D A W)) f).det)) (((b.coord i).compDer (KaehlerDifferential.D A W)) f))

Partial derivatives with invertible Hessian are étale coordinates. Let b be a basis of Ω[W⁄A], with dual partial derivatives ∂ᵢ, and let f ∈ W. After inverting the Hessian determinant det (∂ᵢ ∂ⱼ f), the differentials of the partial derivatives ∂ᵢ f form a basis of Ω.

theorem Module.Basis.exists_etale_eq_algebraMap_add_quadratic {A W : Type u} [CommRing A] [CommRing W] [Algebra A W] [Algebra.Smooth A W] (bW : Basis (Fin 2) W Ω[W⁄A]) (f : W) (P : Ideal W) [P.IsPrime] (hf : ∀ (i : Fin 2), ((bW.coord i).compDer (KaehlerDifferential.D A W)) f ∈ P) (hdet : (TauCeti.hessian (fun (i : Fin 2) => (bW.coord i).compDer (KaehlerDifferential.D A W)) f).det ∉ P) : ∃ (A' : Type u) (x : CommRing A') (x_1 : Algebra A A') (_ : Algebra.Etale A A') (W' : Type u) (x_3 : CommRing W') (x_4 : Algebra W W') (_ : Algebra.Etale W W') (x_6 : Algebra A' W') (x_7 : Algebra A W') (_ : IsScalarTower A W W') (_ : IsScalarTower A A' W') (_ : Algebra.Smooth A' W') (bW' : Basis (Fin 2) W' Ω[W'⁄A']) (P' : Ideal W') (x_11 : P'.IsPrime) (hP' : P = Ideal.comap (algebraMap W W') P') (h : A') (a : W') (b : W') (c : W'), (∀ (i : Fin 2), bW' i = (KaehlerDifferential.D A' W') ((algebraMap W W') (((bW.coord i).compDer (KaehlerDifferential.D A W)) f))) ∧ Function.Bijective ⇑(Ideal.ResidueField.map P P' (algebraMap W W') hP') ∧ (algebraMap W W') f = (algebraMap A' W') h + (a * (algebraMap W W') (((bW.coord 0).compDer (KaehlerDifferential.D A W)) f) ^ 2 + b * (algebraMap W W') (((bW.coord 0).compDer (KaehlerDifferential.D A W)) f) * (algebraMap W W') (((bW.coord 1).compDer (KaehlerDifferential.D A W)) f) + c * (algebraMap W W') (((bW.coord 1).compDer (KaehlerDifferential.D A W)) f) ^ 2) ∧ (algebraMap W' P'.ResidueField) (discrim a b c) ≠ 0

Second-order normal form at a nondegenerate critical point. Let W be a smooth A-algebra, bW a basis of Ω[W⁄A] with dual partial derivatives ∂₀, ∂₁, and P a prime of W. Let f ∈ W be critical at P, in the sense that ∂₀ f, ∂₁ f ∈ P, with Hessian determinant det (∂ᵢ ∂ⱼ f) not in P. Then there are an étale A-algebra A', an étale W-algebra W' which is a smooth A'-algebra, a prime P' of W' above P with the same residue field, h ∈ A' and a, b, c ∈ W' with the following properties: the partial derivatives s = ∂₀ f, t = ∂₁ f are étale coordinates of W' over A' (their differentials form a basis of Ω[W'⁄A']), f = h + a s² + b s t + c t² in W', and the discriminant b² - 4ac does not vanish at P'.