# Pretriangulated Categories #

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

## Implementation Notes #

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

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

class CategoryTheory.Pretriangulated (C : Type u) [∀ (n : ), .Additive] :
Type (max u v)

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

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

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

a class of triangle which are called distinguished

• isomorphic_distinguished : T₁CategoryTheory.Pretriangulated.distinguishedTriangles, ∀ (T₂ : ), (T₂ T₁)T₂ CategoryTheory.Pretriangulated.distinguishedTriangles

a triangle that is isomorphic to a distinguished triangle is distinguished

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

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

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

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

• rotate_distinguished_triangle : ∀ (T : ), T CategoryTheory.Pretriangulated.distinguishedTriangles T.rotate CategoryTheory.Pretriangulated.distinguishedTriangles

a triangle is distinguished iff it is so after rotating it

• complete_distinguished_triangle_morphism : ∀ (T₁ T₂ : ), T₁ CategoryTheory.Pretriangulated.distinguishedTrianglesT₂ CategoryTheory.Pretriangulated.distinguishedTriangles∀ (a : T₁.obj₁ T₂.obj₁) (b : T₁.obj₂ T₂.obj₂), = ∃ (c : T₁.obj₃ T₂.obj₃), = CategoryTheory.CategoryStruct.comp T₁.mor₃ (.map a) =

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

Instances
theorem CategoryTheory.Pretriangulated.isomorphic_distinguished {C : Type u} [∀ (n : ), .Additive] [self : ] :
T₁ CategoryTheory.Pretriangulated.distinguishedTriangles∀ (T₂ : ), (T₂ T₁)T₂ CategoryTheory.Pretriangulated.distinguishedTriangles

a triangle that is isomorphic to a distinguished triangle is distinguished

theorem CategoryTheory.Pretriangulated.contractible_distinguished {C : Type u} [∀ (n : ), .Additive] [self : ] (X : C) :
CategoryTheory.Pretriangulated.distinguishedTriangles

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

theorem CategoryTheory.Pretriangulated.distinguished_cocone_triangle {C : Type u} [∀ (n : ), .Additive] [self : ] {X : C} {Y : C} (f : X Y) :
∃ (Z : C) (g : Y Z) (h : Z .obj X), CategoryTheory.Pretriangulated.distinguishedTriangles

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

theorem CategoryTheory.Pretriangulated.rotate_distinguished_triangle {C : Type u} [∀ (n : ), .Additive] [self : ] :
T CategoryTheory.Pretriangulated.distinguishedTriangles T.rotate CategoryTheory.Pretriangulated.distinguishedTriangles

a triangle is distinguished iff it is so after rotating it

theorem CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism {C : Type u} [∀ (n : ), .Additive] [self : ] :
T₁ CategoryTheory.Pretriangulated.distinguishedTrianglesT₂ CategoryTheory.Pretriangulated.distinguishedTriangles∀ (a : T₁.obj₁ T₂.obj₁) (b : T₁.obj₂ T₂.obj₂), = ∃ (c : T₁.obj₃ T₂.obj₃), = CategoryTheory.CategoryStruct.comp T₁.mor₃ (.map a) =

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

