Commit 2023-09-15 10:01 740d16ac

View on Github →

feat: the quotient category is preadditive (#7049) It is shown in this PR that when an equivalence relation on morphisms in a preadditive category is compatible with the addition, then the quotient category is preadditive.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory.lean

Modified Mathlib/CategoryTheory/Localization/Construction.lean

Modified Mathlib/CategoryTheory/Quotient.lean

added theorem CategoryTheory.Quotient.compClosure_eq_self

added theorem CategoryTheory.Quotient.compClosure_iff_self

Created Mathlib/CategoryTheory/Quotient/Preadditive.lean

added def CategoryTheory.Quotient.Preadditive.add

added def CategoryTheory.Quotient.Preadditive.neg

added theorem CategoryTheory.Quotient.functor_additive

added def CategoryTheory.Quotient.preadditive

Modified Mathlib/Data/Quot.lean

added theorem Equivalence.quot_mk_eq_iff