Commit 2024-06-06 14:57 fac35e85

View on Github →

feat(CategoryTheory): localization of triangulated categories (#11786) In this PR, it is shown that the localization of a triangulated category is not only pretriangulated but also triangulated (if the class of morphisms has both calculus of left and right fractions). Pretriangulated and triangulated instances are set on the categories W.Localization and W.Localization'.

Estimated changes

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

added theorem CategoryTheory.Localization.functor_additive_iff

added theorem CategoryTheory.MorphismProperty.LeftFraction₂.map_add

Modified Mathlib/CategoryTheory/Localization/Triangulated.lean

added theorem CategoryTheory.Triangulated.Localization.isTriangulated

Modified Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean

added theorem CategoryTheory.Functor.hasZeroObject_of_additive

Modified Mathlib/CategoryTheory/Shift/Localization.lean

Modified Mathlib/CategoryTheory/Triangulated/Functor.lean

added def CategoryTheory.Triangulated.Octahedron.map

added theorem CategoryTheory.isTriangulated_of_essSurj_mapComposableArrows_two

Modified Mathlib/CategoryTheory/Triangulated/Triangulated.lean

modified def CategoryTheory.Triangulated.Octahedron.ofIso