Theorems · Theorem · group theory

groupCohomology.cochainsMap_comp_assoc

∀ {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) {Z : CochainComplex (ModuleCat k) ℕ}
  (h : groupCohomology.inhomogeneousCochains C ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (groupCohomology.cochainsMap (f.comp g) (CategoryTheory.CategoryStruct.comp (Rep.resMap g φ) ψ)) h =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsMap f φ)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsMap g ψ) h)

Defined in

Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingGroupGroupGroup