Triangulated functors

In this file, when C and D are categories equipped with a shift by ℤ and F : C ⥤ D is a functor which commutes with the shift, we define the induced functor F.mapTriangle : Triangle C ⥤ Triangle D on the categories of triangles. When C and D are pretriangulated, a triangulated functor is such a functor F which also sends distinguished triangles to distinguished triangles: this defines the typeclass Functor.IsTriangulated.

def CategoryTheory.Functor.mapTriangle {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] : Functor (Pretriangulated.Triangle C) (Pretriangulated.Triangle D)

The functor Triangle C ⥤ Triangle D that is induced by a functor F : C ⥤ D which commutes with shift by ℤ.

@[simp]

theorem CategoryTheory.Functor.mapTriangle_obj {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (T : Pretriangulated.Triangle C) : F.mapTriangle.obj T = Pretriangulated.Triangle.mk (F.map T.mor₁) (F.map T.mor₂) (CategoryStruct.comp (F.map T.mor₃) ((commShiftIso F 1).hom.app T.obj₁))

@[simp]

theorem CategoryTheory.Functor.mapTriangle_map_hom₃ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] {X✝ Y✝ : Pretriangulated.Triangle C} (f : X✝ ⟶ Y✝) : (F.mapTriangle.map f).hom₃ = F.map f.hom₃

@[simp]

theorem CategoryTheory.Functor.mapTriangle_map_hom₁ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] {X✝ Y✝ : Pretriangulated.Triangle C} (f : X✝ ⟶ Y✝) : (F.mapTriangle.map f).hom₁ = F.map f.hom₁

@[simp]

theorem CategoryTheory.Functor.mapTriangle_map_hom₂ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] {X✝ Y✝ : Pretriangulated.Triangle C} (f : X✝ ⟶ Y✝) : (F.mapTriangle.map f).hom₂ = F.map f.hom₂

instance CategoryTheory.Functor.instFaithfulTriangleMapTriangle {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [F.Faithful] : F.mapTriangle.Faithful

instance CategoryTheory.Functor.instFullTriangleMapTriangleOfFaithful {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [F.Full] [F.Faithful] : F.mapTriangle.Full

noncomputable def CategoryTheory.Functor.mapTriangleCommShiftIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (n : ℤ) : (Pretriangulated.Triangle.shiftFunctor C n).comp F.mapTriangle ≅ F.mapTriangle.comp (Pretriangulated.Triangle.shiftFunctor D n)

The functor F.mapTriangle commutes with the shift.

@[simp]

theorem CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₁ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (n : ℤ) (X : Pretriangulated.Triangle C) : ((F.mapTriangleCommShiftIso n).hom.app X).hom₁ = (commShiftIso F n).hom.app X.obj₁

@[simp]

theorem CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₃ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (n : ℤ) (X : Pretriangulated.Triangle C) : ((F.mapTriangleCommShiftIso n).hom.app X).hom₃ = (commShiftIso F n).hom.app X.obj₃

@[simp]

theorem CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₂ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (n : ℤ) (X : Pretriangulated.Triangle C) : ((F.mapTriangleCommShiftIso n).hom.app X).hom₂ = (commShiftIso F n).hom.app X.obj₂

@[simp]

theorem CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₃ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (n : ℤ) (X : Pretriangulated.Triangle C) : ((F.mapTriangleCommShiftIso n).inv.app X).hom₃ = (commShiftIso F n).inv.app X.obj₃

@[simp]

theorem CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₂ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (n : ℤ) (X : Pretriangulated.Triangle C) : ((F.mapTriangleCommShiftIso n).inv.app X).hom₂ = (commShiftIso F n).inv.app X.obj₂

@[simp]

theorem CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₁ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (n : ℤ) (X : Pretriangulated.Triangle C) : ((F.mapTriangleCommShiftIso n).inv.app X).hom₁ = (commShiftIso F n).inv.app X.obj₁

@[implicit_reducible]

noncomputable instance CategoryTheory.Functor.instCommShiftTriangleMapTriangleInt {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] : F.mapTriangle.CommShift ℤ

def CategoryTheory.Functor.mapTriangleRotateIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] : F.mapTriangle.comp (Pretriangulated.rotate D) ≅ (Pretriangulated.rotate C).comp F.mapTriangle

F.mapTriangle commutes with the rotation of triangles.

@[simp]

theorem CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₁ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) : (F.mapTriangleRotateIso.inv.app X).hom₁ = CategoryStruct.id (F.obj X.obj₂)

