Truncations for a t-structure

Let t be a t-structure on a (pre)triangulated category C. In this file, for any n : ℤ, we construct truncation functors t.truncLT n : C ⥤ C, t.truncGE n : C ⥤ C and natural transformations t.truncLTι n : t.truncLT n ⟶ 𝟭 C, t.truncGEπ n : 𝟭 C ⟶ t.truncGE n and t.truncGEδLT n : t.truncGE n ⟶ t.truncLT n ⋙ shiftFunctor C (1 : ℤ) which are part of a distinguished triangle (t.truncLT n).obj X ⟶ X ⟶ (t.truncGE n).obj X ⟶ ((t.truncLT n).obj X)⟦1⟧ for any X : C, with (t.truncLT n).obj X < n and (t.truncGE n).obj X ≥ n.

We obtain various properties of these truncation functors.

theorem CategoryTheory.Triangulated.TStructure.triangle_map_ext {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {T T' : Pretriangulated.Triangle C} {f₁ f₂ : T ⟶ T'} (hT : T ∈ Pretriangulated.distinguishedTriangles) (hT' : T' ∈ Pretriangulated.distinguishedTriangles) (a b : ℤ) (h₀ : t.IsLE T.obj₁ a) (h₁ : t.IsGE T'.obj₃ b) (H : f₁.hom₂ = f₂.hom₂ := by cat_disch) (hab : a ≤ b := by lia) : f₁ = f₂

Two morphisms T ⟶ T' between distinguished triangles must coincide when they coincide on the middle object, and there are integers a ≤ b such that for a t-structure, we have T.obj₁ ≤ a and T'.obj₃ ≥ b.

theorem CategoryTheory.Triangulated.TStructure.triangle_map_exists {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {T T' : Pretriangulated.Triangle C} (hT : T ∈ Pretriangulated.distinguishedTriangles) (hT' : T' ∈ Pretriangulated.distinguishedTriangles) (φ : T.obj₂ ⟶ T'.obj₂) (a b : ℤ) (h₀ : t.IsLE T.obj₁ a) (h₁' : t.IsGE T'.obj₃ b) (h : a < b := by lia) : ∃ (f : T ⟶ T'), f.hom₂ = φ

If a < b, then a morphism T.obj₂ ⟶ T'.obj₂ extends to a morphism T ⟶ T' of distinguished triangles when for a t-structure T.obj₁ ≤ a and T'.obj₃ ≥ b.

theorem CategoryTheory.Triangulated.TStructure.triangle_iso_exists {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {T T' : Pretriangulated.Triangle C} (hT : T ∈ Pretriangulated.distinguishedTriangles) (hT' : T' ∈ Pretriangulated.distinguishedTriangles) (e : T.obj₂ ≅ T'.obj₂) (a b : ℤ) (h₀ : t.IsLE T.obj₁ a) (h₁ : t.IsGE T.obj₃ b) (h₀' : t.IsLE T'.obj₁ a) (h₁' : t.IsGE T'.obj₃ b) (h : a < b := by lia) : ∃ (e' : T ≅ T'), e'.hom.hom₂ = e.hom

If a < b, then an isomorphism T.obj₂ ≅ T'.obj₂ extends to an isomorphism T ≅ T' of distinguished triangles when for a t-structure, both T.obj₁ and T'.obj₁ are ≤ a and both T.obj₃ and T'.obj₃ are ≥ b.

The private definitions in the namespace TStructure.TruncAux are part of the implementation of the truncation functors truncLT, truncGE and the distinguished triangles they fit in.

noncomputable def CategoryTheory.Triangulated.TStructure.truncLT {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : Functor C C

Given a t-structure t on a pretriangulated category C and n : ℤ, this is the < n-truncation functor. See also the natural transformation truncLTι.

Equations

• t.truncLT n = (CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor✝ t n).comp CategoryTheory.Pretriangulated.Triangle.π₁

instance CategoryTheory.Triangulated.TStructure.instAdditiveTruncLT {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : (t.truncLT n).Additive

noncomputable def CategoryTheory.Triangulated.TStructure.truncLTι {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : t.truncLT n ⟶ Functor.id C

The natural transformation t.truncLT n ⟶ 𝟭 C when t is a t-structure on a category C and n : ℤ.

Equations

• t.truncLTι n = (CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor✝ t n).whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂

noncomputable def CategoryTheory.Triangulated.TStructure.truncGE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : Functor C C

Given a t-structure t on a pretriangulated category C and n : ℤ, this is the ≥ n-truncation functor. See also the natural transformation truncGEπ.

Equations

• t.truncGE n = (CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor✝ t n).comp CategoryTheory.Pretriangulated.Triangle.π₃

instance CategoryTheory.Triangulated.TStructure.instAdditiveTruncGE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : (t.truncGE n).Additive

noncomputable def CategoryTheory.Triangulated.TStructure.truncGEπ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : Functor.id C ⟶ t.truncGE n

The natural transformation 𝟭 C ⟶ t.truncGE n when t is a t-structure on a category C and n : ℤ.

Equations

• t.truncGEπ n = (CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor✝ t n).whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncGEπ_naturality {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp ((t.truncGEπ n).app X) ((t.truncGE n).map f) = CategoryStruct.comp f ((t.truncGEπ n).app Y)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncGEπ_naturality_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) {X Y : C} (f : X ⟶ Y) {Z : C} (h : (t.truncGE n).obj Y ⟶ Z) : CategoryStruct.comp ((t.truncGEπ n).app X) (CategoryStruct.comp ((t.truncGE n).map f) h) = CategoryStruct.comp f (CategoryStruct.comp ((t.truncGEπ n).app Y) h)

theorem CategoryTheory.Triangulated.TStructure.isLE_truncLT_obj {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (a b : ℤ) (hn : a ≤ b + 1 := by lia) : t.IsLE ((t.truncLT a).obj X) b

instance CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLTHSubIntOfNat {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n : ℤ) : t.IsLE ((t.truncLT n).obj X) (n - 1)

instance CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLTHAddIntOfNat {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n : ℤ) : t.IsLE ((t.truncLT (n + 1)).obj X) n

theorem CategoryTheory.Triangulated.TStructure.isGE_truncGE_obj {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (a b : ℤ) (hn : b ≤ a := by lia) : t.IsGE ((t.truncGE a).obj X) b

instance CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n : ℤ) : t.IsGE ((t.truncGE n).obj X) n

noncomputable def CategoryTheory.Triangulated.TStructure.truncGEδLT {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : t.truncGE n ⟶ (t.truncLT n).comp (shiftFunctor C 1)

The connecting morphism t.truncGE n ⟶ t.truncLT n ⋙ shiftFunctor C (1 : ℤ) when t is a t-structure on a pretriangulated category and n : ℤ.

Equations

• t.truncGEδLT n = (CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor✝ t n).whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁

noncomputable def CategoryTheory.Triangulated.TStructure.triangleLTGE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : Functor C (Pretriangulated.Triangle C)

The distinguished triangle (t.truncLT n).obj A ⟶ A ⟶ (t.truncGE n).obj A ⟶ ... as a functor C ⥤ Triangle C when t is a t-structure on a pretriangulated category C and n : ℤ.

Equations

• t.triangleLTGE n = CategoryTheory.Pretriangulated.Triangle.functorMk (t.truncLTι n) (t.truncGEπ n) (t.truncGEδLT n)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_obj₃ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (j : C) : ((t.triangleLTGE n).obj j).obj₃ = (t.truncGE n).obj j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₁ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTGE n).map φ).hom₁ = (t.truncLT n).map φ

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_obj₂ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (j : C) : ((t.triangleLTGE n).obj j).obj₂ = j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₂ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTGE n).map φ).hom₂ = φ

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₁ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (j : C) : ((t.triangleLTGE n).obj j).mor₁ = (t.truncLTι n).app j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₃ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTGE n).map φ).hom₃ = (t.truncGE n).map φ

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₃ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (j : C) : ((t.triangleLTGE n).obj j).mor₃ = (t.truncGEδLT n).app j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₂ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (j : C) : ((t.triangleLTGE n).obj j).mor₂ = (t.truncGEπ n).app j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_obj₁ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (j : C) : ((t.triangleLTGE n).obj j).obj₁ = (t.truncLT n).obj j

theorem CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) : (t.triangleLTGE n).obj X ∈ Pretriangulated.distinguishedTriangles

instance CategoryTheory.Triangulated.TStructure.instIsLEObj₁ObjTriangleTriangleLTGEHSubIntOfNat {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n : ℤ) : t.IsLE ((t.triangleLTGE n).obj X).obj₁ (n - 1)

instance CategoryTheory.Triangulated.TStructure.instIsGEObj₃ObjTriangleTriangleLTGE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n : ℤ) : t.IsGE ((t.triangleLTGE n).obj X).obj₃ n

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ_app {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) : CategoryStruct.comp ((t.truncLTι n).app X) ((t.truncGEπ n).app X) = 0

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ_app_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) {Z : C} (h : (t.truncGE n).obj X ⟶ Z) : CategoryStruct.comp ((t.truncLTι n).app X) (CategoryStruct.comp ((t.truncGEπ n).app X) h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT_app {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) : CategoryStruct.comp ((t.truncGEπ n).app X) ((t.truncGEδLT n).app X) = 0

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT_app_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) {Z : C} (h : (shiftFunctor C 1).obj ((t.truncLT n).obj X) ⟶ Z) : CategoryStruct.comp ((t.truncGEπ n).app X) (CategoryStruct.comp ((t.truncGEδLT n).app X) h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι_app {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) : CategoryStruct.comp ((t.truncGEδLT n).app X) ((shiftFunctor C 1).map ((t.truncLTι n).app X)) = 0

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι_app_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) {Z : C} (h : (shiftFunctor C 1).obj X ⟶ Z) : CategoryStruct.comp ((t.truncGEδLT n).app X) (CategoryStruct.comp ((shiftFunctor C 1).map ((t.truncLTι n).app X)) h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : CategoryStruct.comp (t.truncLTι n) (t.truncGEπ n) = 0

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) {Z : Functor C C} (h : t.truncGE n ⟶ Z) : CategoryStruct.comp (t.truncLTι n) (CategoryStruct.comp (t.truncGEπ n) h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : CategoryStruct.comp (t.truncGEπ n) (t.truncGEδLT n) = 0

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) {Z : Functor C C} (h : (t.truncLT n).comp (shiftFunctor C 1) ⟶ Z) : CategoryStruct.comp (t.truncGEπ n) (CategoryStruct.comp (t.truncGEδLT n) h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : CategoryStruct.comp (t.truncGEδLT n) (Functor.whiskerRight (t.truncLTι n) (shiftFunctor C 1)) = 0

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) {Z : Functor C C} (h : (Functor.id C).comp (shiftFunctor C 1) ⟶ Z) : CategoryStruct.comp (t.truncGEδLT n) (CategoryStruct.comp (Functor.whiskerRight (t.truncLTι n) (shiftFunctor C 1)) h) = CategoryStruct.comp 0 h

noncomputable def CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) : t.truncLT a ⟶ t.truncLT b

The natural transformation t.truncLT a ⟶ t.truncLT b when a ≤ b.

Equations

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

noncomputable def CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) : t.truncGE a ⟶ t.truncGE b

The natural transformation t.truncGE a ⟶ t.truncGE b when a ≤ b.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_ι_app {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) (X : C) : CategoryStruct.comp ((t.natTransTruncLTOfLE a b h).app X) ((t.truncLTι b).app X) = (t.truncLTι a).app X

@[simp]

theorem CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_ι_app_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) (X : C) {Z : C} (h✝ : X ⟶ Z) : CategoryStruct.comp ((t.natTransTruncLTOfLE a b h).app X) (CategoryStruct.comp ((t.truncLTι b).app X) h✝) = CategoryStruct.comp ((t.truncLTι a).app X) h✝

@[simp]

theorem CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_ι {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) : CategoryStruct.comp (t.natTransTruncLTOfLE a b h) (t.truncLTι b) = t.truncLTι a

@[simp]

theorem CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_ι_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) {Z : Functor C C} (h✝ : Functor.id C ⟶ Z) : CategoryStruct.comp (t.natTransTruncLTOfLE a b h) (CategoryStruct.comp (t.truncLTι b) h✝) = CategoryStruct.comp (t.truncLTι a) h✝

@[simp]

