# 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

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₃ .obj self.obj₁

the third morphism of a triangle

• )
Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.mk_mor₃ {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : Z .obj X) :
.mor₃ = h
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.mk_mor₂ {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : Z .obj X) :
.mor₂ = g
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.mk_obj₂ {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : Z .obj X) :
.obj₂ = Y
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.mk_obj₁ {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : Z .obj X) :
.obj₁ = X
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.mk_mor₁ {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : Z .obj X) :
.mor₁ = f
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.mk_obj₃ {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : Z .obj X) :
.obj₃ = Z
def CategoryTheory.Pretriangulated.Triangle.mk {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : Z .obj X) :

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
• = { obj₁ := X, obj₂ := Y, obj₃ := Z, mor₁ := f, mor₂ := g, mor₃ := h }
Instances For
Equations
• CategoryTheory.Pretriangulated.instInhabitedTriangle = { default := { obj₁ := 0, obj₂ := 0, obj₃ := 0, mor₁ := 0, mor₂ := 0, mor₃ := 0 } }
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]

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

Equations
Instances For
theorem CategoryTheory.Pretriangulated.TriangleMorphism.ext {C : Type u} :
∀ {inst : } {inst_1 : } {T₁ T₂ : } (x y : ), x.hom₁ = y.hom₁x.hom₂ = y.hom₂x.hom₃ = y.hom₃x = y
theorem CategoryTheory.Pretriangulated.TriangleMorphism.ext_iff {C : Type u} :
∀ {inst : } {inst_1 : } {T₁ T₂ : } (x y : ), x = y x.hom₁ = y.hom₁ x.hom₂ = y.hom₂ x.hom₃ = y.hom₃

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'

Instances For
@[simp]

the first commutative square of a triangle morphism

@[simp]

the second commutative square of a triangle morphism

@[simp]
theorem CategoryTheory.Pretriangulated.TriangleMorphism.comm₃ {C : Type u} (self : ) :
CategoryTheory.CategoryStruct.comp T₁.mor₃ (.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} (self : ) {Z : C} (h : .obj T₂.obj₁ Z) :
@[simp]
@[simp]
@[simp]

The identity triangle morphism.

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

Composition of triangle morphisms gives a triangle morphism.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.triangleCategory_comp {C : Type u} :
∀ {X Y Z : } (f : X Y) (g : Y Z),
@[simp]

Triangles with triangle morphisms form a category.

