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.

Equations

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

@[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.

Equations

• X.IsLE n = DerivedCategory.TStructure.t.IsLE X n

@[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.

Equations

• X.IsGE n = DerivedCategory.TStructure.t.IsGE X n

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)

@[reducible, inline]

abbrev DerivedCategory.Minus (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : Type (max u v)

The bounded above derived category of an abelian category.

Equations

• DerivedCategory.Minus C = DerivedCategory.TStructure.t.minus.FullSubcategory

@[reducible, inline]

abbrev DerivedCategory.Plus (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : Type (max u v)

The bounded below derived category of an abelian category.

Equations

• DerivedCategory.Plus C = DerivedCategory.TStructure.t.plus.FullSubcategory

@[reducible, inline]

abbrev DerivedCategory.Bounded (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : Type (max u v)

The bounded derived category of an abelian category.

Equations

• DerivedCategory.Bounded C = DerivedCategory.TStructure.t.bounded.FullSubcategory

@[reducible, inline]

noncomputable abbrev DerivedCategory.Minus.ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Functor (Minus C) (DerivedCategory C)

The inclusion of the bounded above derived category.

Equations

• DerivedCategory.Minus.ι = DerivedCategory.TStructure.t.minus.ι

@[reducible, inline]

noncomputable abbrev DerivedCategory.Plus.ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Functor (Plus C) (DerivedCategory C)

The inclusion of the bounded below derived category.

Equations

• DerivedCategory.Plus.ι = DerivedCategory.TStructure.t.plus.ι

@[reducible, inline]

noncomputable abbrev DerivedCategory.Bounded.ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Functor (Bounded C) (DerivedCategory C)

The inclusion of the bounded derived category.

Equations

• DerivedCategory.Bounded.ι = DerivedCategory.TStructure.t.bounded.ι