Pretriangulated Categories

This file contains the definition of pretriangulated categories and triangulated functors between them.

Implementation Notes

We work under the assumption that pretriangulated categories are preadditive categories, but not necessarily additive categories, as is assumed in some sources.

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

class CategoryTheory.Pretriangulated (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] : Type (max u v)

• distinguishedTriangles : Set (CategoryTheory.Pretriangulated.Triangle C)

  a class of triangle which are called distinguished

• isomorphic_distinguished : ∀ (T₁ : CategoryTheory.Pretriangulated.Triangle C), T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → ∀ (T₂ : CategoryTheory.Pretriangulated.Triangle C), (T₂ ≅ T₁) → T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

  a triangle that is isomorphic to a distinguished triangle is distinguished

• contractible_distinguished : ∀ (X : C), CategoryTheory.Pretriangulated.contractibleTriangle X ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

  obvious triangles X ⟶ X ⟶ 0 ⟶ X⟦1⟧ are distinguished

• distinguished_cocone_triangle : ∀ {X Y : C} (f : X ⟶ Y), ∃ Z g h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

  any morphism X ⟶ Y is part of a distinguished triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧

• rotate_distinguished_triangle : ∀ (T : CategoryTheory.Pretriangulated.Triangle C), T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ CategoryTheory.Pretriangulated.Triangle.rotate T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

  a triangle is distinguished iff it is so after rotating it

• complete_distinguished_triangle_morphism : ∀ (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C), T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂), CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ → ∃ c, CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧ CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map a) = CategoryTheory.CategoryStruct.comp c T₂.mor₃

  given two distinguished triangle, a commutative square can be extended as morphism of triangles

A preadditive category C with an additive shift, and a class of "distinguished triangles" relative to that shift is called pretriangulated if the following hold:

• Any triangle that is isomorphic to a distinguished triangle is also distinguished.
• Any triangle of the form (X,X,0,id,0,0) is distinguished.
• For any morphism f : X ⟶ Y there exists a distinguished triangle of the form (X,Y,Z,f,g,h).
• The triangle (X,Y,Z,f,g,h) is distinguished if and only if (Y,Z,X⟦1⟧,g,h,-f⟦1⟧) is.
• Given a diagram:

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

  where the left square commutes, and whose rows are distinguished triangles, there exists a morphism c : Z ⟶ Z' such that (a,b,c) is a triangle morphism.

See https://stacks.math.columbia.edu/tag/0145

def CategoryTheory.Pretriangulated.termDistTriang_ : Lean.ParserDescr

distinguished triangles in a pretriangulated category

theorem CategoryTheory.Pretriangulated.distinguished_iff_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] {T₁ : CategoryTheory.Pretriangulated.Triangle C} {T₂ : CategoryTheory.Pretriangulated.Triangle C} (e : T₁ ≅ T₂) : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

