A charted-space structure on a symmetric power #

If a Hausdorff space α is charted by a proper algebraically closed normed field K — the case of interest being a Riemann surface, charted by ℂ — then its n-th symmetric power Sym α n is charted by Fin n → K. This is the local-coordinate part of the manifold structure on the symmetric power of a Riemann surface used by Ozsváth--Szabó (arXiv:math/0101206, §2.1).

The chart at an unordered tuple s is assembled from three inputs, each already available:

in a Hausdorff space the distinct points z₁, …, z_k of s have pairwise disjoint open neighbourhoods V₁, …, V_k inside prescribed ones — here, inside the coordinate patches (chartAt K z_j).source — and s is the concatenation of unordered tuples of points of the V_j, with multiplicities n₁, …, n_k as the degrees (TauCeti.exists_mem_range_sumSubtype_of_t2);
that concatenation is an open embedding Sym^{n₁}(V₁) × ⋯ × Sym^{n_k}(V_k) ↪ Sym α n (TauCeti.Sym.isOpenEmbedding_sumSubtype);
each factor is an open subspace of affine space, charted by the elementary symmetric functions of its points read in the ambient coordinate (TauCeti.Sym.isOpenEmbedding_coeffEquiv_comp_map), and the factors regroup into Fin n → K because the multiplicities add up to n (TauCeti.piSigmaConstHomeomorph).

The charts so obtained depend on choices — of the separating neighbourhoods, and of the regrouping bijection — so the atlas below is a choice of one chart per point, exactly as much as a charted structure asks for. Over ℂ, the transition between any two of the explicit charts is analytic (TauCeti.contDiffOn_symOpenPartialHomeomorph_trans in TauCeti/Geometry/Manifold/SymmetricPower/Transition.lean), so that the symmetric power of a complex curve is a complex analytic manifold for this charted structure (TauCeti.isManifold_symChartedSpace in TauCeti/Geometry/Manifold/SymmetricPower/Manifold.lean). TauCeti/Geometry/Manifold/SymmetricPower/TotallyReal.lean proves the tangent-space criterion for products of locally parametrized immersed curves, which applies to these tori once their attaching curves are locally parametrized.

Main declarations #

TauCeti.symOpenPartialHomeomorph: an explicit elementary-symmetric chart built from a disjoint family of coordinate patches.
TauCeti.exists_symOpenPartialHomeomorph: every unordered tuple lies in the source of a partial homeomorphism from Sym α n to Fin n → K.
TauCeti.symChartAt: a chosen elementary-symmetric chart around each unordered tuple.
TauCeti.symChartedSpace: a charted-space structure on Sym α n over Fin n → K.
TauCeti.symChartedSpace_chartAt and TauCeti.symChartedSpace_atlas: its preferred charts and atlas.
TauCeti.mem_iff_pow_add_sum_symOpenPartialHomeomorph_mul_pow_eq_zero and TauCeti.exists_continuousLinearMap_ne_zero_mem_iff_symChartAt: the unordered tuples through a fixed point z are cut out by one affine equation, with nonzero linear part, in every chart that they meet. For a basepoint z of a Heegaard surface this is the divisor V_z = {z} × Sym^{g-1}(Σ) of Ozsváth--Szabó, which is therefore an affine hyperplane in elementary symmetric coordinates; its topology is in TauCeti/Topology/Sym/Cons.lean.