Theorems · Theorem · group theory

groupHomology.mapShortComplexH2_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 G} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k K} (f : G →* H) (g : H →* K)
  (φ : A ⟶ Rep.res f B) (ψ : B ⟶ Rep.res g C),
  groupHomology.mapShortComplexH2 (g.comp f) (CategoryTheory.CategoryStruct.comp φ ((Rep.resFunctor f).map ψ)) =
    CategoryTheory.CategoryStruct.comp (groupHomology.mapShortComplexH2 f φ) (groupHomology.mapShortComplexH2 g ψ)

Defined in

Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingGroupGroupGroup