Disjoint open embeddings into a symmetric power

Given open embeddings with pairwise disjoint ranges, ordered tuples mapped pointwise through those embeddings embed openly as unordered tuples. In particular, given pairwise disjoint open neighbourhoods U i of n distinct points, their product is an open subspace of Sym α n; obtaining such neighbourhoods in a Hausdorff space is a separate step. The proof comes from TauCeti.Sym.ofFn being continuous and open together with IsOpenEmbedding.piMap.

Splitting over the distinct points of a tuple, with the multiplicities as the degrees, is how the symmetric power of a surface is charted: a neighbourhood of a tuple with distinct points z₁, …, z_k of multiplicities n₁, …, n_k is a product of the symmetric powers Sym^{n_j} of disjoint coordinate discs, each of which 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 coefficient homeomorphism is in TauCeti/Analysis/Polynomial/SymmetricPower.lean, while the charts and charted structure are in TauCeti/Geometry/Manifold/SymmetricPower.lean. Family-level concatenation along disjoint open sets, and the Hausdorff separation producing the family that a given tuple needs, are in TauCeti/Topology/Sym/Family.lean.

Main declaration

• TauCeti.Sym.isOpenEmbedding_ofFn_map: open embeddings with pairwise disjoint ranges induce an open embedding from their product into the symmetric power.

Tuples mapped into pairwise disjoint open ranges

theorem TauCeti.Sym.isOpenEmbedding_ofFn_map {α : Type u_1} [TopologicalSpace α] {n : ℕ} {X : Fin n → Type u_2} [(i : Fin n) → TopologicalSpace (X i)] (f : (i : Fin n) → X i → α) (hf : ∀ (i : Fin n), Topology.IsOpenEmbedding (f i)) (h : Pairwise (Function.onFun Disjoint fun (i : Fin n) => Set.range (f i))) : Topology.IsOpenEmbedding fun (x : (i : Fin n) → X i) => ofFn fun (i : Fin n) => f i (x i)

Away from the diagonal the symmetric power is a product. Open embeddings with pairwise disjoint ranges induce an open embedding from their product into the symmetric power. Applied to subtype inclusions, this says conditionally that given pairwise disjoint open neighbourhoods U i of n distinct points, their product is an open subspace of Sym α n; constructing such a family in a Hausdorff space is a separate step.