Commit 2024-06-04 08:15 07fd5251

View on Github →

feat(CategoryTheory): localization of pretriangulated categories (#11738) In the new file CategoryTheory.Localization.Triangulated, it is shown that if a class of morphisms W in a pretriangulated category is compatible with the triangulation and has a left calculus of fractions, then the localized category is also pretriangulated.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean

added theorem CategoryTheory.Localization.essSurj_mapArrow

deleted theorem CategoryTheory.Localization.essSurj_mapArrow_of_hasLeftCalculusofFractions

added theorem CategoryTheory.Localization.essSurj_mapArrow_of_hasRightCalculusOfFractions

deleted theorem CategoryTheory.Localization.essSurj_mapArrow_of_hasRightCalculusofFractions

Created Mathlib/CategoryTheory/Localization/Triangulated.lean

added theorem CategoryTheory.Functor.complete_distinguished_essImageDistTriang_morphism

added theorem CategoryTheory.Functor.contractible_mem_essImageDistTriang

added def CategoryTheory.Functor.essImageDistTriang

added theorem CategoryTheory.Functor.essImageDistTriang_mem_of_iso

added theorem CategoryTheory.Functor.rotate_essImageDistTriang

added theorem CategoryTheory.Triangulated.Localization.complete_distinguished_triangle_morphism

added theorem CategoryTheory.Triangulated.Localization.distinguished_cocone_triangle

added def CategoryTheory.Triangulated.Localization.pretriangulated

Modified Mathlib/CategoryTheory/Shift/CommShift.lean

modified theorem CategoryTheory.Functor.map_shiftFunctorComm_hom_app

added theorem CategoryTheory.Functor.map_shiftFunctorCompIsoId_hom_app

added theorem CategoryTheory.Functor.map_shiftFunctorCompIsoId_inv_app

Modified Mathlib/CategoryTheory/Triangulated/Basic.lean

added def CategoryTheory.Pretriangulated.contractibleTriangleFunctor

Modified Mathlib/CategoryTheory/Triangulated/Functor.lean