Truncations for a t-structure

Let t be a t-structure on a triangulated category C. In this file, we extend the definition of the truncation functors truncLT and truncGE for indices in ℤ to EInt, as t.eTruncLT : EInt ⥤ C ⥤ C and t.eTruncGE : EInt ⥤ C ⥤ C.

noncomputable def CategoryTheory.Triangulated.TStructure.eTruncLT {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) : Functor EInt (Functor C C)

The functor EInt ⥤ C ⥤ C which sends ⊥ to the zero functor, n : ℤ to t.truncLT n and ⊤ to 𝟭 C.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLT_obj_top {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) : t.eTruncLT.obj ⊤ = Functor.id C

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLT_obj_bot {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) : t.eTruncLT.obj ⊥ = 0

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLT_obj_coe {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.eTruncLT.obj (WithBotTop.coe n) = t.truncLT n

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLT_map_eq_truncLTι {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.eTruncLT.map (homOfLE ⋯) = t.truncLTι n

instance CategoryTheory.Triangulated.TStructure.instAdditiveObjEIntFunctorETruncLT {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) (i : EInt) : (t.eTruncLT.obj i).Additive

noncomputable def CategoryTheory.Triangulated.TStructure.eTruncGE {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) : Functor EInt (Functor C C)

The functor EInt ⥤ C ⥤ C which sends ⊥ to 𝟭 C, n : ℤ to t.truncGE n and ⊤ to the zero functor.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncGE_obj_bot {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) : t.eTruncGE.obj ⊥ = Functor.id C

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncGE_obj_top {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) : t.eTruncGE.obj ⊤ = 0

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncGE_obj_coe {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.eTruncGE.obj (WithBotTop.coe n) = t.truncGE n

instance CategoryTheory.Triangulated.TStructure.instAdditiveObjEIntFunctorETruncGE {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) (i : EInt) : (t.eTruncGE.obj i).Additive

noncomputable def CategoryTheory.Triangulated.TStructure.eTruncGEδLT {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) : t.eTruncGE ⟶ t.eTruncLT.comp ((Functor.whiskeringRight C C C).obj (shiftFunctor C 1))

The connecting homomorphism from t.eTruncGE to the shift by 1 of t.eTruncLT.

Equations

• t.eTruncGEδLT = { app := fun (a : WithBotTop ℤ) => WithBotTop.rec 0 t.truncGEδLT 0 a, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncGEδLT_coe {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.eTruncGEδLT.app (WithBotTop.coe n) = t.truncGEδLT n

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.TStructure.eTruncLTι {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) (i : EInt) : t.eTruncLT.obj i ⟶ Functor.id C

The natural transformation t.eTruncLT.obj i ⟶ 𝟭 C for all i : EInt.

Equations

• t.eTruncLTι i = t.eTruncLT.map (CategoryTheory.homOfLE ⋯)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLT_ι_bot {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) : t.eTruncLTι ⊥ = 0

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLT_ι_coe {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.eTruncLTι (WithBotTop.coe n) = t.truncLTι n

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLT_ι_top {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) : t.eTruncLTι ⊤ = CategoryStruct.id (t.eTruncLT.obj ⊤)

theorem CategoryTheory.Triangulated.TStructure.eTruncLTι_naturality {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) (i : EInt) {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp ((t.eTruncLT.obj i).map f) ((t.eTruncLTι i).app Y) = CategoryStruct.comp ((t.eTruncLTι i).app X) f

theorem CategoryTheory.Triangulated.TStructure.eTruncLTι_naturality_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) (i : EInt) {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp ((t.eTruncLT.obj i).map f) (CategoryStruct.comp ((t.eTruncLTι i).app Y) h) = CategoryStruct.comp ((t.eTruncLTι i).app X) (CategoryStruct.comp f h)

instance CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTιTopEInt {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) : IsIso (t.eTruncLTι ⊤)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLT_map_app_eTruncLTι_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) {i j : EInt} (f : i ⟶ j) (X : C) : CategoryStruct.comp ((t.eTruncLT.map f).app X) ((t.eTruncLTι j).app X) = (t.eTruncLTι i).app X

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLT_map_app_eTruncLTι_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) {i j : EInt} (f : i ⟶ j) (X : C) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp ((t.eTruncLT.map f).app X) (CategoryStruct.comp ((t.eTruncLTι j).app X) h) = CategoryStruct.comp ((t.eTruncLTι i).app X) h

theorem CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_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) (i : EInt) (X : C) : (t.eTruncLT.obj i).map ((t.eTruncLTι i).app X) = (t.eTruncLTι i).app ((t.eTruncLT.obj i).obj X)

theorem CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_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) (i : EInt) (X : C) {Z : C} (h : (t.eTruncLT.obj i).obj X ⟶ Z) : CategoryStruct.comp ((t.eTruncLT.obj i).map ((t.eTruncLTι i).app X)) h = CategoryStruct.comp ((t.eTruncLTι i).app ((t.eTruncLT.obj i).obj X)) h

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.TStructure.eTruncGEπ {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) (i : EInt) : Functor.id C ⟶ t.eTruncGE.obj i

The natural transformation 𝟭 C ⟶ t.eTruncGE.obj i for all i : EInt.

Equations

• t.eTruncGEπ i = t.eTruncGE.map (CategoryTheory.homOfLE ⋯)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncGEπ_bot {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) : t.eTruncGEπ ⊥ = CategoryStruct.id (Functor.id C)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncGEπ_coe {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.eTruncGEπ (WithBotTop.coe n) = t.truncGEπ n

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncGEπ_top {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) : t.eTruncGEπ ⊤ = 0

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncGEπ_naturality {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) (i : EInt) {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp ((t.eTruncGEπ i).app X) ((t.eTruncGE.obj i).map f) = CategoryStruct.comp f ((t.eTruncGEπ i).app Y)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncGEπ_naturality_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) (i : EInt) {X Y : C} (f : X ⟶ Y) {Z : C} (h : (t.eTruncGE.obj i).obj Y ⟶ Z) : CategoryStruct.comp ((t.eTruncGEπ i).app X) (CategoryStruct.comp ((t.eTruncGE.obj i).map f) h) = CategoryStruct.comp f (CategoryStruct.comp ((t.eTruncGEπ i).app Y) h)

instance CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncGEπBotEInt {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) : IsIso (t.eTruncGEπ ⊥)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncGEπ_app_eTruncGE_map_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) {i j : EInt} (f : i ⟶ j) (X : C) : CategoryStruct.comp ((t.eTruncGEπ i).app X) ((t.eTruncGE.map f).app X) = (t.eTruncGEπ j).app X

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncGEπ_app_eTruncGE_map_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) {i j : EInt} (f : i ⟶ j) (X : C) {Z : C} (h : (t.eTruncGE.obj j).obj X ⟶ Z) : CategoryStruct.comp ((t.eTruncGEπ i).app X) (CategoryStruct.comp ((t.eTruncGE.map f).app X) h) = CategoryStruct.comp ((t.eTruncGEπ j).app X) h

theorem CategoryTheory.Triangulated.TStructure.eTruncGE_obj_map_eTruncGEπ_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) (i : EInt) (X : C) : (t.eTruncGE.obj i).map ((t.eTruncGEπ i).app X) = (t.eTruncGEπ i).app ((t.eTruncGE.obj i).obj X)

theorem CategoryTheory.Triangulated.TStructure.eTruncGE_obj_map_eTruncGEπ_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) (i : EInt) (X : C) {Z : C} (h : (t.eTruncGE.obj i).obj ((t.eTruncGE.obj i).obj X) ⟶ Z) : CategoryStruct.comp ((t.eTruncGE.obj i).map ((t.eTruncGEπ i).app X)) h = CategoryStruct.comp ((t.eTruncGEπ i).app ((t.eTruncGE.obj i).obj X)) h

