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

source

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

Type (max u v)

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

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

Given a diagram:

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

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

distinguishedTriangles : Set (Triangle C)
a class of triangle which are called distinguished
isomorphic_distinguished (T₁ : Triangle C) : T₁ ∈ distinguishedTriangles → ∀ (T₂ : Triangle C) (x : T₂ ≅ T₁), T₂ ∈ distinguishedTriangles
a triangle that is isomorphic to a distinguished triangle is distinguished
contractible_distinguished (X : C) : contractibleTriangle X ∈ distinguishedTriangles
obvious triangles X ⟶ X ⟶ 0 ⟶ X⟦1⟧ are distinguished
distinguished_cocone_triangle {X Y : C} (f : X ⟶ Y) : ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ (shiftFunctor C 1).obj X), Triangle.mk f g h ∈ distinguishedTriangles
any morphism X ⟶ Y is part of a distinguished triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧
rotate_distinguished_triangle (T : Triangle C) : T ∈ distinguishedTriangles ↔ T.rotate ∈ distinguishedTriangles
a triangle is distinguished iff it is so after rotating it
complete_distinguished_triangle_morphism (T₁ T₂ : Triangle C) : T₁ ∈ distinguishedTriangles → T₂ ∈ distinguishedTriangles → ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂), CategoryStruct.comp T₁.mor₁ b = CategoryStruct.comp a T₂.mor₁ → ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), CategoryStruct.comp T₁.mor₂ c = CategoryStruct.comp b T₂.mor₂ ∧ CategoryStruct.comp T₁.mor₃ ((shiftFunctor C 1).map a) = CategoryStruct.comp c T₂.mor₃
given two distinguished triangle, a commutative square can be extended as morphism of triangles

Instances

source

def CategoryTheory.Pretriangulated.termDistTriang_ :

Lean.ParserDescr

distinguished triangles in a pretriangulated category

Equations

Instances For

source

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

T₁ ∈ distinguishedTriangles ↔ T₂ ∈ distinguishedTriangles

source

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

T.rotate ∈ distinguishedTriangles

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

source

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

T.invRotate ∈ distinguishedTriangles

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

source

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

CategoryStruct.comp T.mor₁ T.mor₂ = 0

Given any distinguished triangle

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

the composition f ≫ g = 0.

Stacks Tag 0146

source

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

CategoryStruct.comp T.mor₁ (CategoryStruct.comp T.mor₂ h) = CategoryStruct.comp 0 h

source

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

CategoryStruct.comp T.mor₂ T.mor₃ = 0

Given any distinguished triangle

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

the composition g ≫ h = 0.

Stacks Tag 0146

source

theorem CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃_assoc {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T : Triangle C) (H : T ∈ distinguishedTriangles) {Z : C} (h : (shiftFunctor C 1).obj T.obj₁ ⟶ Z) :

CategoryStruct.comp T.mor₂ (CategoryStruct.comp T.mor₃ h) = CategoryStruct.comp 0 h

source

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

CategoryStruct.comp T.mor₃ ((shiftFunctor C 1).map T.mor₁) = 0

Given any distinguished triangle

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

the composition h ≫ f⟦1⟧ = 0.

Stacks Tag 0146

source

theorem CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁_assoc {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] (T : Triangle C) (H : T ∈ distinguishedTriangles) {Z : C} (h : (shiftFunctor C 1).obj T.obj₂ ⟶ Z) :

CategoryStruct.comp T.mor₃ (CategoryStruct.comp ((shiftFunctor C 1).map T.mor₁) h) = CategoryStruct.comp 0 h

source

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

ShortComplex C

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

Equations

Instances For

source

@[simp]

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

(shortComplexOfDistTriangle T hT).f = T.mor₁

source

@[simp]

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

(shortComplexOfDistTriangle T hT).X₂ = T.obj₂

source

@[simp]

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

(shortComplexOfDistTriangle T hT).X₃ = T.obj₃

source

@[simp]

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

(shortComplexOfDistTriangle T hT).X₁ = T.obj₁

source

@[simp]

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

(shortComplexOfDistTriangle T hT).g = T.mor₂

source

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

shortComplexOfDistTriangle T hT ≅ shortComplexOfDistTriangle T' ⋯

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

Equations

Instances For

source

@[simp]

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

(shortComplexOfDistTriangleIsoOfIso e hT).inv.τ₂ = e.inv.hom₂

source

@[simp]

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

(shortComplexOfDistTriangleIsoOfIso e hT).inv.τ₁ = e.inv.hom₁

source

@[simp]

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

(shortComplexOfDistTriangleIsoOfIso e hT).hom.τ₂ = e.hom.hom₂

source

@[simp]

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

(shortComplexOfDistTriangleIsoOfIso e hT).hom.τ₁ = e.hom.hom₁

source

@[simp]

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

(shortComplexOfDistTriangleIsoOfIso e hT).hom.τ₃ = e.hom.hom₃

source

@[simp]

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

(shortComplexOfDistTriangleIsoOfIso e hT).inv.τ₃ = e.inv.hom₃

source

theorem CategoryTheory.Pretriangulated.distinguished_cocone_triangle₁ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] {Y Z : C} (g : Y ⟶ Z) :

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

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

source

theorem CategoryTheory.Pretriangulated.distinguished_cocone_triangle₂ {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] {Z X : C} (h : Z ⟶ (shiftFunctor C 1).obj X) :

∃ (Y : C) (f : X ⟶ Y) (g : Y ⟶ Z), Triangle.mk f g h ∈ distinguishedTriangles

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

source

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

∃ (a : T₁.obj₁ ⟶ T₂.obj₁), CategoryStruct.comp T₁.mor₁ b = CategoryStruct.comp a T₂.mor₁ ∧ CategoryStruct.comp T₁.mor₃ ((shiftFunctor C 1).map a) = CategoryStruct.comp c T₂.mor₃

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

source

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

∃ (b : T₁.obj₂ ⟶ T₂.obj₂), CategoryStruct.comp T₁.mor₁ b = CategoryStruct.comp a T₂.mor₁ ∧ CategoryStruct.comp T₁.mor₂ c = CategoryStruct.comp b T₂.mor₂

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

source

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

Triangle.mk 0 (CategoryStruct.id X) 0 ∈ distinguishedTriangles

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

source

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

Triangle.mk 0 0 (CategoryStruct.id ((shiftFunctor C 1).obj X)) ∈ distinguishedTriangles

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

source

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

∃ (g : T.obj₃ ⟶ X), f = CategoryStruct.comp T.mor₂ g

source

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

∃ (g : (CategoryTheory.shiftFunctor C 1).obj T.obj₁ ⟶ X), f = CategoryStruct.comp T.mor₃ g

source

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

∃ (g : X ⟶ T.obj₁), f = CategoryStruct.comp g T.mor₁

source

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

∃ (g : X ⟶ T.obj₃), f = CategoryStruct.comp g T.mor₃

source

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

∃ (g : X ⟶ T.obj₂), f = CategoryStruct.comp g T.mor₂

source

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

T.mor₃ = 0 ↔ Epi T.mor₂

source

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

T.mor₂ = 0 ↔ Epi T.mor₁

source

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

T.mor₁ = 0 ↔ Epi T.mor₃

source

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

T.mor₃ = 0

source

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

T.mor₂ = 0

source

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

T.mor₁ = 0

source

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

Epi T.mor₂

source

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

Epi T.mor₁

source

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

Epi T.mor₃

source

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

T.mor₁ = 0 ↔ Mono T.mor₂

source

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

T.mor₂ = 0 ↔ Mono T.mor₃

source

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

T.mor₃ = 0 ↔ Mono T.mor₁

source

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

T.mor₁ = 0

source

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

T.mor₂ = 0

source

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

T.mor₃ = 0

source

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

Mono T.mor₂

source

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

Mono T.mor₃

source

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

Mono T.mor₁

source

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

Limits.IsZero T.obj₂ ↔ T.mor₁ = 0 ∧ T.mor₂ = 0

