Commit 2026-03-02 12:12 2be03bd1

View on Github →

feat(CategoryTheory/Abelian): lemmas for diagram chasing in short complexes (#35930)

Estimated changes

Modified Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean

added theorem CategoryTheory.ShortComplex.add_liftCycles

added theorem CategoryTheory.ShortComplex.sub_liftCycles

Modified Mathlib/CategoryTheory/Abelian/Refinements.lean

added theorem CategoryTheory.Limits.CokernelCofork.IsColimit.comp_π_eq_zero_iff_up_to_refinements

added theorem CategoryTheory.ShortComplex.comp_homologyπ_eq_iff_up_to_refinements

added theorem CategoryTheory.ShortComplex.comp_homologyπ_eq_zero_iff_up_to_refinements

added theorem CategoryTheory.ShortComplex.comp_pOpcycles_eq_zero_iff_up_to_refinements

added theorem CategoryTheory.ShortComplex.epi_homologyMap_iff_up_to_refinements

added theorem CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_iff_up_to_refinements

added theorem CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements

added theorem CategoryTheory.ShortComplex.mono_homologyMap_iff_up_to_refinements