The singular homology of a classifying space is group homology

For every group G and every commutative ring k, the singular homology of Milnor's classifying space classifyingSpace G with coefficients in k is Mathlib's group homology of G with coefficients in the trivial representation k, in every degree (TauCeti.classifyingSpaceSingularHomologyIsoGroupHomology):

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

The countable join universalGSpace G is weakly contractible and carries a CW structure, so it is contractible by Whitehead's theorem (TauCeti.instContractibleSpaceUniversalGSpace). The orbit map classifyingSpaceProj G is the quotient covering map of the free action of G on it, so its singular chains are a free resolution of k over k[G] whose coinvariants are the singular chains of classifyingSpace G (IsQuotientCoveringMap.singularHomologyIsoGroupHomology). No hypothesis on G is needed.

The identification is natural in the group. The geometric chain identification commutes with every group homomorphism (MonoidHom.classifyingSpaceSingularChainsCoinvariants_naturality), and on homology, for every φ : G →* H, the map Hₙ(BG; k) ⟶ Hₙ(BH; k) induced by the strictly functorial map MonoidHom.classifyingSpaceMap φ is Mathlib's change-of-group map groupHomology.map φ (MonoidHom.classifyingSpaceSingularHomologyIsoGroupHomology_hom_naturality). No hypothesis on φ is needed.

Main definitions

• TauCeti.classifyingSpaceSingularHomologyIsoGroupHomology: the isomorphism Hₙ(BG; k) ≅ Hₙ(G, k).

Main results

• MonoidHom.classifyingSpaceSingularHomologyIsoGroupHomology_hom_naturality, MonoidHom.classifyingSpaceSingularHomologyIsoGroupHomology_inv_naturality: the isomorphism is natural in the group.

References

• K. S. Brown, Cohomology of Groups, GTM 87, Springer, 1982, Section II.4 and Section III.8.
• J. Milnor, Construction of universal bundles, II, Ann. of Math. 63 (1956), 430--436.

noncomputable def TauCeti.classifyingSpaceSingularHomologyIsoGroupHomology (k : Type u) [CommRing k] (G : Type u) [Group G] (n : ℕ) : HomologicalComplex.homology ((singularChains k).obj ↧(classifyingSpace G)) n ≅ groupHomology (Rep.trivial k G k) n

The singular homology of the classifying space is group homology: for every group G, the singular homology Hₙ(BG; k) of Milnor's classifying space with coefficients in a commutative ring k is Mathlib's group homology Hₙ(G, k) of the trivial representation. It comes from the free resolution of k by the singular chains of universalGSpace G.

theorem MonoidHom.classifyingSpaceSingularChainsCoinvariants_naturality {G H : Type u} [Group G] [Group H] (φ : G →* H) (k : Type u) [CommRing k] : CategoryTheory.CategoryStruct.comp (TauCeti.singularChainsCoinvariantsMap k (TopCat.ofHom φ.universalGSpaceMap) ⋯) (⋯.singularChainsRepCoinvariantsTensorIso k).hom = CategoryTheory.CategoryStruct.comp (⋯.singularChainsRepCoinvariantsTensorIso k).hom ((TauCeti.singularChains k).map (TopCat.ofHom φ.classifyingSpaceMap))

The geometric chain comparison for Milnor classifying spaces is natural in the group. Applying a group homomorphism to the labels in the universal space before passing to coinvariant chains agrees with pushing chains forward along its map of classifying spaces.

theorem MonoidHom.classifyingSpaceSingularChainsCoinvariants_naturality_assoc {G H : Type u} [Group G] [Group H] (φ : G →* H) (k : Type u) [CommRing k] {Z : ChainComplex (ModuleCat k) ℕ} (h : (TauCeti.singularChains k).obj ↧(TauCeti.classifyingSpace H) ⟶ Z) : CategoryTheory.CategoryStruct.comp (TauCeti.singularChainsCoinvariantsMap k (TopCat.ofHom φ.universalGSpaceMap) ⋯) (CategoryTheory.CategoryStruct.comp (⋯.singularChainsRepCoinvariantsTensorIso k).hom h) = CategoryTheory.CategoryStruct.comp (⋯.singularChainsRepCoinvariantsTensorIso k).hom (CategoryTheory.CategoryStruct.comp ((TauCeti.singularChains k).map (TopCat.ofHom φ.classifyingSpaceMap)) h)

The geometric chain comparison for Milnor classifying spaces is natural in the group. Applying a group homomorphism to the labels in the universal space before passing to coinvariant chains agrees with pushing chains forward along its map of classifying spaces.

theorem MonoidHom.classifyingSpaceSingularHomologyIsoGroupHomology_hom_naturality {G H : Type u} [Group G] [Group H] (φ : G →* H) (k : Type u) [CommRing k] (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((TauCeti.singularChains k).map (TopCat.ofHom φ.classifyingSpaceMap)) n) (TauCeti.classifyingSpaceSingularHomologyIsoGroupHomology k H n).hom = CategoryTheory.CategoryStruct.comp (TauCeti.classifyingSpaceSingularHomologyIsoGroupHomology k G n).hom (groupHomology.map φ (CategoryTheory.CategoryStruct.id (Rep.trivial k G k)) n)

The singular homology of the classifying space is naturally group homology. For every group homomorphism φ : G →* H, the identifications Hₙ(BG; k) ≅ Hₙ(G, k) and Hₙ(BH; k) ≅ Hₙ(H, k) carry the map induced by MonoidHom.classifyingSpaceMap φ to Mathlib's change-of-group map groupHomology.map φ, with the identity on the trivial coefficients k.

theorem MonoidHom.classifyingSpaceSingularHomologyIsoGroupHomology_hom_naturality_assoc {G H : Type u} [Group G] [Group H] (φ : G →* H) (k : Type u) [CommRing k] (n : ℕ) {Z : ModuleCat k} (h : groupHomology (Rep.trivial k H k) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((TauCeti.singularChains k).map (TopCat.ofHom φ.classifyingSpaceMap)) n) (CategoryTheory.CategoryStruct.comp (TauCeti.classifyingSpaceSingularHomologyIsoGroupHomology k H n).hom h) = CategoryTheory.CategoryStruct.comp (TauCeti.classifyingSpaceSingularHomologyIsoGroupHomology k G n).hom (CategoryTheory.CategoryStruct.comp (groupHomology.map φ (CategoryTheory.CategoryStruct.id (Rep.trivial k G k)) n) h)

The singular homology of the classifying space is naturally group homology. For every group homomorphism φ : G →* H, the identifications Hₙ(BG; k) ≅ Hₙ(G, k) and Hₙ(BH; k) ≅ Hₙ(H, k) carry the map induced by MonoidHom.classifyingSpaceMap φ to Mathlib's change-of-group map groupHomology.map φ, with the identity on the trivial coefficients k.

theorem MonoidHom.classifyingSpaceSingularHomologyIsoGroupHomology_inv_naturality {G H : Type u} [Group G] [Group H] (φ : G →* H) (k : Type u) [CommRing k] (n : ℕ) : CategoryTheory.CategoryStruct.comp (groupHomology.map φ (CategoryTheory.CategoryStruct.id (Rep.trivial k G k)) n) (TauCeti.classifyingSpaceSingularHomologyIsoGroupHomology k H n).inv = CategoryTheory.CategoryStruct.comp (TauCeti.classifyingSpaceSingularHomologyIsoGroupHomology k G n).inv (HomologicalComplex.homologyMap ((TauCeti.singularChains k).map (TopCat.ofHom φ.classifyingSpaceMap)) n)

The inverse identification of group homology with the singular homology of the classifying space is natural in the group.

theorem MonoidHom.classifyingSpaceSingularHomologyIsoGroupHomology_inv_naturality_assoc {G H : Type u} [Group G] [Group H] (φ : G →* H) (k : Type u) [CommRing k] (n : ℕ) {Z : ModuleCat k} (h : HomologicalComplex.homology ((TauCeti.singularChains k).obj ↧(TauCeti.classifyingSpace H)) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupHomology.map φ (CategoryTheory.CategoryStruct.id (Rep.trivial k G k)) n) (CategoryTheory.CategoryStruct.comp (TauCeti.classifyingSpaceSingularHomologyIsoGroupHomology k H n).inv h) = CategoryTheory.CategoryStruct.comp (TauCeti.classifyingSpaceSingularHomologyIsoGroupHomology k G n).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((TauCeti.singularChains k).map (TopCat.ofHom φ.classifyingSpaceMap)) n) h)

The inverse identification of group homology with the singular homology of the classifying space is natural in the group.