The standard heart of the bounded derived category

The canonical t-structure on DerivedCategory C restricts to its bounded subcategory. This file identifies the heart of that restricted t-structure with C, by lifting singleFunctor C 0 through the bounded inclusion.

This is deliberately separate from Heart.lean: the latter concerns the unbounded derived category, while stability conditions for varieties are carried by Dᵇ(Coh X).

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

singleFunctor C 0, lifted to the bounded derived category.

Equations

• DerivedCategory.boundedSingleFunctor C = DerivedCategory.TStructure.t.bounded.lift (DerivedCategory.singleFunctor C 0) ⋯

instance DerivedCategory.boundedSingleFunctor_additive (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (boundedSingleFunctor C).Additive

instance DerivedCategory.boundedSingleFunctor_full (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (boundedSingleFunctor C).Full

instance DerivedCategory.boundedSingleFunctor_faithful (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (boundedSingleFunctor C).Faithful

@[simp]

theorem DerivedCategory.boundedSingleFunctor_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : C) : ((boundedSingleFunctor C).obj X).obj = (singleFunctor C 0).obj X

theorem DerivedCategory.boundedHeart_singleFunctor_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : C) : TStructure.t.onBounded.heart ((boundedSingleFunctor C).obj X)

An object in the image of boundedSingleFunctor lies in the standard heart of the bounded derived category.

theorem DerivedCategory.essImage_boundedSingleFunctor_eq_boundedHeart (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (boundedSingleFunctor C).essImage = TStructure.t.onBounded.heart

The essential image of boundedSingleFunctor C is exactly the standard heart of DerivedCategory.Bounded C.

@[implicit_reducible]

noncomputable instance DerivedCategory.isBoundedHeart (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : TStructure.t.onBounded.Heart C

The original abelian category is the heart of the induced standard t-structure on its bounded derived category.

Equations

• DerivedCategory.isBoundedHeart C = { ι := DerivedCategory.boundedSingleFunctor C, additive_ι := ⋯, full_ι := ⋯, faithful_ι := ⋯, essImage_eq_heart := ⋯ }

noncomputable def DerivedCategory.toBoundedHeart (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Functor C TStructure.t.onBounded.heart.FullSubcategory

C lifted to the full subcategory underlying the bounded standard heart.

Equations

• DerivedCategory.toBoundedHeart C = DerivedCategory.TStructure.t.onBounded.heart.lift (DerivedCategory.boundedSingleFunctor C) ⋯

@[simp]

theorem DerivedCategory.toBoundedHeart_comp_ι (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (toBoundedHeart C).comp TStructure.t.onBounded.heart.ι = boundedSingleFunctor C

instance DerivedCategory.toBoundedHeart_full (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (toBoundedHeart C).Full

instance DerivedCategory.toBoundedHeart_faithful (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (toBoundedHeart C).Faithful

instance DerivedCategory.toBoundedHeart_essSurj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (toBoundedHeart C).EssSurj

instance DerivedCategory.toBoundedHeart_isEquivalence (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (toBoundedHeart C).IsEquivalence

noncomputable def DerivedCategory.boundedHeartEquivalence (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : C ≌ TStructure.t.onBounded.heart.FullSubcategory

The equivalence from C to the standard heart of Dᵇ(C).

Equations

• DerivedCategory.boundedHeartEquivalence C = (DerivedCategory.toBoundedHeart C).asEquivalence

@[simp]

theorem DerivedCategory.boundedHeartEquivalence_functor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (boundedHeartEquivalence C).functor = toBoundedHeart C

@[simp]

theorem DerivedCategory.toBoundedHeart_obj_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : C) : ((toBoundedHeart C).obj X).obj.obj = (singleFunctor C 0).obj X