theorem CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_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) {i j : EInt} (f : i ⟶ j) (X : C) : CategoryStruct.comp ((t.eTruncLT.obj i).map ((t.eTruncLTι j).app X)) ((t.eTruncLT.map f).app X) = (t.eTruncLTι i).app ((t.eTruncLT.obj j).obj X)

theorem CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_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) {i j : EInt} (f : i ⟶ j) (X : C) {Z : C} (h : (t.eTruncLT.obj j).obj X ⟶ Z) : CategoryStruct.comp ((t.eTruncLT.obj i).map ((t.eTruncLTι j).app X)) (CategoryStruct.comp ((t.eTruncLT.map f).app X) h) = CategoryStruct.comp ((t.eTruncLTι i).app ((t.eTruncLT.obj j).obj X)) h

noncomputable def CategoryTheory.Triangulated.TStructure.eTriangleLTGE {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) : Functor EInt (Functor C (Pretriangulated.Triangle C))

The (distinguished) triangles given by the natural transformations t.eTruncLT.obj i ⟶ 𝟭 C ⟶ t.eTruncGE.obj i ⟶ ... for all i : EInt.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_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) (i : EInt) (j : C) : ((t.eTriangleLTGE.obj i).obj j).obj₁ = (t.eTruncLT.obj i).obj j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_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) {X✝ Y✝ : EInt} (f : X✝ ⟶ Y✝) (j : C) : ((t.eTriangleLTGE.map f).app j).hom₂ = CategoryStruct.id j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_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) (i : EInt) (j : C) : ((t.eTriangleLTGE.obj i).obj j).mor₃ = (t.eTruncGEδLT.app i).app j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_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) (i : EInt) (j : C) : ((t.eTriangleLTGE.obj i).obj j).obj₂ = j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_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) (i : EInt) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.eTriangleLTGE.obj i).map φ).hom₃ = (t.eTruncGE.obj i).map φ

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_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) {X✝ Y✝ : EInt} (f : X✝ ⟶ Y✝) (j : C) : ((t.eTriangleLTGE.map f).app j).hom₃ = (t.eTruncGE.map f).app j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_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) (i : EInt) (j : C) : ((t.eTriangleLTGE.obj i).obj j).mor₂ = (t.eTruncGEπ i).app j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_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) {X✝ Y✝ : EInt} (f : X✝ ⟶ Y✝) (j : C) : ((t.eTriangleLTGE.map f).app j).hom₁ = (t.eTruncLT.map f).app j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_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) (i : EInt) (j : C) : ((t.eTriangleLTGE.obj i).obj j).mor₁ = (t.eTruncLTι i).app j

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_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) (i : EInt) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.eTriangleLTGE.obj i).map φ).hom₂ = φ

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_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) (i : EInt) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.eTriangleLTGE.obj i).map φ).hom₁ = (t.eTruncLT.obj i).map φ

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_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) (i : EInt) (j : C) : ((t.eTriangleLTGE.obj i).obj j).obj₃ = (t.eTruncGE.obj i).obj j

theorem CategoryTheory.Triangulated.TStructure.eTriangleLTGE_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) (i : EInt) (X : C) : (t.eTriangleLTGE.obj i).obj X ∈ Pretriangulated.distinguishedTriangles

instance CategoryTheory.Triangulated.TStructure.instIsLEObjEIntFunctorETruncLT {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] (i : EInt) : t.IsLE ((t.eTruncLT.obj i).obj X) n

instance CategoryTheory.Triangulated.TStructure.instIsGEObjEIntFunctorETruncGE {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.IsGE X n] (i : EInt) : t.IsGE ((t.eTruncGE.obj i).obj X) n

theorem CategoryTheory.Triangulated.TStructure.isGE_eTruncGE_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 : ℤ) (i : EInt) (h : WithBotTop.coe n ≤ i) (X : C) : t.IsGE ((t.eTruncGE.obj i).obj X) n

theorem CategoryTheory.Triangulated.TStructure.isLE_eTruncLT_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 : ℤ) (i : EInt) (h : i ≤ WithBotTop.coe (n + 1)) (X : C) : t.IsLE ((t.eTruncLT.obj i).obj X) n

theorem CategoryTheory.Triangulated.TStructure.isZero_eTruncLT_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) (X : C) (n : ℤ) [t.IsGE X n] (j : EInt) (hj : j ≤ WithBotTop.coe n) : Limits.IsZero ((t.eTruncLT.obj j).obj X)

theorem CategoryTheory.Triangulated.TStructure.isZero_eTruncGE_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) (X : C) (n : ℤ) [t.IsLE X n] (j : EInt) (hj : WithBotTop.coe n < j) : Limits.IsZero ((t.eTruncGE.obj j).obj X)

