Triangles

This file contains the definition of triangles in an additive category with an additive shift. It also defines morphisms between these triangles.

TODO: generalise this to n-angles in n-angulated categories as in https://arxiv.org/abs/1006.4592

structure CategoryTheory.Pretriangulated.Triangle (C : Type u) [Category.{v, u} C] [HasShift C ℤ] : Type (max u v)

A triangle in C is a sextuple (X,Y,Z,f,g,h) where X,Y,Z are objects of C, and f : X ⟶ Y, g : Y ⟶ Z, h : Z ⟶ X⟦1⟧ are morphisms in C.

• mk' :: (
• obj₁ : C

  the first object of a triangle

• obj₂ : C

  the second object of a triangle

• obj₃ : C

  the third object of a triangle

• mor₁ : self.obj₁ ⟶ self.obj₂

  the first morphism of a triangle

• mor₂ : self.obj₂ ⟶ self.obj₃

  the second morphism of a triangle

• mor₃ : self.obj₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj self.obj₁

  the third morphism of a triangle

• )

def CategoryTheory.Pretriangulated.Triangle.mk {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) : Triangle C

A triangle (X,Y,Z,f,g,h) in C is defined by the morphisms f : X ⟶ Y, g : Y ⟶ Z and h : Z ⟶ X⟦1⟧.

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.mk_obj₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) : (mk f g h).obj₁ = X

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.mk_mor₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) : (mk f g h).mor₂ = g

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.mk_mor₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) : (mk f g h).mor₃ = h

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.mk_obj₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) : (mk f g h).obj₃ = Z

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.mk_mor₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) : (mk f g h).mor₁ = f

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.mk_obj₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) : (mk f g h).obj₂ = Y

@[implicit_reducible]

noncomputable instance CategoryTheory.Pretriangulated.instInhabitedTriangle {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] : Inhabited (Triangle C)

noncomputable def CategoryTheory.Pretriangulated.contractibleTriangle {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) : Triangle C

For each object in C, there is a triangle of the form (X,X,0,𝟙 X,0,0)

@[simp]

theorem CategoryTheory.Pretriangulated.contractibleTriangle_obj₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) : (contractibleTriangle X).obj₁ = X

@[simp]

theorem CategoryTheory.Pretriangulated.contractibleTriangle_mor₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) : (contractibleTriangle X).mor₁ = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Pretriangulated.contractibleTriangle_obj₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) : (contractibleTriangle X).obj₂ = X

@[simp]

theorem CategoryTheory.Pretriangulated.contractibleTriangle_mor₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) : (contractibleTriangle X).mor₃ = 0

@[simp]

theorem CategoryTheory.Pretriangulated.contractibleTriangle_mor₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) : (contractibleTriangle X).mor₂ = 0

@[simp]

theorem CategoryTheory.Pretriangulated.contractibleTriangle_obj₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) : (contractibleTriangle X).obj₃ = 0

structure CategoryTheory.Pretriangulated.TriangleMorphism {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (T₁ T₂ : Triangle C) : Type v

A morphism of triangles (X,Y,Z,f,g,h) ⟶ (X',Y',Z',f',g',h') in C is a triple of morphisms a : X ⟶ X', b : Y ⟶ Y', c : Z ⟶ Z' such that a ≫ f' = f ≫ b, b ≫ g' = g ≫ c, and a⟦1⟧' ≫ h = h' ≫ c. In other words, we have a commutative diagram:

     f      g      h
  X  ───> Y  ───> Z  ───> X⟦1⟧
  │       │       │        │
  │a      │b      │c       │a⟦1⟧'
  V       V       V        V
  X' ───> Y' ───> Z' ───> X'⟦1⟧
     f'     g'     h'

• hom₁ : T₁.obj₁ ⟶ T₂.obj₁

  the first morphism in a triangle morphism

• hom₂ : T₁.obj₂ ⟶ T₂.obj₂

  the second morphism in a triangle morphism

• hom₃ : T₁.obj₃ ⟶ T₂.obj₃

  the third morphism in a triangle morphism

• comm₁ : CategoryStruct.comp T₁.mor₁ self.hom₂ = CategoryStruct.comp self.hom₁ T₂.mor₁

  the first commutative square of a triangle morphism

• comm₂ : CategoryStruct.comp T₁.mor₂ self.hom₃ = CategoryStruct.comp self.hom₂ T₂.mor₂

  the second commutative square of a triangle morphism

• comm₃ : CategoryStruct.comp T₁.mor₃ ((shiftFunctor C 1).map self.hom₁) = CategoryStruct.comp self.hom₃ T₂.mor₃

  the third commutative square of a triangle morphism

theorem CategoryTheory.Pretriangulated.TriangleMorphism.ext {C : Type u} {inst✝ : Category.{v, u} C} {inst✝¹ : HasShift C ℤ} {T₁ T₂ : Triangle C} {x y : TriangleMorphism T₁ T₂} (hom₁ : x.hom₁ = y.hom₁) (hom₂ : x.hom₂ = y.hom₂) (hom₃ : x.hom₃ = y.hom₃) : x = y

theorem CategoryTheory.Pretriangulated.TriangleMorphism.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {inst✝¹ : HasShift C ℤ} {T₁ T₂ : Triangle C} {x y : TriangleMorphism T₁ T₂} : x = y ↔ x.hom₁ = y.hom₁ ∧ x.hom₂ = y.hom₂ ∧ x.hom₃ = y.hom₃

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleMorphism.comm₂_assoc {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} (self : TriangleMorphism T₁ T₂) {Z : C} (h : T₂.obj₃ ⟶ Z) : CategoryStruct.comp T₁.mor₂ (CategoryStruct.comp self.hom₃ h) = CategoryStruct.comp self.hom₂ (CategoryStruct.comp T₂.mor₂ h)

the second commutative square of a triangle morphism

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleMorphism.comm₃_assoc {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} (self : TriangleMorphism T₁ T₂) {Z : C} (h : (shiftFunctor C 1).obj T₂.obj₁ ⟶ Z) : CategoryStruct.comp T₁.mor₃ (CategoryStruct.comp ((shiftFunctor C 1).map self.hom₁) h) = CategoryStruct.comp self.hom₃ (CategoryStruct.comp T₂.mor₃ h)

the third commutative square of a triangle morphism

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleMorphism.comm₁_assoc {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} (self : TriangleMorphism T₁ T₂) {Z : C} (h : T₂.obj₂ ⟶ Z) : CategoryStruct.comp T₁.mor₁ (CategoryStruct.comp self.hom₂ h) = CategoryStruct.comp self.hom₁ (CategoryStruct.comp T₂.mor₁ h)

the first commutative square of a triangle morphism

def CategoryTheory.Pretriangulated.triangleMorphismId {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (T : Triangle C) : TriangleMorphism T T

The identity triangle morphism.

@[simp]

theorem CategoryTheory.Pretriangulated.triangleMorphismId_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (T : Triangle C) : (triangleMorphismId T).hom₃ = CategoryStruct.id T.obj₃

@[simp]

theorem CategoryTheory.Pretriangulated.triangleMorphismId_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (T : Triangle C) : (triangleMorphismId T).hom₂ = CategoryStruct.id T.obj₂

@[simp]

theorem CategoryTheory.Pretriangulated.triangleMorphismId_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (T : Triangle C) : (triangleMorphismId T).hom₁ = CategoryStruct.id T.obj₁

@[implicit_reducible]

instance CategoryTheory.Pretriangulated.instInhabitedTriangleMorphism {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (T : Triangle C) : Inhabited (TriangleMorphism T T)

def CategoryTheory.Pretriangulated.TriangleMorphism.comp {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ T₃ : Triangle C} (f : TriangleMorphism T₁ T₂) (g : TriangleMorphism T₂ T₃) : TriangleMorphism T₁ T₃

Composition of triangle morphisms gives a triangle morphism.

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleMorphism.comp_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ T₃ : Triangle C} (f : TriangleMorphism T₁ T₂) (g : TriangleMorphism T₂ T₃) : (f.comp g).hom₁ = CategoryStruct.comp f.hom₁ g.hom₁

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleMorphism.comp_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ T₃ : Triangle C} (f : TriangleMorphism T₁ T₂) (g : TriangleMorphism T₂ T₃) : (f.comp g).hom₃ = CategoryStruct.comp f.hom₃ g.hom₃

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleMorphism.comp_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ T₃ : Triangle C} (f : TriangleMorphism T₁ T₂) (g : TriangleMorphism T₂ T₃) : (f.comp g).hom₂ = CategoryStruct.comp f.hom₂ g.hom₂

@[implicit_reducible]

instance CategoryTheory.Pretriangulated.triangleCategory {C : Type u} [Category.{v, u} C] [HasShift C ℤ] : Category.{v, max u v} (Triangle C)

Triangles with triangle morphisms form a category.

@[simp]

theorem CategoryTheory.Pretriangulated.triangleCategory_comp {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X✝ Y✝ Z✝ : Triangle C} (f : TriangleMorphism X✝ Y✝) (g : TriangleMorphism Y✝ Z✝) : CategoryStruct.comp f g = f.comp g

@[simp]

theorem CategoryTheory.Pretriangulated.triangleCategory_id {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (A : Triangle C) : CategoryStruct.id A = triangleMorphismId A

theorem CategoryTheory.Pretriangulated.Triangle.hom_ext {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Triangle C} (f g : A ⟶ B) (h₁ : f.hom₁ = g.hom₁) (h₂ : f.hom₂ = g.hom₂) (h₃ : f.hom₃ = g.hom₃) : f = g

theorem CategoryTheory.Pretriangulated.Triangle.hom_ext_iff {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Triangle C} {f g : A ⟶ B} : f = g ↔ f.hom₁ = g.hom₁ ∧ f.hom₂ = g.hom₂ ∧ f.hom₃ = g.hom₃

@[simp]

theorem CategoryTheory.Pretriangulated.id_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (A : Triangle C) : (CategoryStruct.id A).hom₁ = CategoryStruct.id A.obj₁

@[simp]

theorem CategoryTheory.Pretriangulated.id_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (A : Triangle C) : (CategoryStruct.id A).hom₂ = CategoryStruct.id A.obj₂

@[simp]

theorem CategoryTheory.Pretriangulated.id_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (A : Triangle C) : (CategoryStruct.id A).hom₃ = CategoryStruct.id A.obj₃

@[simp]

theorem CategoryTheory.Pretriangulated.comp_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryStruct.comp f g).hom₁ = CategoryStruct.comp f.hom₁ g.hom₁

theorem CategoryTheory.Pretriangulated.comp_hom₁_assoc {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Z.obj₁ ⟶ Z✝) : CategoryStruct.comp (CategoryStruct.comp f g).hom₁ h = CategoryStruct.comp f.hom₁ (CategoryStruct.comp g.hom₁ h)

@[simp]

theorem CategoryTheory.Pretriangulated.comp_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryStruct.comp f g).hom₂ = CategoryStruct.comp f.hom₂ g.hom₂

theorem CategoryTheory.Pretriangulated.comp_hom₂_assoc {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Z.obj₂ ⟶ Z✝) : CategoryStruct.comp (CategoryStruct.comp f g).hom₂ h = CategoryStruct.comp f.hom₂ (CategoryStruct.comp g.hom₂ h)

@[simp]

theorem CategoryTheory.Pretriangulated.comp_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryStruct.comp f g).hom₃ = CategoryStruct.comp f.hom₃ g.hom₃

theorem CategoryTheory.Pretriangulated.comp_hom₃_assoc {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X Y Z : Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Z.obj₃ ⟶ Z✝) : CategoryStruct.comp (CategoryStruct.comp f g).hom₃ h = CategoryStruct.comp f.hom₃ (CategoryStruct.comp g.hom₃ h)

def CategoryTheory.Pretriangulated.Triangle.homMk {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (A B : Triangle C) (hom₁ : A.obj₁ ⟶ B.obj₁) (hom₂ : A.obj₂ ⟶ B.obj₂) (hom₃ : A.obj₃ ⟶ B.obj₃) (comm₁ : CategoryStruct.comp A.mor₁ hom₂ = CategoryStruct.comp hom₁ B.mor₁ := by cat_disch) (comm₂ : CategoryStruct.comp A.mor₂ hom₃ = CategoryStruct.comp hom₂ B.mor₂ := by cat_disch) (comm₃ : CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁) = CategoryStruct.comp hom₃ B.mor₃ := by cat_disch) : A ⟶ B

Make a morphism between triangles from the required data.

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.homMk_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (A B : Triangle C) (hom₁ : A.obj₁ ⟶ B.obj₁) (hom₂ : A.obj₂ ⟶ B.obj₂) (hom₃ : A.obj₃ ⟶ B.obj₃) (comm₁ : CategoryStruct.comp A.mor₁ hom₂ = CategoryStruct.comp hom₁ B.mor₁ := by cat_disch) (comm₂ : CategoryStruct.comp A.mor₂ hom₃ = CategoryStruct.comp hom₂ B.mor₂ := by cat_disch) (comm₃ : CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁) = CategoryStruct.comp hom₃ B.mor₃ := by cat_disch) : (A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₃ = hom₃

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.homMk_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (A B : Triangle C) (hom₁ : A.obj₁ ⟶ B.obj₁) (hom₂ : A.obj₂ ⟶ B.obj₂) (hom₃ : A.obj₃ ⟶ B.obj₃) (comm₁ : CategoryStruct.comp A.mor₁ hom₂ = CategoryStruct.comp hom₁ B.mor₁ := by cat_disch) (comm₂ : CategoryStruct.comp A.mor₂ hom₃ = CategoryStruct.comp hom₂ B.mor₂ := by cat_disch) (comm₃ : CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁) = CategoryStruct.comp hom₃ B.mor₃ := by cat_disch) : (A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₁ = hom₁

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.homMk_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (A B : Triangle C) (hom₁ : A.obj₁ ⟶ B.obj₁) (hom₂ : A.obj₂ ⟶ B.obj₂) (hom₃ : A.obj₃ ⟶ B.obj₃) (comm₁ : CategoryStruct.comp A.mor₁ hom₂ = CategoryStruct.comp hom₁ B.mor₁ := by cat_disch) (comm₂ : CategoryStruct.comp A.mor₂ hom₃ = CategoryStruct.comp hom₂ B.mor₂ := by cat_disch) (comm₃ : CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁) = CategoryStruct.comp hom₃ B.mor₃ := by cat_disch) : (A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₂ = hom₂

def CategoryTheory.Pretriangulated.Triangle.isoMk {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (A B : Triangle C) (iso₁ : A.obj₁ ≅ B.obj₁) (iso₂ : A.obj₂ ≅ B.obj₂) (iso₃ : A.obj₃ ≅ B.obj₃) (comm₁ : CategoryStruct.comp A.mor₁ iso₂.hom = CategoryStruct.comp iso₁.hom B.mor₁ := by cat_disch) (comm₂ : CategoryStruct.comp A.mor₂ iso₃.hom = CategoryStruct.comp iso₂.hom B.mor₂ := by cat_disch) (comm₃ : CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map iso₁.hom) = CategoryStruct.comp iso₃.hom B.mor₃ := by cat_disch) : A ≅ B

Make an isomorphism between triangles from the required data.

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.isoMk_inv {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (A B : Triangle C) (iso₁ : A.obj₁ ≅ B.obj₁) (iso₂ : A.obj₂ ≅ B.obj₂) (iso₃ : A.obj₃ ≅ B.obj₃) (comm₁ : CategoryStruct.comp A.mor₁ iso₂.hom = CategoryStruct.comp iso₁.hom B.mor₁ := by cat_disch) (comm₂ : CategoryStruct.comp A.mor₂ iso₃.hom = CategoryStruct.comp iso₂.hom B.mor₂ := by cat_disch) (comm₃ : CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map iso₁.hom) = CategoryStruct.comp iso₃.hom B.mor₃ := by cat_disch) : (A.isoMk B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).inv = B.homMk A iso₁.inv iso₂.inv iso₃.inv ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.isoMk_hom {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (A B : Triangle C) (iso₁ : A.obj₁ ≅ B.obj₁) (iso₂ : A.obj₂ ≅ B.obj₂) (iso₃ : A.obj₃ ≅ B.obj₃) (comm₁ : CategoryStruct.comp A.mor₁ iso₂.hom = CategoryStruct.comp iso₁.hom B.mor₁ := by cat_disch) (comm₂ : CategoryStruct.comp A.mor₂ iso₃.hom = CategoryStruct.comp iso₂.hom B.mor₂ := by cat_disch) (comm₃ : CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map iso₁.hom) = CategoryStruct.comp iso₃.hom B.mor₃ := by cat_disch) : (A.isoMk B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).hom = A.homMk B iso₁.hom iso₂.hom iso₃.hom comm₁ comm₂ comm₃

theorem CategoryTheory.Pretriangulated.Triangle.isIso_of_isIsos {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Triangle C} (f : A ⟶ B) (h₁ : IsIso f.hom₁) (h₂ : IsIso f.hom₂) (h₃ : IsIso f.hom₃) : IsIso f

@[simp]

theorem CategoryTheory.Iso.hom_inv_id_triangle_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Pretriangulated.Triangle C} (e : A ≅ B) : CategoryStruct.comp e.hom.hom₁ e.inv.hom₁ = CategoryStruct.id A.obj₁

@[simp]

theorem CategoryTheory.Iso.hom_inv_id_triangle_hom₁_assoc {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Pretriangulated.Triangle C} (e : A ≅ B) {Z : C} (h : A.obj₁ ⟶ Z) : CategoryStruct.comp e.hom.hom₁ (CategoryStruct.comp e.inv.hom₁ h) = h

@[simp]

theorem CategoryTheory.Iso.hom_inv_id_triangle_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Pretriangulated.Triangle C} (e : A ≅ B) : CategoryStruct.comp e.hom.hom₂ e.inv.hom₂ = CategoryStruct.id A.obj₂

@[simp]

theorem CategoryTheory.Iso.hom_inv_id_triangle_hom₂_assoc {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Pretriangulated.Triangle C} (e : A ≅ B) {Z : C} (h : A.obj₂ ⟶ Z) : CategoryStruct.comp e.hom.hom₂ (CategoryStruct.comp e.inv.hom₂ h) = h

@[simp]

theorem CategoryTheory.Iso.hom_inv_id_triangle_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Pretriangulated.Triangle C} (e : A ≅ B) : CategoryStruct.comp e.hom.hom₃ e.inv.hom₃ = CategoryStruct.id A.obj₃

@[simp]

theorem CategoryTheory.Iso.hom_inv_id_triangle_hom₃_assoc {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Pretriangulated.Triangle C} (e : A ≅ B) {Z : C} (h : A.obj₃ ⟶ Z) : CategoryStruct.comp e.hom.hom₃ (CategoryStruct.comp e.inv.hom₃ h) = h

@[simp]

theorem CategoryTheory.Iso.inv_hom_id_triangle_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Pretriangulated.Triangle C} (e : A ≅ B) : CategoryStruct.comp e.inv.hom₁ e.hom.hom₁ = CategoryStruct.id B.obj₁

@[simp]

theorem CategoryTheory.Iso.inv_hom_id_triangle_hom₁_assoc {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Pretriangulated.Triangle C} (e : A ≅ B) {Z : C} (h : B.obj₁ ⟶ Z) : CategoryStruct.comp e.inv.hom₁ (CategoryStruct.comp e.hom.hom₁ h) = h

@[simp]

theorem CategoryTheory.Iso.inv_hom_id_triangle_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Pretriangulated.Triangle C} (e : A ≅ B) : CategoryStruct.comp e.inv.hom₂ e.hom.hom₂ = CategoryStruct.id B.obj₂

@[simp]

theorem CategoryTheory.Iso.inv_hom_id_triangle_hom₂_assoc {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Pretriangulated.Triangle C} (e : A ≅ B) {Z : C} (h : B.obj₂ ⟶ Z) : CategoryStruct.comp e.inv.hom₂ (CategoryStruct.comp e.hom.hom₂ h) = h

