The canonical t-structure on the derived category

In this file, we introduce the canonical t-structure on the derived category of an abelian category.

noncomputable def DerivedCategory.TStructure.t {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Triangulated.TStructure (DerivedCategory C)

The canonical t-structure on DerivedCategory C.

@[reducible, inline]

abbrev DerivedCategory.IsLE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : DerivedCategory C) (n : ℤ) : Prop

Given X : DerivedCategory C and n : ℤ, this property means that X is ≤ n for the canonical t-structure.

@[reducible, inline]

abbrev DerivedCategory.IsGE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : DerivedCategory C) (n : ℤ) : Prop

Given X : DerivedCategory C and n : ℤ, this property means that X is ≥ n for the canonical t-structure.

theorem DerivedCategory.isGE_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : DerivedCategory C) (n : ℤ) : X.IsGE n ↔ ∀ i < n, CategoryTheory.Limits.IsZero ((homologyFunctor C i).obj X)

theorem DerivedCategory.isLE_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : DerivedCategory C) (n : ℤ) : X.IsLE n ↔ ∀ (i : ℤ), n < i → CategoryTheory.Limits.IsZero ((homologyFunctor C i).obj X)

theorem DerivedCategory.isZero_of_isGE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : DerivedCategory C) (n i : ℤ) (hi : i < n) [hX : X.IsGE n] : CategoryTheory.Limits.IsZero ((homologyFunctor C i).obj X)

theorem DerivedCategory.isZero_of_isLE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : DerivedCategory C) (n i : ℤ) (hi : n < i) [hX : X.IsLE n] : CategoryTheory.Limits.IsZero ((homologyFunctor C i).obj X)

theorem DerivedCategory.isGE_Q_obj_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (K : CochainComplex C ℤ) (n : ℤ) : (Q.obj K).IsGE n ↔ K.IsGE n

theorem DerivedCategory.isLE_Q_obj_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (K : CochainComplex C ℤ) (n : ℤ) : (Q.obj K).IsLE n ↔ K.IsLE n

instance DerivedCategory.instIsGEObjCochainComplexIntQOfIsGE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsGE n] : (Q.obj K).IsGE n

instance DerivedCategory.instIsLEObjCochainComplexIntQOfIsLE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsLE n] : (Q.obj K).IsLE n

instance DerivedCategory.instIsGEObjSingleFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : C) (n : ℤ) : ((singleFunctor C n).obj X).IsGE n

instance DerivedCategory.instIsLEObjSingleFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : C) (n : ℤ) : ((singleFunctor C n).obj X).IsLE n

theorem DerivedCategory.exists_iso_Q_obj_of_isLE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : DerivedCategory C) (n : ℤ) [hX : X.IsLE n] : ∃ (K : CochainComplex C ℤ) (_ : K.IsStrictlyLE n), Nonempty (X ≅ Q.obj K)

theorem DerivedCategory.exists_iso_Q_obj_of_isGE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : DerivedCategory C) (n : ℤ) [hX : X.IsGE n] : ∃ (K : CochainComplex C ℤ) (_ : K.IsStrictlyGE n), Nonempty (X ≅ Q.obj K)

theorem DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : DerivedCategory C) (a b : ℤ) [X.IsGE a] [X.IsLE b] : ∃ (K : CochainComplex C ℤ) (_ : K.IsStrictlyGE a) (_ : K.IsStrictlyLE b), Nonempty (X ≅ Q.obj K)

theorem DerivedCategory.exists_iso_singleFunctor_obj_of_isGE_of_isLE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : DerivedCategory C) (n : ℤ) [X.IsGE n] [X.IsLE n] : ∃ (Y : C), Nonempty (X ≅ (singleFunctor C n).obj Y)