Distinguished triangles of triangulated subcategories

Let P be a triangulated subcategory of a pretriangulated category C. A distinguished triangle of C whose first two vertices lie in P is, up to isomorphism, the image of a distinguished triangle of the full subcategory P.FullSubcategory: complete the first morphism to a distinguished triangle of the subcategory, and compare its image with the given triangle along the identities of the first two vertices. In particular its third vertex is isomorphic to an object of the subcategory, even though the given connecting morphism only exists in C.

Main results

• CategoryTheory.ObjectProperty.exists_distTriang_mapTriangle_iso: an ambient distinguished triangle with its first two vertices in P is isomorphic to the image of a distinguished triangle of P.FullSubcategory.

theorem CategoryTheory.ObjectProperty.exists_distTriang_mapTriangle_iso {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulated] {T : Pretriangulated.Triangle C} (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₁ : P T.obj₁) (h₂ : P T.obj₂) : ∃ T' ∈ Pretriangulated.distinguishedTriangles, Nonempty (P.ι.mapTriangle.obj T' ≅ T)

Ambient triangles in a triangulated subcategory: a distinguished triangle of C whose first two vertices lie in P is isomorphic to the image of a distinguished triangle of P.FullSubcategory under the inclusion.