Simple roots depend analytically on the coefficients

TauCeti.Sym.coeffEquiv presents the n-th symmetric power of an algebraically closed field as the affine space Fin n → K of coefficient tuples, and TauCeti/Analysis/Polynomial/SymmetricPower.lean proves that presentation a homeomorphism: the roots of a monic polynomial depend continuously on its coefficients. This file upgrades continuity to analyticity wherever the roots are simple, which is the analytic input that the elementary symmetric charts of Sym^g(Σ) need in order to be holomorphic.

The argument

The roots are not a polynomial function of the coefficients, so nothing here is formal. The whole file rests on one application of the implicit function theorem to the free monic polynomial

f (c, z) = z ^ n + ∑ i, c i * z ^ i,

that is, to TauCeti.Polynomial.monicOfCoeff, the specialization of Mathlib's Polynomial.freeMonic at a concrete coefficient tuple. It is a polynomial in the coefficient tuple c and the argument z jointly, hence analytic. Its partial derivative in z at a point (c₀, z₀) is the scalar P'(z₀), where P is the monic polynomial with lower coefficients c₀; multiplication by that scalar is an invertible operator exactly when z₀ is a simple root of P. The implicit function theorem then produces a function ψ of the coefficients, analytic at c₀, with ψ c₀ = z₀, whose value stays a root of the nearby polynomials: TauCeti.Polynomial.exists_analyticAt_isRoot_monicOfCoeff.

Applying this at each of the n roots of a polynomial whose roots are pairwise distinct, and noting that pairwise distinctness persists in a neighbourhood, gives an analytic ordered parametrization Ψ of the whole unordered root tuple: TauCeti.Polynomial.exists_analyticAt_monicOfCoeff_eq_prod_X_sub_C. This is the multiplicity-free part of the inverse-chart statement. The colliding-point case over ℂ is proved separately by the contour-integral argument in TauCeti/Analysis/Polynomial/RootSum.lean.

Note that no ordering of the roots is canonical: the conclusion is the existence of an analytic ordered lift of the (unordered) inverse chart, not analyticity of a preferred root function.

Main declarations

• TauCeti.Polynomial.analyticAt_eval_monicOfCoeff: the free monic polynomial is analytic in its coefficients and its argument jointly.
• TauCeti.Polynomial.exists_analyticAt_isRoot_monicOfCoeff: a simple root moves analytically with the coefficients.
• TauCeti.Polynomial.exists_analyticAt_monicOfCoeff_eq_prod_X_sub_C: a monic polynomial with n distinct roots has an analytic ordered parametrization of its roots on a neighbourhood of its coefficient tuple.
• TauCeti.Sym.exists_analyticAt_coeffEquiv_symm_eq_ofFn: the same statement read through the elementary symmetric chart, as an analytic ordered lift of the inverse chart.
• TauCeti.Sym.exists_analyticAt_coeffEquiv_ofFn_localInverse: the coefficient map of an ordered tuple is a local analytic isomorphism at every tuple of pairwise distinct points, the ordered lift being a two-sided local inverse there.
• TauCeti.Sym.analyticAt_coeffEquiv_map_coeffEquiv_symm: a coordinate change acts analytically on the elementary symmetric coordinates at multiplicity-free points. A map φ of the underlying field induces a map of coefficient tuples, sending the coefficients of a polynomial to those of the polynomial whose roots are the φ-images of its roots; it is analytic at every coefficient tuple whose roots are distinct and at which φ is analytic.