theorem CategoryTheory.Triangulated.TStructure.isIso_eTruncGE_obj_map_truncGEπ_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 : EInt) (h : a ≤ b) (X : C) : IsIso ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X))

theorem CategoryTheory.Triangulated.TStructure.isIso_eTruncLT_obj_map_truncLTπ_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 : EInt) (h : a ≤ b) (X : C) : IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι b).app X))

instance CategoryTheory.Triangulated.TStructure.instIsIsoMapObjEIntFunctorETruncLTAppETruncLTι {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 : EInt) (X : C) : IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X))

instance CategoryTheory.Triangulated.TStructure.instIsIsoAppETruncLTιObjEIntFunctorETruncLT {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 : EInt) (X : C) : IsIso ((t.eTruncLTι a).app ((t.eTruncLT.obj a).obj X))

instance CategoryTheory.Triangulated.TStructure.instIsGEObjEIntFunctorETruncLT {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 : ℤ) [t.IsGE X n] (i : EInt) : t.IsGE ((t.eTruncLT.obj i).obj X) n

instance CategoryTheory.Triangulated.TStructure.instIsLEObjEIntFunctorETruncGE {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 : ℤ) [t.IsLE X n] (i : EInt) : t.IsLE ((t.eTruncGE.obj i).obj X) n

noncomputable def CategoryTheory.Triangulated.TStructure.eTruncGEToGEGE {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 : EInt) : t.eTruncGE.obj b ⟶ (t.eTruncGE.obj a).comp (t.eTruncGE.obj b)

The natural transformation t.eTruncGE.obj b ⟶ t.eTruncGE.obj a ⋙ t.eTruncGE.obj b for all a and b in EInt.

Equations

• t.eTruncGEToGEGE a b = CategoryTheory.CategoryStruct.comp (t.eTruncGE.obj b).leftUnitor.inv (CategoryTheory.Functor.whiskerRight (t.eTruncGEπ a) (t.eTruncGE.obj b))

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncGEToGEGE_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 : EInt) (X : C) : (t.eTruncGEToGEGE a b).app X = (t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X)

theorem CategoryTheory.Triangulated.TStructure.isIso_eTruncGEIsoGEGE {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 : EInt) (hab : a ≤ b) : IsIso (t.eTruncGEToGEGE a b)

noncomputable def CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE {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 : EInt) (hab : a ≤ b) : t.eTruncGE.obj b ≅ (t.eTruncGE.obj a).comp (t.eTruncGE.obj b)

The natural isomorphism t.eTruncGE.obj b ≅ t.eTruncGE.obj a ⋙ t.eTruncGE.obj b when a and b in EInt satisfy a ≤ b.

Equations

• t.eTruncGEIsoGEGE a b hab = CategoryTheory.asIso (t.eTruncGEToGEGE a b)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_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) [IsTriangulated C] (a b : EInt) (hab : a ≤ b) : (t.eTruncGEIsoGEGE a b hab).hom = t.eTruncGEToGEGE a b

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_hom_inv_id_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 : EInt) (hab : a ≤ b) (X : C) : CategoryStruct.comp ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X)) ((t.eTruncGEIsoGEGE a b hab).inv.app X) = CategoryStruct.id ((t.eTruncGE.obj b).obj ((Functor.id C).obj X))

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_hom_inv_id_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) [IsTriangulated C] (a b : EInt) (hab : a ≤ b) (X : C) {Z : C} (h : (t.eTruncGE.obj b).obj X ⟶ Z) : CategoryStruct.comp ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X)) (CategoryStruct.comp ((t.eTruncGEIsoGEGE a b hab).inv.app X) h) = h

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_inv_hom_id_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 : EInt) (hab : a ≤ b) (X : C) : CategoryStruct.comp ((t.eTruncGEIsoGEGE a b hab).inv.app X) ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X)) = CategoryStruct.id (((t.eTruncGE.obj a).comp (t.eTruncGE.obj b)).obj X)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_inv_hom_id_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) [IsTriangulated C] (a b : EInt) (hab : a ≤ b) (X : C) {Z : C} (h : (t.eTruncGE.obj b).obj ((t.eTruncGE.obj a).obj X) ⟶ Z) : CategoryStruct.comp ((t.eTruncGEIsoGEGE a b hab).inv.app X) (CategoryStruct.comp ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X)) h) = h

