Transporting distinguished triangles along isomorphisms of vertices

In a pretriangulated category, the distinguished triangles are closed under isomorphisms of triangles. This file records the two forms used to replace the vertices of a distinguished triangle by isomorphic objects: conjugating all three morphisms along isomorphisms of the three vertices, and replacing only the first vertex.

Main results

• CategoryTheory.Pretriangulated.distinguished_mk_of_iso: a triangle transported along isomorphisms of its three vertices is distinguished.
• CategoryTheory.Pretriangulated.distinguished_mk_of_iso₁: a triangle transported along an isomorphism of its first vertex is distinguished.

theorem CategoryTheory.Pretriangulated.distinguished_mk_of_iso {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {T : Triangle C} (hT : T ∈ distinguishedTriangles) {A₁ A₂ A₃ : C} (e₁ : T.obj₁ ≅ A₁) (e₂ : T.obj₂ ≅ A₂) (e₃ : T.obj₃ ≅ A₃) : Triangle.mk (CategoryStruct.comp e₁.inv (CategoryStruct.comp T.mor₁ e₂.hom)) (CategoryStruct.comp e₂.inv (CategoryStruct.comp T.mor₂ e₃.hom)) (CategoryStruct.comp e₃.inv (CategoryStruct.comp T.mor₃ (e₁.hom⟦1⟧'))) ∈ distinguishedTriangles

Transport along vertex isomorphisms: if T is distinguished and eᵢ : T.objᵢ ≅ Aᵢ, the triangle on A₁, A₂, A₃ with the conjugated morphisms is distinguished.

theorem CategoryTheory.Pretriangulated.distinguished_mk_of_iso₁ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {T : Triangle C} (hT : T ∈ distinguishedTriangles) {A₁ : C} (e₁ : T.obj₁ ≅ A₁) : Triangle.mk (CategoryStruct.comp e₁.inv T.mor₁) T.mor₂ (CategoryStruct.comp T.mor₃ (e₁.hom⟦1⟧')) ∈ distinguishedTriangles

Transport along an isomorphism of the first vertex: if T is distinguished and e₁ : T.obj₁ ≅ A₁, the triangle with first vertex A₁ is distinguished.