Orbit spaces of free cellular actions are Hausdorff

Let a group G act on a Hausdorff CW complex E by homeomorphisms, such that each element of G carries every open n-cell onto an open n-cell, and g carries an open cell onto itself only when g = 1. This file proves that the orbit space E / G is Hausdorff.

The orbit space is not Hausdorff for a general free action by homeomorphisms, even when the orbit map is a covering map, so the cellular hypotheses are essential. Nor does a classical CW structure on the orbit space suffice by itself: Mathlib's classical CW complexes need not be Hausdorff.

The proof constructs, for two points x and y in different orbits, a continuous G-invariant function f : E → ℝ with f x = 1 and f y = 0 (TauCeti.exists_invariant_continuousMap_one_zero). It is built skeleton by skeleton. Choose a representative cell in each G-orbit of n-cells. On a representative, extend the function already built on its boundary sphere over the closed ball by the Tietze extension theorem, prescribing the value 1 at the (at most one) interior point of the orbit of x and 0 at that of y. Then transport this extension to the other cells of the orbit by the unique group element carrying the representative to them. The function descends to a continuous function on the orbit space separating the images of x and y.

Main results

• TauCeti.exists_invariant_continuousMap_one_zero: points in different orbits are separated by a continuous G-invariant real function.
• TauCeti.t2Space_orbitRel_quotient: the orbit space MulAction.orbitRel.Quotient G E is Hausdorff.
• IsQuotientCoveringMap.t2Space_of_cwComplex: the base of the quotient covering map of such an action is Hausdorff.

References

• T. tom Dieck, Transformation Groups, de Gruyter, 1987, Section II.1 (free G-CW complexes and their orbit spaces).
• A. Hatcher, Algebraic Topology, Appendix, Proposition A.3 (CW complexes are normal, by extending functions cell by cell).

def TauCeti.cellOrbitSetoid {E : Type u} [TopologicalSpace E] [Topology.CWComplex Set.univ] (G : Type u_1) [Group G] [MulAction G E] (n : ℕ) : Setoid (Topology.RelCWComplex.cell Set.univ n)

Two n-cells are related when a group element carries the open cell of one onto the open cell of the other.

noncomputable def TauCeti.cellRep {E : Type u} [TopologicalSpace E] [Topology.CWComplex Set.univ] (G : Type u_1) [Group G] [MulAction G E] {n : ℕ} (j : Topology.RelCWComplex.cell Set.univ n) : Topology.RelCWComplex.cell Set.univ n

The chosen representative of the orbit of an n-cell.

theorem TauCeti.exists_smul_openCell_cellRep {E : Type u} [TopologicalSpace E] [Topology.CWComplex Set.univ] {G : Type u_1} [Group G] [MulAction G E] {n : ℕ} (j : Topology.RelCWComplex.cell Set.univ n) : ∃ (g : G), g • Topology.RelCWComplex.openCell n (cellRep G j) = Topology.RelCWComplex.openCell n j

noncomputable def TauCeti.cellElt {E : Type u} [TopologicalSpace E] [Topology.CWComplex Set.univ] (G : Type u_1) [Group G] [MulAction G E] {n : ℕ} (j : Topology.RelCWComplex.cell Set.univ n) : G

A group element carrying the representative of the orbit of j onto j.

theorem TauCeti.cellElt_smul_openCell {E : Type u} [TopologicalSpace E] [Topology.CWComplex Set.univ] {G : Type u_1} [Group G] [MulAction G E] {n : ℕ} (j : Topology.RelCWComplex.cell Set.univ n) : cellElt G j • Topology.RelCWComplex.openCell n (cellRep G j) = Topology.RelCWComplex.openCell n j

theorem TauCeti.cellRep_eq_of_smul_openCell {E : Type u} [TopologicalSpace E] [Topology.CWComplex Set.univ] {G : Type u_1} [Group G] [MulAction G E] {n : ℕ} {g : G} {i j : Topology.RelCWComplex.cell Set.univ n} (h : g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n j) : cellRep G i = cellRep G j

