∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep k G} {B : Rep k H} (f : G →* H)
  (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) (i : ℕ),
  ModuleCat.Hom.hom ((groupHomology.chainsMap f φ).f i) =
    Finsupp.mapRange.linearMap (ModuleCat.Hom.hom φ.hom) ∘ₗ Finsupp.lmapDomain (↑A.V) k fun x => ⇑f ∘ x