Refinements

This file contains lemmas about "refinements" that are specific to the study of the homology of HomologicalComplex. General lemmas about refinements and the case of ShortComplex appear in the file CategoryTheory.Abelian.Refinements.

theorem HomologicalComplex.eq_liftCycles_homologyπ_up_to_refinements {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} (K : HomologicalComplex C c) {A : C} {i : ι} (γ : A ⟶ K.homology i) (j : ι) (hj : c.next i = j) : ∃ (A' : C) (π : A' ⟶ A) (_ : CategoryTheory.Epi π) (z : A' ⟶ K.X i) (hz : CategoryTheory.CategoryStruct.comp z (K.d i j) = 0), CategoryTheory.CategoryStruct.comp π γ = CategoryTheory.CategoryStruct.comp (K.liftCycles z j hj hz) (K.homologyπ i)