Commit 2023-10-27 14:12 b65c6a35

View on Github →

feat: the homology of short complexes of abelian groups (#7966)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/ShortComplex/Ab.lean

added def CategoryTheory.ShortComplex.abLeftHomologyData

added theorem CategoryTheory.ShortComplex.abLeftHomologyData_f'

added def CategoryTheory.ShortComplex.abToCycles

added theorem CategoryTheory.ShortComplex.ab_exact_iff

added theorem CategoryTheory.ShortComplex.ab_exact_iff_ker_le_range

added theorem CategoryTheory.ShortComplex.ab_exact_iff_range_eq_ker

added theorem CategoryTheory.ShortComplex.ab_zero_apply

added theorem CategoryTheory.ShortComplex.exact_iff_surjective_abToCycles