theorem CategoryTheory.Triangulated.TStructure.π_natTransTruncGEOfLE_app {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) (X : C) : CategoryStruct.comp ((t.truncGEπ a).app X) ((t.natTransTruncGEOfLE a b h).app X) = (t.truncGEπ b).app X

@[simp]

theorem CategoryTheory.Triangulated.TStructure.π_natTransTruncGEOfLE_app_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) (X : C) {Z : C} (h✝ : (t.truncGE b).obj X ⟶ Z) : CategoryStruct.comp ((t.truncGEπ a).app X) (CategoryStruct.comp ((t.natTransTruncGEOfLE a b h).app X) h✝) = CategoryStruct.comp ((t.truncGEπ b).app X) h✝

theorem CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_natTransTruncLTOfLE_app {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) (X : C) : CategoryStruct.comp ((t.truncGEδLT a).app X) ((shiftFunctor C 1).map ((t.natTransTruncLTOfLE a b h).app X)) = CategoryStruct.comp ((t.natTransTruncGEOfLE a b h).app X) ((t.truncGEδLT b).app X)

theorem CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_natTransTruncLTOfLE_app_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) (X : C) {Z : C} (h✝ : (shiftFunctor C 1).obj ((t.truncLT b).obj X) ⟶ Z) : CategoryStruct.comp ((t.truncGEδLT a).app X) (CategoryStruct.comp ((shiftFunctor C 1).map ((t.natTransTruncLTOfLE a b h).app X)) h✝) = CategoryStruct.comp ((t.natTransTruncGEOfLE a b h).app X) (CategoryStruct.comp ((t.truncGEδLT b).app X) h✝)

theorem CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) : CategoryStruct.comp (t.truncGEδLT a) (Functor.whiskerRight (t.natTransTruncLTOfLE a b h) (shiftFunctor C 1)) = CategoryStruct.comp (t.natTransTruncGEOfLE a b h) (t.truncGEδLT b)

theorem CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) {Z : Functor C C} (h✝ : (t.truncLT b).comp (shiftFunctor C 1) ⟶ Z) : CategoryStruct.comp (t.truncGEδLT a) (CategoryStruct.comp (Functor.whiskerRight (t.natTransTruncLTOfLE a b h) (shiftFunctor C 1)) h✝) = CategoryStruct.comp (t.natTransTruncGEOfLE a b h) (CategoryStruct.comp (t.truncGEδLT b) h✝)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.π_natTransTruncGEOfLE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) : CategoryStruct.comp (t.truncGEπ a) (t.natTransTruncGEOfLE a b h) = t.truncGEπ b

@[simp]

theorem CategoryTheory.Triangulated.TStructure.π_natTransTruncGEOfLE_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) {Z : Functor C C} (h✝ : t.truncGE b ⟶ Z) : CategoryStruct.comp (t.truncGEπ a) (CategoryStruct.comp (t.natTransTruncGEOfLE a b h) h✝) = CategoryStruct.comp (t.truncGEπ b) h✝

noncomputable def CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) : t.triangleLTGE a ⟶ t.triangleLTGE b

The natural transformation t.triangleLTGE a ⟶ t.triangleLTGE b when a ≤ b.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE_refl {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a : ℤ) : t.natTransTriangleLTGEOfLE a a ⋯ = CategoryStruct.id (t.triangleLTGE a)

theorem CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE_trans {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) : CategoryStruct.comp (t.natTransTriangleLTGEOfLE a b hab) (t.natTransTriangleLTGEOfLE b c hbc) = t.natTransTriangleLTGEOfLE a c ⋯

@[simp]

theorem CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_refl {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a : ℤ) : t.natTransTruncLTOfLE a a ⋯ = CategoryStruct.id (t.truncLT a)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_trans {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) : CategoryStruct.comp (t.natTransTruncLTOfLE a b hab) (t.natTransTruncLTOfLE b c hbc) = t.natTransTruncLTOfLE a c ⋯

@[simp]

theorem CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_refl {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a : ℤ) : t.natTransTruncGEOfLE a a ⋯ = CategoryStruct.id (t.truncGE a)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_trans {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) : CategoryStruct.comp (t.natTransTruncGEOfLE a b hab) (t.natTransTruncGEOfLE b c hbc) = t.natTransTruncGEOfLE a c ⋯

theorem CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_refl_app {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a : ℤ) (X : C) : (t.natTransTruncLTOfLE a a ⋯).app X = CategoryStruct.id ((t.truncLT a).obj X)

theorem CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_trans_app {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) (X : C) : CategoryStruct.comp ((t.natTransTruncLTOfLE a b hab).app X) ((t.natTransTruncLTOfLE b c hbc).app X) = (t.natTransTruncLTOfLE a c ⋯).app X

theorem CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_refl_app {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a : ℤ) (X : C) : (t.natTransTruncGEOfLE a a ⋯).app X = CategoryStruct.id ((t.truncGE a).obj X)

theorem CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_trans_app {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) (X : C) : CategoryStruct.comp ((t.natTransTruncGEOfLE a b hab).app X) ((t.natTransTruncGEOfLE b c hbc).app X) = (t.natTransTruncGEOfLE a c ⋯).app X