@[simp]

theorem CategoryTheory.Iso.inv_hom_id_triangle_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Pretriangulated.Triangle C} (e : A ≅ B) : CategoryStruct.comp e.inv.hom₃ e.hom.hom₃ = CategoryStruct.id B.obj₃

@[simp]

theorem CategoryTheory.Iso.inv_hom_id_triangle_hom₃_assoc {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Pretriangulated.Triangle C} (e : A ≅ B) {Z : C} (h : B.obj₃ ⟶ Z) : CategoryStruct.comp e.inv.hom₃ (CategoryStruct.comp e.hom.hom₃ h) = h

theorem CategoryTheory.Pretriangulated.Triangle.eqToHom_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Triangle C} (h : A = B) : (eqToHom h).hom₁ = eqToHom ⋯

theorem CategoryTheory.Pretriangulated.Triangle.eqToHom_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Triangle C} (h : A = B) : (eqToHom h).hom₂ = eqToHom ⋯

theorem CategoryTheory.Pretriangulated.Triangle.eqToHom_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Triangle C} (h : A = B) : (eqToHom h).hom₃ = eqToHom ⋯

@[implicit_reducible]

instance CategoryTheory.Pretriangulated.Triangle.instZeroHom {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] : Zero (T₁ ⟶ T₂)

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.zero_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] : TriangleMorphism.hom₃ 0 = 0

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.zero_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] : TriangleMorphism.hom₁ 0 = 0

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.zero_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] : TriangleMorphism.hom₂ 0 = 0

@[implicit_reducible]

instance CategoryTheory.Pretriangulated.Triangle.instAddHom {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] : Add (T₁ ⟶ T₂)

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.add_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f g : T₁ ⟶ T₂) : (f + g).hom₁ = f.hom₁ + g.hom₁

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.add_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f g : T₁ ⟶ T₂) : (f + g).hom₂ = f.hom₂ + g.hom₂

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.add_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f g : T₁ ⟶ T₂) : (f + g).hom₃ = f.hom₃ + g.hom₃

@[implicit_reducible]

instance CategoryTheory.Pretriangulated.Triangle.instNegHom {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] : Neg (T₁ ⟶ T₂)

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.neg_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f : T₁ ⟶ T₂) : (-f).hom₃ = -f.hom₃

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.neg_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f : T₁ ⟶ T₂) : (-f).hom₂ = -f.hom₂

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.neg_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f : T₁ ⟶ T₂) : (-f).hom₁ = -f.hom₁

@[implicit_reducible]

instance CategoryTheory.Pretriangulated.Triangle.instSubHom {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] : Sub (T₁ ⟶ T₂)

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.sub_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f g : T₁ ⟶ T₂) : (f - g).hom₂ = f.hom₂ - g.hom₂

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.sub_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f g : T₁ ⟶ T₂) : (f - g).hom₃ = f.hom₃ - g.hom₃

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.sub_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f g : T₁ ⟶ T₂) : (f - g).hom₁ = f.hom₁ - g.hom₁

@[implicit_reducible]

instance CategoryTheory.Pretriangulated.Triangle.instSMulHom {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] {R : Type u_1} [Semiring R] [Linear R C] [∀ (n : ℤ), Functor.Linear R (CategoryTheory.shiftFunctor C n)] : SMul R (T₁ ⟶ T₂)

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.smul_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] {R : Type u_1} [Semiring R] [Linear R C] [∀ (n : ℤ), Functor.Linear R (CategoryTheory.shiftFunctor C n)] (n : R) (f : T₁ ⟶ T₂) : (n • f).hom₁ = n • f.hom₁

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.smul_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] {R : Type u_1} [Semiring R] [Linear R C] [∀ (n : ℤ), Functor.Linear R (CategoryTheory.shiftFunctor C n)] (n : R) (f : T₁ ⟶ T₂) : (n • f).hom₂ = n • f.hom₂

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.smul_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] {R : Type u_1} [Semiring R] [Linear R C] [∀ (n : ℤ), Functor.Linear R (CategoryTheory.shiftFunctor C n)] (n : R) (f : T₁ ⟶ T₂) : (n • f).hom₃ = n • f.hom₃

@[implicit_reducible]

instance CategoryTheory.Pretriangulated.Triangle.instAddCommGroupHom {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] : AddCommGroup (T₁ ⟶ T₂)

@[implicit_reducible]

instance CategoryTheory.Pretriangulated.Triangle.instPreadditive {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] : Preadditive (Triangle C)

@[implicit_reducible]

instance CategoryTheory.Pretriangulated.Triangle.instModuleHom {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {T₁ T₂ : Triangle C} [Preadditive C] {R : Type u_1} [Semiring R] [Linear R C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), Functor.Linear R (CategoryTheory.shiftFunctor C n)] : Module R (T₁ ⟶ T₂)

@[implicit_reducible]

instance CategoryTheory.Pretriangulated.Triangle.instLinear {C : Type u} [Category.{v, u} C] [HasShift C ℤ] [Preadditive C] {R : Type u_1} [Semiring R] [Linear R C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), Functor.Linear R (CategoryTheory.shiftFunctor C n)] : Linear R (Triangle C)

noncomputable def CategoryTheory.Pretriangulated.binaryBiproductTriangle {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproduct X₁ X₂] : Triangle C

The obvious triangle X₁ ⟶ X₁ ⊞ X₂ ⟶ X₂ ⟶ X₁⟦1⟧.

@[simp]

theorem CategoryTheory.Pretriangulated.binaryBiproductTriangle_obj₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproduct X₁ X₂] : (binaryBiproductTriangle X₁ X₂).obj₁ = X₁

@[simp]

theorem CategoryTheory.Pretriangulated.binaryBiproductTriangle_mor₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproduct X₁ X₂] : (binaryBiproductTriangle X₁ X₂).mor₃ = 0

@[simp]

theorem CategoryTheory.Pretriangulated.binaryBiproductTriangle_mor₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproduct X₁ X₂] : (binaryBiproductTriangle X₁ X₂).mor₂ = Limits.biprod.snd

@[simp]

theorem CategoryTheory.Pretriangulated.binaryBiproductTriangle_obj₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproduct X₁ X₂] : (binaryBiproductTriangle X₁ X₂).obj₃ = X₂

@[simp]

theorem CategoryTheory.Pretriangulated.binaryBiproductTriangle_mor₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproduct X₁ X₂] : (binaryBiproductTriangle X₁ X₂).mor₁ = Limits.biprod.inl

@[simp]

theorem CategoryTheory.Pretriangulated.binaryBiproductTriangle_obj₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproduct X₁ X₂] : (binaryBiproductTriangle X₁ X₂).obj₂ = (X₁ ⊞ X₂)

