Commit 2024-07-17 21:58 13f0f7a8

View on Github →

feat: Functor.mapDerivedCategory is a triangulated functor (#14153) In this PR, it is shown that an exact functor between abelian categories induces a triangulated functor between the corresponding derived categories.

Estimated changes

Modified Mathlib/Algebra/Homology/DerivedCategory/ExactFunctor.lean

Modified Mathlib/CategoryTheory/Localization/Predicate.lean

added theorem CategoryTheory.Localization.Lifting.compLeft_iso

Modified Mathlib/CategoryTheory/Shift/Localization.lean

added theorem CategoryTheory.Functor.commShiftOfLocalization.iso_hom_app

added theorem CategoryTheory.Functor.commShiftOfLocalization.iso_inv_app

added theorem CategoryTheory.Functor.commShiftOfLocalization_iso_hom_app

added theorem CategoryTheory.Functor.commShiftOfLocalization_iso_inv_app

Modified Mathlib/CategoryTheory/Triangulated/Functor.lean

added theorem CategoryTheory.Functor.isTriangulated_iff_of_iso

added theorem CategoryTheory.Functor.isTriangulated_of_iso

added theorem CategoryTheory.Functor.isTriangulated_of_precomp

added theorem CategoryTheory.Functor.isTriangulated_of_precomp_iso

added def CategoryTheory.Functor.mapTriangleIdIso

added theorem CategoryTheory.Functor.mem_mapTriangle_essImage_of_distinguished