source

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

Limits.IsZero T.obj₁ ↔ T.mor₁ = 0 ∧ T.mor₃ = 0

source

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

Limits.IsZero T.obj₃ ↔ T.mor₂ = 0 ∧ T.mor₃ = 0

source

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

Limits.IsZero T.obj₁

source

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

Limits.IsZero T.obj₂

source

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

Limits.IsZero T.obj₃

source

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

Limits.IsZero T.obj₁ ↔ IsIso T.mor₂

source

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

Limits.IsZero T.obj₂ ↔ IsIso T.mor₃

source

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

Limits.IsZero T.obj₃ ↔ IsIso T.mor₁

source

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

Limits.IsZero T.obj₁

source

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

Limits.IsZero T.obj₂

source

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

Limits.IsZero T.obj₃

source

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

(CategoryTheory.shiftFunctor (Triangle C) n).obj T ∈ distinguishedTriangles

source

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

SplitEpiCategory C

source

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

SplitMonoCategory C

source

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

IsIso φ.hom₂

source

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

IsIso φ.hom₃

source

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

IsIso φ.hom₁

source

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

Limits.BinaryBiproductData T.obj₁ T.obj₃

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

Equations

Instances For

source

@[simp]

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

(binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.pt = T.obj₂

source

@[simp]

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

(binaryBiproductData T hT hT₀ inr inr_snd fst total).isBilimit = Limits.isBinaryBilimitOfTotal { pt := T.obj₂, fst := fst, snd := T.mor₂, inl := T.mor₁, inr := inr, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := inr_snd } total

source

@[simp]

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

(binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.inr = inr

source

@[simp]

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

(binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.inl = T.mor₁

source

@[simp]

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

(binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.snd = T.mor₂

source

@[simp]

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

(binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.fst = fst

source

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

Limits.HasBinaryBiproducts C

source

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

Limits.HasFiniteProducts C

source

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

Limits.HasFiniteCoproducts C

source

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

Limits.HasFiniteBiproducts C

source

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

∃ (e : T.obj₂ ≅ T.obj₁ ⊞ T.obj₃), CategoryStruct.comp T.mor₁ e.hom = Limits.biprod.inl ∧ T.mor₂ = CategoryStruct.comp e.hom Limits.biprod.snd

source

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

binaryBiproductTriangle X₁ X₂ ∈ distinguishedTriangles

source

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

binaryProductTriangle X₁ X₂ ∈ distinguishedTriangles

source

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

T₁ ⟶ T₂

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

Equations

Instances For

source

@[simp]

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

(completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ a b comm).hom₁ = a

source

@[simp]

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

(completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ a b comm).hom₂ = b

source

theorem CategoryTheory.Pretriangulated.productTriangle_distinguished {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [hC : Pretriangulated C] {J : Type u_1} (T : J → Triangle C) (hT : ∀ (j : J), T j ∈ distinguishedTriangles) [Limits.HasProduct fun (j : J) => (T j).obj₁] [Limits.HasProduct fun (j : J) => (T j).obj₂] [Limits.HasProduct fun (j : J) => (T j).obj₃] [Limits.HasProduct fun (j : J) => (shiftFunctor C 1).obj (T j).obj₁] :

productTriangle T ∈ distinguishedTriangles

A product of distinguished triangles is distinguished

source

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

∃ (e' : T₁ ≅ T₂), e'.hom.hom₁ = e.hom.left ∧ e'.hom.hom₂ = e.hom.right

source

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

T₁ ≅ T₂

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

Equations

Instances For

source

@[simp]

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

(isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).inv.hom₂ = e₂.inv

source

@[simp]

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

(isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).inv.hom₁ = e₁.inv

source

@[simp]

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

(isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).hom.hom₂ = e₂.hom

source

@[simp]

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

(isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).hom.hom₁ = e₁.hom

Documentation

Mathlib.CategoryTheory.Triangulated.Pretriangulated

Pretriangulated Categories #

Implementation Notes #