Commit 2023-11-10 13:09 27e5b0c1

View on Github →

feat: homology of short complexes of modules (#8174)

Estimated changes

Modified Mathlib.lean

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

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

added theorem CategoryTheory.ShortComplex.Exact.moduleCat_of_range_eq_ker

added theorem CategoryTheory.ShortComplex.Exact.moduleCat_range_eq_ker

added theorem CategoryTheory.ShortComplex.ShortExact.moduleCat_injective_f

added theorem CategoryTheory.ShortComplex.ShortExact.moduleCat_surjective_g

added theorem CategoryTheory.ShortComplex.exact_iff_surjective_moduleCatToCycles

added def CategoryTheory.ShortComplex.moduleCatLeftHomologyData

added theorem CategoryTheory.ShortComplex.moduleCatLeftHomologyData_f'

added def CategoryTheory.ShortComplex.moduleCatMk

added def CategoryTheory.ShortComplex.moduleCatMkOfKerLERange

added def CategoryTheory.ShortComplex.moduleCatToCycles

added theorem CategoryTheory.ShortComplex.moduleCat_exact_iff

added theorem CategoryTheory.ShortComplex.moduleCat_exact_iff_ker_sub_range

added theorem CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker

added theorem CategoryTheory.ShortComplex.moduleCat_zero_apply