The subspace of unordered tuples with one point in each member of a family

TauCeti.Sym.pi A is the set of unordered n-tuples having one point in each member of a family A : Fin n → Set α of subsets. This file gives it its topology, as a subspace of the symmetric power Sym α n: it is closed when the members of the family are, compact when they are, and, for a pairwise disjoint family of compact sets in a Hausdorff space, homeomorphic to the product ∀ i, ↥(A i) of its members.

The case to keep in mind is the torus T_α = α₁ × ⋯ × α_g ⊆ Sym^g(Σ) attached to the g pairwise disjoint attaching circles of a Heegaard diagram on a surface Σ (Ozsváth--Szabó, Holomorphic disks and topological invariants for closed three-manifolds, §2.1). The circles are compact and pairwise disjoint, so T_α really is an embedded g-torus and not merely a continuous image of one. The companion open-range statement, where the members of the family are open rather than compact and the product is an open subspace, is TauCeti.Sym.isOpenEmbedding_ofFn_map.

Main declarations

• TauCeti.Sym.isClosed_pi and TauCeti.Sym.isCompact_pi: the subspace is closed, respectively compact, when the members of the family are.
• TauCeti.Sym.isClosedEmbedding_ofFn_subtypeVal: for a pairwise disjoint family of compact sets in a Hausdorff space, the parametrization by ordered tuples is a closed embedding.
• TauCeti.Sym.piHomeomorph: the resulting homeomorphism with the product of the members.

References

• P. Ozsváth and Z. Szabó, Holomorphic disks and topological invariants for closed three-manifolds, Ann. of Math. 159 (2004), arXiv:math/0101206, §2.1.

theorem TauCeti.Sym.continuous_ofFn_subtypeVal {α : Type u_1} [TopologicalSpace α] {n : ℕ} {A : Fin n → Set α} : Continuous fun (x : (i : Fin n) → ↑(A i)) => ofFn fun (i : Fin n) => ↑(x i)

The parametrization of TauCeti.Sym.pi A by ordered tuples is continuous.

theorem TauCeti.Sym.isClosed_pi {α : Type u_1} [TopologicalSpace α] {n : ℕ} {A : Fin n → Set α} (hA : ∀ (i : Fin n), IsClosed (A i)) : IsClosed (pi A)

The unordered tuples with one point in each member of a family of closed sets form a closed subspace of the symmetric power: the quotient map onto a symmetric power is closed.

theorem TauCeti.Sym.isCompact_pi {α : Type u_1} [TopologicalSpace α] {n : ℕ} {A : Fin n → Set α} (hA : ∀ (i : Fin n), IsCompact (A i)) : IsCompact (pi A)

The unordered tuples with one point in each member of a family of compact sets form a compact subspace of the symmetric power.

theorem TauCeti.Sym.isClosedEmbedding_ofFn_subtypeVal {α : Type u_1} [TopologicalSpace α] {n : ℕ} {A : Fin n → Set α} [T2Space α] (hA : ∀ (i : Fin n), IsCompact (A i)) (h : Pairwise (Function.onFun Disjoint A)) : Topology.IsClosedEmbedding fun (x : (i : Fin n) → ↑(A i)) => ofFn fun (i : Fin n) => ↑(x i)

The tuples with one point in each member of a pairwise disjoint family of compact sets are an embedded product. For the attaching circles of a Heegaard diagram this says that the torus T_α is embedded, and closed, in the symmetric power of the surface.

noncomputable def TauCeti.Sym.piHomeomorph {α : Type u_1} [TopologicalSpace α] {n : ℕ} {A : Fin n → Set α} [T2Space α] (hA : ∀ (i : Fin n), IsCompact (A i)) (h : Pairwise (Function.onFun Disjoint A)) : ((i : Fin n) → ↑(A i)) ≃ₜ ↑(pi A)

The subspace TauCeti.Sym.pi A is the product of the members of the family, for a pairwise disjoint family of compact sets in a Hausdorff space: the topological refinement of TauCeti.Sym.piEquiv.

Equations

• TauCeti.Sym.piHomeomorph hA h = ⋯.toHomeomorph.trans (Homeomorph.setCongr ⋯)

@[simp]

theorem TauCeti.Sym.coe_piHomeomorph_apply {α : Type u_1} [TopologicalSpace α] {n : ℕ} {A : Fin n → Set α} [T2Space α] (hA : ∀ (i : Fin n), IsCompact (A i)) (h : Pairwise (Function.onFun Disjoint A)) (x : (i : Fin n) → ↑(A i)) : ↑((piHomeomorph hA h) x) = ofFn fun (i : Fin n) => ↑(x i)

The homeomorphism underlying TauCeti.Sym.piHomeomorph is the parametrization by ordered tuples.