Truncations for a t-structure

Let t be a t-structure on a (pre)triangulated category C. In this file, for any n : ℤ, we introduce the truncation functors t.truncLE n : C ⥤ C and t.truncGT n : C ⥤ C, as variants of the functors t.truncLT n : C ⥤ C and t.truncGE n : C ⥤ C introduced in the file Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean.

noncomputable def CategoryTheory.Triangulated.TStructure.truncLE {C : Type u_1} [Category.{v_1, u_1} 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 truncLEι.

instance CategoryTheory.Triangulated.TStructure.instAdditiveTruncLE {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : (t.truncLE n).Additive

theorem CategoryTheory.Triangulated.TStructure.isLE_truncLE_obj {C : Type u_1} [Category.{v_1, u_1} 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 := by lia) : t.IsLE ((t.truncLE a).obj X) b

instance CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLE {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) : t.IsLE ((t.truncLE n).obj X) n

noncomputable def CategoryTheory.Triangulated.TStructure.truncGT {C : Type u_1} [Category.{v_1, u_1} 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 truncGTπ.

instance CategoryTheory.Triangulated.TStructure.instAdditiveTruncGT {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : (t.truncGT n).Additive

theorem CategoryTheory.Triangulated.TStructure.isGE_truncGT_obj {C : Type u_1} [Category.{v_1, u_1} 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 + 1 := by lia) : t.IsGE ((t.truncGT a).obj X) b

instance CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGTHAddIntOfNat {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) : t.IsGE ((t.truncGT n).obj X) (n + 1)

instance CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGTHSubIntOfNat {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) : t.IsGE ((t.truncGT (n - 1)).obj X) n

noncomputable def CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) : t.truncLE a ≅ t.truncLT b

The isomorphism t.truncLE a ≅ t.truncLT b when a + 1 = b.

noncomputable def CategoryTheory.Triangulated.TStructure.truncGTIsoTruncGE {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) : t.truncGT a ≅ t.truncGE b

The isomorphism t.truncGT a ≅ t.truncGE b when a + 1 = b.

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

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

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_hom_ι {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) : CategoryStruct.comp (t.truncLEIsoTruncLT a b h).hom (t.truncLTι b) = t.truncLEι a

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_hom_ι_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) {Z : Functor C C} (h✝ : Functor.id C ⟶ Z) : CategoryStruct.comp (t.truncLEIsoTruncLT a b h).hom (CategoryStruct.comp (t.truncLTι b) h✝) = CategoryStruct.comp (t.truncLEι a) h✝

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_hom_ι_app {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) : CategoryStruct.comp ((t.truncLEIsoTruncLT a b h).hom.app X) ((t.truncLTι b).app X) = (t.truncLEι a).app X

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_hom_ι_app_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) {Z : C} (h✝ : X ⟶ Z) : CategoryStruct.comp ((t.truncLEIsoTruncLT a b h).hom.app X) (CategoryStruct.comp ((t.truncLTι b).app X) h✝) = CategoryStruct.comp ((t.truncLEι a).app X) h✝

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_inv_ι {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) : CategoryStruct.comp (t.truncLEIsoTruncLT a b h).inv (t.truncLEι a) = t.truncLTι b

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_inv_ι_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) {Z : Functor C C} (h✝ : Functor.id C ⟶ Z) : CategoryStruct.comp (t.truncLEIsoTruncLT a b h).inv (CategoryStruct.comp (t.truncLEι a) h✝) = CategoryStruct.comp (t.truncLTι b) h✝

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_inv_ι_app {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) : CategoryStruct.comp ((t.truncLEIsoTruncLT a b h).inv.app X) ((t.truncLEι a).app X) = (t.truncLTι b).app X

@[simp]

theorem CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_inv_ι_app_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) {Z : C} (h✝ : X ⟶ Z) : CategoryStruct.comp ((t.truncLEIsoTruncLT a b h).inv.app X) (CategoryStruct.comp ((t.truncLEι a).app X) h✝) = CategoryStruct.comp ((t.truncLTι b).app X) h✝

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

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

@[simp]

theorem CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_ι_app {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n₀ n₁ : ℤ) (h : n₀ ≤ n₁) (X : C) : CategoryStruct.comp ((t.natTransTruncLEOfLE n₀ n₁ h).app X) ((t.truncLEι n₁).app X) = (t.truncLEι n₀).app X