noncomputable def CategoryTheory.Pretriangulated.binaryProductTriangle {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryProduct X₁ X₂] : Triangle C

The obvious triangle X₁ ⟶ X₁ ⨯ X₂ ⟶ X₂ ⟶ X₁⟦1⟧.

@[simp]

theorem CategoryTheory.Pretriangulated.binaryProductTriangle_obj₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryProduct X₁ X₂] : (binaryProductTriangle X₁ X₂).obj₃ = X₂

@[simp]

theorem CategoryTheory.Pretriangulated.binaryProductTriangle_mor₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryProduct X₁ X₂] : (binaryProductTriangle X₁ X₂).mor₁ = Limits.prod.lift (CategoryStruct.id X₁) 0

@[simp]

theorem CategoryTheory.Pretriangulated.binaryProductTriangle_mor₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryProduct X₁ X₂] : (binaryProductTriangle X₁ X₂).mor₃ = 0

@[simp]

theorem CategoryTheory.Pretriangulated.binaryProductTriangle_mor₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryProduct X₁ X₂] : (binaryProductTriangle X₁ X₂).mor₂ = Limits.prod.snd

@[simp]

theorem CategoryTheory.Pretriangulated.binaryProductTriangle_obj₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryProduct X₁ X₂] : (binaryProductTriangle X₁ X₂).obj₂ = (X₁ ⨯ X₂)

@[simp]

theorem CategoryTheory.Pretriangulated.binaryProductTriangle_obj₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryProduct X₁ X₂] : (binaryProductTriangle X₁ X₂).obj₁ = X₁

noncomputable def CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproduct X₁ X₂] : binaryProductTriangle X₁ X₂ ≅ binaryBiproductTriangle X₁ X₂

The canonical isomorphism of triangles binaryProductTriangle X₁ X₂ ≅ binaryBiproductTriangle X₁ X₂.

@[simp]

theorem CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproduct X₁ X₂] : (binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).inv.hom₁ = CategoryStruct.id X₁

@[simp]

theorem CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproduct X₁ X₂] : (binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).inv.hom₂ = Limits.prod.lift Limits.biprod.fst Limits.biprod.snd

@[simp]

theorem CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproduct X₁ X₂] : (binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).hom.hom₁ = CategoryStruct.id X₁

@[simp]

theorem CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproduct X₁ X₂] : (binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).inv.hom₃ = CategoryStruct.id X₂

@[simp]

theorem CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproduct X₁ X₂] : (binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).hom.hom₃ = CategoryStruct.id X₂

@[simp]

theorem CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (X₁ X₂ : C) [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproduct X₁ X₂] : (binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).hom.hom₂ = Limits.biprod.lift Limits.prod.fst Limits.prod.snd

noncomputable def CategoryTheory.Pretriangulated.productTriangle {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] : Triangle C

The product of a family of triangles.

@[simp]

theorem CategoryTheory.Pretriangulated.productTriangle_mor₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] : (productTriangle T).mor₁ = Limits.Pi.map fun (j : J) => (T j).mor₁

@[simp]

theorem CategoryTheory.Pretriangulated.productTriangle_obj₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] : (productTriangle T).obj₁ = ∏ᶜ fun (j : J) => (T j).obj₁

@[simp]

theorem CategoryTheory.Pretriangulated.productTriangle_obj₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] : (productTriangle T).obj₃ = ∏ᶜ fun (j : J) => (T j).obj₃

@[simp]

theorem CategoryTheory.Pretriangulated.productTriangle_obj₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] : (productTriangle T).obj₂ = ∏ᶜ fun (j : J) => (T j).obj₂

@[simp]

theorem CategoryTheory.Pretriangulated.productTriangle_mor₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] : (productTriangle T).mor₂ = Limits.Pi.map fun (j : J) => (T j).mor₂

@[simp]

theorem CategoryTheory.Pretriangulated.productTriangle_mor₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] : (productTriangle T).mor₃ = CategoryStruct.comp (Limits.Pi.map fun (j : J) => (T j).mor₃) (inv (Limits.piComparison (shiftFunctor C 1) fun (j : J) => (T j).obj₁))

noncomputable def CategoryTheory.Pretriangulated.productTriangle.π {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] (j : J) : productTriangle T ⟶ T j

A projection from the product of a family of triangles.

@[simp]

theorem CategoryTheory.Pretriangulated.productTriangle.π_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] (j : J) : (π T j).hom₁ = Limits.Pi.π (fun (j : J) => (T j).obj₁) j

@[simp]

theorem CategoryTheory.Pretriangulated.productTriangle.π_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] (j : J) : (π T j).hom₂ = Limits.Pi.π (fun (j : J) => (T j).obj₂) j

@[simp]

theorem CategoryTheory.Pretriangulated.productTriangle.π_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] (j : J) : (π T j).hom₃ = Limits.Pi.π (fun (j : J) => (T j).obj₃) j

noncomputable def CategoryTheory.Pretriangulated.productTriangle.fan {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] : Limits.Fan T

The fan given by productTriangle T.

noncomputable def CategoryTheory.Pretriangulated.productTriangle.lift {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] {T' : Triangle C} (φ : (j : J) → T' ⟶ T j) : T' ⟶ productTriangle T

A family of morphisms T' ⟶ T j lifts to a morphism T' ⟶ productTriangle T.

@[simp]

theorem CategoryTheory.Pretriangulated.productTriangle.lift_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] {T' : Triangle C} (φ : (j : J) → T' ⟶ T j) : (lift T φ).hom₃ = Limits.Pi.lift fun (j : J) => (φ j).hom₃

@[simp]

theorem CategoryTheory.Pretriangulated.productTriangle.lift_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] {T' : Triangle C} (φ : (j : J) → T' ⟶ T j) : (lift T φ).hom₁ = Limits.Pi.lift fun (j : J) => (φ j).hom₁

@[simp]

theorem CategoryTheory.Pretriangulated.productTriangle.lift_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] {T' : Triangle C} (φ : (j : J) → T' ⟶ T j) : (lift T φ).hom₂ = Limits.Pi.lift fun (j : J) => (φ j).hom₂

noncomputable def CategoryTheory.Pretriangulated.productTriangle.isLimitFan {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] : Limits.IsLimit (fan T)

The triangle productTriangle T satisfies the universal property of the categorical product of the triangles T.

theorem CategoryTheory.Pretriangulated.productTriangle.zero₃₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} (T : J → Triangle C) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] [Limits.HasZeroMorphisms C] (h : ∀ (j : J), CategoryStruct.comp (T j).mor₃ ((shiftFunctor C 1).map (T j).mor₁) = 0) : CategoryStruct.comp (productTriangle T).mor₃ ((shiftFunctor C 1).map (productTriangle T).mor₁) = 0

noncomputable def CategoryTheory.Pretriangulated.contractibleTriangleFunctor (C : Type u) [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] : Functor C (Triangle C)

The functor C ⥤ Triangle C which sends X to contractibleTriangle X.

@[simp]

theorem CategoryTheory.Pretriangulated.contractibleTriangleFunctor_map_hom₁ (C : Type u) [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((contractibleTriangleFunctor C).map f).hom₁ = f

@[simp]

theorem CategoryTheory.Pretriangulated.contractibleTriangleFunctor_map_hom₂ (C : Type u) [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((contractibleTriangleFunctor C).map f).hom₂ = f

@[simp]

theorem CategoryTheory.Pretriangulated.contractibleTriangleFunctor_map_hom₃ (C : Type u) [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((contractibleTriangleFunctor C).map f).hom₃ = 0

@[simp]

theorem CategoryTheory.Pretriangulated.contractibleTriangleFunctor_obj (C : Type u) [Category.{v, u} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] (X : C) : (contractibleTriangleFunctor C).obj X = contractibleTriangle X

def CategoryTheory.Pretriangulated.Triangle.π₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] : Functor (Triangle C) C

The first projection Triangle C ⥤ C.

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.π₁_map {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) : π₁.map f = f.hom₁

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.π₁_obj {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (T : Triangle C) : π₁.obj T = T.obj₁

def CategoryTheory.Pretriangulated.Triangle.π₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] : Functor (Triangle C) C

The second projection Triangle C ⥤ C.

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.π₂_obj {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (T : Triangle C) : π₂.obj T = T.obj₂

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.π₂_map {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) : π₂.map f = f.hom₂

def CategoryTheory.Pretriangulated.Triangle.π₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] : Functor (Triangle C) C

The third projection Triangle C ⥤ C.

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.π₃_map {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {X✝ Y✝ : Triangle C} (f : X✝ ⟶ Y✝) : π₃.map f = f.hom₃

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.π₃_obj {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (T : Triangle C) : π₃.obj T = T.obj₃

def CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] : π₁ ⟶ π₂

The first morphism of a triangle, as a natural transformation π₁ ⟶ π₂.

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂_app {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (T : Triangle C) : π₁Toπ₂.app T = T.mor₁

def CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] : π₂ ⟶ π₃

The second morphism of a triangle, as a natural transformation π₂ ⟶ π₃.

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃_app {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (T : Triangle C) : π₂Toπ₃.app T = T.mor₂

def CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] : π₃ ⟶ π₁.comp (CategoryTheory.shiftFunctor C 1)

The third morphism of a triangle, as a natural transformation π₃ ⟶ π₁ ⋙ shiftFunctor _ (1 : ℤ).

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁_app {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (T : Triangle C) : π₃Toπ₁.app T = T.mor₃

instance CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Triangle C} (φ : A ⟶ B) [IsIso φ] : IsIso φ.hom₁

instance CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Triangle C} (φ : A ⟶ B) [IsIso φ] : IsIso φ.hom₂

instance CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {A B : Triangle C} (φ : A ⟶ B) [IsIso φ] : IsIso φ.hom₃

def CategoryTheory.Pretriangulated.Triangle.functorMk {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : Functor J C} (mor₁ : obj₁ ⟶ obj₂) (mor₂ : obj₂ ⟶ obj₃) (mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)) : Functor J (Triangle C)

Constructor for functors to the category of triangles.

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorMk_map_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : Functor J C} (mor₁ : obj₁ ⟶ obj₂) (mor₂ : obj₂ ⟶ obj₃) (mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)) {X✝ Y✝ : J} (φ : X✝ ⟶ Y✝) : ((functorMk mor₁ mor₂ mor₃).map φ).hom₂ = obj₂.map φ

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorMk_map_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : Functor J C} (mor₁ : obj₁ ⟶ obj₂) (mor₂ : obj₂ ⟶ obj₃) (mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)) {X✝ Y✝ : J} (φ : X✝ ⟶ Y✝) : ((functorMk mor₁ mor₂ mor₃).map φ).hom₃ = obj₃.map φ

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorMk_obj {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : Functor J C} (mor₁ : obj₁ ⟶ obj₂) (mor₂ : obj₂ ⟶ obj₃) (mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)) (j : J) : (functorMk mor₁ mor₂ mor₃).obj j = mk (mor₁.app j) (mor₂.app j) (mor₃.app j)

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorMk_map_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : Functor J C} (mor₁ : obj₁ ⟶ obj₂) (mor₂ : obj₂ ⟶ obj₃) (mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)) {X✝ Y✝ : J} (φ : X✝ ⟶ Y✝) : ((functorMk mor₁ mor₂ mor₃).map φ).hom₁ = obj₁.map φ

