Actions on the cells of a relative CW complex

A monoid action carrying each open cell onto an open cell of the same dimension induces an action on the cells. Continuous translations also carry closed cells onto the corresponding closed cells when the ambient space is Hausdorff. For a group action, trivial stabilizers of open cells give a free action on cells.

Main results

• TauCeti.cellMulAction: the induced monoid action on cells.
• TauCeti.smul_openCell and TauCeti.smul_mem_openCell_smul: compatibility with open cells.
• TauCeti.smul_closedCell: compatibility with closed cells for continuous translations.
• TauCeti.smul_mem_skeletonLT: a fixed translation carrying each open cell onto an open cell of the same dimension preserves every skeleton of a CW complex.
• TauCeti.smul_closedCell_of_smul_openCell: continuous translations carrying an open cell onto another also carry the corresponding closed cells onto each other.
• TauCeti.isCancelSMul_cell: freeness of the induced group action on cells.
• TauCeti.eq_one_of_mem_openCell_of_smul_mem: only the identity carries a point of an open cell into the same open cell under a free cellular action.

References

• T. tom Dieck, Transformation Groups, de Gruyter, 1987, Section II.1 (free G-CW complexes).
• A. Hatcher, Algebraic Topology, Appendix, Topology of Cell Complexes.

theorem TauCeti.smul_mem_skeletonLT {E : Type u} [TopologicalSpace E] {G : Type u_1} {C : Set E} [Topology.CWComplex C] [T2Space E] [SMul G E] (g : G) (hcell : ∀ (n : ℕ) (i : Topology.RelCWComplex.cell C n), ∃ (j : Topology.RelCWComplex.cell C n), g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n j) {n : ℕ∞} {z : E} (hz : z ∈ ↑(Topology.RelCWComplex.skeletonLT C n)) : g • z ∈ ↑(Topology.RelCWComplex.skeletonLT C n)

Translation by a fixed element carrying each open cell onto an open cell of the same dimension preserves every skeleton of a CW complex.

theorem TauCeti.smul_closedCell_of_smul_openCell {E : Type u} [TopologicalSpace E] {G : Type u_1} {C D : Set E} [Topology.RelCWComplex C D] [T2Space E] [SMul G E] [ContinuousConstSMul G E] {n : ℕ} {g : G} {i j : Topology.RelCWComplex.cell C n} (h : g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n j) : g • Topology.RelCWComplex.closedCell n i = Topology.RelCWComplex.closedCell n j

A continuous translation carrying an open cell onto another also carries the corresponding closed cell onto the other closed cell.

@[implicit_reducible]

noncomputable def TauCeti.cellMulAction {E : Type u} [TopologicalSpace E] {G : Type u_1} {C D : Set E} [Topology.RelCWComplex C D] [Monoid G] [MulAction G E] (hcell : ∀ (g : G) (n : ℕ) (i : Topology.RelCWComplex.cell C n), ∃ (j : Topology.RelCWComplex.cell C n), g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n j) (n : ℕ) : MulAction G (Topology.RelCWComplex.cell C n)

If a monoid G acts on E and carries every open n-cell of the relative CW complex (C, D) onto an open n-cell, this translation of open cells is an action of G on the n-cells. It is the unique such action, since a cell is determined by its open cell (TauCeti.smul_openCell).

theorem TauCeti.smul_openCell {E : Type u} [TopologicalSpace E] {G : Type u_1} {C D : Set E} [Topology.RelCWComplex C D] [Monoid G] [MulAction G E] (hcell : ∀ (g : G) (n : ℕ) (i : Topology.RelCWComplex.cell C n), ∃ (j : Topology.RelCWComplex.cell C n), g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n j) {n : ℕ} (g : G) (i : Topology.RelCWComplex.cell C n) : g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n (g • i)

The action on cells translates open cells.

theorem TauCeti.smul_mem_openCell_smul {E : Type u} [TopologicalSpace E] {G : Type u_1} {C D : Set E} [Topology.RelCWComplex C D] [Monoid G] [MulAction G E] (hcell : ∀ (g : G) (n : ℕ) (i : Topology.RelCWComplex.cell C n), ∃ (j : Topology.RelCWComplex.cell C n), g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n j) {n : ℕ} (g : G) {i : Topology.RelCWComplex.cell C n} {y : E} (hy : y ∈ Topology.RelCWComplex.openCell n i) : g • y ∈ Topology.RelCWComplex.openCell n (g • i)

The translate by g of a point of the open cell of i lies in the open cell of g • i.

theorem TauCeti.smul_closedCell {E : Type u} [TopologicalSpace E] {G : Type u_1} {C D : Set E} [Topology.RelCWComplex C D] [Monoid G] [MulAction G E] (hcell : ∀ (g : G) (n : ℕ) (i : Topology.RelCWComplex.cell C n), ∃ (j : Topology.RelCWComplex.cell C n), g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n j) [T2Space E] [ContinuousConstSMul G E] {n : ℕ} (g : G) (i : Topology.RelCWComplex.cell C n) : g • Topology.RelCWComplex.closedCell n i = Topology.RelCWComplex.closedCell n (g • i)

The action on cells translates closed cells.

theorem TauCeti.isCancelSMul_cell {E : Type u} [TopologicalSpace E] {G : Type u_1} {C D : Set E} [Topology.RelCWComplex C D] [Group G] [MulAction G E] (hcell : ∀ (g : G) (n : ℕ) (i : Topology.RelCWComplex.cell C n), ∃ (j : Topology.RelCWComplex.cell C n), g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n j) (hfree : ∀ (g : G) (n : ℕ) (i : Topology.RelCWComplex.cell C n), g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n i → g = 1) (n : ℕ) : IsCancelSMul G (Topology.RelCWComplex.cell C n)

If g carries an open cell onto itself only when g = 1, then G acts freely on the cells.

theorem TauCeti.eq_one_of_mem_openCell_of_smul_mem {E : Type u} [TopologicalSpace E] {G : Type u_1} {C D : Set E} [Topology.RelCWComplex C D] [Monoid G] [MulAction G E] (hcell : ∀ (g : G) (n : ℕ) (i : Topology.RelCWComplex.cell C n), ∃ (j : Topology.RelCWComplex.cell C n), g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n j) (hfree : ∀ (g : G) (n : ℕ) (i : Topology.RelCWComplex.cell C n), g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n i → g = 1) {n : ℕ} {i : Topology.RelCWComplex.cell C n} {g : G} {z : E} (hz : z ∈ Topology.RelCWComplex.openCell n i) (hgz : g • z ∈ Topology.RelCWComplex.openCell n i) : g = 1

Only the identity carries a point of an open cell into the same open cell.