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.

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 cutsat) : 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 cutsat) : ∃ (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 cutsat) : ∃ (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π₃

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.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_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_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_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_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.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