Bridgeland Stability Conditions

12.2. HeartEquivalence: Basic🔗

12.2.1. isZero_of_obj_isZero🔗

If the underlying object of a full-subcategory element is zero in the ambient category, then the full-subcategory element itself is zero.

Proof: Constructs the unique isomorphism from the given object to the zero object of the full subcategory, using the ambient zero-object isomorphism and the lifting property of full subcategories.

🔗theorem
CategoryTheory.Triangulated.ObjectProperty.FullSubcategory.isZero_of_obj_isZero.{v,
    u}
  {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroMorphisms C]
  {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.Limits.HasZeroMorphisms P.FullSubcategory]
  [CategoryTheory.Limits.HasZeroObject P.FullSubcategory]
  {X : P.FullSubcategory} (hX : CategoryTheory.Limits.IsZero X.obj) :
  CategoryTheory.Limits.IsZero X
CategoryTheory.Triangulated.ObjectProperty.FullSubcategory.isZero_of_obj_isZero.{v,
    u}
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroMorphisms
      C]
  {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.Limits.HasZeroMorphisms
      P.FullSubcategory]
  [CategoryTheory.Limits.HasZeroObject
      P.FullSubcategory]
  {X : P.FullSubcategory}
  (hX :
    CategoryTheory.Limits.IsZero X.obj) :
  CategoryTheory.Limits.IsZero X

Something wrong, better idea? Suggest a change

12.2.2. P_phi_shortExact_triangle🔗

A short exact sequence 0 \to A \to B \to Q \to 0 in the abelian slice \mathcal{P}(\varphi) of a stability condition lifts to a distinguished triangle A \to B \to Q \to A[1] in the ambient triangulated category \mathcal{C}.

Proof: Uses the admissibility of \mathcal{P}(\varphi) as an abelian subcategory together with the Hom-vanishing property to produce the octahedral lift, then verifies that the kernel--cokernel pair in the subcategory matches the triangle's first two morphisms.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.P_phi_shortExact_triangle.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (σ : CategoryTheory.Triangulated.StabilityCondition C) (φ : ℝ)
  {A B Q : (σ.slicing.P φ).FullSubcategory} (f : A ⟶ B) (g : B ⟶ Q)
  (hfg : CategoryTheory.CategoryStruct.comp f g = 0)
  [CategoryTheory.Mono f] [CategoryTheory.Epi g]
  (hexact :
    ∀ {W : (σ.slicing.P φ).FullSubcategory} (α : W ⟶ B),
      CategoryTheory.CategoryStruct.comp α g = 0 →
        ∃ β, CategoryTheory.CategoryStruct.comp β f = α) :
  ∃ h,
    CategoryTheory.Pretriangulated.Triangle.mk f.hom g.hom h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles
CategoryTheory.Triangulated.StabilityCondition.P_phi_shortExact_triangle.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition
      C)
  (φ : ℝ)
  {A B Q :
    (σ.slicing.P φ).FullSubcategory}
  (f : A ⟶ B) (g : B ⟶ Q)
  (hfg :
    CategoryTheory.CategoryStruct.comp f
        g =
      0)
  [CategoryTheory.Mono f]
  [CategoryTheory.Epi g]
  (hexact :
    ∀
      {W :
        (σ.slicing.P φ).FullSubcategory}
      (α : W ⟶ B),
      CategoryTheory.CategoryStruct.comp α
            g =
          0 →
        ∃ β,
          CategoryTheory.CategoryStruct.comp
              β f =
            α) :
  ∃ h,
    CategoryTheory.Pretriangulated.Triangle.mk
        f.hom g.hom h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles

Something wrong, better idea? Suggest a change

12.2.3. stabilityFunctionOnPhase🔗

The central charge Z of a Bridgeland stability condition, restricted to \sigma-semistable objects of phase \varphi \in (0,1], defines a stability function on the abelian category \mathcal{P}(\varphi).

Construction: The Z_{\mathrm{obj}} field sends E \in \mathcal{P}(\varphi) to \sigma.Z([E]) via the inclusion \mathcal{P}(\varphi) \hookrightarrow \mathcal{C}. Additivity comes from K_0-additivity on short exact sequences lifted through \texttt{P\_phi\_shortExact\_triangle}. The upper half-plane condition uses the compatibility axiom Z(E) = m \cdot e^{i\pi\varphi} with m > 0.

🔗def
CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnPhase.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (σ : CategoryTheory.Triangulated.StabilityCondition C) {φ : ℝ}
  (hφ : φ ∈ Set.Ioc 0 1) :
  CategoryTheory.StabilityFunction (σ.slicing.P φ).FullSubcategory
CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnPhase.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition
      C)
  {φ : ℝ} (hφ : φ ∈ Set.Ioc 0 1) :
  CategoryTheory.StabilityFunction
    (σ.slicing.P φ).FullSubcategory

Something wrong, better idea? Suggest a change

12.2.4. phase_eq_of_mem_P_phi🔗

For E \in \mathcal{P}(\varphi) nonzero and \varphi \in (0,1], the stability-function phase of E on the slice equals \varphi.

Proof: The compatibility axiom gives Z(E) = m \, e^{i\pi\varphi} with m > 0. The argument of this complex number is \pi\varphi, so dividing by \pi recovers \varphi exactly.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.phase_eq_of_mem_P_phi.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (σ : CategoryTheory.Triangulated.StabilityCondition C) {φ : ℝ}
  (hφ : φ ∈ Set.Ioc 0 1) (E : (σ.slicing.P φ).FullSubcategory)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  (CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnPhase
          C σ hφ).phase
      E =
    φ
CategoryTheory.Triangulated.StabilityCondition.phase_eq_of_mem_P_phi.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition
      C)
  {φ : ℝ} (hφ : φ ∈ Set.Ioc 0 1)
  (E : (σ.slicing.P φ).FullSubcategory)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  (CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnPhase
          C σ hφ).phase
      E =
    φ

Something wrong, better idea? Suggest a change

12.2.5. stabilityFunctionOnPhase_hasHN🔗

For \varphi \in (0,1], every nonzero object of \mathcal{P}(\varphi) admits a Harder--Narasimhan filtration with respect to the restricted stability function.

Proof: Every nonzero object of \mathcal{P}(\varphi) is already semistable of phase \varphi, so the HN filtration is trivial (a single factor). Existence of semistable filtrations then follows from the general abelian-category HN existence theorem.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnPhase_hasHN.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (σ : CategoryTheory.Triangulated.StabilityCondition C) {φ : ℝ}
  (hφ : φ ∈ Set.Ioc 0 1) :
  (CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnPhase
      C σ hφ).HasHNProperty
CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnPhase_hasHN.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition
      C)
  {φ : ℝ} (hφ : φ ∈ Set.Ioc 0 1) :
  (CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnPhase
      C σ hφ).HasHNProperty

Something wrong, better idea? Suggest a change

12.2.6. HeartStabilityData🔗

A heart stability datum bundles a bounded t-structure on a triangulated category \mathcal{C} with a stability function on its abelian heart that has the Harder--Narasimhan property. This is one side of the equivalence in Bridgeland's Proposition 5.3.

Construction: Fields: a t-structure t, a proof that t is bounded, a stability function Z on t.\mathrm{heart}.\mathrm{FullSubcategory} (which is abelian via \texttt{heartFullSubcategoryAbelian}), and a proof that Z satisfies the HN property.

🔗structure
CategoryTheory.Triangulated.HeartStabilityData.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] :
  Type u
CategoryTheory.Triangulated.HeartStabilityData.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C] :
  Type u

Constructor

CategoryTheory.Triangulated.HeartStabilityData.mk.{v, u}

Fields

t : CategoryTheory.Triangulated.TStructure C

The t-structure on C.

bounded : self.t.IsBounded

The t-structure is bounded.

Z : CategoryTheory.StabilityFunction self.t.heart.FullSubcategory

The stability function on the heart.

hasHN : self.Z.HasHNProperty

The stability function has the HN property.

Something wrong, better idea? Suggest a change

12.2.7. instHeartFullSubcategoryAbelian🔗

The heart of the t-structure in a heart stability datum is an abelian category.

Proof: Delegates to the general result \texttt{heartFullSubcategoryAbelian} applied to the t-structure field.

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

Something wrong, better idea? Suggest a change

12.2.8. heartPresentation🔗

The K_0-presentation for the heart of a bounded t-structure: generators are heart objects and relations are short exact sequences in the heart.

Construction: An abbreviation packaging the three projection functions \mathrm{obj}_1, \mathrm{obj}_2, \mathrm{obj}_3 from the set of short exact short complexes in the heart into the \texttt{K0Presentation} API.

🔗def
CategoryTheory.Triangulated.heartPresentation.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) :
  K0Presentation h.t.heart.FullSubcategory { S // S.ShortExact }
CategoryTheory.Triangulated.heartPresentation.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C) :
  K0Presentation h.t.heart.FullSubcategory
    { S // S.ShortExact }

Something wrong, better idea? Suggest a change

12.2.9. HeartK0🔗

The Grothendieck group K_0(\operatorname{heart}(t)) of the heart of a bounded t-structure, presented by short exact sequence relations.

Construction: Defined as the quotient of the free abelian group on heart objects by the subgroup generated by [B] - [A] - [C] for every short exact sequence 0 \to A \to B \to C \to 0 in the heart.

🔗def
CategoryTheory.Triangulated.HeartK0.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) : Type u
CategoryTheory.Triangulated.HeartK0.{v, u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C) :
  Type u

