The unordered tuples through a fixed point

For a point a of a topological space α, adjoining a is a map Sym α n → Sym α (n + 1) whose range is the set TauCeti.Sym.basepointDivisor a of unordered tuples containing a (TauCeti.Sym.range_cons). This file shows that the map is continuous and, as soon as the points of α are closed, a closed embedding. The unordered (n + 1)-tuples through a therefore form a closed subset of the symmetric power, homeomorphic to Sym α n.

For a surface Σ with a basepoint z this subset of Sym^g(Σ) is the divisor V_z = {z} × Sym^{g-1}(Σ) of Ozsváth--Szabó, through which the basepoint enters Heegaard Floer homology: the multiplicity n_z(φ) of a Whitney disk φ is its intersection number with V_z. That V_z misses the tori of a Heegaard diagram when z lies off the attaching curves is TauCeti.Sym.disjoint_basepointDivisor_pi. It is cut out by a single affine equation in every elementary symmetric chart it meets, as shown by TauCeti.exists_continuousLinearMap_ne_zero_mem_iff_symChartAt.

Main declarations

• TauCeti.Sym.continuous_cons: adjoining a point is continuous.
• TauCeti.Sym.isClosedMap_cons and TauCeti.Sym.isClosedEmbedding_cons: in a T₁ space it is a closed map, hence a closed embedding.
• TauCeti.Sym.isClosed_basepointDivisor: in a T₁ space the unordered tuples through a point form a closed set.

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 and §2.4.

theorem TauCeti.Sym.continuous_cons {α : Type u_1} [TopologicalSpace α] {n : ℕ} (a : α) : Continuous (Sym.cons a)

Adjoining a point to an unordered tuple is continuous.

theorem TauCeti.Sym.isClosedMap_cons {α : Type u_1} [TopologicalSpace α] {n : ℕ} [T1Space α] (a : α) : IsClosedMap (Sym.cons a)

In a space whose points are closed, adjoining a point to an unordered tuple is a closed map.

theorem TauCeti.Sym.isClosedEmbedding_cons {α : Type u_1} [TopologicalSpace α] {n : ℕ} [T1Space α] (a : α) : Topology.IsClosedEmbedding (Sym.cons a)

In a space whose points are closed, adjoining a point is a closed embedding of Sym α n into Sym α (n + 1), with range the unordered tuples through that point (TauCeti.Sym.range_cons).

theorem TauCeti.Sym.isClosed_basepointDivisor {α : Type u_1} [TopologicalSpace α] {n : ℕ} [T1Space α] (a : α) : IsClosed (basepointDivisor a)

In a space whose points are closed, the unordered tuples through a given point form a closed subset of the symmetric power.