Commit 2024-04-18 09:26 1394cf11

View on Github →

feat(CategoryTheory/Localization): the localized category is preadditive (#11728) In this PR, it is shown that if W : MorphismProperty C has a left calculus of fractions and C is preadditive, then the localized category is also preadditive.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean

added theorem CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_eq_map

Created Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean

added theorem CategoryTheory.Localization.Preadditive.add'_assoc

added theorem CategoryTheory.Localization.Preadditive.add'_comm

added theorem CategoryTheory.Localization.Preadditive.add'_comp

added theorem CategoryTheory.Localization.Preadditive.add'_eq

added theorem CategoryTheory.Localization.Preadditive.add'_left_neg'

added theorem CategoryTheory.Localization.Preadditive.add'_map

added theorem CategoryTheory.Localization.Preadditive.add'_zero

added theorem CategoryTheory.Localization.Preadditive.add_comp

added theorem CategoryTheory.Localization.Preadditive.add_eq

added theorem CategoryTheory.Localization.Preadditive.add_eq_add

added theorem CategoryTheory.Localization.Preadditive.comp_add'

added theorem CategoryTheory.Localization.Preadditive.comp_add

added def CategoryTheory.Localization.Preadditive.homEquiv

added theorem CategoryTheory.Localization.Preadditive.map_add

added theorem CategoryTheory.Localization.Preadditive.neg'_eq

added theorem CategoryTheory.Localization.Preadditive.zero_add'

added theorem CategoryTheory.Localization.functor_additive

added def CategoryTheory.MorphismProperty.LeftFraction.neg

added def CategoryTheory.MorphismProperty.LeftFraction₂.add

added theorem CategoryTheory.MorphismProperty.LeftFraction₂.symm_add