Commit 2023-10-20 14:35 1a371eb0

View on Github →

feat: exactness for short complexes coincides with CategoryTheory.Exact (#7280)

Estimated changes

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

added theorem CategoryTheory.ShortComplex.Exact.comp_eq_zero

added theorem CategoryTheory.ShortComplex.Exact.isZero_of_both_zeros

added theorem CategoryTheory.ShortComplex.Exact.map

added theorem CategoryTheory.ShortComplex.Exact.map_of_preservesLeftHomologyOf

added theorem CategoryTheory.ShortComplex.Exact.map_of_preservesRightHomologyOf

added theorem CategoryTheory.ShortComplex.LeftHomologyData.exact_map_iff

added theorem CategoryTheory.ShortComplex.RightHomologyData.exact_map_iff

added theorem CategoryTheory.ShortComplex.exact_iff_iCycles_pOpcycles_zero

added theorem CategoryTheory.ShortComplex.exact_iff_i_p_zero

added theorem CategoryTheory.ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero

added theorem CategoryTheory.ShortComplex.exact_map_iff_of_faithful

added theorem CategoryTheory.exact_iff_shortComplex_exact