Analytic coordinate changes across families of root blocks

An elementary-symmetric chart on a symmetric power of a complex surface separates a tuple into points lying in finitely many disjoint coordinate patches. If the multiplicity in patch i is m i, its coordinates form a block Fin (m i) → ℂ; a bijection (Σ i, Fin (m i)) ≃ Fin n regroups those blocks into the model space Fin n → ℂ.

TauCeti.Sym.analyticAt_coeffEquiv_map_coeffEquiv_symm_of_analyticAt proves that changing a holomorphic surface coordinate is analytic on one block, including where roots collide. This file applies that result to a finite family of blocks and then conjugates the family by the possibly different source and target regroupings. The multiplicity-free RCLike version remains in TauCeti/Analysis/Polynomial/SimpleRoots/Family.lean; the assembled complex statement is TauCeti.Sym.analyticAt_piSigmaConstHomeomorph_coeffEquiv_map_coeffEquiv_symm_of_analyticAt.

Thus the blockwise coordinate-change expression used by elementary-symmetric charts sharing one block partition is analytic at every represented tuple. The transition between charts with arbitrary block partitions is proved directly from the filtered root sums of TauCeti.Sym.analyticAt_sum_map_filter_coeffEquiv_symm in TauCeti/Geometry/Manifold/SymmetricPower/Transition.lean. For background on the symmetric-power setting, see Ozsváth--Szabó, arXiv:math/0101206, Section 2.2. The blockwise analytic statement and proof in this file are developed here, rather than attributed to that section.

theorem TauCeti.Sym.analyticAt_piSigmaConstHomeomorph_coeffEquiv_map_coeffEquiv_symm_of_analyticAt {ι : Type u_1} [Finite ι] {m : ι → ℕ} {n : ℕ} (e e' : (i : ι) × Fin (m i) ≃ Fin n) {φ : ι → ℂ → ℂ} {c₀ : (i : ι) → Fin (m i) → ℂ} (hφ : ∀ (i : ι), ∀ z ∈ (coeffEquiv ℂ (m i)).symm (c₀ i), AnalyticAt ℂ (φ i) z) : AnalyticAt ℂ (fun (c : Fin n → ℂ) => (piSigmaConstHomeomorph ℂ e') fun (i : ι) => (coeffEquiv ℂ (m i)) (Sym.map (φ i) ((coeffEquiv ℂ (m i)).symm ((piSigmaConstHomeomorph ℂ e).symm c i)))) ((piSigmaConstHomeomorph ℂ e) c₀)

A blockwise elementary-symmetric coordinate change is analytic after regrouping.

The bijections e and e' are the independent choices used to identify the source and target families of coefficient blocks with Fin n → ℂ. The transition first undoes e, changes the underlying coordinate separately on each root block, and then regroups along e'. It is analytic at every represented tuple, including tuples with repeated points.