theorem CategoryTheory.Pretriangulated.rot_of_dist_triangle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (H : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.Pretriangulated.Triangle.rotate T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

Given any distinguished triangle T, then we know T.rotate is also distinguished.

theorem CategoryTheory.Pretriangulated.inv_rot_of_dist_triangle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (H : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.Pretriangulated.Triangle.invRotate T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

Given any distinguished triangle T, then we know T.inv_rotate is also distinguished.

theorem CategoryTheory.Pretriangulated.comp_dist_triangle_mor_zero₁₂_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (H : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) {Z : C} (h : T.obj₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp T.mor₁ (CategoryTheory.CategoryStruct.comp T.mor₂ h) = CategoryTheory.CategoryStruct.comp 0 h

theorem CategoryTheory.Pretriangulated.comp_dist_triangle_mor_zero₁₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (H : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.CategoryStruct.comp T.mor₁ T.mor₂ = 0

Given any distinguished triangle

      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧

the composition f ≫ g = 0. See https://stacks.math.columbia.edu/tag/0146

theorem CategoryTheory.Pretriangulated.comp_dist_triangle_mor_zero₂₃_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (H : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj T.obj₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp T.mor₂ (CategoryTheory.CategoryStruct.comp T.mor₃ h) = CategoryTheory.CategoryStruct.comp 0 h

theorem CategoryTheory.Pretriangulated.comp_dist_triangle_mor_zero₂₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (H : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.CategoryStruct.comp T.mor₂ T.mor₃ = 0

Given any distinguished triangle

      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧

the composition g ≫ h = 0. See https://stacks.math.columbia.edu/tag/0146

theorem CategoryTheory.Pretriangulated.comp_dist_triangle_mor_zero₃₁_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (H : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj T.obj₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp T.mor₃ (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map T.mor₁) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem CategoryTheory.Pretriangulated.comp_dist_triangle_mor_zero₃₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (H : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.CategoryStruct.comp T.mor₃ ((CategoryTheory.shiftFunctor C 1).map T.mor₁) = 0

Given any distinguished triangle

      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧

the composition h ≫ f⟦1⟧ = 0. See https://stacks.math.columbia.edu/tag/0146

theorem CategoryTheory.Pretriangulated.distinguished_cocone_triangle₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] {Y : C} {Z : C} (g : Y ⟶ Z) : ∃ X f h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

Any morphism Y ⟶ Z is part of a distinguished triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧

theorem CategoryTheory.Pretriangulated.distinguished_cocone_triangle₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] {Z : C} {X : C} (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) : ∃ Y f g, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

Any morphism Z ⟶ X⟦1⟧ is part of a distinguished triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧

theorem CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T₁ : CategoryTheory.Pretriangulated.Triangle C) (T₂ : CategoryTheory.Pretriangulated.Triangle C) (hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (b : T₁.obj₂ ⟶ T₂.obj₂) (c : T₁.obj₃ ⟶ T₂.obj₃) (comm : CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂) : ∃ a, CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ ∧ CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map a) = CategoryTheory.CategoryStruct.comp c T₂.mor₃

A commutative square involving the morphisms mor₂ of two distinguished triangles can be extended as morphism of triangles

theorem CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T₁ : CategoryTheory.Pretriangulated.Triangle C) (T₂ : CategoryTheory.Pretriangulated.Triangle C) (hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (a : T₁.obj₁ ⟶ T₂.obj₁) (c : T₁.obj₃ ⟶ T₂.obj₃) (comm : CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map a) = CategoryTheory.CategoryStruct.comp c T₂.mor₃) : ∃ b, CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ ∧ CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂

A commutative square involving the morphisms mor₃ of two distinguished triangles can be extended as morphism of triangles

theorem CategoryTheory.Pretriangulated.contractible_distinguished₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (X : C) : CategoryTheory.Pretriangulated.Triangle.mk 0 (CategoryTheory.CategoryStruct.id X) 0 ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

Obvious triangles 0 ⟶ X ⟶ X ⟶ 0⟦1⟧ are distinguished

theorem CategoryTheory.Pretriangulated.contractible_distinguished₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (X : C) : CategoryTheory.Pretriangulated.Triangle.mk 0 0 (CategoryTheory.CategoryStruct.id ((CategoryTheory.shiftFunctor C 1).obj X)) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

Obvious triangles X ⟶ 0 ⟶ X⟦1⟧ ⟶ X⟦1⟧ are distinguished

theorem CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) {X : C} (f : T.obj₂ ⟶ X) (hf : CategoryTheory.CategoryStruct.comp T.mor₁ f = 0) : ∃ g, f = CategoryTheory.CategoryStruct.comp T.mor₂ g

theorem CategoryTheory.Pretriangulated.Triangle.yoneda_exact₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) {X : C} (f : T.obj₃ ⟶ X) (hf : CategoryTheory.CategoryStruct.comp T.mor₂ f = 0) : ∃ g, f = CategoryTheory.CategoryStruct.comp T.mor₃ g

theorem CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) {X : C} (f : X ⟶ T.obj₂) (hf : CategoryTheory.CategoryStruct.comp f T.mor₂ = 0) : ∃ g, f = CategoryTheory.CategoryStruct.comp g T.mor₁

theorem CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) {X : C} (f : X ⟶ (CategoryTheory.shiftFunctor C 1).obj T.obj₁) (hf : CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctor C 1).map T.mor₁) = 0) : ∃ g, f = CategoryTheory.CategoryStruct.comp g T.mor₃

theorem CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) {X : C} (f : X ⟶ T.obj₃) (hf : CategoryTheory.CategoryStruct.comp f T.mor₃ = 0) : ∃ g, f = CategoryTheory.CategoryStruct.comp g T.mor₂

theorem CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_iff_epi₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : T.mor₃ = 0 ↔ CategoryTheory.Epi T.mor₂

theorem CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_iff_epi₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : T.mor₂ = 0 ↔ CategoryTheory.Epi T.mor₁

theorem CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_iff_epi₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : T.mor₁ = 0 ↔ CategoryTheory.Epi T.mor₃

theorem CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_of_epi₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.Epi T.mor₂) : T.mor₃ = 0

theorem CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_of_epi₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.Epi T.mor₁) : T.mor₂ = 0

theorem CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_of_epi₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.Epi T.mor₃) : T.mor₁ = 0

theorem CategoryTheory.Pretriangulated.Triangle.epi₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : T.mor₃ = 0) : CategoryTheory.Epi T.mor₂

theorem CategoryTheory.Pretriangulated.Triangle.epi₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : T.mor₂ = 0) : CategoryTheory.Epi T.mor₁

theorem CategoryTheory.Pretriangulated.Triangle.epi₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : T.mor₁ = 0) : CategoryTheory.Epi T.mor₃

theorem CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_iff_mono₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : T.mor₁ = 0 ↔ CategoryTheory.Mono T.mor₂

theorem CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_iff_mono₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : T.mor₂ = 0 ↔ CategoryTheory.Mono T.mor₃