@[simp]

theorem CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₂ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) : (F.mapTriangleRotateIso.inv.app X).hom₂ = CategoryStruct.id (F.obj X.obj₃)

@[simp]

theorem CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₃ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) : (F.mapTriangleRotateIso.hom.app X).hom₃ = (commShiftIso F 1).inv.app X.obj₁

@[simp]

theorem CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₂ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) : (F.mapTriangleRotateIso.hom.app X).hom₂ = CategoryStruct.id (F.obj X.obj₃)

@[simp]

theorem CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₃ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) : (F.mapTriangleRotateIso.inv.app X).hom₃ = (commShiftIso F 1).hom.app X.obj₁

@[simp]

theorem CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₁ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) : (F.mapTriangleRotateIso.hom.app X).hom₁ = CategoryStruct.id (F.obj X.obj₂)

noncomputable def CategoryTheory.Functor.mapTriangleInvRotateIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] : F.mapTriangle.comp (Pretriangulated.invRotate D) ≅ (Pretriangulated.invRotate C).comp F.mapTriangle

F.mapTriangle commutes with the inverse of the rotation of triangles.

@[simp]

theorem CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₃ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) : (F.mapTriangleInvRotateIso.inv.app X).hom₃ = CategoryStruct.id (F.obj X.obj₂)

@[simp]

theorem CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₁ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) : (F.mapTriangleInvRotateIso.hom.app X).hom₁ = (commShiftIso F (-1)).inv.app X.obj₃

@[simp]

theorem CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₃ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) : (F.mapTriangleInvRotateIso.hom.app X).hom₃ = CategoryStruct.id (F.obj X.obj₂)

@[simp]

theorem CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₁ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) : (F.mapTriangleInvRotateIso.inv.app X).hom₁ = (commShiftIso F (-1)).hom.app X.obj₃

@[simp]

theorem CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₂ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) : (F.mapTriangleInvRotateIso.inv.app X).hom₂ = CategoryStruct.id (F.obj X.obj₁)

@[simp]

theorem CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₂ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) : (F.mapTriangleInvRotateIso.hom.app X).hom₂ = CategoryStruct.id (F.obj X.obj₁)

def CategoryTheory.Functor.mapTriangleIdIso (C : Type u_1) [Category.{v_1, u_1} C] [HasShift C ℤ] : (Functor.id C).mapTriangle ≅ Functor.id (Pretriangulated.Triangle C)

The canonical isomorphism (𝟭 C).mapTriangle ≅ 𝟭 (Triangle C).

@[simp]

theorem CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₂ (C : Type u_1) [Category.{v_1, u_1} C] [HasShift C ℤ] (X : Pretriangulated.Triangle C) : ((mapTriangleIdIso C).inv.app X).hom₂ = CategoryStruct.id X.obj₂

@[simp]

theorem CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₃ (C : Type u_1) [Category.{v_1, u_1} C] [HasShift C ℤ] (X : Pretriangulated.Triangle C) : ((mapTriangleIdIso C).inv.app X).hom₃ = CategoryStruct.id X.obj₃

@[simp]

theorem CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₁ (C : Type u_1) [Category.{v_1, u_1} C] [HasShift C ℤ] (X : Pretriangulated.Triangle C) : ((mapTriangleIdIso C).hom.app X).hom₁ = CategoryStruct.id X.obj₁

@[simp]

theorem CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₃ (C : Type u_1) [Category.{v_1, u_1} C] [HasShift C ℤ] (X : Pretriangulated.Triangle C) : ((mapTriangleIdIso C).hom.app X).hom₃ = CategoryStruct.id X.obj₃

@[simp]

theorem CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₂ (C : Type u_1) [Category.{v_1, u_1} C] [HasShift C ℤ] (X : Pretriangulated.Triangle C) : ((mapTriangleIdIso C).hom.app X).hom₂ = CategoryStruct.id X.obj₂

@[simp]

theorem CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₁ (C : Type u_1) [Category.{v_1, u_1} C] [HasShift C ℤ] (X : Pretriangulated.Triangle C) : ((mapTriangleIdIso C).inv.app X).hom₁ = CategoryStruct.id X.obj₁

def CategoryTheory.Functor.mapTriangleCompIso {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : Functor D E) [G.CommShift ℤ] : (F.comp G).mapTriangle ≅ F.mapTriangle.comp G.mapTriangle

