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) [CategoryTheory.Category.{v, u} C] [CategoryTheory.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 .

• mk' :: (
• obj₁ : C

  the first object of a triangle

• obj₂ : C

  the second object of a triangle

• obj₃ : C

  the third object of a triangle

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

  the first morphism of a triangle

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

  the second morphism of a triangle

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

  the third morphism of a triangle

• )

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Pretriangulated.Triangle.mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj X) : CategoryTheory.Pretriangulated.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 }

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Pretriangulated.contractibleTriangle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Pretriangulated.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

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

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

structure CategoryTheory.Pretriangulated.TriangleMorphism {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (T₁ : CategoryTheory.Pretriangulated.Triangle C) (T₂ : CategoryTheory.Pretriangulated.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 .

• 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₁ : CategoryTheory.CategoryStruct.comp T₁.mor₁ self.hom₂ = CategoryTheory.CategoryStruct.comp self.hom₁ T₂.mor₁

  the first commutative square of a triangle morphism

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

  the second commutative square of a triangle morphism

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

  the third commutative square of a triangle morphism

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The identity triangle morphism.

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Pretriangulated.TriangleMorphism.comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {T₁ : CategoryTheory.Pretriangulated.Triangle C} {T₂ : CategoryTheory.Pretriangulated.Triangle C} {T₃ : CategoryTheory.Pretriangulated.Triangle C} (f : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂) (g : CategoryTheory.Pretriangulated.TriangleMorphism T₂ T₃) : CategoryTheory.Pretriangulated.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.triangleCategory_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (A : CategoryTheory.Pretriangulated.Triangle C) : CategoryTheory.CategoryStruct.id A = CategoryTheory.Pretriangulated.triangleMorphismId A

@[simp]

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

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

Triangles with triangle morphisms form a category.

Equations

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

theorem CategoryTheory.Pretriangulated.Triangle.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {A : CategoryTheory.Pretriangulated.Triangle C} {B : CategoryTheory.Pretriangulated.Triangle C} (f : A ⟶ B) (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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (A : CategoryTheory.Pretriangulated.Triangle C) : (CategoryTheory.CategoryStruct.id A).hom₁ = CategoryTheory.CategoryStruct.id A.obj₁

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.Pretriangulated.Triangle.homMk A B hom₁ hom₂ hom₃ = CategoryTheory.Pretriangulated.TriangleMorphism.mk hom₁ hom₂ hom₃

@[simp]

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

@[simp]

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

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

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Pretriangulated.binaryBiproductTriangle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (X₁ : C) (X₂ : C) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂] : CategoryTheory.Pretriangulated.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.binaryProductTriangle_mor₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (X₁ : C) (X₂ : C) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryProduct X₁ X₂] : (CategoryTheory.Pretriangulated.binaryProductTriangle X₁ X₂).mor₂ = CategoryTheory.Limits.prod.snd

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Pretriangulated.binaryProductTriangle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (X₁ : C) (X₂ : C) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryProduct X₁ X₂] : CategoryTheory.Pretriangulated.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.binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (X₁ : C) (X₂ : C) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂] : (CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).hom.hom₂ = CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (X₁ : C) (X₂ : C) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂] : CategoryTheory.Pretriangulated.binaryProductTriangle X₁ X₂ ≅ CategoryTheory.Pretriangulated.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.productTriangle_obj₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun (j : J) => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun (j : J) => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun (j : J) => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun (j : J) => (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj (T j).obj₁] : (CategoryTheory.Pretriangulated.productTriangle T).obj₂ = ∏ fun (j : J) => (T j).obj₂

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

def CategoryTheory.Pretriangulated.productTriangle.isLimitFan {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun (j : J) => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun (j : J) => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun (j : J) => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun (j : J) => (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj (T j).obj₁] : CategoryTheory.Limits.IsLimit (CategoryTheory.Pretriangulated.productTriangle.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun (j : J) => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun (j : J) => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun (j : J) => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun (j : J) => (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj (T j).obj₁] [CategoryTheory.Limits.HasZeroMorphisms C] (h : ∀ (j : J), CategoryTheory.CategoryStruct.comp (T j).mor₃ ((CategoryTheory.shiftFunctor C 1).toPrefunctor.map (T j).mor₁) = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Pretriangulated.productTriangle T).mor₃ ((CategoryTheory.shiftFunctor C 1).toPrefunctor.map (CategoryTheory.Pretriangulated.productTriangle T).mor₁) = 0