distinguished triangles in a pretriangulated category

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Pretriangulated.distinguished_iff_of_iso {C : Type u} [∀ (n : ), .Additive] [hC : ] (e : T₁ T₂) :
T₁ CategoryTheory.Pretriangulated.distinguishedTriangles T₂ CategoryTheory.Pretriangulated.distinguishedTriangles
theorem CategoryTheory.Pretriangulated.rot_of_distTriang {C : Type u} [∀ (n : ), .Additive] [hC : ] (H : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
T.rotate CategoryTheory.Pretriangulated.distinguishedTriangles

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

theorem CategoryTheory.Pretriangulated.inv_rot_of_distTriang {C : Type u} [∀ (n : ), .Additive] [hC : ] (H : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
T.invRotate CategoryTheory.Pretriangulated.distinguishedTriangles

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

theorem CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂_assoc {C : Type u} [∀ (n : ), .Additive] [hC : ] (H : T CategoryTheory.Pretriangulated.distinguishedTriangles) {Z : C} (h : T.obj₃ Z) :
theorem CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (H : T CategoryTheory.Pretriangulated.distinguishedTriangles) :

Given any distinguished triangle

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

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

theorem CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃_assoc {C : Type u} [∀ (n : ), .Additive] [hC : ] (H : T CategoryTheory.Pretriangulated.distinguishedTriangles) {Z : C} (h : .obj T.obj₁ Z) :
theorem CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (H : T CategoryTheory.Pretriangulated.distinguishedTriangles) :

Given any distinguished triangle

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

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

theorem CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁_assoc {C : Type u} [∀ (n : ), .Additive] [hC : ] (H : T CategoryTheory.Pretriangulated.distinguishedTriangles) {Z : C} (h : .obj T.obj₂ Z) :
theorem CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (H : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
CategoryTheory.CategoryStruct.comp T.mor₃ (.map T.mor₁) = 0

Given any distinguished triangle

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

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

@[simp]
theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_X₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
= T.obj₂
@[simp]
theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_f {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
= T.mor₁
@[simp]
theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_X₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
= T.obj₃
@[simp]
theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_X₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
= T.obj₁
@[simp]
theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_g {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
= T.mor₂
def CategoryTheory.Pretriangulated.shortComplexOfDistTriangle {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_inv_τ₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (e : T T') (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
= e.inv.hom₃
@[simp]
theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_inv_τ₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (e : T T') (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
= e.inv.hom₁
@[simp]
theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_hom_τ₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (e : T T') (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
= e.hom.hom₃
@[simp]
theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_inv_τ₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (e : T T') (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
= e.inv.hom₂
@[simp]
theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_hom_τ₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (e : T T') (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
= e.hom.hom₁
@[simp]
theorem CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_hom_τ₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (e : T T') (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
= e.hom.hom₂
def CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso {C : Type u} [∀ (n : ), .Additive] [hC : ] (e : T T') (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Pretriangulated.distinguished_cocone_triangle₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] {Y : C} {Z : C} (g : Y Z) :
∃ (X : C) (f : X Y) (h : Z .obj X), CategoryTheory.Pretriangulated.distinguishedTriangles

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

theorem CategoryTheory.Pretriangulated.distinguished_cocone_triangle₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] {Z : C} {X : C} (h : Z .obj X) :
∃ (Y : C) (f : X Y) (g : Y Z), CategoryTheory.Pretriangulated.distinguishedTriangles

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

theorem CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT₁ : T₁ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₂ : T₂ CategoryTheory.Pretriangulated.distinguishedTriangles) (b : T₁.obj₂ T₂.obj₂) (c : T₁.obj₃ T₂.obj₃) (comm : = ) :
∃ (a : T₁.obj₁ T₂.obj₁), = CategoryTheory.CategoryStruct.comp T₁.mor₃ (.map a) =

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

theorem CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT₁ : T₁ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₂ : T₂ CategoryTheory.Pretriangulated.distinguishedTriangles) (a : T₁.obj₁ T₂.obj₁) (c : T₁.obj₃ T₂.obj₃) (comm : CategoryTheory.CategoryStruct.comp T₁.mor₃ (.map a) = ) :
∃ (b : T₁.obj₂ T₂.obj₂), = =

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

theorem CategoryTheory.Pretriangulated.contractible_distinguished₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (X : C) :
CategoryTheory.Pretriangulated.distinguishedTriangles

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

theorem CategoryTheory.Pretriangulated.contractible_distinguished₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (X : C) :
CategoryTheory.Pretriangulated.distinguishedTriangles

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

theorem CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) {X : C} (f : T.obj₂ X) (hf : = 0) :
∃ (g : T.obj₃ X), f =
theorem CategoryTheory.Pretriangulated.Triangle.yoneda_exact₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) {X : C} (f : T.obj₃ X) (hf : = 0) :
∃ (g : .obj T.obj₁ X), f =
theorem CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) {X : C} (f : X T.obj₂) (hf : = 0) :
∃ (g : X T.obj₁), f =
theorem CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) {X : C} (f : X .obj T.obj₁) (hf : CategoryTheory.CategoryStruct.comp f (.map T.mor₁) = 0) :
∃ (g : X T.obj₃), f =
theorem CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) {X : C} (f : X T.obj₃) (hf : = 0) :
∃ (g : X T.obj₂), f =
theorem CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_iff_epi₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
T.mor₃ = 0 CategoryTheory.Epi T.mor₂
theorem CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_iff_epi₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
T.mor₂ = 0 CategoryTheory.Epi T.mor₁
theorem CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_iff_epi₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
T.mor₁ = 0 CategoryTheory.Epi T.mor₃
theorem CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_of_epi₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.Epi T.mor₂) :
T.mor₃ = 0
theorem CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_of_epi₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.Epi T.mor₁) :
T.mor₂ = 0
theorem CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_of_epi₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.Epi T.mor₃) :
T.mor₁ = 0
theorem CategoryTheory.Pretriangulated.Triangle.epi₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h : T.mor₃ = 0) :
theorem CategoryTheory.Pretriangulated.Triangle.epi₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h : T.mor₂ = 0) :
theorem CategoryTheory.Pretriangulated.Triangle.epi₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h : T.mor₁ = 0) :
theorem CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_iff_mono₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
T.mor₁ = 0 CategoryTheory.Mono T.mor₂
theorem CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_iff_mono₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
T.mor₂ = 0 CategoryTheory.Mono T.mor₃
theorem CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_iff_mono₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
T.mor₃ = 0 CategoryTheory.Mono T.mor₁
theorem CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_of_mono₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.Mono T.mor₂) :
T.mor₁ = 0
theorem CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_of_mono₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.Mono T.mor₃) :
T.mor₂ = 0
theorem CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_of_mono₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.Mono T.mor₁) :
T.mor₃ = 0
theorem CategoryTheory.Pretriangulated.Triangle.mono₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h : T.mor₁ = 0) :
theorem CategoryTheory.Pretriangulated.Triangle.mono₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h : T.mor₂ = 0) :
theorem CategoryTheory.Pretriangulated.Triangle.mono₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h : T.mor₃ = 0) :
theorem CategoryTheory.Pretriangulated.Triangle.isZero₂_iff {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
T.mor₁ = 0 T.mor₂ = 0
theorem CategoryTheory.Pretriangulated.Triangle.isZero₁_iff {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
T.mor₁ = 0 T.mor₃ = 0
theorem CategoryTheory.Pretriangulated.Triangle.isZero₃_iff {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
T.mor₂ = 0 T.mor₃ = 0
theorem CategoryTheory.Pretriangulated.Triangle.isZero₁_of_isZero₂₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h₂ : ) (h₃ : ) :
theorem CategoryTheory.Pretriangulated.Triangle.isZero₂_of_isZero₁₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h₁ : ) (h₃ : ) :
theorem CategoryTheory.Pretriangulated.Triangle.isZero₃_of_isZero₁₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h₁ : ) (h₂ : ) :
theorem CategoryTheory.Pretriangulated.Triangle.isZero₁_iff_isIso₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
theorem CategoryTheory.Pretriangulated.Triangle.isZero₂_iff_isIso₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
theorem CategoryTheory.Pretriangulated.Triangle.isZero₃_iff_isIso₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
theorem CategoryTheory.Pretriangulated.Triangle.isZero₁_of_isIso₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.IsIso T.mor₂) :
theorem CategoryTheory.Pretriangulated.Triangle.isZero₂_of_isIso₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.IsIso T.mor₃) :
theorem CategoryTheory.Pretriangulated.Triangle.isZero₃_of_isIso₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.IsIso T.mor₁) :
theorem CategoryTheory.Pretriangulated.Triangle.shift_distinguished {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (n : ) :
CategoryTheory.Pretriangulated.distinguishedTriangles
instance CategoryTheory.Pretriangulated.instSplitEpiCategory {C : Type u} [∀ (n : ), .Additive] [hC : ] :
Equations
• =
instance CategoryTheory.Pretriangulated.instSplitMonoCategory {C : Type u} [∀ (n : ), .Additive] [hC : ] :
Equations
• =
theorem CategoryTheory.Pretriangulated.isIso₂_of_isIso₁₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (φ : T T') (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (hT' : T' CategoryTheory.Pretriangulated.distinguishedTriangles) (h₁ : CategoryTheory.IsIso φ.hom₁) (h₃ : CategoryTheory.IsIso φ.hom₃) :
theorem CategoryTheory.Pretriangulated.isIso₃_of_isIso₁₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (φ : T T') (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (hT' : T' CategoryTheory.Pretriangulated.distinguishedTriangles) (h₁ : CategoryTheory.IsIso φ.hom₁) (h₂ : CategoryTheory.IsIso φ.hom₂) :
theorem CategoryTheory.Pretriangulated.isIso₁_of_isIso₂₃ {C : Type u} [∀ (n : ), .Additive] [hC : ] (φ : T T') (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (hT' : T' CategoryTheory.Pretriangulated.distinguishedTriangles) (h₂ : CategoryTheory.IsIso φ.hom₂) (h₃ : CategoryTheory.IsIso φ.hom₃) :
@[simp]
theorem CategoryTheory.Pretriangulated.binaryBiproductData_bicone_inl {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₀ : T.mor₃ = 0) (inr : T.obj₃ T.obj₂) (inr_snd : CategoryTheory.CategoryStruct.comp inr T.mor₂ = ) (fst : T.obj₂ T.obj₁) (total : CategoryTheory.CategoryStruct.comp fst T.mor₁ + CategoryTheory.CategoryStruct.comp T.mor₂ inr = ) :
(CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.inl = T.mor₁
@[simp]
theorem CategoryTheory.Pretriangulated.binaryBiproductData_isBilimit {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₀ : T.mor₃ = 0) (inr : T.obj₃ T.obj₂) (inr_snd : CategoryTheory.CategoryStruct.comp inr T.mor₂ = ) (fst : T.obj₂ T.obj₁) (total : CategoryTheory.CategoryStruct.comp fst T.mor₁ + CategoryTheory.CategoryStruct.comp T.mor₂ inr = ) :
(CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).isBilimit = CategoryTheory.Limits.isBinaryBilimitOfTotal { pt := T.obj₂, fst := fst, snd := T.mor₂, inl := T.mor₁, inr := inr, inl_fst := , inl_snd := , inr_fst := , inr_snd := inr_snd } total
@[simp]
theorem CategoryTheory.Pretriangulated.binaryBiproductData_bicone_inr {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₀ : T.mor₃ = 0) (inr : T.obj₃ T.obj₂) (inr_snd : CategoryTheory.CategoryStruct.comp inr T.mor₂ = ) (fst : T.obj₂ T.obj₁) (total : CategoryTheory.CategoryStruct.comp fst T.mor₁ + CategoryTheory.CategoryStruct.comp T.mor₂ inr = ) :
(CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.inr = inr
@[simp]
theorem CategoryTheory.Pretriangulated.binaryBiproductData_bicone_fst {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₀ : T.mor₃ = 0) (inr : T.obj₃ T.obj₂) (inr_snd : CategoryTheory.CategoryStruct.comp inr T.mor₂ = ) (fst : T.obj₂ T.obj₁) (total : CategoryTheory.CategoryStruct.comp fst T.mor₁ + CategoryTheory.CategoryStruct.comp T.mor₂ inr = ) :
(CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.fst = fst
@[simp]
theorem CategoryTheory.Pretriangulated.binaryBiproductData_bicone_snd {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₀ : T.mor₃ = 0) (inr : T.obj₃ T.obj₂) (inr_snd : CategoryTheory.CategoryStruct.comp inr T.mor₂ = ) (fst : T.obj₂ T.obj₁) (total : CategoryTheory.CategoryStruct.comp fst T.mor₁ + CategoryTheory.CategoryStruct.comp T.mor₂ inr = ) :
(CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.snd = T.mor₂
@[simp]
theorem CategoryTheory.Pretriangulated.binaryBiproductData_bicone_pt {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₀ : T.mor₃ = 0) (inr : T.obj₃ T.obj₂) (inr_snd : CategoryTheory.CategoryStruct.comp inr T.mor₂ = ) (fst : T.obj₂ T.obj₁) (total : CategoryTheory.CategoryStruct.comp fst T.mor₁ + CategoryTheory.CategoryStruct.comp T.mor₂ inr = ) :
(CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.pt = T.obj₂
def CategoryTheory.Pretriangulated.binaryBiproductData {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₀ : T.mor₃ = 0) (inr : T.obj₃ T.obj₂) (inr_snd : CategoryTheory.CategoryStruct.comp inr T.mor₂ = ) (fst : T.obj₂ T.obj₁) (total : CategoryTheory.CategoryStruct.comp fst T.mor₁ + CategoryTheory.CategoryStruct.comp T.mor₂ inr = ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Pretriangulated.instHasBinaryBiproducts {C : Type u} [∀ (n : ), .Additive] [hC : ] :
Equations
• =
instance CategoryTheory.Pretriangulated.instHasFiniteProducts {C : Type u} [∀ (n : ), .Additive] [hC : ] :
Equations
• =
instance CategoryTheory.Pretriangulated.instHasFiniteCoproducts {C : Type u} [∀ (n : ), .Additive] [hC : ] :
Equations
• =
instance CategoryTheory.Pretriangulated.instHasFiniteBiproducts {C : Type u} [∀ (n : ), .Additive] [hC : ] :
Equations
• =
theorem CategoryTheory.Pretriangulated.exists_iso_binaryBiproduct_of_distTriang {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (zero : T.mor₃ = 0) :
∃ (e : T.obj₂ T.obj₁ T.obj₃), CategoryTheory.CategoryStruct.comp T.mor₁ e.hom = CategoryTheory.Limits.biprod.inl T.mor₂ = CategoryTheory.CategoryStruct.comp e.hom CategoryTheory.Limits.biprod.snd
theorem CategoryTheory.Pretriangulated.binaryBiproductTriangle_distinguished {C : Type u} [∀ (n : ), .Additive] [hC : ] (X₁ : C) (X₂ : C) :
CategoryTheory.Pretriangulated.distinguishedTriangles
theorem CategoryTheory.Pretriangulated.binaryProductTriangle_distinguished {C : Type u} [∀ (n : ), .Additive] [hC : ] (X₁ : C) (X₂ : C) :
CategoryTheory.Pretriangulated.distinguishedTriangles
@[simp]
theorem CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism_hom₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT₁ : T₁ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₂ : T₂ CategoryTheory.Pretriangulated.distinguishedTriangles) (a : T₁.obj₁ T₂.obj₁) (b : T₁.obj₂ T₂.obj₂) (comm : = ) :
().hom₁ = a
@[simp]
theorem CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism_hom₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT₁ : T₁ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₂ : T₂ CategoryTheory.Pretriangulated.distinguishedTriangles) (a : T₁.obj₁ T₂.obj₁) (b : T₁.obj₂ T₂.obj₂) (comm : = ) :
().hom₂ = b
def CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT₁ : T₁ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₂ : T₂ CategoryTheory.Pretriangulated.distinguishedTriangles) (a : T₁.obj₁ T₂.obj₁) (b : T₁.obj₂ T₂.obj₂) (comm : = ) :
T₁ T₂

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

Equations
• = let_fun h := ; { hom₁ := a, hom₂ := b, hom₃ := h.choose, comm₁ := comm, comm₂ := , comm₃ := }
Instances For
theorem CategoryTheory.Pretriangulated.productTriangle_distinguished {C : Type u} [∀ (n : ), .Additive] [hC : ] {J : Type u_1} (T : ) (hT : ∀ (j : J), T j CategoryTheory.Pretriangulated.distinguishedTriangles) [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.Pretriangulated.distinguishedTriangles

A product of distinguished triangles is distinguished

theorem CategoryTheory.Pretriangulated.exists_iso_of_arrow_iso {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT₁ : T₁ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₂ : T₂ CategoryTheory.Pretriangulated.distinguishedTriangles) (e : CategoryTheory.Arrow.mk T₁.mor₁ CategoryTheory.Arrow.mk T₂.mor₁) :
∃ (e' : T₁ T₂), e'.hom.hom₁ = e.hom.left e'.hom.hom₂ = e.hom.right
@[simp]
theorem CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂_inv_hom₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT₁ : T₁ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₂ : T₂ CategoryTheory.Pretriangulated.distinguishedTriangles) (e₁ : T₁.obj₁ T₂.obj₁) (e₂ : T₁.obj₂ T₂.obj₂) (comm : CategoryTheory.CategoryStruct.comp T₁.mor₁ e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom T₂.mor₁) :
(CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).inv.hom₂ = e₂.inv
@[simp]
theorem CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂_inv_hom₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT₁ : T₁ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₂ : T₂ CategoryTheory.Pretriangulated.distinguishedTriangles) (e₁ : T₁.obj₁ T₂.obj₁) (e₂ : T₁.obj₂ T₂.obj₂) (comm : CategoryTheory.CategoryStruct.comp T₁.mor₁ e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom T₂.mor₁) :
(CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).inv.hom₁ = e₁.inv
@[simp]
theorem CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂_hom_hom₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT₁ : T₁ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₂ : T₂ CategoryTheory.Pretriangulated.distinguishedTriangles) (e₁ : T₁.obj₁ T₂.obj₁) (e₂ : T₁.obj₂ T₂.obj₂) (comm : CategoryTheory.CategoryStruct.comp T₁.mor₁ e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom T₂.mor₁) :
(CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).hom.hom₂ = e₂.hom
@[simp]
theorem CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂_hom_hom₁ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT₁ : T₁ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₂ : T₂ CategoryTheory.Pretriangulated.distinguishedTriangles) (e₁ : T₁.obj₁ T₂.obj₁) (e₂ : T₁.obj₂ T₂.obj₂) (comm : CategoryTheory.CategoryStruct.comp T₁.mor₁ e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom T₂.mor₁) :
(CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).hom.hom₁ = e₁.hom
def CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ {C : Type u} [∀ (n : ), .Additive] [hC : ] (hT₁ : T₁ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₂ : T₂ CategoryTheory.Pretriangulated.distinguishedTriangles) (e₁ : T₁.obj₁ T₂.obj₁) (e₂ : T₁.obj₂ T₂.obj₂) (comm : CategoryTheory.CategoryStruct.comp T₁.mor₁ e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom T₂.mor₁) :
T₁ T₂

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

Equations
Instances For