The CW structure on the orbit space of a free cellular action #

Let G act on a Hausdorff CW complex E, and let p : E → B be the quotient covering map of the action (IsQuotientCoveringMap p G). Suppose that each element of G carries every open n-cell of E onto an open n-cell, and that G acts freely on the set of cells: g carries an open cell onto itself only when g = 1. Then B is a CW complex (IsQuotientCoveringMap.cwComplexQuotient):

the translation of open cells is an action of G on the n-cells of E (TauCeti.cellMulAction, characterised by TauCeti.smul_openCell), free by hypothesis (TauCeti.isCancelSMul_cell), and the n-cells of B are its orbits (IsQuotientCoveringMap.cellQuotientEquiv);
the characteristic map of an orbit is p ∘ φ for the characteristic map φ of its chosen representative (IsQuotientCoveringMap.map_cellQuotientEquiv_symm);
the covering map carries each open and each closed cell of E onto the open and closed cell of its orbit (IsQuotientCoveringMap.image_openCell and IsQuotientCoveringMap.image_closedCell).

Only the characteristic maps of the representatives are used, and the hypotheses on the action concern open cells rather than characteristic maps: a translation need not carry the characteristic map of a cell to the characteristic map of the translated cell. This is the situation of a group acting by simplicial automorphisms on a realization, whose cells are parametrized through an order on the vertices that the action need not preserve.

The key point is that p restricts to a homeomorphism from each open cell onto its image (IsQuotientCoveringMap.injOn_openCell and IsQuotientCoveringMap.continuousOn_invFunOn_openCell). It is injective there, since a translate of an open cell meeting it is the cell itself, and hence translation by 1. Its inverse is continuous because near a point y of an open n-cell c there is an open set that misses every other closed n-cell and the (n - 1)-skeleton, so a point of the image of c close to p y has exactly one preimage close to y, the one in c, and it is given by a local inverse of p.

The construction does not use that B is Hausdorff; Mathlib's classical CW complexes do not require it.

The action on cells is constructed more generally for a monoid acting on a relative CW complex and carrying each open cell onto an open cell of the same dimension. If its translations are continuous and the ambient space is Hausdorff, they carry the corresponding closed cells onto each other as well.

References #

T. tom Dieck, Transformation Groups, de Gruyter, 1987, Section II.1 (free G-CW complexes and their orbit spaces).
A. Hatcher, Algebraic Topology, Section 1.3 (covering spaces) and the Appendix "Topology of Cell Complexes".

source

Set.InjOn p (Topology.RelCWComplex.openCell n i)

The covering map is injective on every open cell, without any separation assumption on E.

source

ContinuousOn (Function.invFunOn p (Topology.RelCWComplex.openCell n i)) (p '' Topology.RelCWComplex.openCell n i)

The inverse of the restriction of the covering map to an open cell is continuous on the image: together with IsQuotientCoveringMap.injOn_openCell, p maps each open cell homeomorphically onto its image.

source

@[instance_reducible]

noncomputable def IsQuotientCoveringMap.cwComplexQuotient {E : Type u} [TopologicalSpace E] {G : Type u_1} {B : Type u} [TopologicalSpace B] [Topology.CWComplex Set.univ] [Group G] [MulAction G E] [T2Space 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) :

Topology.CWComplex Set.univ

The orbit space of a free cellular action is a CW complex. Let p : E → B be the quotient covering map of an action of G on the Hausdorff CW complex E that carries every open n-cell onto an open n-cell, and carries an open cell onto itself only by 1. Then B is a CW complex whose n-cells are the G-orbits of n-cells of E (IsQuotientCoveringMap.cellQuotientEquiv). The characteristic map of an orbit is p ∘ φ, for φ the characteristic map of the chosen representative of the orbit (IsQuotientCoveringMap.map_cellQuotientEquiv_symm).