Triangles

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

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

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

A triangle in C is a sextuple (X,Y,Z,f,g,h) where X,Y,Z are objects of C, and f : X ⟶ Y, g : Y ⟶ Z, h : Z ⟶ X⟦1⟧ are morphisms in C. See https://stacks.math.columbia.edu/tag/0144.

• mk' :: (
• obj₁ : C

  the first object of a triangle

• obj₂ : C

  the second object of a triangle

• obj₃ : C

  the third object of a triangle

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

  the first morphism of a triangle

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

  the second morphism of a triangle

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

  the third morphism of a triangle

• )

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

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

Equations

• CategoryTheory.Pretriangulated.Triangle.mk f g h = { obj₁ := X, obj₂ := Y, obj₃ := Z, mor₁ := f, mor₂ := g, mor₃ := h }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.Pretriangulated.instInhabitedTriangle = { default := { obj₁ := 0, obj₂ := 0, obj₃ := 0, mor₁ := 0, mor₂ := 0, mor₃ := 0 } }

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

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

Equations

• CategoryTheory.Pretriangulated.contractibleTriangle X = CategoryTheory.Pretriangulated.Triangle.mk (CategoryTheory.CategoryStruct.id X) 0 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

  the first morphism in a triangle morphism

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

  the second morphism in a triangle morphism

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

  the third morphism in a triangle morphism

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

  the first commutative square of a triangle morphism

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

  the second commutative square of a triangle morphism

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

  the third commutative square of a triangle morphism

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The identity triangle morphism.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.Pretriangulated.instInhabitedTriangleMorphism T = { default := CategoryTheory.Pretriangulated.triangleMorphismId T }

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

Composition of triangle morphisms gives a triangle morphism.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Triangles with triangle morphisms form a category.

Equations

• CategoryTheory.Pretriangulated.triangleCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

Equations

• A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃ = { hom₁ := hom₁, hom₂ := hom₂, hom₃ := hom₃, comm₁ := comm₁, comm₂ := comm₂, comm₃ := comm₃ }

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

Equations

• CategoryTheory.Pretriangulated.binaryBiproductTriangle X₁ X₂ = CategoryTheory.Pretriangulated.Triangle.mk CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.snd 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The product of a family of triangles.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

A projection from the product of a family of triangles.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The fan given by productTriangle T.

Equations

• CategoryTheory.Pretriangulated.productTriangle.fan T = CategoryTheory.Limits.Fan.mk (CategoryTheory.Pretriangulated.productTriangle T) (CategoryTheory.Pretriangulated.productTriangle.π T)

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The first projection Triangle C ⥤ C.

Equations

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

@[simp]

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

@[simp]

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

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

The second projection Triangle C ⥤ C.

Equations

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

@[simp]

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

@[simp]

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

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

The third projection Triangle C ⥤ C.

Equations

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

@[simp]

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

@[simp]

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

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

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

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