The canonical isomorphism (F ⋙ G).mapTriangle ≅ F.mapTriangle ⋙ G.mapTriangle.

@[simp]

theorem CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₃ {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : Functor D E) [G.CommShift ℤ] (X : Pretriangulated.Triangle C) : ((F.mapTriangleCompIso G).inv.app X).hom₃ = CategoryStruct.id (G.obj (F.obj X.obj₃))

@[simp]

theorem CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₃ {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : Functor D E) [G.CommShift ℤ] (X : Pretriangulated.Triangle C) : ((F.mapTriangleCompIso G).hom.app X).hom₃ = CategoryStruct.id (G.obj (F.obj X.obj₃))

@[simp]

theorem CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₁ {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : Functor D E) [G.CommShift ℤ] (X : Pretriangulated.Triangle C) : ((F.mapTriangleCompIso G).hom.app X).hom₁ = CategoryStruct.id (G.obj (F.obj X.obj₁))

@[simp]

theorem CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₂ {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : Functor D E) [G.CommShift ℤ] (X : Pretriangulated.Triangle C) : ((F.mapTriangleCompIso G).hom.app X).hom₂ = CategoryStruct.id (G.obj (F.obj X.obj₂))

@[simp]

theorem CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₁ {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : Functor D E) [G.CommShift ℤ] (X : Pretriangulated.Triangle C) : ((F.mapTriangleCompIso G).inv.app X).hom₁ = CategoryStruct.id (G.obj (F.obj X.obj₁))

@[simp]

theorem CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₂ {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : Functor D E) [G.CommShift ℤ] (X : Pretriangulated.Triangle C) : ((F.mapTriangleCompIso G).inv.app X).hom₂ = CategoryStruct.id (G.obj (F.obj X.obj₂))

def CategoryTheory.Functor.mapTriangleIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] : F₁.mapTriangle ≅ F₂.mapTriangle

Two isomorphic functors F₁ and F₂ induce isomorphic functors F₁.mapTriangle and F₂.mapTriangle if the isomorphism F₁ ≅ F₂ is compatible with the shifts.

@[simp]

theorem CategoryTheory.Functor.mapTriangleIso_inv_app_hom₁ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] (X : Pretriangulated.Triangle C) : ((mapTriangleIso e).inv.app X).hom₁ = e.inv.app X.obj₁

@[simp]

theorem CategoryTheory.Functor.mapTriangleIso_hom_app_hom₃ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] (X : Pretriangulated.Triangle C) : ((mapTriangleIso e).hom.app X).hom₃ = e.hom.app X.obj₃

@[simp]

theorem CategoryTheory.Functor.mapTriangleIso_hom_app_hom₁ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] (X : Pretriangulated.Triangle C) : ((mapTriangleIso e).hom.app X).hom₁ = e.hom.app X.obj₁

@[simp]

theorem CategoryTheory.Functor.mapTriangleIso_hom_app_hom₂ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] (X : Pretriangulated.Triangle C) : ((mapTriangleIso e).hom.app X).hom₂ = e.hom.app X.obj₂

@[simp]

theorem CategoryTheory.Functor.mapTriangleIso_inv_app_hom₃ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] (X : Pretriangulated.Triangle C) : ((mapTriangleIso e).inv.app X).hom₃ = e.inv.app X.obj₃

@[simp]

theorem CategoryTheory.Functor.mapTriangleIso_inv_app_hom₂ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] (X : Pretriangulated.Triangle C) : ((mapTriangleIso e).inv.app X).hom₂ = e.inv.app X.obj₂

class CategoryTheory.Functor.IsTriangulated {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] : Prop

A functor which commutes with the shift by ℤ is triangulated if it sends distinguished triangles to distinguished triangles.

• map_distinguished (T : Pretriangulated.Triangle C) : T ∈ Pretriangulated.distinguishedTriangles → F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles

theorem CategoryTheory.Functor.map_distinguished {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] [F.IsTriangulated] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) : F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles

@[instance 100]

instance CategoryTheory.Functor.IsTriangulated.instPreservesZeroMorphisms {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] [F.IsTriangulated] : F.PreservesZeroMorphisms

instance CategoryTheory.Functor.IsTriangulated.instPreservesLimitsOfShapeDiscreteWalkingPair {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] [F.IsTriangulated] : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F

@[instance 100]