theorem CategoryTheory.Triangulated.TStructure.isLE_of_isZero {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X : C} (hX : Limits.IsZero X) (n : ℤ) : t.IsLE X n

theorem CategoryTheory.Triangulated.TStructure.isGE_of_isZero {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X : C} (hX : Limits.IsZero X) (n : ℤ) : t.IsGE X n

instance CategoryTheory.Triangulated.TStructure.instIsLEOfNat {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : t.IsLE 0 n

instance CategoryTheory.Triangulated.TStructure.instIsGEOfNat {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : t.IsGE 0 n

theorem CategoryTheory.Triangulated.TStructure.isLE_iff_isIso_truncLTι_app {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) : t.IsLE X n₀ ↔ IsIso ((t.truncLTι n₁).app X)

theorem CategoryTheory.Triangulated.TStructure.isGE_iff_isIso_truncGEπ_app {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) : t.IsGE X n ↔ IsIso ((t.truncGEπ n).app X)

instance CategoryTheory.Triangulated.TStructure.instIsIsoAppTruncGEπOfIsGE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n : ℤ) [t.IsGE X n] : IsIso ((t.truncGEπ n).app X)

theorem CategoryTheory.Triangulated.TStructure.isGE_iff_isZero_truncLT_obj {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) : t.IsGE X n ↔ Limits.IsZero ((t.truncLT n).obj X)

theorem CategoryTheory.Triangulated.TStructure.isLE_iff_isZero_truncGE_obj {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) : t.IsLE X n₀ ↔ Limits.IsZero ((t.truncGE n₁).obj X)

theorem CategoryTheory.Triangulated.TStructure.isZero_truncLT_obj_of_isGE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) [t.IsGE X n] : Limits.IsZero ((t.truncLT n).obj X)

theorem CategoryTheory.Triangulated.TStructure.isZero_truncGE_obj_of_isLE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) [t.IsLE X n₀] : Limits.IsZero ((t.truncGE n₁).obj X)

theorem CategoryTheory.Triangulated.TStructure.from_truncGE_obj_ext {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {n : ℤ} {X Y : C} {f₁ f₂ : (t.truncGE n).obj X ⟶ Y} (h : CategoryStruct.comp ((t.truncGEπ n).app X) f₁ = CategoryStruct.comp ((t.truncGEπ n).app X) f₂) [t.IsGE Y n] : f₁ = f₂

theorem CategoryTheory.Triangulated.TStructure.to_truncLT_obj_ext {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {n : ℤ} {Y X : C} {f₁ f₂ : Y ⟶ (t.truncLT n).obj X} (h : CategoryStruct.comp f₁ ((t.truncLTι n).app X) = CategoryStruct.comp f₂ ((t.truncLTι n).app X)) [t.IsLE Y (n - 1)] : f₁ = f₂

theorem CategoryTheory.Triangulated.TStructure.truncLT_map_truncLTι_app {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) : (t.truncLT n).map ((t.truncLTι n).app X) = (t.truncLTι n).app ((t.truncLT n).obj X)

theorem CategoryTheory.Triangulated.TStructure.truncLT_map_truncLTι_app_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) {Z : C} (h : (t.truncLT n).obj X ⟶ Z) : CategoryStruct.comp ((t.truncLT n).map ((t.truncLTι n).app X)) h = CategoryStruct.comp ((t.truncLTι n).app ((t.truncLT n).obj X)) h

theorem CategoryTheory.Triangulated.TStructure.truncGE_map_truncGEπ_app {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) : (t.truncGE n).map ((t.truncGEπ n).app X) = (t.truncGEπ n).app ((t.truncGE n).obj X)

theorem CategoryTheory.Triangulated.TStructure.truncGE_map_truncGEπ_app_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) {Z : C} (h : (t.truncGE n).obj ((t.truncGE n).obj X) ⟶ Z) : CategoryStruct.comp ((t.truncGE n).map ((t.truncGEπ n).app X)) h = CategoryStruct.comp ((t.truncGEπ n).app ((t.truncGE n).obj X)) h

