Commit 2023-09-14 13:42 1328e6e2

View on Github →

feat: the category of short complexes is preadditive (#7047)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.ShortComplex.LeftHomologyMapData.add

added def CategoryTheory.ShortComplex.LeftHomologyMapData.neg

added theorem CategoryTheory.ShortComplex.add_τ₁

added theorem CategoryTheory.ShortComplex.add_τ₂

added theorem CategoryTheory.ShortComplex.add_τ₃

added theorem CategoryTheory.ShortComplex.cyclesMap'_add

added theorem CategoryTheory.ShortComplex.cyclesMap'_neg

added theorem CategoryTheory.ShortComplex.cyclesMap'_sub

added theorem CategoryTheory.ShortComplex.cyclesMap_add

added theorem CategoryTheory.ShortComplex.cyclesMap_neg

added theorem CategoryTheory.ShortComplex.cyclesMap_sub

added theorem CategoryTheory.ShortComplex.leftHomologyMap'_add

added theorem CategoryTheory.ShortComplex.leftHomologyMap'_neg

added theorem CategoryTheory.ShortComplex.leftHomologyMap'_sub

added theorem CategoryTheory.ShortComplex.leftHomologyMap_add

added theorem CategoryTheory.ShortComplex.leftHomologyMap_neg

added theorem CategoryTheory.ShortComplex.leftHomologyMap_sub

added theorem CategoryTheory.ShortComplex.neg_τ₁

added theorem CategoryTheory.ShortComplex.neg_τ₂

added theorem CategoryTheory.ShortComplex.neg_τ₃

added theorem CategoryTheory.ShortComplex.sub_τ₁

added theorem CategoryTheory.ShortComplex.sub_τ₂

added theorem CategoryTheory.ShortComplex.sub_τ₃