def CategoryTheory.Pretriangulated.Triangle.functorHomMk {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] (A B : Functor J (Triangle C)) (hom₁ : A.comp π₁ ⟶ B.comp π₁) (hom₂ : A.comp π₂ ⟶ B.comp π₂) (hom₃ : A.comp π₃ ⟶ B.comp π₃) (comm₁ : CategoryStruct.comp (A.whiskerLeft π₁Toπ₂) hom₂ = CategoryStruct.comp hom₁ (B.whiskerLeft π₁Toπ₂) := by cat_disch) (comm₂ : CategoryStruct.comp (A.whiskerLeft π₂Toπ₃) hom₃ = CategoryStruct.comp hom₂ (B.whiskerLeft π₂Toπ₃) := by cat_disch) (comm₃ : CategoryStruct.comp (A.whiskerLeft π₃Toπ₁) (Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp hom₃ (B.whiskerLeft π₃Toπ₁) := by cat_disch) : A ⟶ B

Constructor for natural transformations between functors to the category of triangles.

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorHomMk_app_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] (A B : Functor J (Triangle C)) (hom₁ : A.comp π₁ ⟶ B.comp π₁) (hom₂ : A.comp π₂ ⟶ B.comp π₂) (hom₃ : A.comp π₃ ⟶ B.comp π₃) (comm₁ : CategoryStruct.comp (A.whiskerLeft π₁Toπ₂) hom₂ = CategoryStruct.comp hom₁ (B.whiskerLeft π₁Toπ₂) := by cat_disch) (comm₂ : CategoryStruct.comp (A.whiskerLeft π₂Toπ₃) hom₃ = CategoryStruct.comp hom₂ (B.whiskerLeft π₂Toπ₃) := by cat_disch) (comm₃ : CategoryStruct.comp (A.whiskerLeft π₃Toπ₁) (Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp hom₃ (B.whiskerLeft π₃Toπ₁) := by cat_disch) (j : J) : ((functorHomMk A B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).app j).hom₃ = hom₃.app j

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorHomMk_app_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] (A B : Functor J (Triangle C)) (hom₁ : A.comp π₁ ⟶ B.comp π₁) (hom₂ : A.comp π₂ ⟶ B.comp π₂) (hom₃ : A.comp π₃ ⟶ B.comp π₃) (comm₁ : CategoryStruct.comp (A.whiskerLeft π₁Toπ₂) hom₂ = CategoryStruct.comp hom₁ (B.whiskerLeft π₁Toπ₂) := by cat_disch) (comm₂ : CategoryStruct.comp (A.whiskerLeft π₂Toπ₃) hom₃ = CategoryStruct.comp hom₂ (B.whiskerLeft π₂Toπ₃) := by cat_disch) (comm₃ : CategoryStruct.comp (A.whiskerLeft π₃Toπ₁) (Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp hom₃ (B.whiskerLeft π₃Toπ₁) := by cat_disch) (j : J) : ((functorHomMk A B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).app j).hom₁ = hom₁.app j

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorHomMk_app_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] (A B : Functor J (Triangle C)) (hom₁ : A.comp π₁ ⟶ B.comp π₁) (hom₂ : A.comp π₂ ⟶ B.comp π₂) (hom₃ : A.comp π₃ ⟶ B.comp π₃) (comm₁ : CategoryStruct.comp (A.whiskerLeft π₁Toπ₂) hom₂ = CategoryStruct.comp hom₁ (B.whiskerLeft π₁Toπ₂) := by cat_disch) (comm₂ : CategoryStruct.comp (A.whiskerLeft π₂Toπ₃) hom₃ = CategoryStruct.comp hom₂ (B.whiskerLeft π₂Toπ₃) := by cat_disch) (comm₃ : CategoryStruct.comp (A.whiskerLeft π₃Toπ₁) (Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp hom₃ (B.whiskerLeft π₃Toπ₁) := by cat_disch) (j : J) : ((functorHomMk A B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).app j).hom₂ = hom₂.app j

def CategoryTheory.Pretriangulated.Triangle.functorHomMk' {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : Functor J C} {mor₁ : obj₁ ⟶ obj₂} {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)} {obj₁' obj₂' obj₃' : Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'} {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (hom₁ : obj₁ ⟶ obj₁') (hom₂ : obj₂ ⟶ obj₂') (hom₃ : obj₃ ⟶ obj₃') (comm₁ : CategoryStruct.comp mor₁ hom₂ = CategoryStruct.comp hom₁ mor₁') (comm₂ : CategoryStruct.comp mor₂ hom₃ = CategoryStruct.comp hom₂ mor₂') (comm₃ : CategoryStruct.comp mor₃ (Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp hom₃ mor₃') : functorMk mor₁ mor₂ mor₃ ⟶ functorMk mor₁' mor₂' mor₃'

Constructor for natural transformations between functors constructed with functorMk.

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorHomMk'_app_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : Functor J C} {mor₁ : obj₁ ⟶ obj₂} {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)} {obj₁' obj₂' obj₃' : Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'} {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (hom₁ : obj₁ ⟶ obj₁') (hom₂ : obj₂ ⟶ obj₂') (hom₃ : obj₃ ⟶ obj₃') (comm₁ : CategoryStruct.comp mor₁ hom₂ = CategoryStruct.comp hom₁ mor₁') (comm₂ : CategoryStruct.comp mor₂ hom₃ = CategoryStruct.comp hom₂ mor₂') (comm₃ : CategoryStruct.comp mor₃ (Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp hom₃ mor₃') (j : J) : ((functorHomMk' hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).app j).hom₁ = hom₁.app j

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorHomMk'_app_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : Functor J C} {mor₁ : obj₁ ⟶ obj₂} {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)} {obj₁' obj₂' obj₃' : Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'} {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (hom₁ : obj₁ ⟶ obj₁') (hom₂ : obj₂ ⟶ obj₂') (hom₃ : obj₃ ⟶ obj₃') (comm₁ : CategoryStruct.comp mor₁ hom₂ = CategoryStruct.comp hom₁ mor₁') (comm₂ : CategoryStruct.comp mor₂ hom₃ = CategoryStruct.comp hom₂ mor₂') (comm₃ : CategoryStruct.comp mor₃ (Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp hom₃ mor₃') (j : J) : ((functorHomMk' hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).app j).hom₂ = hom₂.app j

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorHomMk'_app_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : Functor J C} {mor₁ : obj₁ ⟶ obj₂} {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)} {obj₁' obj₂' obj₃' : Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'} {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (hom₁ : obj₁ ⟶ obj₁') (hom₂ : obj₂ ⟶ obj₂') (hom₃ : obj₃ ⟶ obj₃') (comm₁ : CategoryStruct.comp mor₁ hom₂ = CategoryStruct.comp hom₁ mor₁') (comm₂ : CategoryStruct.comp mor₂ hom₃ = CategoryStruct.comp hom₂ mor₂') (comm₃ : CategoryStruct.comp mor₃ (Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp hom₃ mor₃') (j : J) : ((functorHomMk' hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).app j).hom₃ = hom₃.app j