theorem CategoryTheory.Triangulated.TStructure.liftTruncLT_aux {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) [t.IsLE X n₀] : ∃ (f' : X ⟶ (t.truncLT n₁).obj Y), f = CategoryStruct.comp f' ((t.truncLTι n₁).app Y)

noncomputable def CategoryTheory.Triangulated.TStructure.liftTruncLT {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) [t.IsLE X n₀] : X ⟶ (t.truncLT n₁).obj Y

Constructor for morphisms to (t.truncLT n₁).obj Y.

Equations

• t.liftTruncLT f n₀ n₁ h = ⋯.choose

@[simp]

theorem CategoryTheory.Triangulated.TStructure.liftTruncLT_ι {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) [t.IsLE X n₀] : CategoryStruct.comp (t.liftTruncLT f n₀ n₁ h) ((t.truncLTι n₁).app Y) = f

@[simp]

theorem CategoryTheory.Triangulated.TStructure.liftTruncLT_ι_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) [t.IsLE X n₀] {Z : C} (h✝ : Y ⟶ Z) : CategoryStruct.comp (t.liftTruncLT f n₀ n₁ h) (CategoryStruct.comp ((t.truncLTι n₁).app Y) h✝) = CategoryStruct.comp f h✝

theorem CategoryTheory.Triangulated.TStructure.descTruncGE_aux {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X Y : C} (f : X ⟶ Y) (n : ℤ) [t.IsGE Y n] : ∃ (f' : (t.truncGE n).obj X ⟶ Y), f = CategoryStruct.comp ((t.truncGEπ n).app X) f'

noncomputable def CategoryTheory.Triangulated.TStructure.descTruncGE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X Y : C} (f : X ⟶ Y) (n : ℤ) [t.IsGE Y n] : (t.truncGE n).obj X ⟶ Y

Constructor for morphisms from (t.truncGE n).obj X.

Equations

• t.descTruncGE f n = ⋯.choose

@[simp]

theorem CategoryTheory.Triangulated.TStructure.π_descTruncGE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X Y : C} (f : X ⟶ Y) (n : ℤ) [t.IsGE Y n] : CategoryStruct.comp ((t.truncGEπ n).app X) (t.descTruncGE f n) = f

@[simp]

theorem CategoryTheory.Triangulated.TStructure.π_descTruncGE_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X Y : C} (f : X ⟶ Y) (n : ℤ) [t.IsGE Y n] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp ((t.truncGEπ n).app X) (CategoryStruct.comp (t.descTruncGE f n) h) = CategoryStruct.comp f h

theorem CategoryTheory.Triangulated.TStructure.isLE_iff_orthogonal {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) : t.IsLE X n₀ ↔ ∀ (Y : C) (f : X ⟶ Y), t.IsGE Y n₁ → f = 0

theorem CategoryTheory.Triangulated.TStructure.isGE_iff_orthogonal {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) : t.IsGE X n₁ ↔ ∀ (Y : C) (f : Y ⟶ X), t.IsLE Y n₀ → f = 0

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

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

instance CategoryTheory.Triangulated.TStructure.instIsTriangulatedMinus {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) : t.minus.IsTriangulated

instance CategoryTheory.Triangulated.TStructure.instIsTriangulatedPlus {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) : t.plus.IsTriangulated

instance CategoryTheory.Triangulated.TStructure.instIsTriangulatedBounded {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) : t.bounded.IsTriangulated

theorem CategoryTheory.Triangulated.TStructure.isIso_truncLT_map_iff {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X Y : C} (f : X ⟶ Y) (n : ℤ) : IsIso ((t.truncLT n).map f) ↔ ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj X)) (_ : Pretriangulated.Triangle.mk (CategoryStruct.comp ((t.truncLTι n).app X) f) g h ∈ Pretriangulated.distinguishedTriangles), t.IsGE Z n

theorem CategoryTheory.Triangulated.TStructure.isIso_truncGE_map_iff {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {Y Z : C} (g : Y ⟶ Z) (n₀ n₁ : ℤ) (hn : n₀ + 1 = n₁) : IsIso ((t.truncGE n₁).map g) ↔ ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ (shiftFunctor C 1).obj X) (_ : Pretriangulated.Triangle.mk f (CategoryStruct.comp g ((t.truncGEπ n₁).app Z)) h ∈ Pretriangulated.distinguishedTriangles), t.IsLE X n₀

