The heart of a t-structure

Let t be a t-structure on a triangulated category C. We define the heart of t as a property t.heart : ObjectProperty C. As the the heart is usually identified to a particular category in the applications (e.g. the heart of the canonical t-structure on the derived category of an abelian category A identifies to A), instead of working with the full subcategory defined by t.heart, we introduce a typeclass t.Heart H which says that the additive category H identifies to the full subcategory t.heart.

TODO (@joelriou)

• Show that the heart is an abelian category.

References

• Beilinson, Bernstein, Deligne, Gabber, Faisceaux pervers

def CategoryTheory.Triangulated.TStructure.heart {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) : ObjectProperty C

The heart of a t-structure, as the property of objects that are both ≤ 0 and ≥ 0.

Equations

• t.heart = t.le 0 ⊓ t.ge 0

@[instance_reducible]

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

Equations

• ⋯ = ⋯

theorem CategoryTheory.Triangulated.TStructure.mem_heart_iff {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) : t.heart X ↔ t.IsLE X 0 ∧ t.IsGE X 0

class CategoryTheory.Triangulated.TStructure.Heart {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (H : Type u') [Category.{v', u'} H] [Preadditive H] : Type (max (max (max u u') v) v')

Given t : TStructure C and a preadditive category H, this typeclass contains the data of a fully faithful additive functor H ⥤ C which identifies H to the full subcategory of C consisting of the objects satisfying the property t.heart.

• ι : Functor H C

  The inclusion functor.

• additive_ι : (ι t).Additive
• full_ι : (ι t).Full
• faithful_ι : (ι t).Faithful
• essImage_eq_heart : (ι t).essImage = t.heart

def CategoryTheory.Triangulated.TStructure.hasHeartFullSubcategory {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.Heart t.heart.FullSubcategory

Unless a better candidate category is available, the full subcategory of objects satisfying t.heart can be chosen as the heart of a t-structure t.

Equations

• t.hasHeartFullSubcategory = { ι := t.heart.ι, additive_ι := ⋯, full_ι := ⋯, faithful_ι := ⋯, essImage_eq_heart := ⋯ }

def CategoryTheory.Triangulated.TStructure.ιHeart {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {H : Type u'} [Category.{v', u'} H] [Preadditive H] [t.Heart H] : Functor H C

The inclusion H ⥤ C when H is the heart of a t-structure t on C.

Equations

• t.ιHeart = CategoryTheory.Triangulated.TStructure.Heart.ι t

instance CategoryTheory.Triangulated.TStructure.instAdditiveιHeart {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (H : Type u') [Category.{v', u'} H] [Preadditive H] [t.Heart H] : t.ιHeart.Additive

instance CategoryTheory.Triangulated.TStructure.instFullιHeart {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (H : Type u') [Category.{v', u'} H] [Preadditive H] [t.Heart H] : t.ιHeart.Full

instance CategoryTheory.Triangulated.TStructure.instFaithfulιHeart {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (H : Type u') [Category.{v', u'} H] [Preadditive H] [t.Heart H] : t.ιHeart.Faithful

@[simp]

theorem CategoryTheory.Triangulated.TStructure.essImage_ιHeart {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (H : Type u') [Category.{v', u'} H] [Preadditive H] [t.Heart H] : t.ιHeart.essImage = t.heart

theorem CategoryTheory.Triangulated.TStructure.ιHeart_obj_mem {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {H : Type u'} [Category.{v', u'} H] [Preadditive H] [t.Heart H] (X : H) : t.heart (t.ιHeart.obj X)

instance CategoryTheory.Triangulated.TStructure.instIsLEObjιHeartOfNatInt {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (H : Type u') [Category.{v', u'} H] [Preadditive H] [t.Heart H] (X : H) : t.IsLE (t.ιHeart.obj X) 0

instance CategoryTheory.Triangulated.TStructure.instIsGEObjιHeartOfNatInt {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (H : Type u') [Category.{v', u'} H] [Preadditive H] [t.Heart H] (X : H) : t.IsGE (t.ιHeart.obj X) 0