Resolution comparisons commute with change of groups up to homotopy

Let f : G →* H, and let P and Q resolve the trivial representations of G and H. An augmentation-preserving map from P to the restriction of Q commutes, up to homotopy, with the comparison maps from the bar resolutions. The bar map is the existing TauCeti.Rep.barComplex.resChainMap, which applies f to each group label.

This holds for every homomorphism: the restricted target is exact, but is not assumed projective. The homotopy square is the resolution-comparison ingredient for naturality of group homology and cohomology computed from equivariant geometric resolutions.

We use Mathlib's projective-resolution lifts, by Kim Morrison and Joël Riou, and Amelia Livingston's bar resolution. No replacement resolution is introduced.

References

• K. S. Brown, Cohomology of Groups, Chapters I.7 and III.8.

noncomputable def MonoidHom.homotopyOfCompResAugmentationEq {k G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) {P : ChainComplex (Rep.{u, u, u} k G) ℕ} [∀ (n : ℕ), CategoryTheory.Projective (P.X n)] {Z : Rep.{u, u, u} k H} (Q : CategoryTheory.ProjectiveResolution Z) (α β : P ⟶ ((Rep.resFunctor f).mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) (h : CategoryTheory.CategoryStruct.comp (α.f 0) ((Rep.resFunctor f).map (Q.π.f 0)) = CategoryTheory.CategoryStruct.comp (β.f 0) ((Rep.resFunctor f).map (Q.π.f 0))) : Homotopy α β

Maps into a restricted projective resolution that agree after augmentation are homotopic. Only the source complex must be degreewise projective; restriction along f is not assumed to preserve projective objects.

noncomputable def MonoidHom.barResolutionComparisonHomotopy {k G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) (P : CategoryTheory.ProjectiveResolution (Rep.trivial k G k)) (Q : CategoryTheory.ProjectiveResolution (Rep.trivial k H k)) (φ : P.complex ⟶ ((Rep.resFunctor f).mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) (hφ : CategoryTheory.CategoryStruct.comp (φ.f 0) ((Rep.resFunctor f).map (Q.π.f 0)) = P.π.f 0) : Homotopy (CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.lift (CategoryTheory.CategoryStruct.id (Rep.trivial k G k)) (Rep.barResolution k G) P) φ) (CategoryTheory.CategoryStruct.comp (TauCeti.Rep.barComplex.resChainMap f) (((Rep.resFunctor f).mapHomologicalComplex (ComplexShape.down ℕ)).map (CategoryTheory.ProjectiveResolution.lift (CategoryTheory.CategoryStruct.id (Rep.trivial k H k)) (Rep.barResolution k H) Q)))

Bar-resolution comparisons commute with arbitrary change of groups up to homotopy. For an augmentation-preserving map φ from P to the restriction of Q, comparing from the bar resolution before applying φ is homotopic to first relabelling the bar resolution and then comparing to Q. No injectivity assumption on f is needed.