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)