theorem CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_iff_mono₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : T.mor₃ = 0 ↔ CategoryTheory.Mono T.mor₁

theorem CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_of_mono₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.Mono T.mor₂) : T.mor₁ = 0

theorem CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_of_mono₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.Mono T.mor₃) : T.mor₂ = 0

theorem CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_of_mono₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.Mono T.mor₁) : T.mor₃ = 0

theorem CategoryTheory.Pretriangulated.Triangle.mono₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : T.mor₁ = 0) : CategoryTheory.Mono T.mor₂

theorem CategoryTheory.Pretriangulated.Triangle.mono₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : T.mor₂ = 0) : CategoryTheory.Mono T.mor₃

theorem CategoryTheory.Pretriangulated.Triangle.mono₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : T.mor₃ = 0) : CategoryTheory.Mono T.mor₁

theorem CategoryTheory.Pretriangulated.Triangle.isZero₂_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.Limits.IsZero T.obj₂ ↔ T.mor₁ = 0 ∧ T.mor₂ = 0

theorem CategoryTheory.Pretriangulated.Triangle.isZero₁_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.Limits.IsZero T.obj₁ ↔ T.mor₁ = 0 ∧ T.mor₃ = 0

theorem CategoryTheory.Pretriangulated.Triangle.isZero₃_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.Limits.IsZero T.obj₃ ↔ T.mor₂ = 0 ∧ T.mor₃ = 0

theorem CategoryTheory.Pretriangulated.Triangle.isZero₁_of_isZero₂₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h₂ : CategoryTheory.Limits.IsZero T.obj₂) (h₃ : CategoryTheory.Limits.IsZero T.obj₃) : CategoryTheory.Limits.IsZero T.obj₁

theorem CategoryTheory.Pretriangulated.Triangle.isZero₂_of_isZero₁₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h₁ : CategoryTheory.Limits.IsZero T.obj₁) (h₃ : CategoryTheory.Limits.IsZero T.obj₃) : CategoryTheory.Limits.IsZero T.obj₂

theorem CategoryTheory.Pretriangulated.Triangle.isZero₃_of_isZero₁₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h₁ : CategoryTheory.Limits.IsZero T.obj₁) (h₂ : CategoryTheory.Limits.IsZero T.obj₂) : CategoryTheory.Limits.IsZero T.obj₃

theorem CategoryTheory.Pretriangulated.Triangle.isZero₁_iff_isIso₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.Limits.IsZero T.obj₁ ↔ CategoryTheory.IsIso T.mor₂

theorem CategoryTheory.Pretriangulated.Triangle.isZero₂_iff_isIso₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.Limits.IsZero T.obj₂ ↔ CategoryTheory.IsIso T.mor₃

theorem CategoryTheory.Pretriangulated.Triangle.isZero₃_iff_isIso₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.Limits.IsZero T.obj₃ ↔ CategoryTheory.IsIso T.mor₁

theorem CategoryTheory.Pretriangulated.Triangle.isZero₁_of_isIso₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.IsIso T.mor₂) : CategoryTheory.Limits.IsZero T.obj₁

theorem CategoryTheory.Pretriangulated.Triangle.isZero₂_of_isIso₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.IsIso T.mor₃) : CategoryTheory.Limits.IsZero T.obj₂

theorem CategoryTheory.Pretriangulated.Triangle.isZero₃_of_isIso₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.IsIso T.mor₁) : CategoryTheory.Limits.IsZero T.obj₃

theorem CategoryTheory.Pretriangulated.Triangle.shift_distinguished {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n : ℤ) : (CategoryTheory.shiftFunctor (CategoryTheory.Pretriangulated.Triangle C) n).obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

instance CategoryTheory.Pretriangulated.instSplitEpiCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] : CategoryTheory.SplitEpiCategory C

instance CategoryTheory.Pretriangulated.instSplitMonoCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] : CategoryTheory.SplitMonoCategory C

theorem CategoryTheory.Pretriangulated.isIso₂_of_isIso₁₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] {T : CategoryTheory.Pretriangulated.Triangle C} {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : T ⟶ T') (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT' : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h₁ : CategoryTheory.IsIso φ.hom₁) (h₃ : CategoryTheory.IsIso φ.hom₃) : CategoryTheory.IsIso φ.hom₂

theorem CategoryTheory.Pretriangulated.isIso₃_of_isIso₁₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] {T : CategoryTheory.Pretriangulated.Triangle C} {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : T ⟶ T') (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT' : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h₁ : CategoryTheory.IsIso φ.hom₁) (h₂ : CategoryTheory.IsIso φ.hom₂) : CategoryTheory.IsIso φ.hom₃

theorem CategoryTheory.Pretriangulated.isIso₁_of_isIso₂₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] {T : CategoryTheory.Pretriangulated.Triangle C} {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : T ⟶ T') (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT' : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h₂ : CategoryTheory.IsIso φ.hom₂) (h₃ : CategoryTheory.IsIso φ.hom₃) : CategoryTheory.IsIso φ.hom₁