Lane F4.1 of the analytic Heegaard Floer roadmap opens with "Sym^g(Σ) geometry: smooth complex structure (elementary symmetric functions)", after Ozsváth--Szabó (arXiv:math/0101206, §2.1). A holomorphic coordinate on the surface identifies a neighbourhood in Sym^g(Σ) with an open subset of Sym^g(ℂ) (TauCeti.Sym.isOpenEmbedding_coeffEquiv_comp_map), and TauCeti.Sym.analyticAt_coeffEquiv_map_coeffEquiv_symm says that changing that coordinate acts analytically on the elementary symmetric coordinates of one such patch, at multiplicity-free tuples. That is the analytic ingredient for the transition maps of the atlas of TauCeti/Geometry/Manifold/SymmetricPower.lean. A chart there splits a tuple into the factors lying in k disjoint patches, of degrees m 1, …, m k, and regroups the resulting blocks of coefficients along a bijection (Σ i, Fin (m i)) ≃ Fin n; the general blockwise assembly is in TauCeti/Analysis/Polynomial/RootSum/Family.lean. The diagonal, where points collide, is covered over ℂ by TauCeti.Sym.analyticAt_coeffEquiv_map_coeffEquiv_symm_of_analyticAt in TauCeti/Analysis/Polynomial/RootSum.lean.

Everything is stated over an RCLike field, so it covers the real as well as the complex case, except for the elementary polynomial calculus, which needs only a nontrivially normed field; only the statements that mention the chart itself need the field algebraically closed.

The free monic polynomial

theorem TauCeti.Polynomial.analyticAt_eval_monicOfCoeff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} (q : (Fin n → 𝕜) × 𝕜) : AnalyticAt 𝕜 (fun (p : (Fin n → 𝕜) × 𝕜) => Polynomial.eval p.2 (monicOfCoeff p.1)) q

The free monic polynomial of degree n, evaluated at a coefficient tuple and an argument, is analytic in the two jointly: it is z ^ n + ∑ i, c i * z ^ i.

A simple root moves analytically

theorem TauCeti.Polynomial.exists_analyticAt_isRoot_monicOfCoeff {𝕜 : Type u_1} [RCLike 𝕜] {n : ℕ} {c₀ : Fin n → 𝕜} {z₀ : 𝕜} (hroot : (monicOfCoeff c₀).IsRoot z₀) (hsimple : Polynomial.eval z₀ (Polynomial.derivative (monicOfCoeff c₀)) ≠ 0) : ∃ (ψ : (Fin n → 𝕜) → 𝕜), ψ c₀ = z₀ ∧ AnalyticAt 𝕜 ψ c₀ ∧ ∀ᶠ (c : Fin n → 𝕜) in nhds c₀, (monicOfCoeff c).IsRoot (ψ c)

A simple root moves analytically. If z₀ is a root of the monic polynomial with lower coefficients c₀ at which the derivative does not vanish, then there is a function ψ of the coefficients, analytic at c₀, with ψ c₀ = z₀, whose value at every nearby coefficient tuple is a root of the corresponding monic polynomial.

This is the analytic implicit root theorem AnalyticAt.exists_analyticAt_eventually_eq_zero_iff applied to the free monic polynomial, whose partial derivative in the argument at (c₀, z₀) is P'(z₀).

An analytic ordered parametrization of a multiplicity-free root tuple

theorem TauCeti.Polynomial.exists_analyticAt_monicOfCoeff_eq_prod_X_sub_C {𝕜 : Type u_1} [RCLike 𝕜] {n : ℕ} {c₀ z : Fin n → 𝕜} (hz : Function.Injective z) (hc₀ : monicOfCoeff c₀ = ∏ i : Fin n, (Polynomial.X - Polynomial.C (z i))) : ∃ (Ψ : (Fin n → 𝕜) → Fin n → 𝕜), Ψ c₀ = z ∧ AnalyticAt 𝕜 Ψ c₀ ∧ ∀ᶠ (c : Fin n → 𝕜) in nhds c₀, monicOfCoeff c = ∏ i : Fin n, (Polynomial.X - Polynomial.C (Ψ c i))

The roots of a monic polynomial with distinct roots move analytically. If the monic polynomial with lower coefficients c₀ is ∏ i, (X - z i) for a tuple z of pairwise distinct points, then there is a tuple-valued function Ψ, analytic at c₀, with Ψ c₀ = z, which orders the roots of every nearby monic polynomial.

