The singular homology of the base of a contractible free cover is group homology

Let p : E ⟶ B be the quotient covering map of an action of a group G on E, in the sense of Mathlib's IsQuotientCoveringMap, and let k be a commutative ring. The singular chains of E form a chain complex of representations of G, TauCeti.singularChainsRep k E G. Its coinvariants (k ⊗ C(E; k))_G, with k the trivial representation, are the singular chains of B (IsQuotientCoveringMap.singularChainsRepCoinvariantsTensorIso): the class of a ⊗ c goes to a • p_* c, every singular simplex of B lifts to E, and two lifts of one simplex differ by an element of G (IsQuotientCoveringMap.isColimitMapCoconeToSSet).

If E is contractible, the singular chains of E are a projective resolution of the trivial representation (TauCeti.singularChainsResolution), since G acts freely on E. Group homology with trivial coefficients is the homology of the coinvariants of any projective resolution of k (groupHomologyIso), so the singular homology of B is the group homology of G (IsQuotientCoveringMap.singularHomologyIsoGroupHomology):

Hₙ(B; k) ≅ Hₙ(G, k).

This applies to the orbit map of a free, covering-space action of G on a contractible space, such as the universal cover of a classifying space of G.

The chain identification is natural for maps of quotient covers equivariant along arbitrary group homomorphisms (IsQuotientCoveringMap.singularChainsRepCoinvariantsTensorIso_naturality), and so is the comparison with group homology: for a map b : B ⟶ C of bases covered by a map of contractible total spaces equivariant along φ : G →* H, the map b_* on singular homology corresponds to Mathlib's change-of-group map groupHomology.map φ on group homology with trivial coefficients (IsQuotientCoveringMap.singularHomologyIsoGroupHomology_hom_naturality). No hypothesis on φ is needed.

Main definitions

• IsQuotientCoveringMap.singularChainsRepCoinvariantsTensorIso: the coinvariants of the singular chains of E are the singular chains of B.
• IsQuotientCoveringMap.singularHomologyIsoGroupHomology: for contractible E, the singular homology of B is the group homology of G with trivial coefficients.

Main results

• IsQuotientCoveringMap.singularChainsRepCoinvariantsTensorIso_hom_f_coinvariantsTensorMk: the comparison of chains sends the class of a ⊗ c to a • p_* c.
• IsQuotientCoveringMap.singularHomologyIsoGroupHomology_hom_naturality, IsQuotientCoveringMap.singularHomologyIsoGroupHomology_inv_naturality: the comparison with group homology is natural in the covering and the group.

References

• K. S. Brown, Cohomology of Groups, GTM 87, Springer, 1982, Section II.4, Proposition 4.1, Section III.1, and Section III.8.

noncomputable def IsQuotientCoveringMap.singularChainsRepCoinvariantsTensorIso {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] : HomologicalComplex.coinvariantsTensorObj (Rep.trivial k G k) (TauCeti.singularChainsRep k E G) ≅ (TauCeti.singularChains k).obj B

The singular chains of the base of a quotient covering are the coinvariants of those of the total space: for the quotient covering map p : E ⟶ B of an action of G, the chain complex (k ⊗ C(E; k))_G is isomorphic to C(B; k), the class of a ⊗ c going to a • p_* c.

theorem IsQuotientCoveringMap.singularChainsRepCoinvariantsTensorIso_hom_f_coinvariantsTensorMk {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] (n : ℕ) (a : k) (c : ↑(((TauCeti.singularChains k).obj E).X n)) : (ModuleCat.Hom.hom ((hG.singularChainsRepCoinvariantsTensorIso k).hom.f n)) ((((Rep.trivial k G k).coinvariantsTensorMk (Rep.of (TauCeti.singularChainsRepresentation k E G n))) a) c) = a • (CategoryTheory.ConcreteCategory.hom (((TauCeti.singularChains k).map p).f n)) c

The comparison sends the class of a ⊗ c to a • p_* c.

noncomputable def IsQuotientCoveringMap.singularHomologyIsoGroupHomology {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] [ContractibleSpace ↑E] (n : ℕ) : HomologicalComplex.homology ((TauCeti.singularChains k).obj B) n ≅ groupHomology (Rep.trivial k G k) n

The singular homology of the base of a contractible free covering is group homology: for the quotient covering map p : E ⟶ B of an action of G with contractible total space, the singular homology Hₙ(B; k) is Mathlib's group homology Hₙ(G, k) of the trivial representation. The singular chains of E form a free resolution of k over k[G], whose coinvariants are the singular chains of B.

theorem IsQuotientCoveringMap.singularChainsRepCoinvariantsTensorIso_naturality {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] {F C : TopCat} {q : F ⟶ C} {H : Type u} [Group H] [MulAction H ↑F] (hH : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom q)) H) {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) (b : B ⟶ C) (hb : CategoryTheory.CategoryStruct.comp p b = CategoryTheory.CategoryStruct.comp f q) : CategoryTheory.CategoryStruct.comp (TauCeti.singularChainsCoinvariantsMap k f hf) (hH.singularChainsRepCoinvariantsTensorIso k).hom = CategoryTheory.CategoryStruct.comp (hG.singularChainsRepCoinvariantsTensorIso k).hom ((TauCeti.singularChains k).map b)

The identification of quotient-cover chains with coinvariant chains is natural. An equivariant map of total spaces along any group homomorphism, lying over a continuous map of bases, commutes with the chain identification.

theorem IsQuotientCoveringMap.singularChainsRepCoinvariantsTensorIso_naturality_assoc {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] {F C : TopCat} {q : F ⟶ C} {H : Type u} [Group H] [MulAction H ↑F] (hH : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom q)) H) {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) (b : B ⟶ C) (hb : CategoryTheory.CategoryStruct.comp p b = CategoryTheory.CategoryStruct.comp f q) {Z : ChainComplex (ModuleCat k) ℕ} (h : (TauCeti.singularChains k).obj C ⟶ Z) : CategoryTheory.CategoryStruct.comp (TauCeti.singularChainsCoinvariantsMap k f hf) (CategoryTheory.CategoryStruct.comp (hH.singularChainsRepCoinvariantsTensorIso k).hom h) = CategoryTheory.CategoryStruct.comp (hG.singularChainsRepCoinvariantsTensorIso k).hom (CategoryTheory.CategoryStruct.comp ((TauCeti.singularChains k).map b) h)

The identification of quotient-cover chains with coinvariant chains is natural. An equivariant map of total spaces along any group homomorphism, lying over a continuous map of bases, commutes with the chain identification.

theorem IsQuotientCoveringMap.singularChainsRepCoinvariantsTensorIso_inv_naturality {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] {F C : TopCat} {q : F ⟶ C} {H : Type u} [Group H] [MulAction H ↑F] (hH : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom q)) H) {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) (b : B ⟶ C) (hb : CategoryTheory.CategoryStruct.comp p b = CategoryTheory.CategoryStruct.comp f q) : CategoryTheory.CategoryStruct.comp ((TauCeti.singularChains k).map b) (hH.singularChainsRepCoinvariantsTensorIso k).inv = CategoryTheory.CategoryStruct.comp (hG.singularChainsRepCoinvariantsTensorIso k).inv (TauCeti.singularChainsCoinvariantsMap k f hf)

The inverse chain identification is natural for an equivariant map of quotient covers.

theorem IsQuotientCoveringMap.singularChainsRepCoinvariantsTensorIso_inv_naturality_assoc {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] {F C : TopCat} {q : F ⟶ C} {H : Type u} [Group H] [MulAction H ↑F] (hH : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom q)) H) {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) (b : B ⟶ C) (hb : CategoryTheory.CategoryStruct.comp p b = CategoryTheory.CategoryStruct.comp f q) {Z : ChainComplex (ModuleCat k) ℕ} (h : HomologicalComplex.coinvariantsTensorObj (Rep.trivial k H k) (TauCeti.singularChainsRep k F H) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((TauCeti.singularChains k).map b) (CategoryTheory.CategoryStruct.comp (hH.singularChainsRepCoinvariantsTensorIso k).inv h) = CategoryTheory.CategoryStruct.comp (hG.singularChainsRepCoinvariantsTensorIso k).inv (CategoryTheory.CategoryStruct.comp (TauCeti.singularChainsCoinvariantsMap k f hf) h)

The inverse chain identification is natural for an equivariant map of quotient covers.

theorem IsQuotientCoveringMap.singularHomologyIsoGroupHomology_hom_naturality {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] [ContractibleSpace ↑E] {F C : TopCat} {q : F ⟶ C} {H : Type u} [Group H] [MulAction H ↑F] (hH : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom q)) H) [ContractibleSpace ↑F] {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) (b : B ⟶ C) (hb : CategoryTheory.CategoryStruct.comp p b = CategoryTheory.CategoryStruct.comp f q) (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((TauCeti.singularChains k).map b) n) (hH.singularHomologyIsoGroupHomology k n).hom = CategoryTheory.CategoryStruct.comp (hG.singularHomologyIsoGroupHomology k n).hom (groupHomology.map φ (CategoryTheory.CategoryStruct.id (Rep.trivial k G k)) n)

The singular homology of the base of a contractible free cover is naturally group homology. For quotient covers p : E ⟶ B and q : F ⟶ C with contractible total spaces, a map f : E ⟶ F equivariant along any group homomorphism φ : G →* H and lying over b : B ⟶ C, the identifications Hₙ(B; k) ≅ Hₙ(G, k) and Hₙ(C; k) ≅ Hₙ(H, k) carry b_* to the change-of-group map groupHomology.map φ, with the identity on the trivial coefficients k.

theorem IsQuotientCoveringMap.singularHomologyIsoGroupHomology_hom_naturality_assoc {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] [ContractibleSpace ↑E] {F C : TopCat} {q : F ⟶ C} {H : Type u} [Group H] [MulAction H ↑F] (hH : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom q)) H) [ContractibleSpace ↑F] {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) (b : B ⟶ C) (hb : CategoryTheory.CategoryStruct.comp p b = CategoryTheory.CategoryStruct.comp f q) (n : ℕ) {Z : ModuleCat k} (h : groupHomology (Rep.trivial k H k) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((TauCeti.singularChains k).map b) n) (CategoryTheory.CategoryStruct.comp (hH.singularHomologyIsoGroupHomology k n).hom h) = CategoryTheory.CategoryStruct.comp (hG.singularHomologyIsoGroupHomology k n).hom (CategoryTheory.CategoryStruct.comp (groupHomology.map φ (CategoryTheory.CategoryStruct.id (Rep.trivial k G k)) n) h)

The singular homology of the base of a contractible free cover is naturally group homology. For quotient covers p : E ⟶ B and q : F ⟶ C with contractible total spaces, a map f : E ⟶ F equivariant along any group homomorphism φ : G →* H and lying over b : B ⟶ C, the identifications Hₙ(B; k) ≅ Hₙ(G, k) and Hₙ(C; k) ≅ Hₙ(H, k) carry b_* to the change-of-group map groupHomology.map φ, with the identity on the trivial coefficients k.

theorem IsQuotientCoveringMap.singularHomologyIsoGroupHomology_inv_naturality {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] [ContractibleSpace ↑E] {F C : TopCat} {q : F ⟶ C} {H : Type u} [Group H] [MulAction H ↑F] (hH : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom q)) H) [ContractibleSpace ↑F] {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) (b : B ⟶ C) (hb : CategoryTheory.CategoryStruct.comp p b = CategoryTheory.CategoryStruct.comp f q) (n : ℕ) : CategoryTheory.CategoryStruct.comp (groupHomology.map φ (CategoryTheory.CategoryStruct.id (Rep.trivial k G k)) n) (hH.singularHomologyIsoGroupHomology k n).inv = CategoryTheory.CategoryStruct.comp (hG.singularHomologyIsoGroupHomology k n).inv (HomologicalComplex.homologyMap ((TauCeti.singularChains k).map b) n)

The inverse comparison with group homology is natural in the covering and the group.

theorem IsQuotientCoveringMap.singularHomologyIsoGroupHomology_inv_naturality_assoc {E B : TopCat} {p : E ⟶ B} {G : Type u} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (k : Type u) [CommRing k] [ContractibleSpace ↑E] {F C : TopCat} {q : F ⟶ C} {H : Type u} [Group H] [MulAction H ↑F] (hH : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom q)) H) [ContractibleSpace ↑F] {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) (b : B ⟶ C) (hb : CategoryTheory.CategoryStruct.comp p b = CategoryTheory.CategoryStruct.comp f q) (n : ℕ) {Z : ModuleCat k} (h : HomologicalComplex.homology ((TauCeti.singularChains k).obj C) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupHomology.map φ (CategoryTheory.CategoryStruct.id (Rep.trivial k G k)) n) (CategoryTheory.CategoryStruct.comp (hH.singularHomologyIsoGroupHomology k n).inv h) = CategoryTheory.CategoryStruct.comp (hG.singularHomologyIsoGroupHomology k n).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((TauCeti.singularChains k).map b) n) h)

The inverse comparison with group homology is natural in the covering and the group.