noncomputable def CategoryTheory.Triangulated.TStructure.eTruncLTLTToLT {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 : EInt) : (t.eTruncLT.obj a).comp (t.eTruncLT.obj b) ⟶ t.eTruncLT.obj b

The natural transformation t.eTruncLT.obj a ⋙ t.eTruncLT.obj b ⟶ t.eTruncLT.obj b for all a and b in EInt.

Equations

• t.eTruncLTLTToLT a b = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (t.eTruncLTι a) (t.eTruncLT.obj b)) (t.eTruncLT.obj b).leftUnitor.hom

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLTLTToLT_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 : EInt) (X : C) : (t.eTruncLTLTToLT a b).app X = (t.eTruncLT.obj b).map ((t.eTruncLTι a).app X)

theorem CategoryTheory.Triangulated.TStructure.isIso_eTruncLTLTIsoLT {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 : EInt) (hab : b ≤ a) : IsIso (t.eTruncLTLTToLT a b)

noncomputable def CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT {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 : EInt) (hab : b ≤ a) : (t.eTruncLT.obj a).comp (t.eTruncLT.obj b) ≅ t.eTruncLT.obj b

The natural isomorphism t.eTruncLT.obj a ⋙ t.eTruncLT.obj b ⟶ t.eTruncLT.obj b when a and b in EInt satisfy b ≤ a.

Equations

• t.eTruncLTLTIsoLT a b hab = CategoryTheory.asIso (t.eTruncLTLTToLT a b)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_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) [IsTriangulated C] (a b : EInt) (hab : b ≤ a) : (t.eTruncLTLTIsoLT a b hab).hom = t.eTruncLTLTToLT a b

theorem CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_hom_inv_id_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 : EInt) (hab : b ≤ a) (X : C) : CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncLTι a).app X)) ((t.eTruncLTLTIsoLT a b hab).inv.app X) = CategoryStruct.id ((t.eTruncLT.obj b).obj ((t.eTruncLT.obj a).obj X))

theorem CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_hom_inv_id_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) [IsTriangulated C] (a b : EInt) (hab : b ≤ a) (X : C) {Z : C} (h : (t.eTruncLT.obj b).obj ((t.eTruncLT.obj a).obj X) ⟶ Z) : CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncLTι a).app X)) (CategoryStruct.comp ((t.eTruncLTLTIsoLT a b hab).inv.app X) h) = h

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_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 : EInt) (hab : b ≤ a) (X : C) : CategoryStruct.comp ((t.eTruncLTLTIsoLT a b hab).inv.app X) ((t.eTruncLT.obj b).map ((t.eTruncLTι a).app X)) = CategoryStruct.id ((t.eTruncLT.obj b).obj X)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_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) [IsTriangulated C] (a b : EInt) (hab : b ≤ a) (X : C) {Z : C} (h : (t.eTruncLT.obj b).obj X ⟶ Z) : CategoryStruct.comp ((t.eTruncLTLTIsoLT a b hab).inv.app X) (CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncLTι a).app X)) h) = h

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_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) [IsTriangulated C] (a b : EInt) (hab : b ≤ a) (X : C) : CategoryStruct.comp ((t.eTruncLTLTIsoLT a b hab).inv.app ((t.eTruncLT.obj a).obj X)) ((t.eTruncLT.obj b).map ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X))) = CategoryStruct.id ((t.eTruncLT.obj b).obj ((t.eTruncLT.obj a).obj X))

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj_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) [IsTriangulated C] (a b : EInt) (hab : b ≤ a) (X : C) {Z : C} (h : (t.eTruncLT.obj b).obj ((t.eTruncLT.obj a).obj X) ⟶ Z) : CategoryStruct.comp ((t.eTruncLTLTIsoLT a b hab).inv.app ((t.eTruncLT.obj a).obj X)) (CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X))) h) = h

noncomputable def CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToLTGE {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 : EInt) : (t.eTruncLT.obj b).comp ((t.eTruncGE.obj a).comp (t.eTruncLT.obj b)) ⟶ (t.eTruncGE.obj a).comp (t.eTruncLT.obj b)