instance CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLT {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (a b : ℤ) [t.IsLE X b] : t.IsLE ((t.truncLT a).obj X) b

instance CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGE_1 {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (a b : ℤ) [t.IsGE X a] : t.IsGE ((t.truncGE b).obj X) a

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.TStructure.truncGELT {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) : Functor C C

The composition t.truncLT b ⋙ t.truncGE a.

Equations

• t.truncGELT a b = (t.truncLT b).comp (t.truncGE a)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.TStructure.truncLTGE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) : Functor C C

The composition t.truncGE b ⋙ t.truncLT a.

Equations

• t.truncLTGE a b = (t.truncGE a).comp (t.truncLT b)

instance CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGELT {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (a b : ℤ) : t.IsGE ((t.truncGELT a b).obj X) a

instance CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLTGEHSubIntOfNat {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (a b : ℤ) : t.IsLE ((t.truncLTGE a b).obj X) (b - 1)

theorem CategoryTheory.Triangulated.TStructure.isIso₁_truncLT_map_of_isGE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (n : ℤ) (h₃ : t.IsGE T.obj₃ n) : IsIso ((t.truncLT n).map T.mor₁)

theorem CategoryTheory.Triangulated.TStructure.isIso₂_truncGE_map_of_isLE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (h₁ : t.IsLE T.obj₁ n₀) : IsIso ((t.truncGE n₁).map T.mor₂)

instance CategoryTheory.Triangulated.TStructure.instIsGEObjTruncLT {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (X : C) (a b : ℤ) [t.IsGE X a] : t.IsGE ((t.truncLT b).obj X) a

instance CategoryTheory.Triangulated.TStructure.instIsLEObjTruncGE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (X : C) (a b : ℤ) [t.IsLE X b] : t.IsLE ((t.truncGE a).obj X) b

instance CategoryTheory.Triangulated.TStructure.instIsLEObjTruncGELTHSubIntOfNat {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (X : C) (a b : ℤ) : t.IsLE ((t.truncGELT a b).obj X) (b - 1)

instance CategoryTheory.Triangulated.TStructure.instIsGEObjTruncLTGE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (X : C) (a b : ℤ) : t.IsGE ((t.truncLTGE a b).obj X) a

theorem CategoryTheory.Triangulated.TStructure.isIso_truncGE_map_truncGEπ_app {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b : ℤ) (h : b ≤ a) (X : C) : IsIso ((t.truncGE a).map ((t.truncGEπ b).app X))

theorem CategoryTheory.Triangulated.TStructure.isIso_truncLT_map_truncLTι_app {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b : ℤ) (h : a ≤ b) (X : C) : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))

instance CategoryTheory.Triangulated.TStructure.instIsIsoMapTruncLTAppTruncLTι {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (X : C) (n : ℤ) : IsIso ((t.truncLT n).map ((t.truncLTι n).app X))

instance CategoryTheory.Triangulated.TStructure.instIsIsoMapTruncGEAppTruncGEπ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (X : C) (n : ℤ) : IsIso ((t.truncGE n).map ((t.truncGEπ n).app X))

instance CategoryTheory.Triangulated.TStructure.instIsIsoAppTruncLTιObjTruncGETruncLT {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b : ℤ) (X : C) : IsIso ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)))

noncomputable def CategoryTheory.Triangulated.TStructure.truncGELTToLTGE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b : ℤ) : t.truncGELT a b ⟶ t.truncLTGE a b

The natural transformation t.truncGELT a b ⟶ t.truncLTGE a b (which is an isomorphism, see truncGELTIsoLTGE.)

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncGELTToLTGE_app_pentagon {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b : ℤ) (X : C) : CategoryStruct.comp ((t.truncGEπ a).app ((t.truncLT b).obj X)) (CategoryStruct.comp ((t.truncGELTToLTGE a b).app X) ((t.truncLTι b).app ((t.truncGE a).obj X))) = CategoryStruct.comp ((t.truncLTι b).app X) ((t.truncGEπ a).app X)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncGELTToLTGE_app_pentagon_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b : ℤ) (X : C) {Z : C} (h : (t.truncGE a).obj X ⟶ Z) : CategoryStruct.comp ((t.truncGEπ a).app ((t.truncLT b).obj X)) (CategoryStruct.comp ((t.truncGELTToLTGE a b).app X) (CategoryStruct.comp ((t.truncLTι b).app ((t.truncGE a).obj X)) h)) = CategoryStruct.comp ((t.truncLTι b).app X) (CategoryStruct.comp ((t.truncGEπ a).app X) h)

theorem CategoryTheory.Triangulated.TStructure.truncGELTToLTGE_app_pentagon_uniqueness {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] {a b : ℤ} {X : C} (φ : (t.truncGELT a b).obj X ⟶ (t.truncLTGE a b).obj X) (hφ : CategoryStruct.comp ((t.truncGEπ a).app ((t.truncLT b).obj X)) (CategoryStruct.comp φ ((t.truncLTι b).app ((t.truncGE a).obj X))) = CategoryStruct.comp ((t.truncLTι b).app X) ((t.truncGEπ a).app X)) : (t.truncGELTToLTGE a b).app X = φ