No ordering of the roots is canonical, so the ordered lift Ψ is not unique; what is asserted is that some analytic ordering exists near c₀.

theorem TauCeti.Sym.exists_analyticAt_coeffEquiv_symm_eq_ofFn {𝕜 : Type u_1} [RCLike 𝕜] [IsAlgClosed 𝕜] {n : ℕ} {c₀ z : Fin n → 𝕜} (hz : Function.Injective z) (hc₀ : (coeffEquiv 𝕜 n).symm c₀ = ofFn z) : ∃ (Ψ : (Fin n → 𝕜) → Fin n → 𝕜), Ψ c₀ = z ∧ AnalyticAt 𝕜 Ψ c₀ ∧ ∀ᶠ (c : Fin n → 𝕜) in nhds c₀, (coeffEquiv 𝕜 n).symm c = ofFn (Ψ c)

The inverse elementary symmetric chart admits an analytic ordered lift at every multiplicity-free coefficient tuple: near such a tuple the unordered root tuple is ofFn of an analytic ordered tuple.

theorem TauCeti.Sym.exists_analyticAt_coeffEquiv_ofFn_localInverse {𝕜 : Type u_1} [RCLike 𝕜] [IsAlgClosed 𝕜] {n : ℕ} {z : Fin n → 𝕜} (hz : Function.Injective z) : ∃ (Ψ : (Fin n → 𝕜) → Fin n → 𝕜), Ψ ((coeffEquiv 𝕜 n) (ofFn z)) = z ∧ AnalyticAt 𝕜 Ψ ((coeffEquiv 𝕜 n) (ofFn z)) ∧ (∀ᶠ (w : Fin n → 𝕜) in nhds z, Ψ ((coeffEquiv 𝕜 n) (ofFn w)) = w) ∧ ∀ᶠ (c : Fin n → 𝕜) in nhds ((coeffEquiv 𝕜 n) (ofFn z)), (coeffEquiv 𝕜 n) (ofFn (Ψ c)) = c

The coefficient map is a local analytic isomorphism away from the diagonal. At an ordered tuple z of pairwise distinct points there is an analytic Ψ inverting, on both sides and near z, the map that reads off the elementary symmetric coordinates of an ordered tuple.

The left inverse property is what pins the ordering down: a nearby polynomial has the same roots as its ordered lift up to a permutation, and the permutation is forced to be the identity because each Ψ i stays near z i while the z i are distinct.

theorem TauCeti.Sym.analyticAt_coeffEquiv_map_coeffEquiv_symm {𝕜 : Type u_1} [RCLike 𝕜] [IsAlgClosed 𝕜] {n : ℕ} {φ : 𝕜 → 𝕜} {c₀ z : Fin n → 𝕜} (hz : Function.Injective z) (hc₀ : (coeffEquiv 𝕜 n).symm c₀ = ofFn z) (hφ : ∀ (i : Fin n), AnalyticAt 𝕜 φ (z i)) : AnalyticAt 𝕜 (fun (c : Fin n → 𝕜) => (coeffEquiv 𝕜 n) (Sym.map φ ((coeffEquiv 𝕜 n).symm c))) c₀

A coordinate change acts analytically on the elementary symmetric coordinates away from the diagonal. A map φ of the field induces a map of coefficient tuples, taking the coefficients of a monic polynomial to those of the monic polynomial whose roots are the φ-images of its roots. That induced map is analytic at every coefficient tuple whose roots are pairwise distinct and at each of which φ is analytic.

Read on Sym^g(Σ), φ is a change of holomorphic coordinate on the surface, so this is the analytic ingredient, at multiplicity-free tuples, for the holomorphy of the transition maps of the elementary symmetric atlas of TauCeti/Geometry/Manifold/SymmetricPower.lean: it treats one coordinate patch (TauCeti.Sym.isOpenEmbedding_coeffEquiv_comp_map), and assembling the patches a chart there decomposes a tuple into is not done.