Commit 2023-06-07 10:11 5dce2150

View on Github →

feat: more substantial API for the left homology of short complexes (#4787) This PR continues the development of the API for the left homology of short complexes.

Estimated changes

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

added theorem CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono'_f'

added theorem CategoryTheory.ShortComplex.LeftHomologyData.τ₁_ofEpiOfIsIsoOfMono_f'

added def CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono

added theorem CategoryTheory.ShortComplex.comp_liftCycles

added theorem CategoryTheory.ShortComplex.cycles_ext

added theorem CategoryTheory.ShortComplex.cycles_ext_iff

added theorem CategoryTheory.ShortComplex.hasLeftHomology_of_epi_of_isIso_of_mono'

added theorem CategoryTheory.ShortComplex.hasLeftHomology_of_epi_of_isIso_of_mono

added theorem CategoryTheory.ShortComplex.hasLeftHomology_of_iso

added theorem CategoryTheory.ShortComplex.leftHomology_ext

added theorem CategoryTheory.ShortComplex.leftHomology_ext_iff

added theorem CategoryTheory.ShortComplex.liftCycles_i