∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B : Rep k G} (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (groupHomology.map (MonoidHom.id G) f 0) (groupHomology.H0Iso B).hom =
    CategoryTheory.CategoryStruct.comp (groupHomology.H0Iso A).hom ((Rep.coinvariantsFunctor k G).map f)