theorem CategoryTheory.Triangulated.TStructure.truncLT_map_truncGE_map_truncLTι_app_fac {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b : ℤ) (X : C) : CategoryStruct.comp ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X))) ((t.truncGELTToLTGE a b).app X) = (t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X))

theorem CategoryTheory.Triangulated.TStructure.truncLT_map_truncGE_map_truncLTι_app_fac_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b : ℤ) (X : C) {Z : C} (h : (t.truncLT b).obj ((t.truncGE a).obj X) ⟶ Z) : CategoryStruct.comp ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X))) (CategoryStruct.comp ((t.truncGELTToLTGE a b).app X) h) = CategoryStruct.comp ((t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X))) h

noncomputable def CategoryTheory.Triangulated.TStructure.truncGELTδLT {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) : t.truncGELT a b ⟶ (t.truncLT a).comp (shiftFunctor C 1)

The connecting homomorphism (t.truncGELT a b).obj X ⟶ ((t.truncLT a).obj X)⟦1⟧, as a natural transformation.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncGELTδLT_app {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (X : C) : (t.truncGELTδLT a b).app X = CategoryStruct.comp ((t.truncGEδLT a).app ((t.truncLT b).obj X)) ((shiftFunctor C 1).map ((t.truncLT a).map ((t.truncLTι b).app X)))

noncomputable def CategoryTheory.Triangulated.TStructure.triangleLTLTGELT {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) : Functor C (Pretriangulated.Triangle C)

The functorial (distinguished) triangle (t.truncLT a).obj X ⟶ (t.truncLT b).obj X ⟶ (t.truncGELT a b).obj X ⟶ ... when a ≤ b.

Equations

• t.triangleLTLTGELT a b h = CategoryTheory.Pretriangulated.Triangle.functorMk (t.natTransTruncLTOfLE a b h) ((t.truncLT b).whiskerLeft (t.truncGEπ a)) (t.truncGELTδLT a b)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_obj₁ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) (j : C) : ((t.triangleLTLTGELT a b h).obj j).obj₁ = (t.truncLT a).obj j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_mor₃ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) (j : C) : ((t.triangleLTLTGELT a b h).obj j).mor₃ = CategoryStruct.comp ((t.truncGEδLT a).app ((t.truncLT b).obj j)) ((shiftFunctor C 1).map ((t.truncLT a).map ((t.truncLTι b).app j)))

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_obj₂ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) (j : C) : ((t.triangleLTLTGELT a b h).obj j).obj₂ = (t.truncLT b).obj j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_map_hom₃ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTLTGELT a b h).map φ).hom₃ = (t.truncGE a).map ((t.truncLT b).map φ)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_map_hom₁ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTLTGELT a b h).map φ).hom₁ = (t.truncLT a).map φ

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_obj₃ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) (j : C) : ((t.triangleLTLTGELT a b h).obj j).obj₃ = (t.truncGE a).obj ((t.truncLT b).obj j)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_mor₂ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) (j : C) : ((t.triangleLTLTGELT a b h).obj j).mor₂ = (t.truncGEπ a).app ((t.truncLT b).obj j)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_map_hom₂ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTLTGELT a b h).map φ).hom₂ = (t.truncLT b).map φ

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_mor₁ {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a ≤ b) (j : C) : ((t.triangleLTLTGELT a b h).obj j).mor₁ = (t.natTransTruncLTOfLE a b h).app j

theorem CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_distinguished {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b : ℤ) (h : a ≤ b) (X : C) : (t.triangleLTLTGELT a b h).obj X ∈ Pretriangulated.distinguishedTriangles

instance CategoryTheory.Triangulated.TStructure.instIsIsoFunctorTruncGELTToLTGE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b : ℤ) : IsIso (t.truncGELTToLTGE a b)

instance CategoryTheory.Triangulated.TStructure.instIsIsoMapTruncLTTruncGEAppTruncLTι {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b : ℤ) (X : C) : IsIso ((t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X)))

noncomputable def CategoryTheory.Triangulated.TStructure.truncGELTIsoLTGE {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b : ℤ) : t.truncGELT a b ≅ t.truncLTGE a b

The natural transformation t.truncGELT a b ≅ t.truncLTGE a b.

Equations

• t.truncGELTIsoLTGE a b = CategoryTheory.asIso (t.truncGELTToLTGE a b)