Group cohomology from a projective resolution, through a comparison map

For a projective resolution P of the trivial representation k of G, Mathlib's groupCohomologyIso A n P : Hⁿ(G, A) ≅ Hⁿ(Hom(P, A)) is defined through Ext. This file makes its inverse 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 cohomology by

Hom(P, A) ⟶ Hom(bar, A) ≅ Fun(Gⁿ, A),

precomposition with φ followed by the identification of Hom(bar, A) with the inhomogeneous cochains. This is how an explicit comparison map computes a cohomology isomorphism that Mathlib constructs abstractly, such as Shapiro's isomorphism or the periodicity isomorphism of a finite cyclic group.

Main results

• TauCeti.Rep.groupCohomologyIso_inv_eq_homologyMap: the inverse of groupCohomologyIso A n P is the map on cohomology 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).

theorem TauCeti.Rep.groupCohomologyIso_inv_eq_homologyMap {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (P : CategoryTheory.ProjectiveResolution (Rep.trivial k G k)) (φ : (Rep.barResolution k G).complex ⟶ P.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (P.π.f 0) = (Rep.barResolution k G).π.f 0) (n : ℕ) : (groupCohomologyIso A n P).inv = HomologicalComplex.homologyMap (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.unopFunctor (ModuleCat k) (ComplexShape.down ℕ)).map ((((CategoryTheory.linearYoneda k (Rep k G)).obj A).rightOp.mapHomologicalComplex (ComplexShape.down ℕ)).map φ).op) (groupCohomology.inhomogeneousCochainsIso A).inv) n

Group cohomology 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, the inverse of groupCohomologyIso A n P is the map on cohomology induced by precomposition with φ, followed by the identification of Hom(bar, A) with the inhomogeneous cochains.