def CategoryTheory.Pretriangulated.Triangle.functorIsoMk {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] (A B : Functor J (Triangle C)) (iso₁ : A.comp π₁ ≅ B.comp π₁) (iso₂ : A.comp π₂ ≅ B.comp π₂) (iso₃ : A.comp π₃ ≅ B.comp π₃) (comm₁ : CategoryStruct.comp (A.whiskerLeft π₁Toπ₂) iso₂.hom = CategoryStruct.comp iso₁.hom (B.whiskerLeft π₁Toπ₂)) (comm₂ : CategoryStruct.comp (A.whiskerLeft π₂Toπ₃) iso₃.hom = CategoryStruct.comp iso₂.hom (B.whiskerLeft π₂Toπ₃)) (comm₃ : CategoryStruct.comp (A.whiskerLeft π₃Toπ₁) (Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp iso₃.hom (B.whiskerLeft π₃Toπ₁)) : A ≅ B

Constructor for natural isomorphisms between functors to the category of triangles.

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorIsoMk_inv {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] (A B : Functor J (Triangle C)) (iso₁ : A.comp π₁ ≅ B.comp π₁) (iso₂ : A.comp π₂ ≅ B.comp π₂) (iso₃ : A.comp π₃ ≅ B.comp π₃) (comm₁ : CategoryStruct.comp (A.whiskerLeft π₁Toπ₂) iso₂.hom = CategoryStruct.comp iso₁.hom (B.whiskerLeft π₁Toπ₂)) (comm₂ : CategoryStruct.comp (A.whiskerLeft π₂Toπ₃) iso₃.hom = CategoryStruct.comp iso₂.hom (B.whiskerLeft π₂Toπ₃)) (comm₃ : CategoryStruct.comp (A.whiskerLeft π₃Toπ₁) (Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp iso₃.hom (B.whiskerLeft π₃Toπ₁)) : (functorIsoMk A B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).inv = functorHomMk B A iso₁.inv iso₂.inv iso₃.inv ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorIsoMk_hom {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] (A B : Functor J (Triangle C)) (iso₁ : A.comp π₁ ≅ B.comp π₁) (iso₂ : A.comp π₂ ≅ B.comp π₂) (iso₃ : A.comp π₃ ≅ B.comp π₃) (comm₁ : CategoryStruct.comp (A.whiskerLeft π₁Toπ₂) iso₂.hom = CategoryStruct.comp iso₁.hom (B.whiskerLeft π₁Toπ₂)) (comm₂ : CategoryStruct.comp (A.whiskerLeft π₂Toπ₃) iso₃.hom = CategoryStruct.comp iso₂.hom (B.whiskerLeft π₂Toπ₃)) (comm₃ : CategoryStruct.comp (A.whiskerLeft π₃Toπ₁) (Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp iso₃.hom (B.whiskerLeft π₃Toπ₁)) : (functorIsoMk A B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).hom = functorHomMk A B iso₁.hom iso₂.hom iso₃.hom comm₁ comm₂ comm₃

def CategoryTheory.Pretriangulated.Triangle.functorIsoMk' {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : Functor J C} {mor₁ : obj₁ ⟶ obj₂} {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)} {obj₁' obj₂' obj₃' : Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'} {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (iso₁ : obj₁ ≅ obj₁') (iso₂ : obj₂ ≅ obj₂') (iso₃ : obj₃ ≅ obj₃') (comm₁ : CategoryStruct.comp mor₁ iso₂.hom = CategoryStruct.comp iso₁.hom mor₁') (comm₂ : CategoryStruct.comp mor₂ iso₃.hom = CategoryStruct.comp iso₂.hom mor₂') (comm₃ : CategoryStruct.comp mor₃ (Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp iso₃.hom mor₃') : functorMk mor₁ mor₂ mor₃ ≅ functorMk mor₁' mor₂' mor₃'

Constructor for natural isomorphisms between functors constructed with functorMk.

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_inv_app_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : Functor J C} {mor₁ : obj₁ ⟶ obj₂} {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)} {obj₁' obj₂' obj₃' : Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'} {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (iso₁ : obj₁ ≅ obj₁') (iso₂ : obj₂ ≅ obj₂') (iso₃ : obj₃ ≅ obj₃') (comm₁ : CategoryStruct.comp mor₁ iso₂.hom = CategoryStruct.comp iso₁.hom mor₁') (comm₂ : CategoryStruct.comp mor₂ iso₃.hom = CategoryStruct.comp iso₂.hom mor₂') (comm₃ : CategoryStruct.comp mor₃ (Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp iso₃.hom mor₃') (j : J) : ((functorIsoMk' iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).inv.app j).hom₁ = iso₁.inv.app j

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_inv_app_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : Functor J C} {mor₁ : obj₁ ⟶ obj₂} {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)} {obj₁' obj₂' obj₃' : Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'} {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (iso₁ : obj₁ ≅ obj₁') (iso₂ : obj₂ ≅ obj₂') (iso₃ : obj₃ ≅ obj₃') (comm₁ : CategoryStruct.comp mor₁ iso₂.hom = CategoryStruct.comp iso₁.hom mor₁') (comm₂ : CategoryStruct.comp mor₂ iso₃.hom = CategoryStruct.comp iso₂.hom mor₂') (comm₃ : CategoryStruct.comp mor₃ (Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp iso₃.hom mor₃') (j : J) : ((functorIsoMk' iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).inv.app j).hom₃ = iso₃.inv.app j

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_hom_app_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : Functor J C} {mor₁ : obj₁ ⟶ obj₂} {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)} {obj₁' obj₂' obj₃' : Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'} {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (iso₁ : obj₁ ≅ obj₁') (iso₂ : obj₂ ≅ obj₂') (iso₃ : obj₃ ≅ obj₃') (comm₁ : CategoryStruct.comp mor₁ iso₂.hom = CategoryStruct.comp iso₁.hom mor₁') (comm₂ : CategoryStruct.comp mor₂ iso₃.hom = CategoryStruct.comp iso₂.hom mor₂') (comm₃ : CategoryStruct.comp mor₃ (Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp iso₃.hom mor₃') (j : J) : ((functorIsoMk' iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).hom.app j).hom₂ = iso₂.hom.app j

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_inv_app_hom₂ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : Functor J C} {mor₁ : obj₁ ⟶ obj₂} {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)} {obj₁' obj₂' obj₃' : Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'} {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (iso₁ : obj₁ ≅ obj₁') (iso₂ : obj₂ ≅ obj₂') (iso₃ : obj₃ ≅ obj₃') (comm₁ : CategoryStruct.comp mor₁ iso₂.hom = CategoryStruct.comp iso₁.hom mor₁') (comm₂ : CategoryStruct.comp mor₂ iso₃.hom = CategoryStruct.comp iso₂.hom mor₂') (comm₃ : CategoryStruct.comp mor₃ (Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp iso₃.hom mor₃') (j : J) : ((functorIsoMk' iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).inv.app j).hom₂ = iso₂.inv.app j

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_hom_app_hom₁ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : Functor J C} {mor₁ : obj₁ ⟶ obj₂} {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)} {obj₁' obj₂' obj₃' : Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'} {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (iso₁ : obj₁ ≅ obj₁') (iso₂ : obj₂ ≅ obj₂') (iso₃ : obj₃ ≅ obj₃') (comm₁ : CategoryStruct.comp mor₁ iso₂.hom = CategoryStruct.comp iso₁.hom mor₁') (comm₂ : CategoryStruct.comp mor₂ iso₃.hom = CategoryStruct.comp iso₂.hom mor₂') (comm₃ : CategoryStruct.comp mor₃ (Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp iso₃.hom mor₃') (j : J) : ((functorIsoMk' iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).hom.app j).hom₁ = iso₁.hom.app j

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_hom_app_hom₃ {C : Type u} [Category.{v, u} C] [HasShift C ℤ] {J : Type u_1} [Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : Functor J C} {mor₁ : obj₁ ⟶ obj₂} {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)} {obj₁' obj₂' obj₃' : Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'} {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (iso₁ : obj₁ ≅ obj₁') (iso₂ : obj₂ ≅ obj₂') (iso₃ : obj₃ ≅ obj₃') (comm₁ : CategoryStruct.comp mor₁ iso₂.hom = CategoryStruct.comp iso₁.hom mor₁') (comm₂ : CategoryStruct.comp mor₂ iso₃.hom = CategoryStruct.comp iso₂.hom mor₂') (comm₃ : CategoryStruct.comp mor₃ (Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) = CategoryStruct.comp iso₃.hom mor₃') (j : J) : ((functorIsoMk' iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).hom.app j).hom₃ = iso₃.hom.app j