Equations
• CategoryTheory.Pretriangulated.triangleCategory =
theorem CategoryTheory.Pretriangulated.Triangle.hom_ext {C : Type u} (f : A B) (g : A B) (h₁ : f.hom₁ = g.hom₁) (h₂ : f.hom₂ = g.hom₂) (h₃ : f.hom₃ = g.hom₃) :
f = g
theorem CategoryTheory.Pretriangulated.comp_hom₁_assoc {C : Type u} (f : X Y) (g : Y Z✝) {Z : C} (h : Z✝.obj₁ Z) :
@[simp]
theorem CategoryTheory.Pretriangulated.comp_hom₁ {C : Type u} (f : X Y) (g : Y Z) :
.hom₁ = CategoryTheory.CategoryStruct.comp f.hom₁ g.hom₁
theorem CategoryTheory.Pretriangulated.comp_hom₂_assoc {C : Type u} (f : X Y) (g : Y Z✝) {Z : C} (h : Z✝.obj₂ Z) :
@[simp]
theorem CategoryTheory.Pretriangulated.comp_hom₂ {C : Type u} (f : X Y) (g : Y Z) :
.hom₂ = CategoryTheory.CategoryStruct.comp f.hom₂ g.hom₂
theorem CategoryTheory.Pretriangulated.comp_hom₃_assoc {C : Type u} (f : X Y) (g : Y Z✝) {Z : C} (h : Z✝.obj₃ Z) :
@[simp]
theorem CategoryTheory.Pretriangulated.comp_hom₃ {C : Type u} (f : X Y) (g : Y Z) :
.hom₃ = CategoryTheory.CategoryStruct.comp f.hom₃ g.hom₃
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.homMk_hom₃ {C : Type u} (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₃ (.map hom₁) = CategoryTheory.CategoryStruct.comp hom₃ B.mor₃) _auto✝) :
(A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₃ = hom₃
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.homMk_hom₁ {C : Type u} (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₃ (.map hom₁) = CategoryTheory.CategoryStruct.comp hom₃ B.mor₃) _auto✝) :
(A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₁ = hom₁
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.homMk_hom₂ {C : Type u} (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₃ (.map hom₁) = CategoryTheory.CategoryStruct.comp hom₃ B.mor₃) _auto✝) :
(A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₂ = hom₂
def CategoryTheory.Pretriangulated.Triangle.homMk {C : Type u} (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₃ (.map hom₁) = CategoryTheory.CategoryStruct.comp hom₃ B.mor₃) _auto✝) :
A B
Equations
• A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃ = { hom₁ := hom₁, hom₂ := hom₂, hom₃ := hom₃, comm₁ := comm₁, comm₂ := comm₂, comm₃ := comm₃ }
Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.isoMk_hom {C : Type u} (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₃ (.map iso₁.hom) = CategoryTheory.CategoryStruct.comp iso₃.hom B.mor₃) _auto✝) :
(A.isoMk B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).hom = A.homMk B iso₁.hom iso₂.hom iso₃.hom comm₁ comm₂ comm₃
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.isoMk_inv {C : Type u} (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₃ (.map iso₁.hom) = CategoryTheory.CategoryStruct.comp iso₃.hom B.mor₃) _auto✝) :
(A.isoMk B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).inv = B.homMk A iso₁.inv iso₂.inv iso₃.inv
def CategoryTheory.Pretriangulated.Triangle.isoMk {C : Type u} (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₃ (.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.
Instances For
theorem CategoryTheory.Pretriangulated.Triangle.isIso_of_isIsos {C : Type u} (f : A B) (h₁ : CategoryTheory.IsIso f.hom₁) (h₂ : CategoryTheory.IsIso f.hom₂) (h₃ : CategoryTheory.IsIso f.hom₃) :
@[simp]
theorem CategoryTheory.Iso.hom_inv_id_triangle_hom₁_assoc {C : Type u} (e : A B) {Z : C} (h : A.obj₁ Z) :
@[simp]
theorem CategoryTheory.Iso.hom_inv_id_triangle_hom₁ {C : Type u} (e : A B) :
CategoryTheory.CategoryStruct.comp e.hom.hom₁ e.inv.hom₁ =
@[simp]
theorem CategoryTheory.Iso.hom_inv_id_triangle_hom₂_assoc {C : Type u} (e : A B) {Z : C} (h : A.obj₂ Z) :
@[simp]
theorem CategoryTheory.Iso.hom_inv_id_triangle_hom₂ {C : Type u} (e : A B) :
CategoryTheory.CategoryStruct.comp e.hom.hom₂ e.inv.hom₂ =
@[simp]
theorem CategoryTheory.Iso.hom_inv_id_triangle_hom₃_assoc {C : Type u} (e : A B) {Z : C} (h : A.obj₃ Z) :
@[simp]
theorem CategoryTheory.Iso.hom_inv_id_triangle_hom₃ {C : Type u} (e : A B) :
CategoryTheory.CategoryStruct.comp e.hom.hom₃ e.inv.hom₃ =
@[simp]
theorem CategoryTheory.Iso.inv_hom_id_triangle_hom₁_assoc {C : Type u} (e : A B) {Z : C} (h : B.obj₁ Z) :
@[simp]
theorem CategoryTheory.Iso.inv_hom_id_triangle_hom₁ {C : Type u} (e : A B) :
CategoryTheory.CategoryStruct.comp e.inv.hom₁ e.hom.hom₁ =
@[simp]
theorem CategoryTheory.Iso.inv_hom_id_triangle_hom₂_assoc {C : Type u} (e : A B) {Z : C} (h : B.obj₂ Z) :
@[simp]
theorem CategoryTheory.Iso.inv_hom_id_triangle_hom₂ {C : Type u} (e : A B) :
CategoryTheory.CategoryStruct.comp e.inv.hom₂ e.hom.hom₂ =
@[simp]
theorem CategoryTheory.Iso.inv_hom_id_triangle_hom₃_assoc {C : Type u} (e : A B) {Z : C} (h : B.obj₃ Z) :
@[simp]
theorem CategoryTheory.Iso.inv_hom_id_triangle_hom₃ {C : Type u} (e : A B) :
CategoryTheory.CategoryStruct.comp e.inv.hom₃ e.hom.hom₃ =
@[simp]
theorem CategoryTheory.Pretriangulated.binaryBiproductTriangle_obj₂ {C : Type u} (X₁ : C) (X₂ : C) :
= (X₁ X₂)
@[simp]
theorem CategoryTheory.Pretriangulated.binaryBiproductTriangle_mor₁ {C : Type u} (X₁ : C) (X₂ : C) :
= CategoryTheory.Limits.biprod.inl
@[simp]
theorem CategoryTheory.Pretriangulated.binaryBiproductTriangle_mor₃ {C : Type u} (X₁ : C) (X₂ : C) :
= 0
@[simp]
theorem CategoryTheory.Pretriangulated.binaryBiproductTriangle_mor₂ {C : Type u} (X₁ : C) (X₂ : C) :
= CategoryTheory.Limits.biprod.snd
@[simp]
theorem CategoryTheory.Pretriangulated.binaryBiproductTriangle_obj₁ {C : Type u} (X₁ : C) (X₂ : C) :
= X₁
@[simp]
theorem CategoryTheory.Pretriangulated.binaryBiproductTriangle_obj₃ {C : Type u} (X₁ : C) (X₂ : C) :
= X₂

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.binaryProductTriangle_obj₃ {C : Type u} (X₁ : C) (X₂ : C) :
.obj₃ = X₂
@[simp]
theorem CategoryTheory.Pretriangulated.binaryProductTriangle_mor₂ {C : Type u} (X₁ : C) (X₂ : C) :
.mor₂ = CategoryTheory.Limits.prod.snd
@[simp]
theorem CategoryTheory.Pretriangulated.binaryProductTriangle_mor₃ {C : Type u} (X₁ : C) (X₂ : C) :
.mor₃ = 0
@[simp]
theorem CategoryTheory.Pretriangulated.binaryProductTriangle_obj₂ {C : Type u} (X₁ : C) (X₂ : C) :
.obj₂ = (X₁ X₂)
@[simp]
theorem CategoryTheory.Pretriangulated.binaryProductTriangle_obj₁ {C : Type u} (X₁ : C) (X₂ : C) :
.obj₁ = X₁
@[simp]

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
theorem CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₂ {C : Type u} (X₁ : C) (X₂ : C) :
= CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd
@[simp]
@[simp]
theorem CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₂ {C : Type u} (X₁ : C) (X₂ : C) :
= CategoryTheory.Limits.prod.lift CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd
@[simp]
@[simp]

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.productTriangle_obj₃ {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] :
= ∏ᶜ fun (j : J) => (T j).obj₃
@[simp]
theorem CategoryTheory.Pretriangulated.productTriangle_obj₁ {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] :
= ∏ᶜ fun (j : J) => (T j).obj₁
@[simp]
theorem CategoryTheory.Pretriangulated.productTriangle_mor₁ {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] :
= CategoryTheory.Limits.Pi.map fun (j : J) => (T j).mor₁
@[simp]
theorem CategoryTheory.Pretriangulated.productTriangle_mor₂ {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] :
= CategoryTheory.Limits.Pi.map fun (j : J) => (T j).mor₂
@[simp]
theorem CategoryTheory.Pretriangulated.productTriangle_mor₃ {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] :
@[simp]
theorem CategoryTheory.Pretriangulated.productTriangle_obj₂ {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] :
= ∏ᶜ fun (j : J) => (T j).obj₂
def CategoryTheory.Pretriangulated.productTriangle {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] :

The product of a family of triangles.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.productTriangle.π_hom₃ {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] (j : J) :
= CategoryTheory.Limits.Pi.π (fun (j : J) => (T j).obj₃) j
@[simp]
theorem CategoryTheory.Pretriangulated.productTriangle.π_hom₂ {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] (j : J) :
= CategoryTheory.Limits.Pi.π (fun (j : J) => (T j).obj₂) j
@[simp]
theorem CategoryTheory.Pretriangulated.productTriangle.π_hom₁ {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] (j : J) :
= CategoryTheory.Limits.Pi.π (fun (j : J) => (T j).obj₁) j
def CategoryTheory.Pretriangulated.productTriangle.π {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] (j : J) :

A projection from the product of a family of triangles.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Pretriangulated.productTriangle.fan {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] :

The fan given by productTriangle T.

Equations
Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.productTriangle.lift_hom₃ {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] (φ : (j : J) → T' T j) :
= CategoryTheory.Limits.Pi.lift fun (j : J) => (φ j).hom₃
@[simp]
theorem CategoryTheory.Pretriangulated.productTriangle.lift_hom₂ {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] (φ : (j : J) → T' T j) :
= CategoryTheory.Limits.Pi.lift fun (j : J) => (φ j).hom₂
@[simp]
theorem CategoryTheory.Pretriangulated.productTriangle.lift_hom₁ {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] (φ : (j : J) → T' T j) :
= CategoryTheory.Limits.Pi.lift fun (j : J) => (φ j).hom₁
def CategoryTheory.Pretriangulated.productTriangle.lift {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] (φ : (j : J) → T' T j) :

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.
Instances For
def CategoryTheory.Pretriangulated.productTriangle.isLimitFan {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] :

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.
Instances For
theorem CategoryTheory.Pretriangulated.productTriangle.zero₃₁ {C : Type u} {J : Type u_1} (T : ) [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) => .obj (T j).obj₁] (h : ∀ (j : J), CategoryTheory.CategoryStruct.comp (T j).mor₃ (.map (T j).mor₁) = 0) :
@[simp]
theorem CategoryTheory.Pretriangulated.contractibleTriangleFunctor_map_hom₃ (C : Type u) :
∀ {X Y : C} (f : X Y), .hom₃ = 0
@[simp]
theorem CategoryTheory.Pretriangulated.contractibleTriangleFunctor_map_hom₂ (C : Type u) :
∀ {X Y : C} (f : X Y), .hom₂ = f
@[simp]
@[simp]
theorem CategoryTheory.Pretriangulated.contractibleTriangleFunctor_map_hom₁ (C : Type u) :
∀ {X Y : C} (f : X Y), .hom₁ = f

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.π₁_map {C : Type u} :
∀ {X Y : } (f : X Y), CategoryTheory.Pretriangulated.Triangle.π₁.map f = f.hom₁
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.π₁_obj {C : Type u} :
CategoryTheory.Pretriangulated.Triangle.π₁.obj T = T.obj₁

The first projection Triangle C ⥤ C.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.π₂_map {C : Type u} :
∀ {X Y : } (f : X Y), CategoryTheory.Pretriangulated.Triangle.π₂.map f = f.hom₂
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.π₂_obj {C : Type u} :
CategoryTheory.Pretriangulated.Triangle.π₂.obj T = T.obj₂

The second projection Triangle C ⥤ C.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.π₃_obj {C : Type u} :
CategoryTheory.Pretriangulated.Triangle.π₃.obj T = T.obj₃
@[simp]
theorem CategoryTheory.Pretriangulated.Triangle.π₃_map {C : Type u} :
∀ {X Y : } (f : X Y), CategoryTheory.Pretriangulated.Triangle.π₃.map f = f.hom₃

The third projection Triangle C ⥤ C.

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