Documentation

BridgelandStability.TStructure.HeartAbelian

The heart of a t-structure is abelian #

We show that the heart of a t-structure on a triangulated category is abelian, following [BBD, Faisceaux pervers, Théorème 1.3.6].

The proof uses the criterion AbelianSubcategory.abelian, which requires:

  1. No negative Hom spaces: for heart objects X, Y, every morphism ι X ⟶ (ι Y)⟦n⟧ is zero when n < 0.
  2. Admissibility: every morphism in the heart is admissible. Given f₁ : X₁ → X₂ in the heart, the cone X₃ of ι.map f₁ is IsLE 0 and IsGE (-1). The truncation functors decompose X₃ as τ<0(X₃) → X₃ → τ≥0(X₃), where both τ≥0(X₃) and τ<0(X₃)⟦-1⟧ lie in the heart.

Main results #

References #

source
theorem CategoryTheory.Triangulated.TStructure.heart_hι {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 Y : H⦄ ⦃n : ℤ⦄ (f : t.ιHeart.obj X ⟶ (shiftFunctor C n).obj (t.ιHeart.obj Y)) :
n < 0 → f = 0

No negative Hom spaces in the heart. For heart objects X and Y, every morphism ι X ⟶ (ι Y)⟦n⟧ is zero when n < 0.

source
theorem CategoryTheory.Triangulated.TStructure.heart_admissible {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] :
AbelianSubcategory.admissibleMorphism t.ιHeart = ⊤

Admissibility of heart morphisms. Every morphism in the heart is admissible: for f₁ : X₁ → X₂ in the heart, the cone X₃ of ι.map f₁ decomposes as (ι K)⟦1⟧ → X₃ → ι Q via the truncation triangle, with K, Q in the heart.

source
@[reducible]
noncomputable def CategoryTheory.Triangulated.TStructure.heartAbelian {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] [IsTriangulated C] [Limits.HasFiniteProducts H] :
Abelian H

Heart abelianity. The heart of a t-structure on a triangulated category is abelian, assuming the heart has finite products.

Equations
Instances For

    The heart contains zero and is closed under binary products #

    source
    instance CategoryTheory.Triangulated.TStructure.heart_containsZero {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.ContainsZero

    The zero object lies in the heart of any t-structure.

    source
    theorem CategoryTheory.Triangulated.TStructure.heart_biprod {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 Y : C) (hX : t.heart X) (hY : t.heart Y) :
    t.heart (X ⊞ Y)

    The biproduct of two heart objects lies in the heart.

    source
    instance CategoryTheory.Triangulated.TStructure.heart_closedUnderBinaryProducts {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.IsClosedUnderBinaryProducts

    The heart of a t-structure is closed under binary products.

    source
    instance CategoryTheory.Triangulated.TStructure.heart_closedUnderFiniteProducts {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.IsClosedUnderFiniteProducts

    The heart of a t-structure is closed under finite products.

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

    The full subcategory defined by the heart has finite products.

    source
    @[reducible]
    noncomputable def CategoryTheory.Triangulated.TStructure.heartFullSubcategoryAbelian {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] :
    Abelian t.heart.FullSubcategory

    Heart abelianity (canonical form). The full subcategory of heart objects of a t-structure on a triangulated category is abelian.

    Equations
    Instances For