Analytic coordinate changes for families of simple roots

An elementary-symmetric chart on a symmetric power of a surface separates a tuple into the 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 proves that changing the surface coordinate is analytic on one block when its roots are distinct. 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 assembled statement is TauCeti.Sym.analyticAt_piSigmaConstHomeomorph_coeffEquiv_map_coeffEquiv_symm.

Thus the blockwise coordinate-change expression used by elementary-symmetric charts is analytic at tuples that are multiplicity-free inside every block. At colliding tuples, the polynomial case is TauCeti.Sym.analyticOnNhd_coeffEquiv_map_eval_coeffEquiv_symm in TauCeti/Analysis/Polynomial/SymmetricPower.lean. The complex colliding-point case, including general holomorphic coordinate changes, is proved separately in TauCeti/Analysis/Polynomial/RootSum/Family.lean.

This is the multiplicity-free assembly step in Lane F4.1 of the analytic Heegaard Floer roadmap, whose first target is the smooth complex structure on Sym^g(Σ) from elementary symmetric functions. The organization follows Ozsváth--Szabó, arXiv:math/0101206, Section 2.1.

theorem TauCeti.Sym.analyticAt_piSigmaConstHomeomorph_coeffEquiv_map_coeffEquiv_symm {𝕜 : Type u_1} [RCLike 𝕜] [IsAlgClosed 𝕜] {ι : Type u_2} [Finite ι] {m : ι → ℕ} {n : ℕ} (e e' : (i : ι) × Fin (m i) ≃ Fin n) {φ : ι → 𝕜 → 𝕜} {c₀ z : (i : ι) → Fin (m i) → 𝕜} (hz : ∀ (i : ι), Function.Injective (z i)) (hc₀ : ∀ (i : ι), (coeffEquiv 𝕜 (m i)).symm (c₀ i) = ofFn (z i)) (hφ : ∀ (i : ι) (j : Fin (m i)), AnalyticAt 𝕜 (φ i) (z i j)) : 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 tuple whose roots are pairwise distinct inside each block.