Commit 2025-01-12 15:00 296f6b3b

feat(CategoryTheory/Triangulated/Adjunction): the left adjoint of a triangulated functor is triangulated (#20543) If a functor G : D ⥤ C between pretriangulated categories is triangulated, and if we have an adjunction F ⊣ G (that commutes with the shifts), then F is also a triangulated functor. We prove this from the symmetric statement (F triangulated implies G triangulated) using opposite categories.

• depends on: #20363