Theorems · Theorem · group theory

groupHomology.map_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) (n : ℕ),
  groupHomology.map (g.comp f) (CategoryTheory.CategoryStruct.comp φ ((Rep.resFunctor f).map ψ)) n =
    CategoryTheory.CategoryStruct.comp (groupHomology.map f φ n) (groupHomology.map g ψ n)

Defined in

Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingGroupGroupGroup