Group homology from a projective resolution, through a comparison map

For a projective resolution P of the trivial representation k of G, Mathlib's groupHomologyIso A n P : Hₙ(G, A) ≅ Hₙ((A ⊗ P)_G) is defined through Tor. This file makes it explicit: given a chain map φ from the bar resolution of G to P lying over the identity of k, it is the map induced on homology by

Cₙ(G, A) ≅ (A ⊗ bar)_G ⟶ (A ⊗ P)_G,

the identification of the inhomogeneous chains with the bar coinvariants followed by A ⊗ φ. This is the homological counterpart of TauCeti.Rep.groupCohomologyIso_inv_eq_homologyMap.

Main results

• Rep.groupHomologyIso_hom_eq_homologyMap: groupHomologyIso A n P is the map on homology induced by a comparison map from the bar resolution to P.

References

• K. S. Brown, Cohomology of Groups, Graduate Texts in Mathematics 87, Springer (1982), Chapter I, §7 (comparison of projective resolutions) and Chapter III, §1.

The comparisons groupHomologyIso and groupHomology.inhomogeneousChainsIso are Mathlib's constructions by Amelia Livingston; the proof uses Mathlib's computation of left derived functors by projective resolutions, ProjectiveResolution.isoLeftDerivedObj_hom_naturality.

theorem Rep.groupHomologyIso_hom_eq_homologyMap {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (A : Rep k G) (P : CategoryTheory.ProjectiveResolution (trivial k G k)) (φ : barComplex k G ⟶ P.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (P.π.f 0) = (barResolution k G).π.f 0) (n : ℕ) : (groupHomologyIso A n P).hom = HomologicalComplex.homologyMap (CategoryTheory.CategoryStruct.comp (groupHomology.inhomogeneousChainsIso A).hom ((((coinvariantsTensor k G).obj A).mapHomologicalComplex (ComplexShape.down ℕ)).map φ)) n

Group homology from a projective resolution, through a comparison map. For a projective resolution P of the trivial representation k and a chain map φ from the bar resolution to P lying over the identity of k, groupHomologyIso A n P is the map on homology induced by the identification of the inhomogeneous chains with (A ⊗ bar)_G followed by A ⊗ φ.