Something wrong, better idea? Suggest a change

12.2.10. instAddCommGroup🔗

The Grothendieck group of the heart carries a natural abelian group structure.

Proof: Inherited from the quotient construction in \texttt{K0Presentation.K0}.

🔗def
CategoryTheory.Triangulated.HeartK0.instAddCommGroup.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) :
  AddCommGroup (CategoryTheory.Triangulated.HeartK0 C h)
CategoryTheory.Triangulated.HeartK0.instAddCommGroup.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C) :
  AddCommGroup
    (CategoryTheory.Triangulated.HeartK0 C
      h)

Something wrong, better idea? Suggest a change

12.2.11. of🔗

The class [E] \in K_0(\operatorname{heart}(t)) of a heart object E.

Construction: The image of the free-abelian-group generator \langle E \rangle under the quotient map.

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

Something wrong, better idea? Suggest a change

12.2.12. heartPresentation_of🔗

The \texttt{K0Presentation.of} map agrees with \texttt{HeartK0.of}.

Proof: Immediate by definition.

🔗theorem
CategoryTheory.Triangulated.HeartK0.heartPresentation_of.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) :
  (CategoryTheory.Triangulated.heartPresentation C h).of E =
    CategoryTheory.Triangulated.HeartK0.of C h E
CategoryTheory.Triangulated.HeartK0.heartPresentation_of.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) :
  (CategoryTheory.Triangulated.heartPresentation
          C h).of
      E =
    CategoryTheory.Triangulated.HeartK0.of
      C h E

Something wrong, better idea? Suggest a change

12.2.13. hom_ext🔗

Two group homomorphisms from K_0(\operatorname{heart}) that agree on all object classes [E] are equal.

Proof: Since object classes generate, the universal property of the quotient forces equality.

🔗theorem
CategoryTheory.Triangulated.HeartK0.hom_ext.{v, u, u_1} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) {A : Type u_1}
  [AddCommGroup A] {f g : CategoryTheory.Triangulated.HeartK0 C h →+ A}
  (hfg :
    ∀ (E : h.t.heart.FullSubcategory),
      f (CategoryTheory.Triangulated.HeartK0.of C h E) =
        g (CategoryTheory.Triangulated.HeartK0.of C h E)) :
  f = g
CategoryTheory.Triangulated.HeartK0.hom_ext.{v,
    u, u_1}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {A : Type u_1} [AddCommGroup A]
  {f g :
    CategoryTheory.Triangulated.HeartK0 C
        h →+
      A}
  (hfg :
    ∀ (E : h.t.heart.FullSubcategory),
      f
          (CategoryTheory.Triangulated.HeartK0.of
            C h E) =
        g
          (CategoryTheory.Triangulated.HeartK0.of
            C h E)) :
  f = g

Something wrong, better idea? Suggest a change

12.2.14. hom_ext_iff🔗

Two group homomorphisms from K_0(\operatorname{heart}) are equal if and only if they agree on all object classes.

Proof: Follows from the extensionality criterion \texttt{hom\_ext} by splitting the biconditional.

