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) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] : Type (max u v)

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

• distinguishedTriangles : Set (Triangle C)

  a class of triangle which are called distinguished

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

  a triangle that is isomorphic to a distinguished triangle is distinguished

• contractible_distinguished (X : C) : contractibleTriangle X ∈ distinguishedTriangles

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

• distinguished_cocone_triangle {X Y : C} (f : X ⟶ Y) : ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ (shiftFunctor C 1).obj X), Triangle.mk f g h ∈ distinguishedTriangles

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

• rotate_distinguished_triangle (T : Triangle C) : T ∈ distinguishedTriangles ↔ T.rotate ∈ distinguishedTriangles

  a triangle is distinguished iff it is so after rotating it

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

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

def CategoryTheory.Pretriangulated.termDistTriang_ : Lean.ParserDescr

distinguished triangles in a pretriangulated category

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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

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

theorem CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T : Triangle C) (H : T ∈ distinguishedTriangles) : 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_distTriang_mor_zero₁₂_assoc {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T : Triangle C) (H : T ∈ distinguishedTriangles) {Z : C} (h : T.obj₃ ⟶ Z) : CategoryStruct.comp T.mor₁ (CategoryStruct.comp T.mor₂ h) = CategoryStruct.comp 0 h

theorem CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T : Triangle C) (H : T ∈ distinguishedTriangles) : 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_distTriang_mor_zero₂₃_assoc {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T : Triangle C) (H : T ∈ distinguishedTriangles) {Z : C} (h : (shiftFunctor C 1).obj T.obj₁ ⟶ Z) : CategoryStruct.comp T.mor₂ (CategoryStruct.comp T.mor₃ h) = CategoryStruct.comp 0 h

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

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

The short complex T.obj₁ ⟶ T.obj₂ ⟶ T.obj₃ attached to a distinguished triangle.

Equations

• CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT = CategoryTheory.ShortComplex.mk T.mor₁ T.mor₂ ⋯

@[simp]

theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_f {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T : Triangle C) (hT : T ∈ distinguishedTriangles) : (shortComplexOfDistTriangle T hT).f = T.mor₁

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_g {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T : Triangle C) (hT : T ∈ distinguishedTriangles) : (shortComplexOfDistTriangle T hT).g = T.mor₂

def CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] {T T' : Triangle C} (e : T ≅ T') (hT : T ∈ distinguishedTriangles) : shortComplexOfDistTriangle T hT ≅ shortComplexOfDistTriangle T' ⋯

The isomorphism between the short complex attached to two isomorphic distinguished triangles.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_inv_τ₂ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] {T T' : Triangle C} (e : T ≅ T') (hT : T ∈ distinguishedTriangles) : (shortComplexOfDistTriangleIsoOfIso e hT).inv.τ₂ = e.inv.hom₂

@[simp]

theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_inv_τ₁ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] {T T' : Triangle C} (e : T ≅ T') (hT : T ∈ distinguishedTriangles) : (shortComplexOfDistTriangleIsoOfIso e hT).inv.τ₁ = e.inv.hom₁

@[simp]

theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_hom_τ₂ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] {T T' : Triangle C} (e : T ≅ T') (hT : T ∈ distinguishedTriangles) : (shortComplexOfDistTriangleIsoOfIso e hT).hom.τ₂ = e.hom.hom₂

@[simp]

theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_hom_τ₁ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] {T T' : Triangle C} (e : T ≅ T') (hT : T ∈ distinguishedTriangles) : (shortComplexOfDistTriangleIsoOfIso e hT).hom.τ₁ = e.hom.hom₁

@[simp]

theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_hom_τ₃ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] {T T' : Triangle C} (e : T ≅ T') (hT : T ∈ distinguishedTriangles) : (shortComplexOfDistTriangleIsoOfIso e hT).hom.τ₃ = e.hom.hom₃

@[simp]

theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_inv_τ₃ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] {T T' : Triangle C} (e : T ≅ T') (hT : T ∈ distinguishedTriangles) : (shortComplexOfDistTriangleIsoOfIso e hT).inv.τ₃ = e.inv.hom₃

