Commit 2023-09-15 09:18 31f3bd86

View on Github →

feat: exactness of short complexes (#7052) This PR introduces the definition of a proposition S.Exact when S is a short complex.

Estimated changes

Modified Mathlib.lean

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

added theorem CategoryTheory.ShortComplex.Exact.hasHomology

added theorem CategoryTheory.ShortComplex.Exact.hasZeroObject

added theorem CategoryTheory.ShortComplex.Exact.op

added theorem CategoryTheory.ShortComplex.Exact.unop

added structure CategoryTheory.ShortComplex.Exact

added theorem CategoryTheory.ShortComplex.HomologyData.exact_iff'

added theorem CategoryTheory.ShortComplex.HomologyData.exact_iff

added theorem CategoryTheory.ShortComplex.HomologyData.exact_iff_i_p_zero

added theorem CategoryTheory.ShortComplex.LeftHomologyData.exact_iff

added theorem CategoryTheory.ShortComplex.RightHomologyData.exact_iff

added theorem CategoryTheory.ShortComplex.exact_iff_homology_iso_zero

added theorem CategoryTheory.ShortComplex.exact_iff_isZero_homology

added theorem CategoryTheory.ShortComplex.exact_iff_isZero_leftHomology

added theorem CategoryTheory.ShortComplex.exact_iff_isZero_right_homology

added theorem CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono

added theorem CategoryTheory.ShortComplex.exact_iff_of_iso

added theorem CategoryTheory.ShortComplex.exact_of_isZero_X₂

added theorem CategoryTheory.ShortComplex.exact_of_iso

added theorem CategoryTheory.ShortComplex.exact_op_iff

added theorem CategoryTheory.ShortComplex.exact_unop_iff