🔗theorem
CategoryTheory.Triangulated.HeartK0.hom_ext_iff.{v, u, u_1} {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {h : CategoryTheory.Triangulated.HeartStabilityData C} {A : Type u_1}
  [AddCommGroup A]
  {f g : CategoryTheory.Triangulated.HeartK0 C h →+ A} :
  f = g ↔
    ∀ (E : h.t.heart.FullSubcategory),
      f (CategoryTheory.Triangulated.HeartK0.of C h E) =
        g (CategoryTheory.Triangulated.HeartK0.of C h E)
CategoryTheory.Triangulated.HeartK0.hom_ext_iff.{v,
    u, u_1}
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {h :
    CategoryTheory.Triangulated.HeartStabilityData
      C}
  {A : Type u_1} [AddCommGroup A]
  {f g :
    CategoryTheory.Triangulated.HeartK0 C
        h →+
      A} :
  f = g ↔
    ∀ (E : h.t.heart.FullSubcategory),
      f
          (CategoryTheory.Triangulated.HeartK0.of
            C h E) =
        g
          (CategoryTheory.Triangulated.HeartK0.of
            C h E)

Something wrong, better idea? Suggest a change

12.2.15. of_shortExact🔗

A short exact sequence 0 \to A \to B \to C \to 0 in the heart gives [B] = [A] + [C] in K_0(\operatorname{heart}).

Proof: This is the defining relation of the Grothendieck group presentation.

🔗theorem
CategoryTheory.Triangulated.HeartK0.of_shortExact.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  {S : CategoryTheory.ShortComplex h.t.heart.FullSubcategory}
  (hS : S.ShortExact) :
  CategoryTheory.Triangulated.HeartK0.of C h S.X₂ =
    CategoryTheory.Triangulated.HeartK0.of C h S.X₁ +
      CategoryTheory.Triangulated.HeartK0.of C h S.X₃
CategoryTheory.Triangulated.HeartK0.of_shortExact.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {S :
    CategoryTheory.ShortComplex
      h.t.heart.FullSubcategory}
  (hS : S.ShortExact) :
  CategoryTheory.Triangulated.HeartK0.of C
      h S.X₂ =
    CategoryTheory.Triangulated.HeartK0.of
        C h S.X₁ +
      CategoryTheory.Triangulated.HeartK0.of
        C h S.X₃

Something wrong, better idea? Suggest a change

12.2.16. of_exact🔗

For an exact sequence A \xrightarrow{f} B \xrightarrow{g} D in the heart, [B] = [\operatorname{im}(f)] + [\operatorname{im}(g)].

Proof: Factors through two short exact sequences: 0 \to \operatorname{im}(f) \to B \to \operatorname{im}(g) \to 0 (using exactness and the first isomorphism theorem) and then applies \texttt{of\_shortExact}.

🔗theorem
CategoryTheory.Triangulated.HeartK0.of_exact.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  {A B D : h.t.heart.FullSubcategory} {f : A ⟶ B} {g : B ⟶ D}
  [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasImage g]
  (w : CategoryTheory.CategoryStruct.comp f g = 0)
  (hex :
    { X₁ := A, X₂ := B, X₃ := D, f := f, g := g, zero := w }.Exact) :
  CategoryTheory.Triangulated.HeartK0.of C h B =
    CategoryTheory.Triangulated.HeartK0.of C h
        (CategoryTheory.Limits.image f) +
      CategoryTheory.Triangulated.HeartK0.of C h
        (CategoryTheory.Limits.image g)
CategoryTheory.Triangulated.HeartK0.of_exact.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {A B D : h.t.heart.FullSubcategory}
  {f : A ⟶ B} {g : B ⟶ D}
  [CategoryTheory.Limits.HasImage f]
  [CategoryTheory.Limits.HasImage g]
  (w :
    CategoryTheory.CategoryStruct.comp f
        g =
      0)
  (hex :
    { X₁ := A, X₂ := B, X₃ := D, f := f,
        g := g, zero := w }.Exact) :
  CategoryTheory.Triangulated.HeartK0.of C
      h B =
    CategoryTheory.Triangulated.HeartK0.of
        C h
        (CategoryTheory.Limits.image f) +
      CategoryTheory.Triangulated.HeartK0.of
        C h
        (CategoryTheory.Limits.image g)

Something wrong, better idea? Suggest a change

12.2.17. of_exact_five🔗

For a five-term exact sequence A_0 \to A_1 \to A_2 \to A_3 \to A_4 in the heart, [A_1] - [A_2] + [A_3] = [\operatorname{im}(f_0)] + [\operatorname{im}(f_3)].

Proof: Applies \texttt{of\_exact} to each consecutive pair and uses the abelian group relation to telescope.

🔗theorem
CategoryTheory.Triangulated.HeartK0.of_exact_five.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  {A₀ A₁ A₂ A₃ A₄ : h.t.heart.FullSubcategory} {f₀ : A₀ ⟶ A₁}
  {f₁ : A₁ ⟶ A₂} {f₂ : A₂ ⟶ A₃} {f₃ : A₃ ⟶ A₄}
  [CategoryTheory.Limits.HasImage f₀]
  [CategoryTheory.Limits.HasImage f₁]
  [CategoryTheory.Limits.HasImage f₂]
  [CategoryTheory.Limits.HasImage f₃]
  (w₀ : CategoryTheory.CategoryStruct.comp f₀ f₁ = 0)
  (w₁ : CategoryTheory.CategoryStruct.comp f₁ f₂ = 0)
  (w₂ : CategoryTheory.CategoryStruct.comp f₂ f₃ = 0)
  (hex₀ :
    { X₁ := A₀, X₂ := A₁, X₃ := A₂, f := f₀, g := f₁,
        zero := w₀ }.Exact)
  (hex₁ :
    { X₁ := A₁, X₂ := A₂, X₃ := A₃, f := f₁, g := f₂,
        zero := w₁ }.Exact)
  (hex₂ :
    { X₁ := A₂, X₂ := A₃, X₃ := A₄, f := f₂, g := f₃,
        zero := w₂ }.Exact) :
  CategoryTheory.Triangulated.HeartK0.of C h A₁ -
        CategoryTheory.Triangulated.HeartK0.of C h A₂ +
      CategoryTheory.Triangulated.HeartK0.of C h A₃ =
    CategoryTheory.Triangulated.HeartK0.of C h
        (CategoryTheory.Limits.image f₀) +
      CategoryTheory.Triangulated.HeartK0.of C h
        (CategoryTheory.Limits.image f₃)
CategoryTheory.Triangulated.HeartK0.of_exact_five.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {A₀ A₁ A₂ A₃ A₄ :
    h.t.heart.FullSubcategory}
  {f₀ : A₀ ⟶ A₁} {f₁ : A₁ ⟶ A₂}
  {f₂ : A₂ ⟶ A₃} {f₃ : A₃ ⟶ A₄}
  [CategoryTheory.Limits.HasImage f₀]
  [CategoryTheory.Limits.HasImage f₁]
  [CategoryTheory.Limits.HasImage f₂]
  [CategoryTheory.Limits.HasImage f₃]
  (w₀ :
    CategoryTheory.CategoryStruct.comp f₀
        f₁ =
      0)
  (w₁ :
    CategoryTheory.CategoryStruct.comp f₁
        f₂ =
      0)
  (w₂ :
    CategoryTheory.CategoryStruct.comp f₂
        f₃ =
      0)
  (hex₀ :
    { X₁ := A₀, X₂ := A₁, X₃ := A₂,
        f := f₀, g := f₁,
        zero := w₀ }.Exact)
  (hex₁ :
    { X₁ := A₁, X₂ := A₂, X₃ := A₃,
        f := f₁, g := f₂,
        zero := w₁ }.Exact)
  (hex₂ :
    { X₁ := A₂, X₂ := A₃, X₃ := A₄,
        f := f₂, g := f₃,
        zero := w₂ }.Exact) :
  CategoryTheory.Triangulated.HeartK0.of C
          h A₁ -
        CategoryTheory.Triangulated.HeartK0.of
          C h A₂ +
      CategoryTheory.Triangulated.HeartK0.of
        C h A₃ =
    CategoryTheory.Triangulated.HeartK0.of
        C h
        (CategoryTheory.Limits.image f₀) +
      CategoryTheory.Triangulated.HeartK0.of
        C h
        (CategoryTheory.Limits.image f₃)

Something wrong, better idea? Suggest a change

12.2.18. of_isZero🔗

The class of a zero object in the heart vanishes: [0] = 0 in K_0(\operatorname{heart}).

Proof: Constructs a degenerate short exact sequence 0 \to 0 \to E \to 0 and applies the defining relation.

🔗theorem
CategoryTheory.Triangulated.HeartK0.of_isZero.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  {E : h.t.heart.FullSubcategory}
  (hE : CategoryTheory.Limits.IsZero E) :
  CategoryTheory.Triangulated.HeartK0.of C h E = 0
CategoryTheory.Triangulated.HeartK0.of_isZero.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {E : h.t.heart.FullSubcategory}
  (hE : CategoryTheory.Limits.IsZero E) :
  CategoryTheory.Triangulated.HeartK0.of C
      h E =
    0

Something wrong, better idea? Suggest a change

12.2.19. of_zero🔗

The class of the explicit zero object vanishes in K_0(\operatorname{heart}).

Proof: Special case of \texttt{of\_isZero} applied to \texttt{isZero\_zero}.

🔗theorem
CategoryTheory.Triangulated.HeartK0.of_zero.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) :
  CategoryTheory.Triangulated.HeartK0.of C h 0 = 0
CategoryTheory.Triangulated.HeartK0.of_zero.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C) :
  CategoryTheory.Triangulated.HeartK0.of C
      h 0 =
    0

Something wrong, better idea? Suggest a change

12.2.20. of_iso🔗

Isomorphic heart objects have equal classes in K_0(\operatorname{heart}).

Proof: Constructs a short exact sequence from the isomorphism with trivial cokernel, then reads off the relation.

🔗theorem
CategoryTheory.Triangulated.HeartK0.of_iso.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  {E F : h.t.heart.FullSubcategory} (e : E ≅ F) :
  CategoryTheory.Triangulated.HeartK0.of C h E =
    CategoryTheory.Triangulated.HeartK0.of C h F
CategoryTheory.Triangulated.HeartK0.of_iso.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {E F : h.t.heart.FullSubcategory}
  (e : E ≅ F) :
  CategoryTheory.Triangulated.HeartK0.of C
      h E =
    CategoryTheory.Triangulated.HeartK0.of
      C h F

Something wrong, better idea? Suggest a change

12.2.21. of_image_eq_zero🔗

The K_0-class of the image of a zero morphism vanishes.

Proof: The image of the zero map is isomorphic to the zero object, so [\operatorname{im}(0)] = [0] = 0 by \texttt{of\_iso} and \texttt{of\_zero}.

🔗theorem
CategoryTheory.Triangulated.HeartK0.of_image_eq_zero.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  {A B : h.t.heart.FullSubcategory} {f : A ⟶ B}
  [CategoryTheory.Limits.HasImage f] (hf : f = 0) :
  CategoryTheory.Triangulated.HeartK0.of C h
      (CategoryTheory.Limits.image f) =
    0
CategoryTheory.Triangulated.HeartK0.of_image_eq_zero.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {A B : h.t.heart.FullSubcategory}
  {f : A ⟶ B}
  [CategoryTheory.Limits.HasImage f]
  (hf : f = 0) :
  CategoryTheory.Triangulated.HeartK0.of C
      h (CategoryTheory.Limits.image f) =
    0

Something wrong, better idea? Suggest a change

12.2.22. heartZObj🔗

The object-level central charge Z(E) for a heart object E, viewed as a plain function \operatorname{heart}(t) \to \mathbb{C}.

Construction: Unwraps the \texttt{StabilityFunction.Zobj} field from the heart stability datum, making the abelian instance explicit.

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

Something wrong, better idea? Suggest a change

12.2.23. ZOnHeartK0🔗

The heart stability function Z descends to a group homomorphism K_0(\operatorname{heart}(t)) \to \mathbb{C}.

Construction: Lifts Z_{\mathrm{obj}} through the free abelian group, then checks that the short-exact-sequence relations map to zero by additivity of Z.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) :
  CategoryTheory.Triangulated.HeartK0 C h →+ ℂ
CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C) :
  CategoryTheory.Triangulated.HeartK0 C
      h →+
    ℂ

Something wrong, better idea? Suggest a change

12.2.24. ZOnHeartK0_of🔗

Z_{K_0}([E]) = Z(E) for every heart object E.

Proof: Immediate from the lifting construction.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0_of.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) :
  (CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0 C h)
      (CategoryTheory.Triangulated.HeartK0.of C h E) =
    CategoryTheory.Triangulated.HeartStabilityData.heartZObj C h E
CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0_of.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) :
  (CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0
        C h)
      (CategoryTheory.Triangulated.HeartK0.of
        C h E) =
    CategoryTheory.Triangulated.HeartStabilityData.heartZObj
      C h E

Something wrong, better idea? Suggest a change

12.2.25. heartFullSubcategory_shortExact_triangle🔗

A short exact sequence 0 \to A \to B \to Q \to 0 in the heart of a t-structure lifts to a distinguished triangle A \to B \to Q \to A[1] in the ambient triangulated category.

Proof: Uses the admissibility of the heart as a full abelian subcategory: a short exact sequence yields a cofiber sequence via the triangulated-abelian-subcategory machinery, then the kernel--cokernel pair is identified with the given mono--epi pair by uniqueness.

🔗theorem
CategoryTheory.Triangulated.TStructure.heartFullSubcategory_shortExact_triangle.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C)
  {A B Q : t.heart.FullSubcategory} (f : A ⟶ B) (g : B ⟶ Q)
  (hfg : CategoryTheory.CategoryStruct.comp f g = 0)
  [CategoryTheory.Mono f] [CategoryTheory.Epi g]
  (hexact :
    ∀ {W : t.heart.FullSubcategory} (α : W ⟶ B),
      CategoryTheory.CategoryStruct.comp α g = 0 →
        ∃ β, CategoryTheory.CategoryStruct.comp β f = α) :
  ∃ h,
    CategoryTheory.Pretriangulated.Triangle.mk f.hom g.hom h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles
CategoryTheory.Triangulated.TStructure.heartFullSubcategory_shortExact_triangle.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t :
    CategoryTheory.Triangulated.TStructure
      C)
  {A B Q : t.heart.FullSubcategory}
  (f : A ⟶ B) (g : B ⟶ Q)
  (hfg :
    CategoryTheory.CategoryStruct.comp f
        g =
      0)
  [CategoryTheory.Mono f]
  [CategoryTheory.Epi g]
  (hexact :
    ∀ {W : t.heart.FullSubcategory}
      (α : W ⟶ B),
      CategoryTheory.CategoryStruct.comp α
            g =
          0 →
        ∃ β,
          CategoryTheory.CategoryStruct.comp
              β f =
            α) :
  ∃ h,
    CategoryTheory.Pretriangulated.Triangle.mk
        f.hom g.hom h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles

Something wrong, better idea? Suggest a change

12.2.26. heartFullSubcategory_shortExact_of_distTriang🔗

A distinguished triangle whose three vertices lie in the heart induces a short exact sequence in the heart abelian category.

Proof: Applies the kernel and cokernel fork constructions from the triangulated-abelian-subcategory API to the given triangle, verifying monicity of the first map and epicity of the second.

🔗theorem
CategoryTheory.Triangulated.TStructure.heartFullSubcategory_shortExact_of_distTriang.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C)
  {A B Q : t.heart.FullSubcategory} {f : A ⟶ B} {g : B ⟶ Q}
  {δ : Q.obj ⟶ (CategoryTheory.shiftFunctor C 1).obj A.obj}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f.hom g.hom δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  { X₁ := A, X₂ := B, X₃ := Q, f := f, g := g, zero := ⋯ }.ShortExact
CategoryTheory.Triangulated.TStructure.heartFullSubcategory_shortExact_of_distTriang.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (t :
    CategoryTheory.Triangulated.TStructure
      C)
  {A B Q : t.heart.FullSubcategory}
  {f : A ⟶ B} {g : B ⟶ Q}
  {δ :
    Q.obj ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        A.obj}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f.hom g.hom δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  { X₁ := A, X₂ := B, X₃ := Q, f := f,
      g := g, zero := ⋯ }.ShortExact

Something wrong, better idea? Suggest a change

12.2.27. heartK0ToK0🔗

The canonical group homomorphism K_0(\operatorname{heart}(t)) \to K_0(\mathcal{C}) sending [E] to the class of its underlying object.

Construction: Lifts the function E \mapsto [E_{\mathrm{obj}}] through the quotient, using the fact that short exact sequences in the heart lift to distinguished triangles and thus satisfy the ambient K_0 relation.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  [CategoryTheory.IsTriangulated C] :
  CategoryTheory.Triangulated.HeartK0 C h →+
    CategoryTheory.Triangulated.K₀ C
CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  [CategoryTheory.IsTriangulated C] :
  CategoryTheory.Triangulated.HeartK0 C
      h →+
    CategoryTheory.Triangulated.K₀ C

Something wrong, better idea? Suggest a change

12.2.28. heartK0ToK0_of🔗

\operatorname{heartK0ToK0}([E]) = [E_{\mathrm{obj}}] in K_0(\mathcal{C}).

Proof: Immediate from the lifting construction.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0_of.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  [CategoryTheory.IsTriangulated C] (E : h.t.heart.FullSubcategory) :
  (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0 C h)
      (CategoryTheory.Triangulated.HeartK0.of C h E) =
    CategoryTheory.Triangulated.K₀.of C E.obj
CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0_of.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  [CategoryTheory.IsTriangulated C]
  (E : h.t.heart.FullSubcategory) :
  (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0
        C h)
      (CategoryTheory.Triangulated.HeartK0.of
        C h E) =
    CategoryTheory.Triangulated.K₀.of C
      E.obj

Something wrong, better idea? Suggest a change

12.2.29. of_shift_nat🔗

Shifting by a natural number n multiplies the Grothendieck-group class by (-1)^n: [X[n]] = (-1)^n [X].

Proof: Induction on n: the base case is the shift-by-zero identity, and the inductive step uses [X[1]] = -[X].

🔗theorem
CategoryTheory.Triangulated.K₀.of_shift_nat.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] (X : C) (n : ℕ) :
  CategoryTheory.Triangulated.K₀.of C
      ((CategoryTheory.shiftFunctor C ↑n).obj X) =
    (-1) ^ n • CategoryTheory.Triangulated.K₀.of C X
CategoryTheory.Triangulated.K₀.of_shift_nat.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (X : C) (n : ℕ) :
  CategoryTheory.Triangulated.K₀.of C
      ((CategoryTheory.shiftFunctor C
            ↑n).obj
        X) =
    (-1) ^ n •
      CategoryTheory.Triangulated.K₀.of C
        X

Something wrong, better idea? Suggest a change

12.2.30. of_shift_negSucc🔗

Shifting by -(n+1) multiplies the Grothendieck-group class by (-1)^{n+1}: [X[-(n+1)]] = (-1)^{n+1}[X].

Proof: Induction on n: uses [X[-1]] = -[X] and the inductive step for the negative direction.

🔗theorem
CategoryTheory.Triangulated.K₀.of_shift_negSucc.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] (X : C) (n : ℕ) :
  CategoryTheory.Triangulated.K₀.of C
      ((CategoryTheory.shiftFunctor C (Int.negSucc n)).obj X) =
    (-1) ^ (n + 1) • CategoryTheory.Triangulated.K₀.of C X
CategoryTheory.Triangulated.K₀.of_shift_negSucc.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (X : C) (n : ℕ) :
  CategoryTheory.Triangulated.K₀.of C
      ((CategoryTheory.shiftFunctor C
            (Int.negSucc n)).obj
        X) =
    (-1) ^ (n + 1) •
      CategoryTheory.Triangulated.K₀.of C
        X

Something wrong, better idea? Suggest a change

12.2.31. of_shift_int🔗

Shifting by n \in \mathbb{Z} multiplies the Grothendieck-group class by the parity sign: [X[n]] = (-1)^{|n|} \cdot [X] in K_0(\mathcal{C}).

Proof: By induction on n (natural and negative separately), each step uses [X[1]] = -[X] from the distinguished triangle X \to 0 \to X[1].

🔗theorem
CategoryTheory.Triangulated.K₀.of_shift_int.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] (X : C) (n : ℤ) :
  CategoryTheory.Triangulated.K₀.of C
      ((CategoryTheory.shiftFunctor C n).obj X) =
    (-1) ^ n.natAbs • CategoryTheory.Triangulated.K₀.of C X
CategoryTheory.Triangulated.K₀.of_shift_int.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (X : C) (n : ℤ) :
  CategoryTheory.Triangulated.K₀.of C
      ((CategoryTheory.shiftFunctor C
            n).obj
        X) =
    (-1) ^ n.natAbs •
      CategoryTheory.Triangulated.K₀.of C
        X

Something wrong, better idea? Suggest a change

12.2.32. heartShiftOfPure🔗

If X is concentrated in t-degree n (i.e. X \in \mathcal{C}^{\le n} \cap \mathcal{C}^{\ge n}), then X[n] lies in the heart.

Construction: Returns \langle X[n], \text{proof} \rangle where the proof that X[n] \in \operatorname{heart}(t) follows from shifting the amplitude bounds by n.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.heartShiftOfPure.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) {X : C} (n : ℤ)
  (hLE : h.t.IsLE X n) (hGE : h.t.IsGE X n) : h.t.heart.FullSubcategory
CategoryTheory.Triangulated.HeartStabilityData.heartShiftOfPure.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {X : C} (n : ℤ) (hLE : h.t.IsLE X n)
  (hGE : h.t.IsGE X n) :
  h.t.heart.FullSubcategory

Something wrong, better idea? Suggest a change

12.2.33. exists_preimage_of_pure🔗

A t-pure object of degree n has a preimage under the canonical map K_0(\operatorname{heart}) \to K_0(\mathcal{C}).

Proof: The preimage is (-1)^{|n|} \cdot [X[n]] where X[n] is the heart shift. The K_0-shift-parity formula verifies the identity.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.exists_preimage_of_pure.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  [CategoryTheory.IsTriangulated C] {X : C} (n : ℤ) (hLE : h.t.IsLE X n)
  (hGE : h.t.IsGE X n) :
  ∃ x,
    (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0 C h) x =
      CategoryTheory.Triangulated.K₀.of C X
CategoryTheory.Triangulated.HeartStabilityData.exists_preimage_of_pure.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  [CategoryTheory.IsTriangulated C]
  {X : C} (n : ℤ) (hLE : h.t.IsLE X n)
  (hGE : h.t.IsGE X n) :
  ∃ x,
    (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0
          C h)
        x =
      CategoryTheory.Triangulated.K₀.of C
        X

Something wrong, better idea? Suggest a change

12.2.34. exists_preimage_of_width🔗

Every object of bounded amplitude [b, b+n] has a preimage in K_0(\operatorname{heart}) under the canonical map.

Proof: Induction on the width n: the base case is a pure object, the inductive step splits via the truncation triangle \tau^{<b+n+1} E \to E \to \tau^{\ge b+n+1} E and assembles the two preimages.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.exists_preimage_of_width.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  [CategoryTheory.IsTriangulated C] (b : ℤ) (n : ℕ) {E : C} :
  h.t.IsLE E (b + ↑n) →
    h.t.IsGE E b →
      ∃ x,
        (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0 C h)
            x =
          CategoryTheory.Triangulated.K₀.of C E
CategoryTheory.Triangulated.HeartStabilityData.exists_preimage_of_width.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  [CategoryTheory.IsTriangulated C]
  (b : ℤ) (n : ℕ) {E : C} :
  h.t.IsLE E (b + ↑n) →
    h.t.IsGE E b →
      ∃ x,
        (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0
              C h)
            x =
          CategoryTheory.Triangulated.K₀.of
            C E

Something wrong, better idea? Suggest a change

12.2.35. heartK0ToK0_surjective🔗

The canonical map K_0(\operatorname{heart}(t)) \to K_0(\mathcal{C}) is surjective for a bounded t-structure.

Proof: Every generator [E] of K_0(\mathcal{C}) has a preimage by \texttt{exists\_preimage\_of\_width} applied to the bounded amplitude of E. The result extends to the full quotient by the universal property.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0_surjective.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  [CategoryTheory.IsTriangulated C] :
  Function.Surjective
    ⇑(CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0 C h)
CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0_surjective.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  [CategoryTheory.IsTriangulated C] :
  Function.Surjective
    ⇑(CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0
        C h)

Something wrong, better idea? Suggest a change