Documentation

TauCeti.AlgebraicTopology.Cellular.Resolution

The cellular chains of a contractible free cover as a projective resolution #

Let p : E → B be the quotient covering map of a free action of a group G on E (IsQuotientCoveringMap p G), let C be a CW complex in the Hausdorff space B, and give p ⁻¹' C the lifted CW structure TauCeti.cwComplexPreimage. With coefficients in a commutative ring R, the cellular chain complex of p ⁻¹' C is a chain complex of representations of G, TauCeti.cellularChainComplexRep, in which g acts by the chain map of translation by g, and each of its terms is free over R[G] (TauCeti.cellularChainRepIsoFree), hence projective (TauCeti.projective_cellularChainComplexRep_X).

Translations are cellular, and the augmentation of cellular chains is natural under cellular maps, so the augmentation is a morphism of representations to the trivial representation (TauCeti.cellularAugmentationRep). If p ⁻¹' C is contractible, the augmented cellular chain complex is exact (TauCeti.quasiIso_cellularChainComplexAugmentation), so the cellular chains of p ⁻¹' C form a projective resolution of the trivial representation of G over R (TauCeti.cellularResolution).

This applies to the universal cover of a K(G, 1) CW complex: if B carries a CW structure on the whole space and is aspherical, and E is simply connected, then E is weakly contractible, and since it has CW type, it is contractible by Whitehead's theorem (IsCoveringMap.contractibleSpace_preimage_univ_of_isAspherical, in TauCeti.AlgebraicTopology.EilenbergMacLane.Contractible). The group acting is G, acting on E by the given action; Mathlib's IsQuotientCoveringMap.fundamentalGroupEquiv identifies G with the opposite of the fundamental group of B. This resolution is the input for identifying the cellular homology and cohomology of B with the group homology and cohomology of G.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.cellularAugmentationRep {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] :
Rep.of (cellularChainRepresentation C hG R 0) ⟶ Rep.trivial R G R

The augmentation of the cellular chains of the lift p ⁻¹' C of C in degree 0, as a morphism to the trivial representation: translation by an element of G is cellular, and the augmentation is natural under cellular maps.

Instances For
    source
    @[simp]
    theorem TauCeti.cellularAugmentationRep_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] :
    (Rep.Hom.hom (cellularAugmentationRep C hG R)).toLinearMap = ModuleCat.Hom.hom (cellularAugmentation (p ⁻¹' C) ↧R)

    The underlying linear map of TauCeti.cellularAugmentationRep is the augmentation of the cellular chains of p ⁻¹' C.

    source
    @[simp]
    theorem TauCeti.cellularDifferentialRep_comp_cellularAugmentationRep {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.CategoryStruct.comp (cellularDifferentialRep C hG R 0) (cellularAugmentationRep C hG R) = 0

    The equivariant augmentation vanishes on the boundaries of lifted 1-cells.

    source
    @[simp]
    theorem TauCeti.cellularDifferentialRep_comp_cellularAugmentationRep_assoc {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] {Z : Rep R G} (h : Rep.trivial R G R ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (cellularDifferentialRep C hG R 0) (CategoryTheory.CategoryStruct.comp (cellularAugmentationRep C hG R) h) = CategoryTheory.CategoryStruct.comp 0 h

    The equivariant augmentation vanishes on the boundaries of lifted 1-cells.

    source
    noncomputable def TauCeti.cellularChainComplexRepAugmentation {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] :
    cellularChainComplexRep C hG R ⟶ (ChainComplex.single₀ (Rep R G)).obj (Rep.trivial R G R)

    The augmentation of the lifted cellular chain complex, as a chain map of complexes of representations to the trivial representation placed in degree 0.

    Instances For
      source
      @[simp]
      theorem TauCeti.cellularChainComplexRepAugmentation_f_zero {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] :
      (cellularChainComplexRepAugmentation C hG R).f 0 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (cellularAugmentationRep C hG R)

      In degree 0 the augmentation of the lifted cellular chain complex is TauCeti.cellularAugmentationRep.

      source
      theorem TauCeti.quasiIso_cellularChainComplexRepAugmentation {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] [ContractibleSpace ↑(p ⁻¹' C)] :
      QuasiIso (cellularChainComplexRepAugmentation C hG R)

      The augmented lifted cellular chain complex of a contractible cover is exact: forgetting the action, the augmentation is that of the cellular chain complex of the contractible CW complex p ⁻¹' C.

      source
      instance TauCeti.projective_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 : ℕ) :
      CategoryTheory.Projective ((cellularChainComplexRep C hG R).X n)

      The terms of the lifted cellular chain complex are projective representations: each is free over the group ring, with basis one chosen lift of each cell of C.

      source
      noncomputable def TauCeti.cellularResolution {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] [ContractibleSpace ↑(p ⁻¹' C)] :
      CategoryTheory.ProjectiveResolution (Rep.trivial R G R)

      The cellular chains of a contractible free cover are a projective resolution of the trivial representation of G over R: if the lift p ⁻¹' C of the CW complex C is contractible, its cellular chain complex, on which G acts through translation of the lifted cells, is a complex of free representations whose augmentation is a quasi-isomorphism.

      Instances For
        source
        @[simp]
        theorem TauCeti.cellularResolution_complex {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] [ContractibleSpace ↑(p ⁻¹' C)] :
        (cellularResolution C hG R).complex = cellularChainComplexRep C hG R

        The complex of TauCeti.cellularResolution is the lifted cellular chain complex.

        source
        @[simp]
        theorem TauCeti.cellularResolution_π {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] [ContractibleSpace ↑(p ⁻¹' C)] :
        (cellularResolution C hG R).π = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (cellularChainComplexRepAugmentation C hG R)

        The augmentation of TauCeti.cellularResolution is that of the lifted cellular chain complex.