Functoriality of group cohomology

The map on group cohomology along the trivial homomorphism 1 : G →* H factors through the cohomology of the trivial group, so it vanishes in every positive degree. In degree one this is Mathlib's groupCohomology.map₁_one.

It also evaluates Mathlib's pullback groupCohomology.mapCocycles₂ of a 2-cocycle along a compatible pair (f, φ) at a pair of group elements, without unfolding the cochain map.

Main statements

• TauCeti.groupCohomology.map_one_succ: the map along the trivial homomorphism vanishes in positive degrees.
• TauCeti.groupCohomology.mapCocycles₂_apply: the value of a pulled-back 2-cocycle.

@[simp]

theorem TauCeti.groupCohomology.map_one_succ {k G : Type u} [CommRing k] [Group G] {H : Type u} [Group H] {B : Rep k H} {C : Rep k G} (φ : Rep.res 1 B ⟶ C) (n : ℕ) : groupCohomology.map 1 φ (n + 1) = 0

The map on cohomology along the trivial homomorphism vanishes in positive degrees, because it factors through the cohomology of the trivial group. In degree one this is Mathlib's groupCohomology.map₁_one.

theorem TauCeti.groupCohomology.mapCocycles₂_apply {k G : Type u} [CommRing k] [Group G] {H : Type u} [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (c : ↥(groupCohomology.cocycles₂ A)) (q : G × G) : ((CategoryTheory.ConcreteCategory.hom (groupCohomology.mapCocycles₂ f φ)) c) q = (Rep.Hom.hom φ) (c (f q.1, f q.2))

The pullback of a 2-cocycle c along a compatible pair (f, φ) takes the value φ (c (f g₁, f g₂)) at (g₁, g₂). Not @[simp]: simp first rewrites the left-hand side by Mathlib's groupCohomology.coe_mapCocycles₂.