theorem TauCeti.eq_cellElt_of_smul_openCell {E : Type u} [TopologicalSpace E] [Topology.CWComplex Set.univ] {G : Type u_1} [Group G] [MulAction G E] (hfree : ∀ (g : G) (n : ℕ) (i : Topology.RelCWComplex.cell Set.univ n), g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n i → g = 1) {n : ℕ} {g : G} {j : Topology.RelCWComplex.cell Set.univ n} (h : g • Topology.RelCWComplex.openCell n (cellRep G j) = Topology.RelCWComplex.openCell n j) : g = cellElt G j

The element carrying the representative onto a cell is the only one doing so.

theorem TauCeti.exists_cellElt_smul_map {E : Type u} [TopologicalSpace E] [Topology.CWComplex Set.univ] {G : Type u_1} [Group G] [MulAction G E] {n : ℕ} {z : E} {j : Topology.RelCWComplex.cell Set.univ n} (hz : z ∈ Topology.RelCWComplex.openCell n j) : ∃ (u : Fin n → ℝ), ‖u‖ < 1 ∧ cellElt G j • ↑(Topology.RelCWComplex.map n (cellRep G j)) u = z

A point of an open n-cell is the translate, by the chosen element, of a point of the open cell of the representative.

theorem TauCeti.exists_invariant_continuousMap_one_zero {E : Type u} [TopologicalSpace E] [Topology.CWComplex Set.univ] {G : Type u_1} [Group G] [MulAction G E] (hcell : ∀ (g : G) (n : ℕ) (i : Topology.RelCWComplex.cell Set.univ n), ∃ (j : Topology.RelCWComplex.cell Set.univ n), g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n j) (hfree : ∀ (g : G) (n : ℕ) (i : Topology.RelCWComplex.cell Set.univ n), g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n i → g = 1) [T2Space E] {x y : E} [ContinuousConstSMul G E] (hxy : y ∉ MulAction.orbit G x) : ∃ (f : C(E, ℝ)), (∀ (g : G) (z : E), f (g • z) = f z) ∧ f x = 1 ∧ f y = 0

Invariant separating functions. Let G act on a Hausdorff CW complex E by homeomorphisms so that every element carries each open n-cell onto an open n-cell, and only 1 carries an open cell onto itself. Then two points x and y in different orbits are separated by a continuous G-invariant function f : E → ℝ with f x = 1 and f y = 0.

theorem TauCeti.t2Space_orbitRel_quotient {E : Type u} [TopologicalSpace E] [Topology.CWComplex Set.univ] {G : Type u_1} [Group G] [MulAction G E] (hcell : ∀ (g : G) (n : ℕ) (i : Topology.RelCWComplex.cell Set.univ n), ∃ (j : Topology.RelCWComplex.cell Set.univ n), g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n j) (hfree : ∀ (g : G) (n : ℕ) (i : Topology.RelCWComplex.cell Set.univ n), g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n i → g = 1) [T2Space E] [ContinuousConstSMul G E] : T2Space (MulAction.orbitRel.Quotient G E)

The orbit space of a free cellular action is Hausdorff. Let G act on a Hausdorff CW complex E by homeomorphisms so that every element carries each open n-cell onto an open n-cell, and only 1 carries an open cell onto itself. Then the orbit space is Hausdorff.

theorem IsQuotientCoveringMap.t2Space_of_cwComplex {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [T2Space E] [Topology.CWComplex Set.univ] [TopologicalSpace B] {G : Type u_3} [Group G] [MulAction G E] {p : E → B} (hp : IsQuotientCoveringMap p G) (hcell : ∀ (g : G) (n : ℕ) (i : Topology.RelCWComplex.cell Set.univ n), ∃ (j : Topology.RelCWComplex.cell Set.univ n), g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n j) (hfree : ∀ (g : G) (n : ℕ) (i : Topology.RelCWComplex.cell Set.univ n), g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n i → g = 1) : T2Space B

The base of the quotient covering map of a free cellular action is Hausdorff. Let G act on a Hausdorff CW complex E so that every element carries each open n-cell onto an open n-cell, and only 1 carries an open cell onto itself. If p : E → B is the quotient covering map of the action, then B is Hausdorff.