The natural transformation from t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b to t.eTruncGE.obj a ⋙ t.eTruncLT.obj b. (This is an isomorphism.)

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToLTGE_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 : EInt) (X : C) : (t.eTruncLTGELTSelfToLTGE a b).app X = (t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X))

noncomputable def CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToGELT {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 : EInt) : (t.eTruncLT.obj b).comp ((t.eTruncGE.obj a).comp (t.eTruncLT.obj b)) ⟶ (t.eTruncLT.obj b).comp (t.eTruncGE.obj a)

The natural transformation from t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b to t.eTruncLT.obj b ⋙ t.eTruncGE.obj a. (This is an isomorphism.)

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToGELT_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 : EInt) (X : C) : (t.eTruncLTGELTSelfToGELT a b).app X = (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X))

instance CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTGELTSelfToLTGE {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 : EInt) : IsIso (t.eTruncLTGELTSelfToLTGE a b)

instance CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTGELTSelfToGELT {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 : EInt) : IsIso (t.eTruncLTGELTSelfToGELT a b)

noncomputable def CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT {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 : EInt) : (t.eTruncGE.obj a).comp (t.eTruncLT.obj b) ≅ (t.eTruncLT.obj b).comp (t.eTruncGE.obj a)

The commutation natural isomorphism t.eTruncGE.obj a ⋙ t.eTruncLT.obj b ≅ t.eTruncLT.obj b ⋙ t.eTruncGE.obj a for all a and b in EInt.

Equations

• t.eTruncLTGEIsoGELT a b = (CategoryTheory.asIso (t.eTruncLTGELTSelfToLTGE a b)).symm ≪≫ CategoryTheory.asIso (t.eTruncLTGELTSelfToGELT a b)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_naturality {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 : EInt) {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map f)) ((t.eTruncLTGEIsoGELT a b).hom.app Y) = CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X) ((t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map f))

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_naturality_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) [IsTriangulated C] (a b : EInt) {X Y : C} (f : X ⟶ Y) {Z : C} (h : (t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj Y) ⟶ Z) : CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map f)) (CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app Y) h) = CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X) (CategoryStruct.comp ((t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map f)) h)

theorem CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac {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 : EInt) (X : C) : CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X))) ((t.eTruncLTGEIsoGELT a b).hom.app X) = (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X))

theorem CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac_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) [IsTriangulated C] (a b : EInt) (X : C) {Z : C} (h : (t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X) ⟶ Z) : CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X))) (CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X) h) = CategoryStruct.comp ((t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X))) h

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac' {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 : EInt) (X : C) : CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X) ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X)) = (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj X)

@[simp]

theorem CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac'_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) [IsTriangulated C] (a b : EInt) (X : C) {Z : C} (h : (t.eTruncGE.obj a).obj X ⟶ Z) : CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X) (CategoryStruct.comp ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X)) h) = CategoryStruct.comp ((t.eTruncLTι b).app ((t.eTruncGE.obj a).obj X)) h

theorem CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_naturality_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 : EInt) (hab : a ≤ b) (a' b' : EInt) (hab' : a' ≤ b') (φ : ComposableArrows.mk₁ (homOfLE hab) ⟶ ComposableArrows.mk₁ (homOfLE hab')) (X : C) : CategoryStruct.comp ((t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj X)) (CategoryStruct.comp ((t.eTruncLT.obj b').map ((t.eTruncGE.map (φ.app 0)).app X)) ((t.eTruncLTGEIsoGELT a' b').hom.app X)) = CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X) (CategoryStruct.comp ((t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X)) ((t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app X)))

theorem CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_naturality_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) [IsTriangulated C] (a b : EInt) (hab : a ≤ b) (a' b' : EInt) (hab' : a' ≤ b') (φ : ComposableArrows.mk₁ (homOfLE hab) ⟶ ComposableArrows.mk₁ (homOfLE hab')) (X : C) {Z : C} (h : (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X) ⟶ Z) : CategoryStruct.comp ((t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj X)) (CategoryStruct.comp ((t.eTruncLT.obj b').map ((t.eTruncGE.map (φ.app 0)).app X)) (CategoryStruct.comp ((t.eTruncLTGEIsoGELT a' b').hom.app X) h)) = CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X) (CategoryStruct.comp ((t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X)) (CategoryStruct.comp ((t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app X)) h))