instance CategoryTheory.Functor.IsTriangulated.instAdditive {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] [F.IsTriangulated] : F.Additive

instance CategoryTheory.Functor.IsTriangulated.instId {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : (Functor.id C).IsTriangulated

instance CategoryTheory.Functor.IsTriangulated.instComp {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : Functor D E) [G.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasZeroObject E] [Preadditive C] [Preadditive D] [Preadditive E] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [∀ (n : ℤ), (shiftFunctor E n).Additive] [Pretriangulated C] [Pretriangulated D] [Pretriangulated E] [F.IsTriangulated] [G.IsTriangulated] : (F.comp G).IsTriangulated

theorem CategoryTheory.Functor.map_distinguished_iff {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] [F.IsTriangulated] [F.Full] [F.Faithful] (T : Pretriangulated.Triangle C) : F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles ↔ T ∈ Pretriangulated.distinguishedTriangles

theorem CategoryTheory.Functor.isTriangulated_of_iso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] [F₁.IsTriangulated] : F₂.IsTriangulated

theorem CategoryTheory.Functor.isTriangulated_iff_of_iso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] : F₁.IsTriangulated ↔ F₂.IsTriangulated

theorem CategoryTheory.Functor.isTriangulated_iff_comp_right {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasZeroObject E] [Preadditive C] [Preadditive D] [Preadditive E] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [∀ (n : ℤ), (shiftFunctor E n).Additive] [Pretriangulated C] [Pretriangulated D] [Pretriangulated E] {F : Functor C D} {G : Functor D E} {H : Functor C E} (e : F.comp G ≅ H) [F.CommShift ℤ] [G.CommShift ℤ] [H.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] [G.IsTriangulated] [G.Full] [G.Faithful] : F.IsTriangulated ↔ H.IsTriangulated

theorem CategoryTheory.Functor.mem_mapTriangle_essImage_of_distinguished {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] [F.IsTriangulated] [F.mapArrow.EssSurj] (T : Pretriangulated.Triangle D) (hT : T ∈ Pretriangulated.distinguishedTriangles) : ∃ (T' : Pretriangulated.Triangle C) (_ : T' ∈ Pretriangulated.distinguishedTriangles), Nonempty (F.mapTriangle.obj T' ≅ T)

theorem CategoryTheory.Functor.isTriangulated_of_precomp {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : Functor D E) [G.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasZeroObject E] [Preadditive C] [Preadditive D] [Preadditive E] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [∀ (n : ℤ), (shiftFunctor E n).Additive] [Pretriangulated C] [Pretriangulated D] [Pretriangulated E] [(F.comp G).IsTriangulated] [F.IsTriangulated] [F.mapArrow.EssSurj] : G.IsTriangulated

theorem CategoryTheory.Functor.isTriangulated_of_precomp_iso {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] {F : Functor C D} [F.CommShift ℤ] {G : Functor D E} [G.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasZeroObject E] [Preadditive C] [Preadditive D] [Preadditive E] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [∀ (n : ℤ), (shiftFunctor E n).Additive] [Pretriangulated C] [Pretriangulated D] [Pretriangulated E] {H : Functor C E} (e : F.comp G ≅ H) [H.CommShift ℤ] [H.IsTriangulated] [F.IsTriangulated] [F.mapArrow.EssSurj] [NatTrans.CommShift e.hom ℤ] : G.IsTriangulated

def CategoryTheory.Triangulated.Octahedron.map {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] : Octahedron ⋯ ⋯ ⋯ ⋯

The image of an octahedron by a triangulated functor.

@[simp]

theorem CategoryTheory.Triangulated.Octahedron.map_m₁ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] : (h.map F).m₁ = F.map h.m₁

@[simp]

theorem CategoryTheory.Triangulated.Octahedron.map_m₃ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] : (h.map F).m₃ = F.map h.m₃

theorem CategoryTheory.isTriangulated_of_essSurj_mapComposableArrows_two {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] [(F.mapComposableArrows 2).EssSurj] [IsTriangulated C] : IsTriangulated D

If F : C ⥤ D is a triangulated functor from a triangulated category, then D is also triangulated if tuples of composable arrows in D can be lifted to C.

theorem CategoryTheory.IsTriangulated.of_fully_faithful_triangulated_functor {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [HasShift C ℤ] [HasShift D ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] [F.Full] [F.Faithful] [IsTriangulated D] : IsTriangulated C