Theorems · Theorem · group theory

groupCohomology.cocyclesMap_comp

∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k K} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k G} (f : H →* K) (g : G →* H)
  (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) (n : ℕ),
  groupCohomology.cocyclesMap (f.comp g) (CategoryTheory.CategoryStruct.comp ((Rep.resFunctor g).map φ) ψ) n =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesMap f φ n) (groupCohomology.cocyclesMap g ψ n)

Defined in

Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Cited by

1 results in Mathlib

Foundations

Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingGroupGroupGroup