Bridgeland Stability Conditions

6.2. TStructure: HeartAbelian🔗

6.2.1. heart_hι🔗

No negative Hom spaces in the heart. For objects X, Y in the heart of a t-structure t, every morphism \iota(X) \to \iota(Y)[n] is zero when n < 0.

Proof: Since \iota(Y)[n] is \operatorname{IsGE}(-n) with -n > 0 and \iota(X) is \operatorname{IsLE}(0), the vanishing t.\operatorname{zero} applies.

🔗theorem
CategoryTheory.Triangulated.TStructure.heart_hι.{v', u', v, u}
  {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {H : Type u'}
  [CategoryTheory.Category.{v', u'} H] [CategoryTheory.Preadditive H]
  [t.Heart H] ⦃X Y : H⦄ ⦃n : ℤ⦄
  (f :
    t.ιHeart.obj X ⟶
      (CategoryTheory.shiftFunctor C n).obj (t.ιHeart.obj Y)) :
  n < 0 → f = 0
CategoryTheory.Triangulated.TStructure.heart_hι.{v',
    u', v, u}
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t :
    CategoryTheory.Triangulated.TStructure
      C)
  {H : Type u'}
  [CategoryTheory.Category.{v', u'} H]
  [CategoryTheory.Preadditive H]
  [t.Heart H] ⦃X Y : H⦄ ⦃n : ℤ⦄
  (f :
    t.ιHeart.obj X ⟶
      (CategoryTheory.shiftFunctor C
            n).obj
        (t.ιHeart.obj Y)) :
  n < 0 → f = 0

Something wrong, better idea? Suggest a change

6.2.2. heart_admissible🔗

Admissibility of heart morphisms. Every morphism in the heart is admissible in the sense of AbelianSubcategory: given f_1 \colon X_1 \to X_2 in the heart, the cone X_3 of \iota(f_1) decomposes as \iota(K)[1] \to X_3 \to \iota(Q) with K, Q in the heart.

Proof: The cone X_3 satisfies \operatorname{IsLE}(0) and \operatorname{IsGE}(-1) (from the rotated distinguished triangle and the heart conditions on X_1, X_2). The truncation triangle \tau_{<0}(X_3) \to X_3 \to \tau_{\ge 0}(X_3) provides Q = \tau_{\ge 0}(X_3) (which is \operatorname{IsLE}(0) and \operatorname{IsGE}(0), hence in the heart) and K = \tau_{<0}(X_3)[-1] (which is \operatorname{IsLE}(0) and \operatorname{IsGE}(0) after unshifting, hence in the heart). The essential image of \iota recovers actual heart objects, and the admissible triangle is built from the truncation triangle via explicit isomorphisms.

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

Something wrong, better idea? Suggest a change

6.2.3. heartAbelian🔗

Heart abelianity. The heart of a t-structure on a triangulated category is abelian, assuming the heart has finite products. This is cite(Th'eor`eme 1.3.6)(bbd-1982).

Construction: Constructed by applying AbelianSubcategory.abelian to the heart embedding \iota, using heart_hι (no negative Hom spaces) and heart_admissible (all morphisms admissible).

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

Something wrong, better idea? Suggest a change

6.2.4. heart_containsZero🔗

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

Proof: The zero object is both \operatorname{IsLE}(0) and \operatorname{IsGE}(0).

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

Something wrong, better idea? Suggest a change

6.2.5. heart_biprod🔗

The biproduct of two heart objects lies in the heart.

Proof: The biproduct triangle X \oplus Y \to X \to Y \to (X \oplus Y)[1] is distinguished. Apply isLE\sb{2} and isGE\sb{2} to the \operatorname{IsLE}(0) and \operatorname{IsGE}(0) conditions of X and Y.

🔗theorem
CategoryTheory.Triangulated.TStructure.heart_biprod.{v, u} {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X Y : C)
  (hX : t.heart X) (hY : t.heart Y) : t.heart (X ⊞ Y)
CategoryTheory.Triangulated.TStructure.heart_biprod.{v,
    u}
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t :
    CategoryTheory.Triangulated.TStructure
      C)
  (X Y : C) (hX : t.heart X)
  (hY : t.heart Y) : t.heart (X ⊞ Y)

Something wrong, better idea? Suggest a change

6.2.6. heart_closedUnderBinaryProducts🔗

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

Proof: Any binary product X \times Y is isomorphic to X \oplus Y (via the biproduct--product isomorphism in a preadditive category), and heart_biprod shows X \oplus Y lies in the heart.

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

Something wrong, better idea? Suggest a change

6.2.7. heart_closedUnderFiniteProducts🔗

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

Proof: Follows from closure under binary products and the zero object via ObjectProperty.IsClosedUnderFiniteProducts.mk'.

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

Something wrong, better idea? Suggest a change

6.2.8. heart_hasFiniteProducts🔗

The full subcategory defined by the heart has finite products.

Proof: Combine the terminal object (from heart_containsZero) and binary products (from heart_closedUnderBinaryProducts) via hasFiniteProducts_of_has_binary_and_terminal.

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

Something wrong, better idea? Suggest a change

6.2.9. heartFullSubcategoryAbelian🔗

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

Construction: Instantiates heartAbelian with the canonical heart full subcategory, using heart_hasFiniteProducts for the finite products hypothesis.

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

Something wrong, better idea? Suggest a change