The symmetric power is locally a product, along a family

This file presents Sym α n locally as a product over a finite family U : ι → Set α of pairwise disjoint open sets, and then produces the family that a given tuple needs: in a Hausdorff space the distinct points of an unordered n-tuple have pairwise disjoint open neighbourhoods, as small as one likes, and the tuple is a concatenation along them, with the multiplicities as the degrees.

Together these two statements are what charts the symmetric power of a surface. A tuple with distinct points z₁, …, z_k of multiplicities n₁, …, n_k has a neighbourhood in Sym^n(Σ) homeomorphic to Sym^{n₁}(U₁) × ⋯ × Sym^{n_k}(U_k) for disjoint coordinate discs U_j ∋ z_j, and each factor is an open subspace of affine space by TauCeti.Sym.isOpenEmbedding_coeffEquiv_comp_map. Lane F4.1 of the analytic Heegaard Floer roadmap needs exactly this to give Sym^g(Σ) its complex structure, after Ozsváth--Szabó (arXiv:math/0101206, §2.1); the charted structure itself is in TauCeti/Geometry/Manifold/SymmetricPower.lean.

The open-embedding proof reduces to ordered tuples: TauCeti.Sym.ofFn is an open quotient map on each member of the family, hence so is the product of those maps, and read on ordered tuples the concatenation is the regrouping of n entries along a bijection (Σ i, Fin (m i)) ≃ Fin n, which is a homeomorphism followed by the (open) inclusions of the members of the family.

Main declarations

• TauCeti.Sym.isOpenEmbedding_sumSubtype: for a pairwise disjoint family of open sets, concatenation identifies the product of the symmetric powers of the members with an open subspace of Sym α n.
• TauCeti.exists_mem_range_sumSubtype_of_t2: in a Hausdorff space, every unordered tuple lies in the range of such a concatenation, along a family of arbitrarily small neighbourhoods of its distinct points indexed by those points.

Concatenation along a pairwise disjoint family of open sets

theorem TauCeti.Sym.continuous_sumSubtype {α : Type u_1} [TopologicalSpace α] {ι : Type u_2} [Fintype ι] {U : ι → Set α} {m : ι → ℕ} {n : ℕ} (hn : ∑ i : ι, m i = n) : Continuous (sumSubtype U m hn)

Concatenating unordered tuples of points of the members of a family is continuous.

theorem TauCeti.Sym.isOpenMap_sumSubtype {α : Type u_1} [TopologicalSpace α] {ι : Type u_2} [Fintype ι] {U : ι → Set α} {m : ι → ℕ} {n : ℕ} (hU : ∀ (i : ι), IsOpen (U i)) (hn : ∑ i : ι, m i = n) : IsOpenMap (sumSubtype U m hn)

For a family of open sets, concatenating unordered tuples of points of its members is an open map.

theorem TauCeti.Sym.isOpenEmbedding_sumSubtype {α : Type u_1} [TopologicalSpace α] {ι : Type u_2} [Fintype ι] {U : ι → Set α} {m : ι → ℕ} {n : ℕ} (hU : ∀ (i : ι), IsOpen (U i)) (h : Pairwise (Function.onFun Disjoint U)) (hn : ∑ i : ι, m i = n) : Topology.IsOpenEmbedding (sumSubtype U m hn)

The symmetric power is locally a product. For a pairwise disjoint family of open sets, concatenation identifies the product of the symmetric powers of its members with an open subspace of Sym α n, namely the unordered tuples supported in the union of the family with exactly m i of their points in U i (TauCeti.Sym.mem_range_sumSubtype).

The family attached to a tuple in a Hausdorff space

theorem TauCeti.exists_mem_range_sumSubtype_of_t2 {α : Type u_1} [TopologicalSpace α] [T2Space α] [DecidableEq α] {n : ℕ} (w : Sym α n) (W : α → Set α) (hWo : ∀ a ∈ w, IsOpen (W a)) (hWm : ∀ a ∈ w, a ∈ W a) : ∃ (V : ↥(↑w).toFinset → Set α), (∀ (i : ↥(↑w).toFinset), IsOpen (V i)) ∧ (∀ (i : ↥(↑w).toFinset), ↑i ∈ V i) ∧ (∀ (i : ↥(↑w).toFinset), V i ⊆ W ↑i) ∧ Pairwise (Function.onFun Disjoint V) ∧ ∃ (hm : ∑ i : ↥(↑w).toFinset, Multiset.count ↑i ↑w = n), w ∈ Set.range (Sym.sumSubtype V (fun (i : ↥(↑w).toFinset) => Multiset.count ↑i ↑w) hm)

Every unordered tuple in a Hausdorff space is a concatenation along a pairwise disjoint family of arbitrarily small open sets, one member of the family for each of its distinct points and that point's multiplicity as the degree.

This is the separation step that turns TauCeti.Sym.isOpenEmbedding_sumSubtype into an atlas: the open sets V i may be taken inside any prescribed open neighbourhoods W a ∋ a, so in a space charted by a fixed model they may be taken inside coordinate patches.