theorem CategoryTheory.Pretriangulated.distinguished_cocone_triangle₁ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] {Y Z : C} (g : Y ⟶ Z) : ∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ (shiftFunctor C 1).obj X), Triangle.mk f g h ∈ 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} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] {Z X : C} (h : Z ⟶ (shiftFunctor C 1).obj X) : ∃ (Y : C) (f : X ⟶ Y) (g : Y ⟶ Z), Triangle.mk f g h ∈ 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} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T₁ T₂ : Triangle C) (hT₁ : T₁ ∈ distinguishedTriangles) (hT₂ : T₂ ∈ distinguishedTriangles) (b : T₁.obj₂ ⟶ T₂.obj₂) (c : T₁.obj₃ ⟶ T₂.obj₃) (comm : CategoryStruct.comp T₁.mor₂ c = CategoryStruct.comp b T₂.mor₂) : ∃ (a : T₁.obj₁ ⟶ T₂.obj₁), CategoryStruct.comp T₁.mor₁ b = CategoryStruct.comp a T₂.mor₁ ∧ CategoryStruct.comp T₁.mor₃ ((shiftFunctor C 1).map a) = 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} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T₁ T₂ : Triangle C) (hT₁ : T₁ ∈ distinguishedTriangles) (hT₂ : T₂ ∈ distinguishedTriangles) (a : T₁.obj₁ ⟶ T₂.obj₁) (c : T₁.obj₃ ⟶ T₂.obj₃) (comm : CategoryStruct.comp T₁.mor₃ ((shiftFunctor C 1).map a) = CategoryStruct.comp c T₂.mor₃) : ∃ (b : T₁.obj₂ ⟶ T₂.obj₂), CategoryStruct.comp T₁.mor₁ b = CategoryStruct.comp a T₂.mor₁ ∧ CategoryStruct.comp T₁.mor₂ c = 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} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (X : C) : Triangle.mk 0 (CategoryStruct.id X) 0 ∈ distinguishedTriangles

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

def CategoryTheory.Pretriangulated.binaryBiproductData {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T : Triangle C) (hT : T ∈ distinguishedTriangles) (hT₀ : T.mor₃ = 0) (inr : T.obj₃ ⟶ T.obj₂) (inr_snd : CategoryStruct.comp inr T.mor₂ = CategoryStruct.id T.obj₃) (fst : T.obj₂ ⟶ T.obj₁) (total : CategoryStruct.comp fst T.mor₁ + CategoryStruct.comp T.mor₂ inr = CategoryStruct.id T.obj₂) : Limits.BinaryBiproductData T.obj₁ T.obj₃

