The symmetric power of a complex curve is a complex analytic manifold

Let α be a Hausdorff one-dimensional complex manifold, a Riemann surface in the case of interest. Its n-th symmetric power Sym α n carries the elementary-symmetric charted structure TauCeti.symChartedSpace, modelled on Fin n → ℂ. Its charts are the explicit charts TauCeti.symOpenPartialHomeomorph, built from disjoint coordinate patches of α around the distinct points of a tuple, and the transition between any two of them is analytic on its source (TauCeti.contDiffOn_symOpenPartialHomeomorph_trans), because the changes of coordinate on α are (TauCeti.analyticAt_symm_trans). Hence Sym α n is an analytic manifold: this is the complex structure of Sym^g(Σ) in Ozsváth–Szabó, Holomorphic disks and topological invariants for closed three-manifolds (arXiv:math/0101206), §2.2, given there by the observation that the elementary symmetric functions of local coordinates are holomorphic coordinates on the symmetric power.

The statement is phrased with the explicit charted structure TauCeti.symChartedSpace, which is deliberately not an instance; see its docstring.

Main declarations

• TauCeti.isManifold_symChartedSpace: the symmetric power of a Hausdorff complex curve is a complex analytic manifold for its elementary-symmetric charts.
• TauCeti.analyticAt_symChartAt_symm_trans: the transition between two chosen elementary-symmetric charts is analytic, so that analyticity of a map into the symmetric power can be checked in any of them (TauCeti.analyticAt_symChartAt_comp_of_analyticAt).

theorem TauCeti.isManifold_symChartedSpace {α : Type u_1} [TopologicalSpace α] [T2Space α] [ChartedSpace ℂ α] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 α] {n : ℕ} : IsManifold (modelWithCornersSelf ℂ (Fin n → ℂ)) ⊤ (Sym α n)

The symmetric power of a complex curve is a complex analytic manifold. For a Hausdorff one-dimensional complex manifold α, the elementary-symmetric charts of Sym α n have analytic transition maps, so TauCeti.symChartedSpace makes Sym α n an analytic manifold modelled on Fin n → ℂ.

theorem TauCeti.analyticAt_symChartAt_symm_trans {α : Type u_1} [TopologicalSpace α] [T2Space α] [ChartedSpace ℂ α] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 α] {n : ℕ} {s s' x : Sym α n} (hs : x ∈ (symChartAt s).source) (hs' : x ∈ (symChartAt s').source) : AnalyticAt ℂ (fun (c : Fin n → ℂ) => ↑(symChartAt s') (↑(symChartAt s).symm c)) (↑(symChartAt s) x)

The transition between two chosen elementary-symmetric charts is analytic. For tuples s, s' of a complex curve, the change of coordinates from symChartAt s to symChartAt s' is analytic at the coordinates of every tuple lying in both chart sources.

theorem TauCeti.analyticAt_symChartAt_comp_of_analyticAt {α : Type u_1} [TopologicalSpace α] [T2Space α] [ChartedSpace ℂ α] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 α] {n : ℕ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → Sym α n} {w : E} {s s' : Sym α n} (hf : ContinuousAt f w) (hs : f w ∈ (symChartAt s).source) (hs' : f w ∈ (symChartAt s').source) (ha : AnalyticAt ℂ (fun (t : E) => ↑(symChartAt s) (f t)) w) : AnalyticAt ℂ (fun (t : E) => ↑(symChartAt s') (f t)) w

Analyticity of a map into a symmetric power does not depend on the elementary-symmetric chart. If f is continuous at w and its coordinates in the chosen chart at s are analytic at w, then so are its coordinates in the chosen chart at any s' whose source contains f w.