Documentation

TauCeti.Topology.Sym.Basic

The symmetric power of a topological space #

The n-th symmetric power Sym α n of a type is the type of unordered n-tuples of points of α. It is the quotient of the space Fin n → α of ordered tuples by the permutation action, and this file gives it the corresponding quotient topology, together with the API that a quotient topology is used through: the quotient map is continuous, and a map out of Sym α n is continuous exactly when its composition with the quotient map is.

The quotient map is TauCeti.Sym.ofFn of TauCeti/Data/Sym/Basic.lean, which reads an ordered tuple as an unordered one; the Fin n → α form is the one that carries a product topology, so it is what the quotient topology is defined against. Its surjectivity and the description TauCeti.Sym.ofFn_eq_ofFn_iff of its fibres as the orbits of the permutation action are the two facts about it used below.

Main declarations #

Lane F4.1 of the analytic Heegaard Floer roadmap needs Sym^g(Σ) as a space before it can be given a complex structure; this file supplies the underlying topology, and TauCeti/Analysis/Polynomial/SymmetricPower.lean identifies it, over an algebraically closed normed field, with affine space through the elementary symmetric functions.

The fibres of the quotient map #

source
theorem TauCeti.Sym.preimage_image_ofFn {α : Type u_1} {n : ℕ} (s : Set (Fin n → α)) :
ofFn ⁻¹' ofFn '' s = ⋃ (σ : Equiv.Perm (Fin n)), (fun (x : Fin n → α) => x ∘ ⇑σ) ⁻¹' s

The saturation of a set of ordered tuples under ofFn is the union of its reindexings.

The quotient topology #

source
@[instance_reducible]
instance TauCeti.Sym.instTopologicalSpace {α : Type u_1} {n : ℕ} [TopologicalSpace α] :
TopologicalSpace (Sym α n)

The n-th symmetric power of a topological space carries the quotient topology of the permutation action on ordered n-tuples, presented as the topology coinduced along TauCeti.Sym.ofFn.

Equations
source
theorem TauCeti.Sym.continuous_ofFn {α : Type u_1} {n : ℕ} [TopologicalSpace α] :
Continuous ofFn

The quotient map onto the symmetric power is continuous.

source
theorem TauCeti.Sym.isQuotientMap_ofFn {α : Type u_1} {n : ℕ} [TopologicalSpace α] :
Topology.IsQuotientMap ofFn

ofFn presents Sym α n as a topological quotient of Fin n → α.

source
theorem TauCeti.Sym.continuous_iff_comp_ofFn {α : Type u_1} {β : Type u_2} {n : ℕ} [TopologicalSpace α] [TopologicalSpace β] {g : Sym α n → β} :
Continuous g ↔ Continuous (g ∘ ofFn)

A map out of a symmetric power is continuous exactly when the associated map on ordered tuples is; this is the universal property of the quotient topology.

source
theorem TauCeti.Sym.isOpenMap_ofFn {α : Type u_1} {n : ℕ} [TopologicalSpace α] :
IsOpenMap ofFn

The quotient map onto the symmetric power is open: the saturation of an open set is the union of its reindexings, each of them open.

source
theorem TauCeti.Sym.isClosedMap_ofFn {α : Type u_1} {n : ℕ} [TopologicalSpace α] :
IsClosedMap ofFn

The quotient map onto the symmetric power is closed: the saturation of a closed set is the union of its reindexings, a finite union of closed sets.

source
theorem TauCeti.Sym.isOpenQuotientMap_ofFn {α : Type u_1} {n : ℕ} [TopologicalSpace α] :
IsOpenQuotientMap ofFn

The quotient map onto the symmetric power is an open quotient map.

Functoriality #

source
theorem TauCeti.Sym.continuous_map {α : Type u_1} {β : Type u_2} {n : ℕ} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) :
Continuous (Sym.map f)

The symmetric power of a continuous map is continuous.

source
theorem TauCeti.Sym.isOpenMap_map {α : Type u_1} {β : Type u_2} {n : ℕ} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : IsOpenMap f) :
IsOpenMap (Sym.map f)

The symmetric power of an open map is open.

source
theorem TauCeti.Sym.isOpenEmbedding_map {α : Type u_1} {β : Type u_2} {n : ℕ} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Topology.IsOpenEmbedding f) :
Topology.IsOpenEmbedding (Sym.map f)

The symmetric power of an open embedding is an open embedding: the n-th symmetric power of an open subspace is an open subspace of the n-th symmetric power.

source
theorem TauCeti.Sym.isOpen_setOf_forall_mem {α : Type u_1} {n : ℕ} [TopologicalSpace α] {V : Set α} (hV : IsOpen V) :
IsOpen {s : Sym α n | ∀ a ∈ s, a ∈ V}

The unordered tuples all of whose points lie in an open set form an open subset of the symmetric power: the range of the symmetric power of the inclusion of that open set.

source
theorem TauCeti.Sym.continuous_append {α : Type u_1} {m n : ℕ} [TopologicalSpace α] :
Continuous fun (p : Sym α n × Sym α m) => p.1.append p.2

Concatenation of two symmetric-power points is continuous.

source
theorem TauCeti.Sym.isOpenMap_append {α : Type u_1} {m n : ℕ} [TopologicalSpace α] :
IsOpenMap fun (p : Sym α n × Sym α m) => p.1.append p.2

Concatenation of two symmetric-power points is an open map.

Separation and compactness #

source
instance TauCeti.Sym.instCompactSpace {α : Type u_1} {n : ℕ} [TopologicalSpace α] [CompactSpace α] :
CompactSpace (Sym α n)

The symmetric power of a compact space is compact, being a continuous image of a finite power of that space.

source
instance TauCeti.Sym.instT2Space {α : Type u_1} {n : ℕ} [TopologicalSpace α] [T2Space α] :
T2Space (Sym α n)

The symmetric power of a Hausdorff space is Hausdorff: ofFn is an open quotient map, and the relation it induces is the finite union, over permutations, of the graphs of the reindexing maps, hence closed.