Bridgeland Stability Conditions

12.1. HeartEquivalence: AmplitudeFormulas🔗

12.1.1. triangleLTGE_iso_of_amp_negOne_zero🔗

For an object X of amplitude (-1, 0) presented by a distinguished triangle K[1] \to X \to Q \to K[2] with K, Q in the heart, the canonical truncation triangle \tau^{<0} X \to X \to \tau^{\ge 0} X is isomorphic to this triangle via a triangle isomorphism fixing X.

Proof: The amplitude hypothesis forces K[1] \in \mathcal{C}^{\le -1} and Q \in \mathcal{C}^{\ge 0}, so the given triangle satisfies the universal property of the truncation triangle. Uniqueness yields the isomorphism.

🔗theorem
CategoryTheory.Triangulated.TStructure.triangleLTGE_iso_of_amp_negOne_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]
  (t : CategoryTheory.Triangulated.TStructure C) {X K Q : C}
  (hK : t.heart K) (hQ : t.heart Q)
  {α : (CategoryTheory.shiftFunctor C 1).obj K ⟶ X} {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C 1).obj
        ((CategoryTheory.shiftFunctor C 1).obj K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  ∃ e, e.hom.hom₂ = CategoryTheory.CategoryStruct.id X
CategoryTheory.Triangulated.TStructure.triangleLTGE_iso_of_amp_negOne_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]
  (t :
    CategoryTheory.Triangulated.TStructure
      C)
  {X K Q : C} (hK : t.heart K)
  (hQ : t.heart Q)
  {α :
    (CategoryTheory.shiftFunctor C 1).obj
        K ⟶
      X}
  {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        ((CategoryTheory.shiftFunctor C
              1).obj
          K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  ∃ e,
    e.hom.hom₂ =
      CategoryTheory.CategoryStruct.id X

Something wrong, better idea? Suggest a change

12.1.2. heartCoh_negOne_iso_of_amp_negOne_zero🔗

For an object of amplitude (-1, 0) presented by a triangle K[1] \to X \to Q \to K[2] with K, Q in the heart, the (-1)-st heart cohomology of X is canonically isomorphic to K.

Construction: Chains three isomorphisms: (1) \tau^{[-1,-1]} X \cong \tau^{[-1,0)} X via the truncation comparison, (2) \tau^{[-1,0)} X \cong \tau^{<0} X since X \in \mathcal{C}^{\ge -1}, (3) \tau^{<0} X \cong K[1] from the triangle isomorphism. Shifting by -1 recovers K.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.heartCoh_negOne_iso_of_amp_negOne_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.IsTriangulated C] {X K Q : C} (hK : h.t.heart K)
  (hQ : h.t.heart Q) {α : (CategoryTheory.shiftFunctor C 1).obj K ⟶ X}
  {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C 1).obj
        ((CategoryTheory.shiftFunctor C 1).obj K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  [h.t.IsGE X (-1)] :
  CategoryTheory.Triangulated.HeartStabilityData.heartCoh C h (-1) X ≅
    { obj := K, property := hK }
CategoryTheory.Triangulated.HeartStabilityData.heartCoh_negOne_iso_of_amp_negOne_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.IsTriangulated C]
  {X K Q : C} (hK : h.t.heart K)
  (hQ : h.t.heart Q)
  {α :
    (CategoryTheory.shiftFunctor C 1).obj
        K ⟶
      X}
  {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        ((CategoryTheory.shiftFunctor C
              1).obj
          K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  [h.t.IsGE X (-1)] :
  CategoryTheory.Triangulated.HeartStabilityData.heartCoh
      C h (-1) X ≅
    { obj := K, property := hK }

Something wrong, better idea? Suggest a change

12.1.3. heartCoh_zero_iso_of_amp_negOne_zero🔗

For an object of amplitude (-1, 0) presented by a triangle K[1] \to X \to Q \to K[2] with K, Q in the heart, the 0-th heart cohomology of X is canonically isomorphic to Q.

Construction: Chains isomorphisms: \tau^{[0,0]} X \cong \tau^{\ge 0} X since X \in \mathcal{C}^{\le 0}, then \tau^{\ge 0} X \cong Q from the triangle isomorphism.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.heartCoh_zero_iso_of_amp_negOne_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.IsTriangulated C] {X K Q : C} (hK : h.t.heart K)
  (hQ : h.t.heart Q) {α : (CategoryTheory.shiftFunctor C 1).obj K ⟶ X}
  {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C 1).obj
        ((CategoryTheory.shiftFunctor C 1).obj K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  [h.t.IsLE X 0] :
  CategoryTheory.Triangulated.HeartStabilityData.heartCoh C h 0 X ≅
    { obj := Q, property := hQ }
CategoryTheory.Triangulated.HeartStabilityData.heartCoh_zero_iso_of_amp_negOne_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.IsTriangulated C]
  {X K Q : C} (hK : h.t.heart K)
  (hQ : h.t.heart Q)
  {α :
    (CategoryTheory.shiftFunctor C 1).obj
        K ⟶
      X}
  {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        ((CategoryTheory.shiftFunctor C
              1).obj
          K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  [h.t.IsLE X 0] :
  CategoryTheory.Triangulated.HeartStabilityData.heartCoh
      C h 0 X ≅
    { obj := Q, property := hQ }

Something wrong, better idea? Suggest a change

12.1.4. heartCohClassSum_of_amp_negOne_zero🔗

For X of amplitude (-1, 0) in a triangle K[1] \to X \to Q \to K[2], \sum_{j=-1}^{0} (-1)^{|j|} [H^j_t(X)] = -[K] + [Q] in K_0(\operatorname{heart}).

Proof: Evaluates the two-term sum using the cohomology isomorphisms H^{-1}_t(X) \cong K and H^0_t(X) \cong Q.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_of_amp_negOne_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.IsTriangulated C] {X K Q : C} (hK : h.t.heart K)
  (hQ : h.t.heart Q) {α : (CategoryTheory.shiftFunctor C 1).obj K ⟶ X}
  {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C 1).obj
        ((CategoryTheory.shiftFunctor C 1).obj K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  [h.t.IsLE X 0] [h.t.IsGE X (-1)] :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h
      (-1) 1 X =
    -CategoryTheory.Triangulated.HeartK0.of C h
          { obj := K, property := hK } +
      CategoryTheory.Triangulated.HeartK0.of C h
        { obj := Q, property := hQ }
CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_of_amp_negOne_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.IsTriangulated C]
  {X K Q : C} (hK : h.t.heart K)
  (hQ : h.t.heart Q)
  {α :
    (CategoryTheory.shiftFunctor C 1).obj
        K ⟶
      X}
  {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        ((CategoryTheory.shiftFunctor C
              1).obj
          K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  [h.t.IsLE X 0] [h.t.IsGE X (-1)] :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h (-1) 1 X =
    -CategoryTheory.Triangulated.HeartK0.of
          C h
          { obj := K, property := hK } +
      CategoryTheory.Triangulated.HeartK0.of
        C h { obj := Q, property := hQ }

Something wrong, better idea? Suggest a change

12.1.5. ZOnHeartK0_heartCohClassSum_of_amp_negOne_zero🔗

For X of amplitude (-1, 0), Z_{K_0}(\sum (-1)^{|j|} [H^j_t(X)]) = -Z(K) + Z(Q).

Proof: Applies the group homomorphism Z_{K_0} to \texttt{heartCohClassSum\_of\_amp\_negOne\_zero}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0_heartCohClassSum_of_amp_negOne_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.IsTriangulated C] {X K Q : C} (hK : h.t.heart K)
  (hQ : h.t.heart Q) {α : (CategoryTheory.shiftFunctor C 1).obj K ⟶ X}
  {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C 1).obj
        ((CategoryTheory.shiftFunctor C 1).obj K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  [h.t.IsLE X 0] [h.t.IsGE X (-1)] :
  (CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0 C h)
      (CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C
        h (-1) 1 X) =
    -CategoryTheory.Triangulated.HeartStabilityData.heartZObj C h
          { obj := K, property := hK } +
      CategoryTheory.Triangulated.HeartStabilityData.heartZObj C h
        { obj := Q, property := hQ }
CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0_heartCohClassSum_of_amp_negOne_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.IsTriangulated C]
  {X K Q : C} (hK : h.t.heart K)
  (hQ : h.t.heart Q)
  {α :
    (CategoryTheory.shiftFunctor C 1).obj
        K ⟶
      X}
  {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        ((CategoryTheory.shiftFunctor C
              1).obj
          K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  [h.t.IsLE X 0] [h.t.IsGE X (-1)] :
  (CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0
        C h)
      (CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
        C h (-1) 1 X) =
    -CategoryTheory.Triangulated.HeartStabilityData.heartZObj
          C h
          { obj := K, property := hK } +
      CategoryTheory.Triangulated.HeartStabilityData.heartZObj
        C h { obj := Q, property := hQ }

Something wrong, better idea? Suggest a change

12.1.6. heartEulerClassObj_of_amp_negOne_zero🔗

For X of amplitude (-1, 0), \texttt{heartEulerClassObj}(X) = -[K] + [Q].

Proof: Identifies the Euler class with the heart cohomology class sum via \texttt{heartEulerClassObj\_eq\_heartCohClassSum}, then applies the amplitude formula.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_of_amp_negOne_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.IsTriangulated C] {X K Q : C} (hK : h.t.heart K)
  (hQ : h.t.heart Q) {α : (CategoryTheory.shiftFunctor C 1).obj K ⟶ X}
  {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C 1).obj
        ((CategoryTheory.shiftFunctor C 1).obj K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  [h.t.IsLE X 0] [h.t.IsGE X (-1)] :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C h
      X =
    -CategoryTheory.Triangulated.HeartK0.of C h
          { obj := K, property := hK } +
      CategoryTheory.Triangulated.HeartK0.of C h
        { obj := Q, property := hQ }
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_of_amp_negOne_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.IsTriangulated C]
  {X K Q : C} (hK : h.t.heart K)
  (hQ : h.t.heart Q)
  {α :
    (CategoryTheory.shiftFunctor C 1).obj
        K ⟶
      X}
  {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        ((CategoryTheory.shiftFunctor C
              1).obj
          K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  [h.t.IsLE X 0] [h.t.IsGE X (-1)] :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
      C h X =
    -CategoryTheory.Triangulated.HeartK0.of
          C h
          { obj := K, property := hK } +
      CategoryTheory.Triangulated.HeartK0.of
        C h { obj := Q, property := hQ }

Something wrong, better idea? Suggest a change

12.1.7. eulerZObj_of_amp_negOne_zero🔗

For X of amplitude (-1, 0), \texttt{eulerZObj}(X) = -Z(K) + Z(Q).

Proof: Composes \texttt{heartEulerClassObj\_of\_amp\_negOne\_zero} with Z_{K_0}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_of_amp_negOne_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.IsTriangulated C] {X K Q : C} (hK : h.t.heart K)
  (hQ : h.t.heart Q) {α : (CategoryTheory.shiftFunctor C 1).obj K ⟶ X}
  {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C 1).obj
        ((CategoryTheory.shiftFunctor C 1).obj K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  [h.t.IsLE X 0] [h.t.IsGE X (-1)] :
  CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h X =
    -CategoryTheory.Triangulated.HeartStabilityData.heartZObj C h
          { obj := K, property := hK } +
      CategoryTheory.Triangulated.HeartStabilityData.heartZObj C h
        { obj := Q, property := hQ }
CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_of_amp_negOne_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.IsTriangulated C]
  {X K Q : C} (hK : h.t.heart K)
  (hQ : h.t.heart Q)
  {α :
    (CategoryTheory.shiftFunctor C 1).obj
        K ⟶
      X}
  {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        ((CategoryTheory.shiftFunctor C
              1).obj
          K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  [h.t.IsLE X 0] [h.t.IsGE X (-1)] :
  CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
      C h X =
    -CategoryTheory.Triangulated.HeartStabilityData.heartZObj
          C h
          { obj := K, property := hK } +
      CategoryTheory.Triangulated.HeartStabilityData.heartZObj
        C h { obj := Q, property := hQ }

Something wrong, better idea? Suggest a change

12.1.8. heartEulerClassObj_triangle_of_amp_negOne_zero🔗

Triangle additivity of the Euler class for objects of amplitude (-1, 0): \texttt{heartEulerClassObj}(X) = \texttt{heartEulerClassObj}(K[1]) + \texttt{heartEulerClassObj}(Q).

Proof: Rewrites the Euler classes of K[1] and Q using the heart and heart-shift formulas, then matches with the amplitude formula.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_triangle_of_amp_negOne_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.IsTriangulated C] {X K Q : C} (hK : h.t.heart K)
  (hQ : h.t.heart Q) {α : (CategoryTheory.shiftFunctor C 1).obj K ⟶ X}
  {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C 1).obj
        ((CategoryTheory.shiftFunctor C 1).obj K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  [h.t.IsLE X 0] [h.t.IsGE X (-1)] :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C h
      X =
    CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C
        h ((CategoryTheory.shiftFunctor C 1).obj K) +
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h Q
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_triangle_of_amp_negOne_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.IsTriangulated C]
  {X K Q : C} (hK : h.t.heart K)
  (hQ : h.t.heart Q)
  {α :
    (CategoryTheory.shiftFunctor C 1).obj
        K ⟶
      X}
  {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        ((CategoryTheory.shiftFunctor C
              1).obj
          K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  [h.t.IsLE X 0] [h.t.IsGE X (-1)] :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
      C h X =
    CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h
        ((CategoryTheory.shiftFunctor C
              1).obj
          K) +
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h Q

Something wrong, better idea? Suggest a change

12.1.9. eulerZObj_triangle_of_amp_negOne_zero🔗

Triangle additivity of \texttt{eulerZObj} for objects of amplitude (-1, 0): \texttt{eulerZObj}(X) = \texttt{eulerZObj}(K[1]) + \texttt{eulerZObj}(Q).

Proof: Analogous to \texttt{heartEulerClassObj\_triangle\_of\_amp\_negOne\_zero}, applying Z_{K_0} throughout.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_triangle_of_amp_negOne_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.IsTriangulated C] {X K Q : C} (hK : h.t.heart K)
  (hQ : h.t.heart Q) {α : (CategoryTheory.shiftFunctor C 1).obj K ⟶ X}
  {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C 1).obj
        ((CategoryTheory.shiftFunctor C 1).obj K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  [h.t.IsLE X 0] [h.t.IsGE X (-1)] :
  CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h X =
    CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h
        ((CategoryTheory.shiftFunctor C 1).obj K) +
      CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h Q
CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_triangle_of_amp_negOne_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.IsTriangulated C]
  {X K Q : C} (hK : h.t.heart K)
  (hQ : h.t.heart Q)
  {α :
    (CategoryTheory.shiftFunctor C 1).obj
        K ⟶
      X}
  {β : X ⟶ Q}
  {γ :
    Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        ((CategoryTheory.shiftFunctor C
              1).obj
          K)}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        α β γ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  [h.t.IsLE X 0] [h.t.IsGE X (-1)] :
  CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
      C h X =
    CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
        C h
        ((CategoryTheory.shiftFunctor C
              1).obj
          K) +
      CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
        C h Q

Something wrong, better idea? Suggest a change

12.1.10. heartEulerClassObj_triangle_of_bounds🔗

Full bounded triangle additivity: for a distinguished triangle X_1 \to X_2 \to X_3 \to X_1[1] with compatible amplitude bounds, \texttt{heartEulerClassObj}(X_2) = \texttt{heartEulerClassObj}(X_1) + \texttt{heartEulerClassObj}(X_3).

Proof: Uses the five-term relation and a telescoping argument. The image terms vanish at the boundary degrees because the H^0 functor kills objects outside their amplitude range. The telescoping sum collapses by the standard Finset identity \sum_{j=0}^{m} (f(j) - f(j+1)) = f(0) - f(m+1).

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_triangle_of_bounds.{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.HeartStabilityData.H0Functor C
        h).IsHomological]
  (T : CategoryTheory.Pretriangulated.Triangle C)
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {b a : ℤ} (hab : b ≤ a) (h₁LE : h.t.IsLE T.obj₁ (a + 1))
  (h₁GE : h.t.IsGE T.obj₁ (b + 1)) (h₂LE : h.t.IsLE T.obj₂ a)
  (h₂GE : h.t.IsGE T.obj₂ b) (h₃LE : h.t.IsLE T.obj₃ a)
  (h₃GE : h.t.IsGE T.obj₃ b) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C h
      T.obj₂ =
    CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C
        h T.obj₁ +
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h T.obj₃
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_triangle_of_bounds.{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.HeartStabilityData.H0Functor
        C h).IsHomological]
  (T :
    CategoryTheory.Pretriangulated.Triangle
      C)
  (hT :
    T ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  {b a : ℤ} (hab : b ≤ a)
  (h₁LE : h.t.IsLE T.obj₁ (a + 1))
  (h₁GE : h.t.IsGE T.obj₁ (b + 1))
  (h₂LE : h.t.IsLE T.obj₂ a)
  (h₂GE : h.t.IsGE T.obj₂ b)
  (h₃LE : h.t.IsLE T.obj₃ a)
  (h₃GE : h.t.IsGE T.obj₃ b) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
      C h T.obj₂ =
    CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h T.obj₁ +
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h T.obj₃

Something wrong, better idea? Suggest a change

12.1.11. heartEulerClassObj_isTriangleAdditive🔗

The Euler class lift E \mapsto \texttt{heartEulerClassObj}(E) is additive on distinguished triangles (assuming H^0_t is homological).

Proof: For an arbitrary distinguished triangle, chooses compatible bounds containing the amplitude of all three vertices (shifted appropriately), then delegates to \texttt{heartEulerClassObj\_triangle\_of\_bounds}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_isTriangleAdditive.{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.HeartStabilityData.H0Functor C
        h).IsHomological] :
  CategoryTheory.Triangulated.IsTriangleAdditive fun E =>
    CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C
      h E
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_isTriangleAdditive.{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.HeartStabilityData.H0Functor
        C h).IsHomological] :
  CategoryTheory.Triangulated.IsTriangleAdditive
    fun E =>
    CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
      C h E

Something wrong, better idea? Suggest a change