theorem GroupCohomology.homology_long_exact_sequence_exact₁ {k : Type u} [CommRing k] {G : Type u} [Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hX : X.ShortExact) {i j : ℕ} (hij : j + 1 = i) : (groupHomology.mapShortComplex₁ hX hij).Exact