Holomorphic transitions between elementary-symmetric charts

An elementary-symmetric chart on Sym^n X separates a tuple into finitely many blocks lying in disjoint coordinate patches of X, and records each block by the elementary symmetric functions of its points read in the patch coordinate. Two such charts may separate a tuple into blocks in different ways. Where both are defined, a change from one to the other regroups the points: a block of the target chart collects, from every block of the source chart, the points that lie in its patch, applies the change of surface coordinate to them, and takes their elementary symmetric functions.

This file proves that this transition is holomorphic. The analytic input is TauCeti.Sym.analyticAt_sum_map_filter_coeffEquiv_symm: sums of a holomorphic function over the roots of a monic polynomial lying in a region depend analytically on the coefficients, colliding roots included. Applied to the power sums of the points of one target block, and combined with Newton's identities, it shows that each target block of coordinates is analytic in the source coordinates. Repeated points are included throughout. The regularity claims assume that, for every point z of a tuple lying in both chart sources, and for every source patch V i and target patch W j containing z, the change of surface coordinate fun w : ℂ => ψ j ((φ i).symm w) is analytic at φ i z; on a complex curve this holds for any two charts of the atlas.

For background on the symmetric-power setting, see Ozsváth–Szabó, Holomorphic disks and topological invariants for closed three-manifolds (arXiv:math/0101206), §2.2. The chart construction and transition calculation in this file are developed here, rather than attributed to that section.

Main declarations

• TauCeti.symOpenPartialHomeomorph_transition_apply: for two charts using the same block partition, the transition is the blockwise change of surface coordinate on elementary symmetric coordinates.
• TauCeti.analyticAt_symOpenPartialHomeomorph_transition: the transition between two elementary-symmetric charts, with arbitrary block partitions, is analytic at the coordinates of every tuple lying in both sources.
• TauCeti.contDiffOn_symOpenPartialHomeomorph_trans: the transition partial homeomorphism is analytic on its source, in the form used by Mathlib's manifold atlas API.

theorem TauCeti.symOpenPartialHomeomorph_transition_apply {α : Type u_1} [TopologicalSpace α] {ι : Type u_2} [Fintype ι] {n : ℕ} (φ ψ : ι → OpenPartialHomeomorph α ℂ) (V : ι → Set α) (m : ι → ℕ) (hm : ∑ i : ι, m i = n) (hVo : ∀ (i : ι), IsOpen (V i)) (hVsubφ : ∀ (i : ι), V i ⊆ (φ i).source) (hVsubψ : ∀ (i : ι), V i ⊆ (ψ i).source) (hVdisj : Pairwise (Function.onFun Disjoint V)) (e e' : (i : ι) × Fin (m i) ≃ Fin n) (hp : Nonempty ((i : ι) → Sym (↑(V i)) (m i))) (c : Fin n → ℂ) (hc : c ∈ (symOpenPartialHomeomorph φ V m hm hVo hVsubφ hVdisj e hp).target) : ((piSigmaConstHomeomorph ℂ e') fun (i : ι) => (Sym.coeffEquiv ℂ (m i)) (Sym.map (fun (w : ℂ) => ↑(ψ i) (↑(φ i).symm w)) ((Sym.coeffEquiv ℂ (m i)).symm ((piSigmaConstHomeomorph ℂ e).symm c i)))) = ↑(symOpenPartialHomeomorph ψ V m hm hVo hVsubψ hVdisj e' hp) (↑(symOpenPartialHomeomorph φ V m hm hVo hVsubφ hVdisj e hp).symm c)

The coefficient expression is the same-partition chart transition on the source target.

theorem TauCeti.analyticAt_symOpenPartialHomeomorph_transition {α : Type u_1} [TopologicalSpace α] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] {n : ℕ} (φ : ι → OpenPartialHomeomorph α ℂ) (ψ : κ → OpenPartialHomeomorph α ℂ) (V : ι → Set α) (m : ι → ℕ) (hm : ∑ i : ι, m i = n) (W : κ → Set α) (p : κ → ℕ) (hp : ∑ j : κ, p j = n) (hVo : ∀ (i : ι), IsOpen (V i)) (hVsub : ∀ (i : ι), V i ⊆ (φ i).source) (hVdisj : Pairwise (Function.onFun Disjoint V)) (hWo : ∀ (j : κ), IsOpen (W j)) (hWsub : ∀ (j : κ), W j ⊆ (ψ j).source) (hWdisj : Pairwise (Function.onFun Disjoint W)) (e : (i : ι) × Fin (m i) ≃ Fin n) (e' : (j : κ) × Fin (p j) ≃ Fin n) (hq : Nonempty ((i : ι) → Sym (↑(V i)) (m i))) (hr : Nonempty ((j : κ) → Sym (↑(W j)) (p j))) {t : Sym α n} (ht : t ∈ (symOpenPartialHomeomorph φ V m hm hVo hVsub hVdisj e hq).source) (ht' : t ∈ (symOpenPartialHomeomorph ψ W p hp hWo hWsub hWdisj e' hr).source) (hφψ : ∀ (i : ι) (j : κ), ∀ z ∈ V i ∩ W j, z ∈ t → AnalyticAt ℂ (fun (w : ℂ) => ↑(ψ j) (↑(φ i).symm w)) (↑(φ i) z)) : AnalyticAt ℂ (fun (c : Fin n → ℂ) => ↑(symOpenPartialHomeomorph ψ W p hp hWo hWsub hWdisj e' hr) (↑(symOpenPartialHomeomorph φ V m hm hVo hVsub hVdisj e hq).symm c)) (↑(symOpenPartialHomeomorph φ V m hm hVo hVsub hVdisj e hq) t)

The transition between two elementary-symmetric charts is analytic at every tuple lying in both sources. The charts are built from disjoint patch families V, W with multiplicities m, p, surface coordinates φ, ψ and regrouping bijections e, e', which may all differ. Repeated points in the tuple t are allowed. The hypothesis hφψ requires the change of surface coordinate ψ j ∘ (φ i).symm to be analytic at φ i z for every point z of t lying in V i ∩ W j.

theorem TauCeti.contDiffOn_symOpenPartialHomeomorph_trans {α : Type u_1} [TopologicalSpace α] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] {n : ℕ} (φ : ι → OpenPartialHomeomorph α ℂ) (ψ : κ → OpenPartialHomeomorph α ℂ) (V : ι → Set α) (m : ι → ℕ) (hm : ∑ i : ι, m i = n) (W : κ → Set α) (p : κ → ℕ) (hp : ∑ j : κ, p j = n) (hVo : ∀ (i : ι), IsOpen (V i)) (hVsub : ∀ (i : ι), V i ⊆ (φ i).source) (hVdisj : Pairwise (Function.onFun Disjoint V)) (hWo : ∀ (j : κ), IsOpen (W j)) (hWsub : ∀ (j : κ), W j ⊆ (ψ j).source) (hWdisj : Pairwise (Function.onFun Disjoint W)) (e : (i : ι) × Fin (m i) ≃ Fin n) (e' : (j : κ) × Fin (p j) ≃ Fin n) (hq : Nonempty ((i : ι) → Sym (↑(V i)) (m i))) (hr : Nonempty ((j : κ) → Sym (↑(W j)) (p j))) (hφψ : ∀ t ∈ (symOpenPartialHomeomorph φ V m hm hVo hVsub hVdisj e hq).source ∩ (symOpenPartialHomeomorph ψ W p hp hWo hWsub hWdisj e' hr).source, ∀ (i : ι) (j : κ), ∀ z ∈ V i ∩ W j, z ∈ t → AnalyticAt ℂ (fun (w : ℂ) => ↑(ψ j) (↑(φ i).symm w)) (↑(φ i) z)) : ContDiffOn ℂ ⊤ (↑((symOpenPartialHomeomorph φ V m hm hVo hVsub hVdisj e hq).symm.trans (symOpenPartialHomeomorph ψ W p hp hWo hWsub hWdisj e' hr))) ((symOpenPartialHomeomorph φ V m hm hVo hVsub hVdisj e hq).symm.trans (symOpenPartialHomeomorph ψ W p hp hWo hWsub hWdisj e' hr)).source

The transition partial homeomorphism between two elementary-symmetric charts is analytic on its source. This is the source-and-target form consumed by isManifold_of_contDiffOn. Here hφψ requires the change of surface coordinate ψ j ∘ (φ i).symm to be analytic at φ i z for every point z of V i ∩ W j belonging to some tuple t in both chart sources; no condition is imposed at points of V i ∩ W j outside every such tuple.