The cellular chains of a lifted CW structure are free over the group ring

Let p : E → B be the quotient covering map of a free action of a group G on E (IsQuotientCoveringMap p G), and let C be a CW complex in the Hausdorff space B. Then p ⁻¹' C carries the lifted CW structure TauCeti.cwComplexPreimage, and G permutes its cells freely, with one orbit over each cell of C, translating characteristic maps (TauCeti.map_smul_cellPreimage).

Translation by g is therefore cellular (TauCeti.isCellular_preimageSMul) and sends the cellular basis vector of a lifted cell to that of its translate. With coefficients in a commutative ring R, this makes each cellular chain group of p ⁻¹' C, the relative homology of consecutive skeleta of p ⁻¹' C with coefficients in R, a representation of G (TauCeti.cellularChainRepresentation), on which g acts by the chain map of the translation. The cellular differentials are G-equivariant, so the cellular chain complex of p ⁻¹' C is a chain complex of representations (TauCeti.cellularChainComplexRep), whose underlying chain complex of R-modules is the cellular chain complex of p ⁻¹' C (TauCeti.cellularChainComplexRepForget₂Iso).

Each of its terms is free over R[G], with basis one chosen lift of each cell of C (TauCeti.cellularChainRepIsoFree): for a choice s of lifts, the basis vector of the lifted cell g • s i corresponds to the generator single i (single g 1) of Rep.free R G (cell C n).

Main definitions

• TauCeti.cellularChainRepresentation: the action of G on a cellular chain group of the lift.
• TauCeti.cellularChainComplexRep: the cellular chain complex of the lift, as a chain complex of representations of G.
• TauCeti.cellularChainComplexRepForget₂Iso: forgetting the action, it is the cellular chain complex of the lift.
• TauCeti.cellularChainRepIsoFree: each of its terms is the free representation on the cells of C.

References

• K. S. Brown, Cohomology of Groups, GTM 87, Springer, 1982, Section I.4, free G-complexes and their cellular chains.
• T. tom Dieck, Transformation Groups, de Gruyter, 1987, Section II.1.

noncomputable def TauCeti.cellularChainRepresentation {E B : Type w} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (C : Set B) {G : Type w} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) [T2Space B] [Topology.CWComplex C] (R : Type w) [CommRing R] (n : ℕ) : Representation R G ↑(cellularChainGroup (p ⁻¹' C) (↧R) n)

The action of G on the n-th cellular chain group of the lift p ⁻¹' C of C, in which g acts by the chain map of translation by g.

@[simp]

theorem TauCeti.cellularChainRepresentation_apply {E B : Type w} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (C : Set B) {G : Type w} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) [T2Space B] [Topology.CWComplex C] (R : Type w) [CommRing R] (n : ℕ) (g : G) : (cellularChainRepresentation C hG R n) g = ModuleCat.Hom.hom (cellularChainGroupMap (p ⁻¹' C) (p ⁻¹' C) ⋯ (↧R) n)

An element g acts on the cellular chains of the lift by the chain map of translation by g.

theorem TauCeti.cellularChainRepresentation_cellularChainBasis {E B : Type w} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (C : Set B) {G : Type w} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) [T2Space B] [Topology.CWComplex C] (R : Type w) [CommRing R] {n : ℕ} (g : G) (c : Topology.RelCWComplex.cell (p ⁻¹' C) n) : ((cellularChainRepresentation C hG R n) g) ((cellularChainBasis (p ⁻¹' C) R n) c) = (cellularChainBasis (p ⁻¹' C) R n) (g • c)

An element g sends the cellular basis vector of a lifted cell to that of its translate. This is not a simp lemma: simp unfolds TauCeti.cellularChainBasis by TauCeti.cellularChainBasis_apply first.

noncomputable def TauCeti.cellularDifferentialRep {E B : Type w} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (C : Set B) {G : Type w} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) [T2Space B] [Topology.CWComplex C] (R : Type w) [CommRing R] (n : ℕ) : Rep.of (cellularChainRepresentation C hG R (n + 1)) ⟶ Rep.of (cellularChainRepresentation C hG R n)

The cellular differential of the lift is G-equivariant, so it is a morphism of representations.

@[simp]

theorem TauCeti.cellularDifferentialRep_hom_toLinearMap {E B : Type w} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (C : Set B) {G : Type w} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) [T2Space B] [Topology.CWComplex C] (R : Type w) [CommRing R] (n : ℕ) : (Rep.Hom.hom (cellularDifferentialRep C hG R n)).toLinearMap = ModuleCat.Hom.hom (cellularDifferential (p ⁻¹' C) (↧R) n)

The underlying linear map of TauCeti.cellularDifferentialRep is the cellular differential.

noncomputable def TauCeti.cellularChainComplexRep {E B : Type w} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (C : Set B) {G : Type w} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) [T2Space B] [Topology.CWComplex C] (R : Type w) [CommRing R] : ChainComplex (Rep R G) ℕ

The cellular chain complex of the lift is a chain complex of representations of G: its terms are the representations TauCeti.cellularChainRepresentation and its differentials are the cellular differentials.

@[simp]

theorem TauCeti.cellularChainComplexRep_X {E B : Type w} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (C : Set B) {G : Type w} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) [T2Space B] [Topology.CWComplex C] (R : Type w) [CommRing R] (n : ℕ) : (cellularChainComplexRep C hG R).X n = Rep.of (cellularChainRepresentation C hG R n)

