The heart of the canonical t-structure is the original abelian category

For an abelian category C with a derived category, the heart of the canonical t-structure on DerivedCategory C is C itself, embedded by singleFunctor C 0.

Mathlib states this as the motivating example of TStructure.Heart and does not prove it; nothing in either tree identified the heart of the canonical t-structure with anything. This file supplies the identification, in Mathlib's own designated form.

What the proof is

Nothing new. Both halves are already in Mathlib and only had to be put together:

• singleFunctor C 0 is additive, full and faithful — DerivedCategory.Basic and DerivedCategory.FullyFaithful;
• its objects are ≤ 0 and ≥ 0, so they lie in the heart — the two instances beside exists_iso_singleFunctor_obj_of_isGE_of_isLE;
• conversely an object of the heart is ≤ 0 and ≥ 0, so exists_iso_singleFunctor_obj_of_isGE_of_isLE at n = 0 puts it in the essential image.

That is exactly the four fields of TStructure.Heart, so the identification is registered as an instance and every consumer of ιHeart gets it.

Why this exists

Numerical data on an abelian category — a rank, a degree, a Mukai class, all of them homomorphisms out of K₀Ab — is written against the category the sheaves live in. The stability machinery is written against the heart of a t-structure. Without this identification the two cannot meet, and the abstract stability theory can never be instantiated on a category of sheaves.

heartEquivalence is the transport vehicle; combined with K₀Ab.congr it moves a homomorphism out of K₀Ab C to one out of K₀Ab of the heart.

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

An object in the essential image of singleFunctor C 0 lies in the heart.

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

The essential image of singleFunctor C 0 is exactly the heart.

@[implicit_reducible]

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

C is the heart of the canonical t-structure on DerivedCategory C.

Mathlib names this as the motivating example of TStructure.Heart and leaves it unproved. All four fields come from existing results; see the module docstring.

Equations

• DerivedCategory.isHeart C = { ι := DerivedCategory.singleFunctor C 0, additive_ι := ⋯, full_ι := ⋯, faithful_ι := ⋯, essImage_eq_heart := ⋯ }

theorem DerivedCategory.ιHeart_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : TStructure.t.ιHeart = singleFunctor C 0

The inclusion supplied by isHeart is singleFunctor C 0.

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

singleFunctor C 0 lifted to the heart as a full subcategory.

Equations

• DerivedCategory.toHeart C = DerivedCategory.TStructure.t.heart.lift (DerivedCategory.singleFunctor C 0) ⋯

@[simp]

theorem DerivedCategory.toHeart_comp_ι (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (toHeart C).comp TStructure.t.heart.ι = singleFunctor C 0

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

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

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

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

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

The heart of the canonical t-structure is C.

This is the transport vehicle: numerical data written on C moves to the heart along it, which is what lets stability theory stated for a heart be instantiated on a category of sheaves.

Equations

• DerivedCategory.heartEquivalence C = (DerivedCategory.toHeart C).asEquivalence

@[simp]

theorem DerivedCategory.heartEquivalence_functor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (heartEquivalence C).functor = toHeart C

@[simp]

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