@[simp]

theorem CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_ι_app_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n₀ n₁ : ℤ) (h : n₀ ≤ n₁) (X : C) {Z : C} (h✝ : X ⟶ Z) : CategoryStruct.comp ((t.natTransTruncLEOfLE n₀ n₁ h).app X) (CategoryStruct.comp ((t.truncLEι n₁).app X) h✝) = CategoryStruct.comp ((t.truncLEι n₀).app X) h✝

@[simp]

theorem CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_ι {C : Type u_1} [Category.{v_1, u_1} 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.natTransTruncLEOfLE a b h) (t.truncLEι b) = t.truncLEι a

@[simp]

theorem CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_ι_assoc {C : Type u_1} [Category.{v_1, u_1} 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.natTransTruncLEOfLE a b h) (CategoryStruct.comp (t.truncLEι b) h✝) = CategoryStruct.comp (t.truncLEι a) h✝

@[simp]

theorem CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_refl {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a : ℤ) : t.natTransTruncLEOfLE a a ⋯ = CategoryStruct.id (t.truncLE a)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_trans {C : Type u_1} [Category.{v_1, u_1} 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.natTransTruncLEOfLE a b hab) (t.natTransTruncLEOfLE b c hbc) = t.natTransTruncLEOfLE a c ⋯

theorem CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_refl_app {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a : ℤ) (X : C) : (t.natTransTruncLEOfLE a a ⋯).app X = CategoryStruct.id ((t.truncLE a).obj X)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_trans_app {C : Type u_1} [Category.{v_1, u_1} 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.natTransTruncLEOfLE a b hab).app X) ((t.natTransTruncLEOfLE b c hbc).app X) = (t.natTransTruncLEOfLE a c ⋯).app X

@[simp]

theorem CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_trans_app_assoc {C : Type u_1} [Category.{v_1, u_1} 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) {Z : C} (h : (t.truncLE c).obj X ⟶ Z) : CategoryStruct.comp ((t.natTransTruncLEOfLE a b hab).app X) (CategoryStruct.comp ((t.natTransTruncLEOfLE b c hbc).app X) h) = CategoryStruct.comp ((t.natTransTruncLEOfLE a c ⋯).app X) h

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

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

@[simp]

theorem CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_hom {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) : CategoryStruct.comp (t.truncGTπ a) (t.truncGTIsoTruncGE a b h).hom = t.truncGEπ b

@[simp]

theorem CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_hom_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) {Z : Functor C C} (h✝ : t.truncGE b ⟶ Z) : CategoryStruct.comp (t.truncGTπ a) (CategoryStruct.comp (t.truncGTIsoTruncGE a b h).hom h✝) = CategoryStruct.comp (t.truncGEπ b) h✝

@[simp]

theorem CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_hom_ι_app {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) : CategoryStruct.comp ((t.truncGTπ a).app X) ((t.truncGTIsoTruncGE a b h).hom.app X) = (t.truncGEπ b).app X

@[simp]

theorem CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_hom_ι_app_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) {Z : C} (h✝ : (t.truncGE b).obj X ⟶ Z) : CategoryStruct.comp ((t.truncGTπ a).app X) (CategoryStruct.comp ((t.truncGTIsoTruncGE a b h).hom.app X) h✝) = CategoryStruct.comp ((t.truncGEπ b).app X) h✝

@[simp]

theorem CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_inv {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) : CategoryStruct.comp (t.truncGEπ b) (t.truncGTIsoTruncGE a b h).inv = t.truncGTπ a

@[simp]

theorem CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_inv_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) {Z : Functor C C} (h✝ : t.truncGT a ⟶ Z) : CategoryStruct.comp (t.truncGEπ b) (CategoryStruct.comp (t.truncGTIsoTruncGE a b h).inv h✝) = CategoryStruct.comp (t.truncGTπ a) h✝

@[simp]

theorem CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_inv_ι_app {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) : CategoryStruct.comp ((t.truncGEπ b).app X) ((t.truncGTIsoTruncGE a b h).inv.app X) = (t.truncGTπ a).app X

@[simp]