The objects of TauCeti.cellularChainComplexRep are the representations TauCeti.cellularChainRepresentation.

@[simp]

theorem TauCeti.cellularChainComplexRep_d {E B : Type w} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (C : Set B) {G : Type w} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) [T2Space B] [Topology.CWComplex C] (R : Type w) [CommRing R] (n : ℕ) : (cellularChainComplexRep C hG R).d (n + 1) n = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (cellularDifferentialRep C hG R n) (CategoryTheory.eqToHom ⋯))

The differentials of TauCeti.cellularChainComplexRep are the equivariant cellular differentials, transported across TauCeti.cellularChainComplexRep_X.

noncomputable def TauCeti.cellularChainComplexRepForget₂Iso {E B : Type w} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (C : Set B) {G : Type w} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) [T2Space B] [Topology.CWComplex C] (R : Type w) [CommRing R] : ((CategoryTheory.forget₂ (Rep R G) (ModuleCat R)).mapHomologicalComplex (ComplexShape.down ℕ)).obj (cellularChainComplexRep C hG R) ≅ cellularChainComplex (p ⁻¹' C) ↧R

Forgetting the action of G, TauCeti.cellularChainComplexRep is the cellular chain complex of the lift: the components of this isomorphism are transports along equalities of objects that hold by definition.

@[simp]

theorem TauCeti.cellularChainComplexRepForget₂Iso_hom_f {E B : Type w} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (C : Set B) {G : Type w} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) [T2Space B] [Topology.CWComplex C] (R : Type w) [CommRing R] (n : ℕ) : (cellularChainComplexRepForget₂Iso C hG R).hom.f n = CategoryTheory.eqToHom ⋯

The components of TauCeti.cellularChainComplexRepForget₂Iso are the transports along the equalities of objects that hold by definition.

noncomputable def TauCeti.cellularChainRepIsoFree {E B : Type w} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (C : Set B) {G : Type w} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) [T2Space B] [Topology.CWComplex C] (R : Type w) [CommRing R] {n : ℕ} (s : Topology.RelCWComplex.cell C n → Topology.RelCWComplex.cell (p ⁻¹' C) n) (hs : ∀ (i : Topology.RelCWComplex.cell C n), ((cellPreimageEquiv C ⋯ n) (s i)).fst = i) : Rep.of (cellularChainRepresentation C hG R n) ≅ Rep.free R G (Topology.RelCWComplex.cell C n)

The cellular chains of the lift are free over the group ring, with basis one chosen lift of each cell of C: given a lift s i of each n-cell i of C, the n-th cellular chain group of p ⁻¹' C is isomorphic, as a representation of G, to the free representation on the n-cells of C, the generator single i (single g 1) corresponding to the cellular basis vector of the lifted cell g • s i.

@[simp]

theorem TauCeti.cellularChainRepIsoFree_inv_hom_single {E B : Type w} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (C : Set B) {G : Type w} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) [T2Space B] [Topology.CWComplex C] (R : Type w) [CommRing R] {n : ℕ} (s : Topology.RelCWComplex.cell C n → Topology.RelCWComplex.cell (p ⁻¹' C) n) (hs : ∀ (i : Topology.RelCWComplex.cell C n), ((cellPreimageEquiv C ⋯ n) (s i)).fst = i) (i : Topology.RelCWComplex.cell C n) (g : G) : (Rep.Hom.hom (cellularChainRepIsoFree C hG R s hs).inv) (Finsupp.single i (MonoidAlgebra.single g 1)) = (cellularChainBasis (p ⁻¹' C) R n) (g • s i)

The generator single i (single g 1) of the free representation corresponds to the cellular basis vector of the lifted cell g • s i.

theorem TauCeti.cellularChainRepIsoFree_hom_hom_cellularChainBasis {E B : Type w} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (C : Set B) {G : Type w} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) [T2Space B] [Topology.CWComplex C] (R : Type w) [CommRing R] {n : ℕ} (s : Topology.RelCWComplex.cell C n → Topology.RelCWComplex.cell (p ⁻¹' C) n) (hs : ∀ (i : Topology.RelCWComplex.cell C n), ((cellPreimageEquiv C ⋯ n) (s i)).fst = i) (i : Topology.RelCWComplex.cell C n) (g : G) : (Rep.Hom.hom (cellularChainRepIsoFree C hG R s hs).hom) ((cellularChainBasis (p ⁻¹' C) R n) (g • s i)) = Finsupp.single i (MonoidAlgebra.single g 1)

The cellular basis vector of the lifted cell g • s i corresponds to the generator single i (single g 1) of the free representation. This is not a simp lemma: simp unfolds TauCeti.cellularChainBasis by TauCeti.cellularChainBasis_apply first.