Given a distinguished triangle T such that T.mor₃ = 0 and the datum of morphisms inr : T.obj₃ ⟶ T.obj₂ and fst : T.obj₂ ⟶ T.obj₁ satisfying suitable relations, this is the binary biproduct data expressing that T.obj₂ identifies to the binary biproduct of T.obj₁ and T.obj₃. See also exists_iso_binaryBiproduct_of_distTriang.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Pretriangulated.binaryBiproductData_bicone_pt {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T : Triangle C) (hT : T ∈ distinguishedTriangles) (hT₀ : T.mor₃ = 0) (inr : T.obj₃ ⟶ T.obj₂) (inr_snd : CategoryStruct.comp inr T.mor₂ = CategoryStruct.id T.obj₃) (fst : T.obj₂ ⟶ T.obj₁) (total : CategoryStruct.comp fst T.mor₁ + CategoryStruct.comp T.mor₂ inr = CategoryStruct.id T.obj₂) : (binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.pt = T.obj₂

@[simp]

theorem CategoryTheory.Pretriangulated.binaryBiproductData_isBilimit {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T : Triangle C) (hT : T ∈ distinguishedTriangles) (hT₀ : T.mor₃ = 0) (inr : T.obj₃ ⟶ T.obj₂) (inr_snd : CategoryStruct.comp inr T.mor₂ = CategoryStruct.id T.obj₃) (fst : T.obj₂ ⟶ T.obj₁) (total : CategoryStruct.comp fst T.mor₁ + CategoryStruct.comp T.mor₂ inr = CategoryStruct.id T.obj₂) : (binaryBiproductData T hT hT₀ inr inr_snd fst total).isBilimit = Limits.isBinaryBilimitOfTotal { pt := T.obj₂, fst := fst, snd := T.mor₂, inl := T.mor₁, inr := inr, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := inr_snd } total

@[simp]

theorem CategoryTheory.Pretriangulated.binaryBiproductData_bicone_inr {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T : Triangle C) (hT : T ∈ distinguishedTriangles) (hT₀ : T.mor₃ = 0) (inr : T.obj₃ ⟶ T.obj₂) (inr_snd : CategoryStruct.comp inr T.mor₂ = CategoryStruct.id T.obj₃) (fst : T.obj₂ ⟶ T.obj₁) (total : CategoryStruct.comp fst T.mor₁ + CategoryStruct.comp T.mor₂ inr = CategoryStruct.id T.obj₂) : (binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.inr = inr

@[simp]

theorem CategoryTheory.Pretriangulated.binaryBiproductData_bicone_inl {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T : Triangle C) (hT : T ∈ distinguishedTriangles) (hT₀ : T.mor₃ = 0) (inr : T.obj₃ ⟶ T.obj₂) (inr_snd : CategoryStruct.comp inr T.mor₂ = CategoryStruct.id T.obj₃) (fst : T.obj₂ ⟶ T.obj₁) (total : CategoryStruct.comp fst T.mor₁ + CategoryStruct.comp T.mor₂ inr = CategoryStruct.id T.obj₂) : (binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.inl = T.mor₁

@[simp]

theorem CategoryTheory.Pretriangulated.binaryBiproductData_bicone_snd {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T : Triangle C) (hT : T ∈ distinguishedTriangles) (hT₀ : T.mor₃ = 0) (inr : T.obj₃ ⟶ T.obj₂) (inr_snd : CategoryStruct.comp inr T.mor₂ = CategoryStruct.id T.obj₃) (fst : T.obj₂ ⟶ T.obj₁) (total : CategoryStruct.comp fst T.mor₁ + CategoryStruct.comp T.mor₂ inr = CategoryStruct.id T.obj₂) : (binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.snd = T.mor₂

@[simp]

theorem CategoryTheory.Pretriangulated.binaryBiproductData_bicone_fst {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T : Triangle C) (hT : T ∈ distinguishedTriangles) (hT₀ : T.mor₃ = 0) (inr : T.obj₃ ⟶ T.obj₂) (inr_snd : CategoryStruct.comp inr T.mor₂ = CategoryStruct.id T.obj₃) (fst : T.obj₂ ⟶ T.obj₁) (total : CategoryStruct.comp fst T.mor₁ + CategoryStruct.comp T.mor₂ inr = CategoryStruct.id T.obj₂) : (binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.fst = fst

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

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

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

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

theorem CategoryTheory.Pretriangulated.exists_iso_binaryBiproduct_of_distTriang {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T : Triangle C) (hT : T ∈ distinguishedTriangles) (zero : T.mor₃ = 0) : ∃ (e : T.obj₂ ≅ T.obj₁ ⊞ T.obj₃), CategoryStruct.comp T.mor₁ e.hom = Limits.biprod.inl ∧ T.mor₂ = CategoryStruct.comp e.hom Limits.biprod.snd

theorem CategoryTheory.Pretriangulated.binaryBiproductTriangle_distinguished {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (X₁ X₂ : C) : binaryBiproductTriangle X₁ X₂ ∈ distinguishedTriangles

theorem CategoryTheory.Pretriangulated.binaryProductTriangle_distinguished {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (X₁ X₂ : C) : binaryProductTriangle X₁ X₂ ∈ distinguishedTriangles

def CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T₁ T₂ : Triangle C) (hT₁ : T₁ ∈ distinguishedTriangles) (hT₂ : T₂ ∈ distinguishedTriangles) (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂) (comm : CategoryStruct.comp T₁.mor₁ b = CategoryStruct.comp a T₂.mor₁) : T₁ ⟶ T₂

A chosen extension of a commutative square into a morphism of distinguished triangles.

Equations

• CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ a b comm = { hom₁ := a, hom₂ := b, hom₃ := ⋯.choose, comm₁ := comm, comm₂ := ⋯, comm₃ := ⋯ }

@[simp]

theorem CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism_hom₁ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T₁ T₂ : Triangle C) (hT₁ : T₁ ∈ distinguishedTriangles) (hT₂ : T₂ ∈ distinguishedTriangles) (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂) (comm : CategoryStruct.comp T₁.mor₁ b = CategoryStruct.comp a T₂.mor₁) : (completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ a b comm).hom₁ = a

@[simp]

theorem CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism_hom₂ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T₁ T₂ : Triangle C) (hT₁ : T₁ ∈ distinguishedTriangles) (hT₂ : T₂ ∈ distinguishedTriangles) (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂) (comm : CategoryStruct.comp T₁.mor₁ b = CategoryStruct.comp a T₂.mor₁) : (completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ a b comm).hom₂ = b

theorem CategoryTheory.Pretriangulated.productTriangle_distinguished {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] {J : Type u_1} (T : J → Triangle C) (hT : ∀ (j : J), T j ∈ distinguishedTriangles) [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 ∈ distinguishedTriangles

A product of distinguished triangles is distinguished

theorem CategoryTheory.Pretriangulated.exists_iso_of_arrow_iso {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T₁ T₂ : Triangle C) (hT₁ : T₁ ∈ distinguishedTriangles) (hT₂ : T₂ ∈ distinguishedTriangles) (e : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁) : ∃ (e' : T₁ ≅ T₂), e'.hom.hom₁ = e.hom.left ∧ e'.hom.hom₂ = e.hom.right

def CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T₁ T₂ : Triangle C) (hT₁ : T₁ ∈ distinguishedTriangles) (hT₂ : T₂ ∈ distinguishedTriangles) (e₁ : T₁.obj₁ ≅ T₂.obj₁) (e₂ : T₁.obj₂ ≅ T₂.obj₂) (comm : CategoryStruct.comp T₁.mor₁ e₂.hom = CategoryStruct.comp e₁.hom T₂.mor₁) : T₁ ≅ T₂

A choice of isomorphism T₁ ≅ T₂ between two distinguished triangles when we are given two isomorphisms e₁ : T₁.obj₁ ≅ T₂.obj₁ and e₂ : T₁.obj₂ ≅ T₂.obj₂.

Equations

• CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm = T₁.isoMk T₂ e₁ e₂ (CategoryTheory.Pretriangulated.Triangle.π₃.mapIso ⋯.choose) comm ⋯ ⋯

@[simp]

theorem CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂_inv_hom₂ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T₁ T₂ : Triangle C) (hT₁ : T₁ ∈ distinguishedTriangles) (hT₂ : T₂ ∈ distinguishedTriangles) (e₁ : T₁.obj₁ ≅ T₂.obj₁) (e₂ : T₁.obj₂ ≅ T₂.obj₂) (comm : CategoryStruct.comp T₁.mor₁ e₂.hom = CategoryStruct.comp e₁.hom T₂.mor₁) : (isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).inv.hom₂ = e₂.inv

@[simp]

theorem CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂_inv_hom₁ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T₁ T₂ : Triangle C) (hT₁ : T₁ ∈ distinguishedTriangles) (hT₂ : T₂ ∈ distinguishedTriangles) (e₁ : T₁.obj₁ ≅ T₂.obj₁) (e₂ : T₁.obj₂ ≅ T₂.obj₂) (comm : CategoryStruct.comp T₁.mor₁ e₂.hom = CategoryStruct.comp e₁.hom T₂.mor₁) : (isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).inv.hom₁ = e₁.inv

@[simp]

theorem CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂_hom_hom₂ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T₁ T₂ : Triangle C) (hT₁ : T₁ ∈ distinguishedTriangles) (hT₂ : T₂ ∈ distinguishedTriangles) (e₁ : T₁.obj₁ ≅ T₂.obj₁) (e₂ : T₁.obj₂ ≅ T₂.obj₂) (comm : CategoryStruct.comp T₁.mor₁ e₂.hom = CategoryStruct.comp e₁.hom T₂.mor₁) : (isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).hom.hom₂ = e₂.hom

@[simp]

theorem CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂_hom_hom₁ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T₁ T₂ : Triangle C) (hT₁ : T₁ ∈ distinguishedTriangles) (hT₂ : T₂ ∈ distinguishedTriangles) (e₁ : T₁.obj₁ ≅ T₂.obj₁) (e₂ : T₁.obj₂ ≅ T₂.obj₂) (comm : CategoryStruct.comp T₁.mor₁ e₂.hom = CategoryStruct.comp e₁.hom T₂.mor₁) : (isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).hom.hom₁ = e₁.hom