theorem CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_inv_ι_app_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) {Z : C} (h✝ : (t.truncGT a).obj X ⟶ Z) : CategoryStruct.comp ((t.truncGEπ b).app X) (CategoryStruct.comp ((t.truncGTIsoTruncGE a b h).inv.app X) h✝) = CategoryStruct.comp ((t.truncGTπ a).app X) h✝

noncomputable def CategoryTheory.Triangulated.TStructure.truncGEδLE {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) : t.truncGE b ⟶ (t.truncLE a).comp (shiftFunctor C 1)

The connecting homomorphism (t.truncGE b).obj X ⟶ ((t.truncLE a).obj X)⟦1⟧ when a + 1 = b, as a natural transformation.

noncomputable def CategoryTheory.Triangulated.TStructure.triangleLEGE {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) : Functor C (Pretriangulated.Triangle C)

The distinguished triangle (t.truncLE a).obj A ⟶ A ⟶ (t.truncGE b).obj A ⟶ ... as a functor C ⥤ Triangle C when t is a t-structure on a pretriangulated category C and a + 1 = b.

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGE_map_hom₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLEGE a b h).map φ).hom₁ = (t.truncLE a).map φ

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_mor₃ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) (j : C) : ((t.triangleLEGE a b h).obj j).mor₃ = (t.truncGEδLE a b h).app j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_mor₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) (j : C) : ((t.triangleLEGE a b h).obj j).mor₁ = (t.truncLEι a).app j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGE_map_hom₃ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLEGE a b h).map φ).hom₃ = (t.truncGE b).map φ

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGE_map_hom₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLEGE a b h).map φ).hom₂ = φ

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_obj₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) (j : C) : ((t.triangleLEGE a b h).obj j).obj₂ = j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_obj₃ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) (j : C) : ((t.triangleLEGE a b h).obj j).obj₃ = (t.truncGE b).obj j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_mor₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) (j : C) : ((t.triangleLEGE a b h).obj j).mor₂ = (t.truncGEπ b).app j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_obj₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) (j : C) : ((t.triangleLEGE a b h).obj j).obj₁ = (t.truncLE a).obj j

noncomputable def CategoryTheory.Triangulated.TStructure.triangleLEGEIsoTriangleLTGE {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) : t.triangleLEGE a b h ≅ t.triangleLTGE b

The natural isomorphism of triangles t.triangleLEGE a b h ≅ t.triangleLTGE b when a + 1 = b.

theorem CategoryTheory.Triangulated.TStructure.triangleLEGE_distinguished {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) : (t.triangleLEGE a b h).obj X ∈ Pretriangulated.distinguishedTriangles

noncomputable def CategoryTheory.Triangulated.TStructure.truncGTδLE {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : t.truncGT n ⟶ (t.truncLE n).comp (shiftFunctor C 1)

The connecting homomorphism (t.truncGT n).obj X ⟶ ((t.truncLE n).obj X)⟦1⟧ for n : ℤ, as a natural transformation.

noncomputable def CategoryTheory.Triangulated.TStructure.triangleLEGT {C : Type u_1} [Category.{v_1, u_1} 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.truncLE n).obj A ⟶ A ⟶ (t.truncGT n).obj A ⟶ ... as a functor C ⥤ Triangle C when t is a t-structure on a pretriangulated category C and n : ℤ.

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_obj₃ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (j : C) : ((t.triangleLEGT n).obj j).obj₃ = (t.truncGT n).obj j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGT_map_hom₃ {C : Type u_1} [Category.{v_1, u_1} 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.triangleLEGT n).map φ).hom₃ = (t.truncGT n).map φ

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_mor₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (j : C) : ((t.triangleLEGT n).obj j).mor₂ = (t.truncGTπ n).app j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGT_map_hom₁ {C : Type u_1} [Category.{v_1, u_1} 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.triangleLEGT n).map φ).hom₁ = (t.truncLE n).map φ

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_mor₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (j : C) : ((t.triangleLEGT n).obj j).mor₁ = (t.truncLEι n).app j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_obj₂ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (j : C) : ((t.triangleLEGT n).obj j).obj₂ = j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_mor₃ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (j : C) : ((t.triangleLEGT n).obj j).mor₃ = (t.truncGTδLE n).app j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGT_map_hom₂ {C : Type u_1} [Category.{v_1, u_1} 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.triangleLEGT n).map φ).hom₂ = φ

@[simp]

theorem CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_obj₁ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (j : C) : ((t.triangleLEGT n).obj j).obj₁ = (t.truncLE n).obj j

noncomputable def CategoryTheory.Triangulated.TStructure.triangleLEGTIsoTriangleLEGE {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b : ℤ) (h : a + 1 = b) : t.triangleLEGT a ≅ t.triangleLEGE a b h

The natural isomorphism t.triangleLEGT a ≅ t.triangleLEGE a b h when a + 1 = b.

theorem CategoryTheory.Triangulated.TStructure.triangleLEGT_distinguished {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) : (t.triangleLEGT n).obj X ∈ Pretriangulated.distinguishedTriangles

theorem CategoryTheory.Triangulated.TStructure.isLE_iff_isIso_truncLEι_app {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) : t.IsLE X n ↔ IsIso ((t.truncLEι n).app X)

theorem CategoryTheory.Triangulated.TStructure.isGE_iff_isIso_truncGTπ_app {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) (X : C) : t.IsGE X n₁ ↔ IsIso ((t.truncGTπ n₀).app X)

instance CategoryTheory.Triangulated.TStructure.instIsIsoAppTruncLEιOfIsLE {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X : C) (n : ℤ) [t.IsLE X n] : IsIso ((t.truncLEι n).app X)

theorem CategoryTheory.Triangulated.TStructure.isLE_iff_isZero_truncGT_obj {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) (X : C) : t.IsLE X n ↔ Limits.IsZero ((t.truncGT n).obj X)

theorem CategoryTheory.Triangulated.TStructure.isGE_iff_isZero_truncLE_obj {C : Type u_1} [Category.{v_1, u_1} 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₁ ↔ Limits.IsZero ((t.truncLE n₀).obj X)

theorem CategoryTheory.Triangulated.TStructure.isZero_truncLE_obj_of_isGE {C : Type u_1} [Category.{v_1, u_1} 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₁] : Limits.IsZero ((t.truncLE n₀).obj X)

theorem CategoryTheory.Triangulated.TStructure.to_truncLE_obj_ext {C : Type u_1} [Category.{v_1, u_1} 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.truncLE n).obj X} (h : CategoryStruct.comp f₁ ((t.truncLEι n).app X) = CategoryStruct.comp f₂ ((t.truncLEι n).app X)) [t.IsLE Y n] : f₁ = f₂

theorem CategoryTheory.Triangulated.TStructure.liftTruncLE_aux {C : Type u_1} [Category.{v_1, u_1} 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.IsLE X n] : ∃ (f' : X ⟶ (t.truncLE n).obj Y), f = CategoryStruct.comp f' ((t.truncLEι n).app Y)

noncomputable def CategoryTheory.Triangulated.TStructure.liftTruncLE {C : Type u_1} [Category.{v_1, u_1} 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.IsLE X n] : X ⟶ (t.truncLE n).obj Y

Constructor for morphisms to (t.truncLE n).obj Y.

@[simp]

theorem CategoryTheory.Triangulated.TStructure.liftTruncLE_ι {C : Type u_1} [Category.{v_1, u_1} 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.IsLE X n] : CategoryStruct.comp (t.liftTruncLE f n) ((t.truncLEι n).app Y) = f

@[simp]

theorem CategoryTheory.Triangulated.TStructure.liftTruncLE_ι_assoc {C : Type u_1} [Category.{v_1, u_1} 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.IsLE X n] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (t.liftTruncLE f n) (CategoryStruct.comp ((t.truncLEι n).app Y) h) = CategoryStruct.comp f h

theorem CategoryTheory.Triangulated.TStructure.descTruncGT_aux {C : Type u_1} [Category.{v_1, u_1} 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.IsGE Y n₁] : ∃ (f' : (t.truncGT n₀).obj X ⟶ Y), f = CategoryStruct.comp ((t.truncGTπ n₀).app X) f'

noncomputable def CategoryTheory.Triangulated.TStructure.descTruncGT {C : Type u_1} [Category.{v_1, u_1} 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.IsGE Y n₁] : (t.truncGT n₀).obj X ⟶ Y

Constructor for morphisms from (t.truncGT n₀).obj Y.

@[simp]

theorem CategoryTheory.Triangulated.TStructure.π_descTruncGT {C : Type u_1} [Category.{v_1, u_1} 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.IsGE Y n₁] : CategoryStruct.comp ((t.truncGTπ n₀).app X) (t.descTruncGT f n₀ n₁ h) = f

@[simp]

theorem CategoryTheory.Triangulated.TStructure.π_descTruncGT_assoc {C : Type u_1} [Category.{v_1, u_1} 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.IsGE Y n₁] {Z : C} (h✝ : Y ⟶ Z) : CategoryStruct.comp ((t.truncGTπ n₀).app X) (CategoryStruct.comp (t.descTruncGT f n₀ n₁ h) h✝) = CategoryStruct.comp f h✝

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

theorem CategoryTheory.Triangulated.TStructure.isIso_truncGT_map_iff {C : Type u_1} [Category.{v_1, u_1} 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 : ℤ) : IsIso ((t.truncGT n).map g) ↔ ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGT n).obj Z ⟶ (shiftFunctor C 1).obj X) (_ : Pretriangulated.Triangle.mk f (CategoryStruct.comp g ((t.truncGTπ n).app Z)) h ∈ Pretriangulated.distinguishedTriangles), t.IsLE X n

instance CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLE_1 {C : Type u_1} [Category.{v_1, u_1} 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.truncLE a).obj X) b

instance CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGT {C : Type u_1} [Category.{v_1, u_1} 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.truncGT b).obj X) a

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.TStructure.truncLEGE {C : Type u_1} [Category.{v_1, u_1} 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 a ⋙ t.truncGE b.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.TStructure.truncGELE {C : Type u_1} [Category.{v_1, u_1} 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.truncLE b ⋙ t.truncGE a.

instance CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGELE {C : Type u_1} [Category.{v_1, u_1} 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.truncGELE a b).obj X) a

noncomputable def CategoryTheory.Triangulated.TStructure.truncGELEIsoTruncGELT {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (a b b' : ℤ) (hb' : b + 1 = b') : t.truncGELE a b ≅ t.truncGELT a b'

The natural isomorphism t.truncGELE a b ≅ t.truncGELT a b' when b + 1 = b'.

theorem CategoryTheory.Triangulated.TStructure.isIso₁_truncLE_map_of_isGE {C : Type u_1} [Category.{v_1, u_1} 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.IsGE T.obj₃ n₁) : IsIso ((t.truncLE n₀).map T.mor₁)

theorem CategoryTheory.Triangulated.TStructure.isIso₂_truncGT_map_of_isLE {C : Type u_1} [Category.{v_1, u_1} 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.IsLE T.obj₁ n₀) : IsIso ((t.truncGT n₀).map T.mor₂)

instance CategoryTheory.Triangulated.TStructure.instIsGEObjTruncLE {C : Type u_1} [Category.{v_1, u_1} 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.truncLE b).obj X) a

instance CategoryTheory.Triangulated.TStructure.instIsLEObjTruncGT {C : Type u_1} [Category.{v_1, u_1} 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.truncGT a).obj X) b

instance CategoryTheory.Triangulated.TStructure.instIsGEObjTruncLE_1 {C : Type u_1} [Category.{v_1, u_1} 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.truncLE b).obj X) a

instance CategoryTheory.Triangulated.TStructure.instIsLEObjTruncGELE {C : Type u_1} [Category.{v_1, u_1} 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.truncGELE a b).obj X) b

theorem CategoryTheory.Triangulated.TStructure.isIso_truncLE_map_truncLEι_app {C : Type u_1} [Category.{v_1, u_1} 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.truncLE a).map ((t.truncLEι b).app X))

theorem CategoryTheory.Triangulated.TStructure.isIso_truncGT_map_truncGTπ_app {C : Type u_1} [Category.{v_1, u_1} 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.truncGT a).map ((t.truncGTπ b).app X))

instance CategoryTheory.Triangulated.TStructure.instIsIsoMapTruncLEAppTruncLEι {C : Type u_1} [Category.{v_1, u_1} 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.truncLE n).map ((t.truncLEι n).app X))

noncomputable def CategoryTheory.Triangulated.TStructure.truncGELEIsoLEGE {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] (a b : ℤ) : t.truncGELE a b ≅ t.truncLEGE a b

The natural isomorphism t.truncGELE a b ≅ t.truncLEGE a b.