12.7. HeartEquivalence: PureAdditivity🔗

12.7.1. heartCohClass_of_heart_shift🔗

For a heart object E and integer n, \texttt{heartCohClass}(n, E[-n]) = (-1)^{|n|} \cdot [E] in K_0(\operatorname{heart}).

Proof: The heart cohomology of a pure object concentrated in degree n is isomorphic to E itself after shifting back. The result follows from \texttt{heartCohObjIsoOfHeartShift}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_of_heart_shift.{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) (n : ℤ) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h n
      ((CategoryTheory.shiftFunctor C (-n)).obj E.obj) =
    (-1) ^ n.natAbs • CategoryTheory.Triangulated.HeartK0.of C h E
CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_of_heart_shift.{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)
  (n : ℤ) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
      C h n
      ((CategoryTheory.shiftFunctor C
            (-n)).obj
        E.obj) =
    (-1) ^ n.natAbs •
      CategoryTheory.Triangulated.HeartK0.of
        C h E

Something wrong, better idea? Suggest a change

12.7.2. heartCohIso_of_truncLT🔗

Truncating above degree a does not change the nth heart cohomology when n < a: H^n_t(\tau^{<a} E) \cong H^n_t(E).

Construction: The truncation map \tau^{<a} E \hookrightarrow E induces an isomorphism on \tau^{[n,n]} for n < a because \tau^{\le n} commutes with the inclusion.

def

CategoryTheory.Triangulated.HeartStabilityData.heartCohIso_of_truncLT.{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 : C) (n a : ℤ) (hna : n < a) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCoh C h n
      ((h.t.truncLT a).obj E) ≅
    CategoryTheory.Triangulated.HeartStabilityData.heartCoh C h n E
CategoryTheory.Triangulated.HeartStabilityData.heartCohIso_of_truncLT.{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 : C) (n a : ℤ) (hna : n < a) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCoh
      C h n ((h.t.truncLT a).obj E) ≅
    CategoryTheory.Triangulated.HeartStabilityData.heartCoh
      C h n E

Something wrong, better idea? Suggest a change

12.7.3. heartCohClass_of_truncLT🔗

For n < a, \texttt{heartCohClass}(n, \tau^{<a} E) = \texttt{heartCohClass}(n, E).

Proof: Follows from the isomorphism \texttt{heartCohIso\_of\_truncLT} and invariance of K_0-classes under isomorphism.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_of_truncLT.{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 : C) (n a : ℤ) (hna : n < a) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h n
      ((h.t.truncLT a).obj E) =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h n E
CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_of_truncLT.{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 : C) (n a : ℤ) (hna : n < a) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
      C h n ((h.t.truncLT a).obj E) =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
      C h n E

Something wrong, better idea? Suggest a change

12.7.4. heartEulerClassObj_of_heart🔗

For a heart object E, the Euler lift is [E] itself: \texttt{heartEulerClassObj}(E) = [E] \in K_0(\operatorname{heart}).

Proof: A heart object is concentrated in degree 0, so the alternating sum reduces to the single term [H^0_t(E)] = [E].

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_of_heart.{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.heartEulerClassObj C h
      E.obj =
    CategoryTheory.Triangulated.HeartK0.of C h E
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_of_heart.{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.heartEulerClassObj
      C h E.obj =
    CategoryTheory.Triangulated.HeartK0.of
      C h E

Something wrong, better idea? Suggest a change

12.7.5. eulerZObj🔗

The object-level central charge candidate: \texttt{eulerZObj}(E) = Z_{K_0}(\texttt{heartEulerClassObj}(E)) \in \mathbb{C}.

Construction: Composes the Euler class lift to K_0(\operatorname{heart}) with the descended heart central charge Z_{K_0}.

def

CategoryTheory.Triangulated.HeartStabilityData.eulerZObj.{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 : C) : ℂ
CategoryTheory.Triangulated.HeartStabilityData.eulerZObj.{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 : C) : ℂ

Something wrong, better idea? Suggest a change

12.7.6. eulerZObj_of_heart🔗

For a heart object E, \texttt{eulerZObj}(E) = Z(E).

Proof: Follows from \texttt{heartEulerClassObj\_of\_heart} and the definition of Z_{K_0}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_of_heart.{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.eulerZObj C h E.obj =
    CategoryTheory.Triangulated.HeartStabilityData.heartZObj C h E
CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_of_heart.{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.eulerZObj
      C h E.obj =
    CategoryTheory.Triangulated.HeartStabilityData.heartZObj
      C h E

Something wrong, better idea? Suggest a change

12.7.7. heartK0FromK0🔗

The canonical map K_0(\mathcal{C}) \to K_0(\operatorname{heart}) induced by the Euler-class lift, assuming triangle additivity.

Construction: Lifts E \mapsto \texttt{heartEulerClassObj}(E) through the universal property of K_0(\mathcal{C}).

def

CategoryTheory.Triangulated.HeartStabilityData.heartK0FromK0.{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.IsTriangleAdditive fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E] :
  CategoryTheory.Triangulated.K₀ C →+
    CategoryTheory.Triangulated.HeartK0 C h
CategoryTheory.Triangulated.HeartStabilityData.heartK0FromK0.{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.IsTriangleAdditive
      fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E] :
  CategoryTheory.Triangulated.K₀ C →+
    CategoryTheory.Triangulated.HeartK0 C
      h

Something wrong, better idea? Suggest a change

12.7.8. heartK0FromK0_of🔗

\texttt{heartK0FromK0}([E]) = \texttt{heartEulerClassObj}(E).

Proof: Immediate from the lifting construction.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartK0FromK0_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.Triangulated.IsTriangleAdditive fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E]
  (E : C) :
  (CategoryTheory.Triangulated.HeartStabilityData.heartK0FromK0 C h)
      (CategoryTheory.Triangulated.K₀.of C E) =
    CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C
      h E
CategoryTheory.Triangulated.HeartStabilityData.heartK0FromK0_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.Triangulated.IsTriangleAdditive
      fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E]
  (E : C) :
  (CategoryTheory.Triangulated.HeartStabilityData.heartK0FromK0
        C h)
      (CategoryTheory.Triangulated.K₀.of C
        E) =
    CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
      C h E

Something wrong, better idea? Suggest a change

12.7.9. heartK0ToK0_comp_heartK0FromK0🔗

The composition \texttt{heartK0ToK0} \circ \texttt{heartK0FromK0} = \operatorname{id}_{K_0(\mathcal{C})}.

Proof: On generators [E], the round-trip gives [E] by \texttt{heartK0ToK0\_heartEulerClassObj}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0_comp_heartK0FromK0.{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.IsTriangleAdditive fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E] :
  (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0 C h).comp
      (CategoryTheory.Triangulated.HeartStabilityData.heartK0FromK0 C
        h) =
    AddMonoidHom.id (CategoryTheory.Triangulated.K₀ C)
CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0_comp_heartK0FromK0.{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.IsTriangleAdditive
      fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E] :
  (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0
          C h).comp
      (CategoryTheory.Triangulated.HeartStabilityData.heartK0FromK0
        C h) =
    AddMonoidHom.id
      (CategoryTheory.Triangulated.K₀ C)

Something wrong, better idea? Suggest a change

12.7.10. heartK0FromK0_comp_heartK0ToK0🔗

The composition \texttt{heartK0FromK0} \circ \texttt{heartK0ToK0} = \operatorname{id}_{K_0(\operatorname{heart})}.

Proof: On generators [E] for heart objects, the round-trip gives [E] by \texttt{heartEulerClassObj\_of\_heart}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartK0FromK0_comp_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.IsTriangleAdditive fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E] :
  (CategoryTheory.Triangulated.HeartStabilityData.heartK0FromK0 C
          h).comp
      (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0 C h) =
    AddMonoidHom.id (CategoryTheory.Triangulated.HeartK0 C h)
CategoryTheory.Triangulated.HeartStabilityData.heartK0FromK0_comp_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.IsTriangleAdditive
      fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E] :
  (CategoryTheory.Triangulated.HeartStabilityData.heartK0FromK0
          C h).comp
      (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0
        C h) =
    AddMonoidHom.id
      (CategoryTheory.Triangulated.HeartK0
        C h)

Something wrong, better idea? Suggest a change

12.7.11. heartK0EquivK0🔗

If the Euler lift is triangle-additive, the canonical map K_0(\operatorname{heart}(t)) \to K_0(\mathcal{C}) is an isomorphism of abelian groups.

Construction: An \texttt{AddEquiv} built from \texttt{heartK0ToK0} and \texttt{heartK0FromK0}, with the two round-trip identities as proofs.

def

CategoryTheory.Triangulated.HeartStabilityData.heartK0EquivK0.{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.IsTriangleAdditive fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E] :
  CategoryTheory.Triangulated.HeartK0 C h ≃+
    CategoryTheory.Triangulated.K₀ C
CategoryTheory.Triangulated.HeartStabilityData.heartK0EquivK0.{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.IsTriangleAdditive
      fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E] :
  CategoryTheory.Triangulated.HeartK0 C
      h ≃+
    CategoryTheory.Triangulated.K₀ C

Something wrong, better idea? Suggest a change

12.7.12. eulerZObj_isTriangleAdditive🔗

If the Euler class lift is triangle-additive, then so is the object-level central charge \texttt{eulerZObj}.

Proof: Applies the group homomorphism Z_{K_0} to the triangle-additivity relation for \texttt{heartEulerClassObj}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_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.Triangulated.IsTriangleAdditive fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E] :
  CategoryTheory.Triangulated.IsTriangleAdditive fun E =>
    CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h E
CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_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.Triangulated.IsTriangleAdditive
      fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E] :
  CategoryTheory.Triangulated.IsTriangleAdditive
    fun E =>
    CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
      C h E

Something wrong, better idea? Suggest a change

12.7.13. ambientZ🔗

If the Euler lift is triangle-additive, the heart central charge extends to an ambient homomorphism K_0(\mathcal{C}) \to \mathbb{C}.

Construction: Lifts E \mapsto \texttt{eulerZObj}(E) through the universal property of K_0(\mathcal{C}).

def

CategoryTheory.Triangulated.HeartStabilityData.ambientZ.{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.IsTriangleAdditive fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E] :
  CategoryTheory.Triangulated.K₀ C →+ ℂ
CategoryTheory.Triangulated.HeartStabilityData.ambientZ.{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.IsTriangleAdditive
      fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E] :
  CategoryTheory.Triangulated.K₀ C →+ ℂ

Something wrong, better idea? Suggest a change

12.7.14. ambientZ_of🔗

\texttt{ambientZ}([E]) = \texttt{eulerZObj}(E).

Proof: Immediate from the lifting construction.

theorem

CategoryTheory.Triangulated.HeartStabilityData.ambientZ_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.Triangulated.IsTriangleAdditive fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E]
  (E : C) :
  (CategoryTheory.Triangulated.HeartStabilityData.ambientZ C h)
      (CategoryTheory.Triangulated.K₀.of C E) =
    CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h E
CategoryTheory.Triangulated.HeartStabilityData.ambientZ_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.Triangulated.IsTriangleAdditive
      fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E]
  (E : C) :
  (CategoryTheory.Triangulated.HeartStabilityData.ambientZ
        C h)
      (CategoryTheory.Triangulated.K₀.of C
        E) =
    CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
      C h E

Something wrong, better idea? Suggest a change

12.7.15. ambientZ_eq_ZOnHeartK0_comp_heartK0FromK0🔗

\texttt{ambientZ} = Z_{K_0} \circ \texttt{heartK0FromK0}.

Proof: Both sides agree on generators by definition.

theorem

CategoryTheory.Triangulated.HeartStabilityData.ambientZ_eq_ZOnHeartK0_comp_heartK0FromK0.{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.IsTriangleAdditive fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E] :
  CategoryTheory.Triangulated.HeartStabilityData.ambientZ C h =
    (CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0 C h).comp
      (CategoryTheory.Triangulated.HeartStabilityData.heartK0FromK0 C h)
CategoryTheory.Triangulated.HeartStabilityData.ambientZ_eq_ZOnHeartK0_comp_heartK0FromK0.{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.IsTriangleAdditive
      fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E] :
  CategoryTheory.Triangulated.HeartStabilityData.ambientZ
      C h =
    (CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0
          C h).comp
      (CategoryTheory.Triangulated.HeartStabilityData.heartK0FromK0
        C h)

Something wrong, better idea? Suggest a change

12.7.16. ambientZ_comp_heartK0ToK0🔗

\texttt{ambientZ} \circ \texttt{heartK0ToK0} = Z_{K_0}.

Proof: On heart generators [E], both sides evaluate to Z(E).

theorem

CategoryTheory.Triangulated.HeartStabilityData.ambientZ_comp_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.IsTriangleAdditive fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E] :
  (CategoryTheory.Triangulated.HeartStabilityData.ambientZ C h).comp
      (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0 C h) =
    CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0 C h
CategoryTheory.Triangulated.HeartStabilityData.ambientZ_comp_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.IsTriangleAdditive
      fun E =>
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E] :
  (CategoryTheory.Triangulated.HeartStabilityData.ambientZ
          C h).comp
      (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0
        C h) =
    CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0
      C h

Something wrong, better idea? Suggest a change

12.7.17. ZOnHeartK0_heartCohClass🔗

Z_{K_0}(\texttt{heartCohClass}(n, E)) = (-1)^{|n|} \cdot Z(H^n_t(E)).

Proof: Unfolds the definition of \texttt{heartCohClass}, applies \texttt{map\_zsmul}, and uses Z_{K_0}([H]) = Z(H).

theorem

CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0_heartCohClass.{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) (n : ℤ)
  (E : C) :
  (CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0 C h)
      (CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h
        n E) =
    (-1) ^ n.natAbs •
      CategoryTheory.Triangulated.HeartStabilityData.heartZObj C h
        (CategoryTheory.Triangulated.HeartStabilityData.heartCoh C h n
          E)
CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0_heartCohClass.{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)
  (n : ℤ) (E : C) :
  (CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0
        C h)
      (CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
        C h n E) =
    (-1) ^ n.natAbs •
      CategoryTheory.Triangulated.HeartStabilityData.heartZObj
        C h
        (CategoryTheory.Triangulated.HeartStabilityData.heartCoh
          C h n E)

Something wrong, better idea? Suggest a change

12.7.18. heartK0_relation_of_pure_distTriang🔗

A distinguished triangle concentrated in a single t-degree n yields the expected short exact relation in the heart Grothendieck group after shifting by n.

Proof: Shifting the triangle by n places all three vertices in the heart. The shifted triangle is then a short exact sequence in the heart, and the K_0 relation follows from \texttt{HeartK0.of\_shortExact}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartK0_relation_of_pure_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]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  [CategoryTheory.IsTriangulated C] {X₁ X₂ X₃ : C} {f : X₁ ⟶ X₂}
  {g : X₂ ⟶ X₃} {δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  (n : ℤ)
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h₁LE : h.t.IsLE X₁ n) (h₁GE : h.t.IsGE X₁ n) (h₂LE : h.t.IsLE X₂ n)
  (h₂GE : h.t.IsGE X₂ n) (h₃LE : h.t.IsLE X₃ n) (h₃GE : h.t.IsGE X₃ n) :
  have H₁ :=
    CategoryTheory.Triangulated.HeartStabilityData.heartShiftOfPure C h
      n h₁LE h₁GE;
  have H₂ :=
    CategoryTheory.Triangulated.HeartStabilityData.heartShiftOfPure C h
      n h₂LE h₂GE;
  have H₃ :=
    CategoryTheory.Triangulated.HeartStabilityData.heartShiftOfPure C h
      n h₃LE h₃GE;
  (-1) ^ n.natAbs • CategoryTheory.Triangulated.HeartK0.of C h H₂ =
    (-1) ^ n.natAbs • CategoryTheory.Triangulated.HeartK0.of C h H₁ +
      (-1) ^ n.natAbs • CategoryTheory.Triangulated.HeartK0.of C h H₃
CategoryTheory.Triangulated.HeartStabilityData.heartK0_relation_of_pure_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]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  [CategoryTheory.IsTriangulated C]
  {X₁ X₂ X₃ : C} {f : X₁ ⟶ X₂}
  {g : X₂ ⟶ X₃}
  {δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X₁}
  (n : ℤ)
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h₁LE : h.t.IsLE X₁ n)
  (h₁GE : h.t.IsGE X₁ n)
  (h₂LE : h.t.IsLE X₂ n)
  (h₂GE : h.t.IsGE X₂ n)
  (h₃LE : h.t.IsLE X₃ n)
  (h₃GE : h.t.IsGE X₃ n) :
  have H₁ :=
    CategoryTheory.Triangulated.HeartStabilityData.heartShiftOfPure
      C h n h₁LE h₁GE;
  have H₂ :=
    CategoryTheory.Triangulated.HeartStabilityData.heartShiftOfPure
      C h n h₂LE h₂GE;
  have H₃ :=
    CategoryTheory.Triangulated.HeartStabilityData.heartShiftOfPure
      C h n h₃LE h₃GE;
  (-1) ^ n.natAbs •
      CategoryTheory.Triangulated.HeartK0.of
        C h H₂ =
    (-1) ^ n.natAbs •
        CategoryTheory.Triangulated.HeartK0.of
          C h H₁ +
      (-1) ^ n.natAbs •
        CategoryTheory.Triangulated.HeartK0.of
          C h H₃

Something wrong, better idea? Suggest a change

12.7.19. heartCohClass_eq_zero_of_lt_bound🔗

If m < n and X \in \mathcal{C}^{\ge n}, then \texttt{heartCohClass}(m, X) = 0.

Proof: The pure truncation \tau^{[m,m]} X vanishes because \tau^{\le m} X = 0, so the heart cohomology is zero and its K_0-class vanishes.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_eq_zero_of_lt_bound.{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}
  {m n : ℤ} (hmn : m < n) (hGE : h.t.IsGE X n) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h m X =
    0
CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_eq_zero_of_lt_bound.{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} {m n : ℤ} (hmn : m < n)
  (hGE : h.t.IsGE X n) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
      C h m X =
    0

Something wrong, better idea? Suggest a change

12.7.20. heartCohClass_eq_zero_of_lt_pure🔗

If X is a pure object of degree n and m < n, then \texttt{heartCohClass}(m, X) = 0.

Proof: The pure truncation \tau^{[m,m]} X vanishes since X \in \mathcal{C}^{\ge n} and m < n.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_eq_zero_of_lt_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) {X : C}
  {m n : ℤ} (hmn : m < n) (hGE : h.t.IsGE X n) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h m X =
    0
CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_eq_zero_of_lt_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)
  {X : C} {m n : ℤ} (hmn : m < n)
  (hGE : h.t.IsGE X n) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
      C h m X =
    0

Something wrong, better idea? Suggest a change

12.7.21. heartCohClass_eq_zero_of_gt_bound🔗

If n < m and X \in \mathcal{C}^{\le n}, then \texttt{heartCohClass}(m, X) = 0.

Proof: The pure truncation \tau^{[m,m]} X vanishes because \tau^{\ge m} of \tau^{\le m} X \cong X is zero for m > n.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_eq_zero_of_gt_bound.{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}
  {m n : ℤ} (hmn : n < m) (hLE : h.t.IsLE X n) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h m X =
    0
CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_eq_zero_of_gt_bound.{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} {m n : ℤ} (hmn : n < m)
  (hLE : h.t.IsLE X n) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
      C h m X =
    0

Something wrong, better idea? Suggest a change

12.7.22. heartCohClass_eq_zero_of_gt_pure🔗

If X is a pure object of degree n and m > n, then \texttt{heartCohClass}(m, X) = 0.

Proof: The pure truncation \tau^{[m,m]} X vanishes since X \in \mathcal{C}^{\le n} and m > n.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_eq_zero_of_gt_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) {X : C}
  {m n : ℤ} (hmn : n < m) (hLE : h.t.IsLE X n) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h m X =
    0
CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_eq_zero_of_gt_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)
  {X : C} {m n : ℤ} (hmn : n < m)
  (hLE : h.t.IsLE X n) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
      C h m X =
    0

Something wrong, better idea? Suggest a change

12.7.23. heartCohClassSum_eq_zero_of_lt_bound🔗

If b + n < m (i.e., the entire range [b, b+n] is below the support), then \texttt{heartCohClassSum}(b, n, X) = 0 for X \in \mathcal{C}^{\ge m}.

Proof: Each summand vanishes by \texttt{heartCohClass\_eq\_zero\_of\_lt\_bound}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_eq_zero_of_lt_bound.{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}
  {b c : ℤ} {n : ℕ} (hbc : b + ↑n < c) (hGE : h.t.IsGE X c) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h b
      n X =
    0
CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_eq_zero_of_lt_bound.{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} {b c : ℤ} {n : ℕ}
  (hbc : b + ↑n < c)
  (hGE : h.t.IsGE X c) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h b n X =
    0

Something wrong, better idea? Suggest a change

12.7.24. heartCohClassSum_eq_zero_of_gt_bound🔗

If n < b (i.e., the entire range [b, b+m] is above the support), then \texttt{heartCohClassSum}(b, m, X) = 0 for X \in \mathcal{C}^{\le n}.

Proof: Each summand \texttt{heartCohClass}(b+j, X) vanishes by \texttt{heartCohClass\_eq\_zero\_of\_gt\_bound}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_eq_zero_of_gt_bound.{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}
  {b c : ℤ} {n : ℕ} (hcb : c < b) (hLE : h.t.IsLE X c) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h b
      n X =
    0
CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_eq_zero_of_gt_bound.{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} {b c : ℤ} {n : ℕ} (hcb : c < b)
  (hLE : h.t.IsLE X c) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h b n X =
    0

Something wrong, better idea? Suggest a change

12.7.25. heartCohClass_eq_zero_of_isZero🔗

If E is zero, then \texttt{heartCohClass}(n, E) = 0 for all n.

Proof: All truncations of the zero object are zero, so H^n_t(0) = 0 and [0] = 0 in K_0.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_eq_zero_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) {X : C}
  (hX : CategoryTheory.Limits.IsZero X) (n : ℤ) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h n X =
    0
CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_eq_zero_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)
  {X : C}
  (hX : CategoryTheory.Limits.IsZero X)
  (n : ℤ) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
      C h n X =
    0

Something wrong, better idea? Suggest a change

12.7.26. heartCohClassSum_eq_zero_of_isZero🔗

If E is zero, then \texttt{heartCohClassSum}(b, n, E) = 0.

Proof: Each summand \texttt{heartCohClass}(b+j, E) vanishes since the zero object has all heart cohomology zero.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_eq_zero_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) {X : C}
  (hX : CategoryTheory.Limits.IsZero X) (b : ℤ) (n : ℕ) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h b
      n X =
    0
CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_eq_zero_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)
  {X : C}
  (hX : CategoryTheory.Limits.IsZero X)
  (b : ℤ) (n : ℕ) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h b n X =
    0

Something wrong, better idea? Suggest a change

12.7.27. heartCohClassSum_pred_upper🔗

The alternating sum from b to b+n equals the sum from b to b+n-1 plus the (b+n)th cohomology class.

Proof: Peels off the top term using \texttt{heartCohClassSum\_succ} shifted by one.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_pred_upper.{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}
  {b a : ℤ} (hba : b < a) (hLE : h.t.IsLE X (a - 1)) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h b
      (a - b).toNat X =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h
      b (a - 1 - b).toNat X
CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_pred_upper.{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} {b a : ℤ} (hba : b < a)
  (hLE : h.t.IsLE X (a - 1)) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h b (a - b).toNat X =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h b (a - 1 - b).toNat X

Something wrong, better idea? Suggest a change

12.7.28. heartCohClassSum_shrink_lower🔗

The alternating sum \texttt{heartCohClassSum}(b, n, E) for E \in \mathcal{C}^{\ge b} equals the sum starting at b+1, if the bth cohomology class vanishes.

Proof: The first term \texttt{heartCohClass}(b, E) = 0 by the lower bound hypothesis; the remaining sum is \texttt{heartCohClassSum}(b+1, n-1, E).

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_shrink_lower.{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}
  {c b a : ℤ} (hcb : c ≤ b) (hba : b ≤ a) (hGE : h.t.IsGE X b) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h c
      (a - c).toNat X =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h
      b (a - b).toNat X
CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_shrink_lower.{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} {c b a : ℤ} (hcb : c ≤ b)
  (hba : b ≤ a) (hGE : h.t.IsGE X b) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h c (a - c).toNat X =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h b (a - b).toNat X

Something wrong, better idea? Suggest a change

12.7.29. heartCohClassSum_shrink_upper🔗

The alternating sum \texttt{heartCohClassSum}(b, n, E) for E \in \mathcal{C}^{\le b+n} equals the sum ending at b+n-1, if the (b+n)th cohomology class vanishes.

Proof: The last term \texttt{heartCohClass}(b+n, E) = 0 by the upper bound hypothesis; the remaining sum is \texttt{heartCohClassSum}(b, n-1, E).

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_shrink_upper.{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}
  {b a c : ℤ} (hba : b ≤ a) (hac : a ≤ c) (hLE : h.t.IsLE X a) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h b
      (c - b).toNat X =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h
      b (a - b).toNat X
CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_shrink_upper.{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} {b a c : ℤ} (hba : b ≤ a)
  (hac : a ≤ c) (hLE : h.t.IsLE X a) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h b (c - b).toNat X =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h b (a - b).toNat X

Something wrong, better idea? Suggest a change

12.7.30. heartCohClassSum_eq_of_bounds🔗

The alternating heart cohomology class sum is independent of the choice of bounds, as long as the bounds contain the amplitude of X.

Proof: Uses \texttt{heartCohClass\_eq\_zero\_of\_lt\_bound} and \texttt{heartCohClass\_eq\_zero\_of\_gt\_bound} to show the extra terms vanish outside the amplitude.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_eq_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) {X : C}
  {b₁ a₁ b₂ a₂ : ℤ} (h₁ : b₁ ≤ a₁) (h₂ : b₂ ≤ a₂) (hLE₁ : h.t.IsLE X a₁)
  (hGE₁ : h.t.IsGE X b₁) (hLE₂ : h.t.IsLE X a₂) (hGE₂ : h.t.IsGE X b₂) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h b₁
      (a₁ - b₁).toNat X =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h
      b₂ (a₂ - b₂).toNat X
CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_eq_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)
  {X : C} {b₁ a₁ b₂ a₂ : ℤ} (h₁ : b₁ ≤ a₁)
  (h₂ : b₂ ≤ a₂) (hLE₁ : h.t.IsLE X a₁)
  (hGE₁ : h.t.IsGE X b₁)
  (hLE₂ : h.t.IsLE X a₂)
  (hGE₂ : h.t.IsGE X b₂) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h b₁ (a₁ - b₁).toNat X =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h b₂ (a₂ - b₂).toNat X

Something wrong, better idea? Suggest a change

12.7.31. heartCohClassSum_of_truncLT🔗

For n < a, \texttt{heartCohClassSum}(b, n, \tau^{<a} E) = \texttt{heartCohClassSum}(b, n, E).

Proof: Each summand satisfies \texttt{heartCohClass}(b+j, \tau^{<a} E) = \texttt{heartCohClass}(b+j, E) for b+j \le n < a by \texttt{heartCohClass\_of\_truncLT}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_of_truncLT.{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 : C} {b a : ℤ} (hba : b < a) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h b
      (a - 1 - b).toNat ((h.t.truncLT a).obj E) =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h
      b (a - 1 - b).toNat E
CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_of_truncLT.{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 : C} {b a : ℤ} (hba : b < a) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h b (a - 1 - b).toNat
      ((h.t.truncLT a).obj E) =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h b (a - 1 - b).toNat E

Something wrong, better idea? Suggest a change

12.7.32. heartEulerClassObj_eq_heartCohClassSum🔗

The Euler class lift equals the heart cohomology class sum for any choice of bounds [b, a] containing the amplitude of X.

Proof: Uses the bound-independence lemma \texttt{heartCohClassSum\_eq\_of\_bounds} to equate the sum for the chosen classical bounds with the sum for the given bounds.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_eq_heartCohClassSum.{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}
  {b a : ℤ} (hab : b ≤ a) (hLE : h.t.IsLE X a) (hGE : h.t.IsGE X b) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C h
      X =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h
      b (a - b).toNat X
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_eq_heartCohClassSum.{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} {b a : ℤ} (hab : b ≤ a)
  (hLE : h.t.IsLE X a)
  (hGE : h.t.IsGE X b) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
      C h X =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h b (a - b).toNat X

Something wrong, better idea? Suggest a change

12.7.33. heartEulerClassObj_eq_zero_of_isZero🔗

If E is zero, then \texttt{heartEulerClassObj}(E) = 0.

Proof: The alternating sum is empty or all terms are zero since H^n_t(0) = 0; alternatively, uses \texttt{heartCohClassSum\_eq\_zero\_of\_isZero}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_eq_zero_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) {X : C}
  (hX : CategoryTheory.Limits.IsZero X) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C h
      X =
    0
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_eq_zero_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)
  {X : C}
  (hX : CategoryTheory.Limits.IsZero X) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
      C h X =
    0

Something wrong, better idea? Suggest a change

12.7.34. eulerZObj_eq_zero_of_isZero🔗

If E is zero, then \texttt{eulerZObj}(E) = 0.

Proof: All heart cohomology objects of the zero object are zero, so the Euler class is 0 and Z_{K_0}(0) = 0.

theorem

CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_eq_zero_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) {X : C}
  (hX : CategoryTheory.Limits.IsZero X) :
  CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h X = 0
CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_eq_zero_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)
  {X : C}
  (hX : CategoryTheory.Limits.IsZero X) :
  CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
      C h X =
    0

Something wrong, better idea? Suggest a change

12.7.35. heartEulerClassObj_eq_truncLT_add_heartCohClass🔗

The Euler class satisfies a peeling formula: \texttt{heartEulerClassObj}(E) = \texttt{heartEulerClassObj}(\tau^{<a} E) + \texttt{heartCohClass}(a, E).

Proof: Writes the sum from b to a as the sum from b to a-1 plus the a-th term, then identifies the partial sum with the Euler class of the truncation using \texttt{heartCohClass\_of\_truncLT}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_eq_truncLT_add_heartCohClass.{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 : C} {b a : ℤ} (hba : b < a)
  (hLE : h.t.IsLE E a) (hGE : h.t.IsGE E b) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C h
      E =
    CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C
        h ((h.t.truncLT a).obj E) +
      CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h a
        E
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_eq_truncLT_add_heartCohClass.{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 : C} {b a : ℤ} (hba : b < a)
  (hLE : h.t.IsLE E a)
  (hGE : h.t.IsGE E b) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
      C h E =
    CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h ((h.t.truncLT a).obj E) +
      CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
        C h a E

Something wrong, better idea? Suggest a change

12.7.36. eulerZObj_eq_truncLT_add_heartCohClass🔗

The Euler class satisfies the peeling formula: \texttt{eulerZObj}(E) = \texttt{eulerZObj}(\tau^{<a} E) + Z_{K_0}(\texttt{heartCohClass}(a, E)).

Proof: Applies Z_{K_0} to the peeling identity \texttt{heartEulerClassObj\_eq\_truncLT\_add\_heartCohClass}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_eq_truncLT_add_heartCohClass.{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 : C} {b a : ℤ} (hba : b < a)
  (hLE : h.t.IsLE E a) (hGE : h.t.IsGE E b) :
  CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h E =
    CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h
        ((h.t.truncLT a).obj E) +
      (CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0 C h)
        (CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C
          h a E)
CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_eq_truncLT_add_heartCohClass.{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 : C} {b a : ℤ} (hba : b < a)
  (hLE : h.t.IsLE E a)
  (hGE : h.t.IsGE E b) :
  CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
      C h E =
    CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
        C h ((h.t.truncLT a).obj E) +
      (CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0
          C h)
        (CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
          C h a E)

Something wrong, better idea? Suggest a change

12.7.37. heartCohClassSum_eq_single_of_pure🔗

For a pure object concentrated in degree n, the alternating heart cohomology class sum \texttt{heartCohClassSum}(b, m, X) (with b \le n \le b+m) equals the single term \texttt{heartCohClass}(n, X).

Proof: All terms except index n vanish by \texttt{heartCohClass\_eq\_zero\_of\_gt\_pure} and \texttt{heartCohClass\_eq\_zero\_of\_lt\_pure}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_eq_single_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) {X : C}
  {n b : ℤ} {m : ℕ} (hLE : h.t.IsLE X n) (hGE : h.t.IsGE X n)
  (hb : b ≤ n) (hn : n ≤ b + ↑m) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h b
      m X =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h n X
CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_eq_single_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)
  {X : C} {n b : ℤ} {m : ℕ}
  (hLE : h.t.IsLE X n)
  (hGE : h.t.IsGE X n) (hb : b ≤ n)
  (hn : n ≤ b + ↑m) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h b m X =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
      C h n X

Something wrong, better idea? Suggest a change

12.7.38. heartCohClassSum_eq_top_of_pure🔗

For a pure object concentrated in degree n, the alternating sum \texttt{heartCohClassSum}(b, m, X) (with b \le n \le b+m) equals the parity-weighted class: (-1)^{|n|} \cdot [\texttt{heartShiftOfPure}(X, n)].

Proof: Uses \texttt{heartCohClassSum\_eq\_single\_of\_pure} and then the definition of \texttt{heartCohClass} and \texttt{heartCoh} for a pure object.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_eq_top_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) {X : C}
  {a b : ℤ} (hab : b ≤ a) (hLE : h.t.IsLE X a) (hGE : h.t.IsGE X a) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h b
      (a - b).toNat X =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h a X
CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_eq_top_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)
  {X : C} {a b : ℤ} (hab : b ≤ a)
  (hLE : h.t.IsLE X a)
  (hGE : h.t.IsGE X a) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h b (a - b).toNat X =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
      C h a X

Something wrong, better idea? Suggest a change

12.7.39. ZOnHeartK0_heartCohClassSum_eq_top_of_pure🔗

For a pure object X concentrated in degree n, the heart central charge applied to the alternating sum of heart cohomology classes equals Z(X).

Proof: The cohomology class sum has only the degree-n term nonzero (all other \texttt{heartCohClass} vanish outside the support). Simplifies using \texttt{ZOnHeartK0\_heartCohClassSum\_of\_pure}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0_heartCohClassSum_eq_top_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) {X : C}
  {a b : ℤ} (hab : b ≤ a) (hLE : h.t.IsLE X a) (hGE : h.t.IsGE X a) :
  (CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0 C h)
      (CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C
        h b (a - b).toNat X) =
    (CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0 C h)
      (CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h
        a X)
CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0_heartCohClassSum_eq_top_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)
  {X : C} {a b : ℤ} (hab : b ≤ a)
  (hLE : h.t.IsLE X a)
  (hGE : h.t.IsGE X a) :
  (CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0
        C h)
      (CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
        C h b (a - b).toNat X) =
    (CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0
        C h)
      (CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
        C h a X)

Something wrong, better idea? Suggest a change

12.7.40. ZOnHeartK0_heartCohClassSum_of_pure🔗

For a pure object of degree n, the Euler-form-weighted central charge sum Z_{K_0}(\texttt{heartCohClassSum}(b, m, X)) simplifies to a single term.

Proof: All heart cohomology classes outside degree n vanish; the single remaining term is computed from \texttt{ZOnHeartK0\_heartCohClass} and purity.

theorem

CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0_heartCohClassSum_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) {X : C}
  {a b : ℤ} (hab : b ≤ a) (hLE : h.t.IsLE X a) (hGE : h.t.IsGE X a) :
  (CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0 C h)
      (CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C
        h b (a - b).toNat X) =
    (-1) ^ a.natAbs •
      CategoryTheory.Triangulated.HeartStabilityData.heartZObj C h
        (CategoryTheory.Triangulated.HeartStabilityData.heartCoh C h a
          X)
CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0_heartCohClassSum_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)
  {X : C} {a b : ℤ} (hab : b ≤ a)
  (hLE : h.t.IsLE X a)
  (hGE : h.t.IsGE X a) :
  (CategoryTheory.Triangulated.HeartStabilityData.ZOnHeartK0
        C h)
      (CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
        C h b (a - b).toNat X) =
    (-1) ^ a.natAbs •
      CategoryTheory.Triangulated.HeartStabilityData.heartZObj
        C h
        (CategoryTheory.Triangulated.HeartStabilityData.heartCoh
          C h a X)

Something wrong, better idea? Suggest a change

12.7.41. heartEulerClassObj_of_pure🔗

For a pure object X concentrated in degree n, \texttt{heartEulerClassObj}(X) = (-1)^{|n|} \cdot [\texttt{heartShiftOfPure}(X, n)].

Proof: Reduces to a single-term sum by \texttt{heartCohClassSum\_eq\_single\_of\_pure} and then uses \texttt{heartCohClass} for the single term.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_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) {X : C} {n : ℤ}
  (hLE : h.t.IsLE X n) (hGE : h.t.IsGE X n) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C h
      X =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h n X
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_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)
  {X : C} {n : ℤ} (hLE : h.t.IsLE X n)
  (hGE : h.t.IsGE X n) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
      C h X =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
      C h n X

Something wrong, better idea? Suggest a change

12.7.42. heartCohIso_of_pure🔗

For a pure object concentrated in degree n, H^n_t(X) \cong \texttt{heartShiftOfPure}(X, n).

Construction: The pure truncation \tau^{[n,n]} X \cong X (since X is already concentrated in degree n), and shifting by n gives the heart object \texttt{heartShiftOfPure}(X, n).

def

CategoryTheory.Triangulated.HeartStabilityData.heartCohIso_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) {X : C} {n : ℤ}
  (hLE : h.t.IsLE X n) (hGE : h.t.IsGE X n) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCoh C h n X ≅
    CategoryTheory.Triangulated.HeartStabilityData.heartShiftOfPure C h
      n hLE hGE
CategoryTheory.Triangulated.HeartStabilityData.heartCohIso_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)
  {X : C} {n : ℤ} (hLE : h.t.IsLE X n)
  (hGE : h.t.IsGE X n) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCoh
      C h n X ≅
    CategoryTheory.Triangulated.HeartStabilityData.heartShiftOfPure
      C h n hLE hGE

Something wrong, better idea? Suggest a change

12.7.43. heartCohClass_eq_pureClass🔗

The heart cohomology class \texttt{heartCohClass}(n, E) equals the purity-weighted class \texttt{pureClass}(n, E).

Proof: Follows from the definition of \texttt{pureClass} and \texttt{heartCohClass}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_eq_pureClass.{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) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h n X =
    (-1) ^ n.natAbs •
      CategoryTheory.Triangulated.HeartK0.of C h
        (CategoryTheory.Triangulated.HeartStabilityData.heartShiftOfPure
          C h n hLE hGE)
CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_eq_pureClass.{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) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
      C h n X =
    (-1) ^ n.natAbs •
      CategoryTheory.Triangulated.HeartK0.of
        C h
        (CategoryTheory.Triangulated.HeartStabilityData.heartShiftOfPure
          C h n hLE hGE)

Something wrong, better idea? Suggest a change

12.7.44. heartCohIso_of_truncGE_of_isLE🔗

Truncating below degree a does not change the degree-a heart cohomology object when the original object is t-nonpositive in degree a: H^a_t(\tau^{\ge a} X) \cong H^a_t(X) for X \in \mathcal{C}^{\le a}.

Construction: The \tau^{\ge a}-projection X \to \tau^{\ge a} X induces an isomorphism on \tau^{[a,a]} when X \in \mathcal{C}^{\le a}, which after shifting by a gives the heart isomorphism.

def

CategoryTheory.Triangulated.HeartStabilityData.heartCohIso_of_truncGE_of_isLE.{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 : C) (a : ℤ)
  (hLE : h.t.IsLE E a) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCoh C h a
      ((h.t.truncGE a).obj E) ≅
    CategoryTheory.Triangulated.HeartStabilityData.heartCoh C h a E
CategoryTheory.Triangulated.HeartStabilityData.heartCohIso_of_truncGE_of_isLE.{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 : C) (a : ℤ) (hLE : h.t.IsLE E a) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCoh
      C h a ((h.t.truncGE a).obj E) ≅
    CategoryTheory.Triangulated.HeartStabilityData.heartCoh
      C h a E

Something wrong, better idea? Suggest a change

12.7.45. heartCohClass_of_truncGE_of_isLE🔗

For X \in \mathcal{C}^{\le a}, \texttt{heartCohClass}(a, \tau^{\ge a} X) = \texttt{heartCohClass}(a, X).

Proof: Uses the isomorphism \texttt{heartCohIso\_of\_truncGE\_of\_isLE} and invariance of K_0-classes under isomorphism.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_of_truncGE_of_isLE.{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 : C) (a : ℤ)
  (hLE : h.t.IsLE E a) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h a
      ((h.t.truncGE a).obj E) =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h a E
CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_of_truncGE_of_isLE.{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 : C) (a : ℤ) (hLE : h.t.IsLE E a) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
      C h a ((h.t.truncGE a).obj E) =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
      C h a E

Something wrong, better idea? Suggest a change

12.7.46. heartEulerClassObj_of_truncGE_of_isLE🔗

For X \in \mathcal{C}^{\le a}, \texttt{heartEulerClassObj}(\tau^{\ge a} X) = \texttt{heartCohClass}(a, X).

Proof: The truncation \tau^{\ge a} X is pure of degree a when X \in \mathcal{C}^{\le a}, so the sum reduces to the single degree-a term.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_of_truncGE_of_isLE.{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 : C) (a : ℤ)
  (hLE : h.t.IsLE E a) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C h
      ((h.t.truncGE a).obj E) =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h a E
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_of_truncGE_of_isLE.{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 : C) (a : ℤ) (hLE : h.t.IsLE E a) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
      C h ((h.t.truncGE a).obj E) =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
      C h a E

Something wrong, better idea? Suggest a change

12.7.47. heartEulerClassObj_eq_truncLT_add_truncGE🔗

The Euler class satisfies: \texttt{heartEulerClassObj}(E) = \texttt{heartEulerClassObj}(\tau^{<a} E) + \texttt{heartEulerClassObj}(\tau^{\ge a} E) - \texttt{heartEulerClassObj}(\tau^{<a}(\tau^{\ge a} E)).

Proof: Combines \texttt{heartEulerClassObj\_eq\_truncLT\_add\_heartCohClass} with the identification of the heart cohomology class of E at degree a with that of \tau^{\ge a} E via \texttt{heartCohClass\_of\_truncGE\_of\_isLE}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_eq_truncLT_add_truncGE.{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 : C} {b a : ℤ} (hba : b < a)
  (hLE : h.t.IsLE E a) (hGE : h.t.IsGE E b) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C h
      E =
    CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C
        h ((h.t.truncLT a).obj E) +
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h ((h.t.truncGE a).obj E)
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_eq_truncLT_add_truncGE.{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 : C} {b a : ℤ} (hba : b < a)
  (hLE : h.t.IsLE E a)
  (hGE : h.t.IsGE E b) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
      C h E =
    CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h ((h.t.truncLT a).obj E) +
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h ((h.t.truncGE a).obj E)

Something wrong, better idea? Suggest a change

12.7.48. eulerZObj_eq_truncLT_add_truncGE🔗

The Euler-form central charge satisfies: \texttt{eulerZObj}(E) = \texttt{eulerZObj}(\tau^{<a} E) + \texttt{eulerZObj}(\tau^{\ge a} E).

Proof: Uses \texttt{eulerZObj\_eq\_truncLT\_add\_heartCohClass} and the identification of the heart cohomology class with the Euler class of the pure truncation.

theorem

CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_eq_truncLT_add_truncGE.{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 : C} {b a : ℤ} (hba : b < a)
  (hLE : h.t.IsLE E a) (hGE : h.t.IsGE E b) :
  CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h E =
    CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h
        ((h.t.truncLT a).obj E) +
      CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h
        ((h.t.truncGE a).obj E)
CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_eq_truncLT_add_truncGE.{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 : C} {b a : ℤ} (hba : b < a)
  (hLE : h.t.IsLE E a)
  (hGE : h.t.IsGE E b) :
  CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
      C h E =
    CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
        C h ((h.t.truncLT a).obj E) +
      CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
        C h ((h.t.truncGE a).obj E)

Something wrong, better idea? Suggest a change

12.7.49. heartEulerClassObj_of_heart_shift🔗

For a heart object E and integer n, \texttt{heartEulerClassObj}(E[-n]) = (-1)^{|n|} \cdot [E] in K_0(\operatorname{heart}).

Proof: The object E[-n] is pure of degree n, so the alternating sum reduces to a single term \texttt{heartCohClass}(n, E[-n]) = (-1)^{|n|} \cdot [E] by \texttt{heartCohClass\_of\_heart\_shift}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_of_heart_shift.{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) (n : ℤ) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C h
      ((CategoryTheory.shiftFunctor C (-n)).obj E.obj) =
    (-1) ^ n.natAbs • CategoryTheory.Triangulated.HeartK0.of C h E
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_of_heart_shift.{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)
  (n : ℤ) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
      C h
      ((CategoryTheory.shiftFunctor C
            (-n)).obj
        E.obj) =
    (-1) ^ n.natAbs •
      CategoryTheory.Triangulated.HeartK0.of
        C h E

Something wrong, better idea? Suggest a change

12.7.50. eulerZObj_of_pure🔗

For a pure object X concentrated in degree n, \texttt{eulerZObj}(X) = (-1)^{|n|} \cdot Z(\texttt{heartShiftOfPure}(X, n)).

Proof: Applies Z_{K_0} to \texttt{heartEulerClassObj\_of\_pure}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_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) {X : C} {n : ℤ}
  (hLE : h.t.IsLE X n) (hGE : h.t.IsGE X n) :
  CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h X =
    (-1) ^ n.natAbs •
      CategoryTheory.Triangulated.HeartStabilityData.heartZObj C h
        (CategoryTheory.Triangulated.HeartStabilityData.heartCoh C h n
          X)
CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_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)
  {X : C} {n : ℤ} (hLE : h.t.IsLE X n)
  (hGE : h.t.IsGE X n) :
  CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
      C h X =
    (-1) ^ n.natAbs •
      CategoryTheory.Triangulated.HeartStabilityData.heartZObj
        C h
        (CategoryTheory.Triangulated.HeartStabilityData.heartCoh
          C h n X)

Something wrong, better idea? Suggest a change

12.7.51. heartEulerClassObj_triangle_of_pure_distTriang🔗

For a pure distinguished triangle concentrated in degree n, \texttt{heartEulerClassObj}(X_2) = \texttt{heartEulerClassObj}(X_1) + \texttt{heartEulerClassObj}(X_3).

Proof: All three objects are pure of degree n; the sum reduces to a single-term identity using \texttt{heartK0\_relation\_of\_pure\_distTriang}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_triangle_of_pure_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]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  [CategoryTheory.IsTriangulated C] {X₁ X₂ X₃ : C} {f : X₁ ⟶ X₂}
  {g : X₂ ⟶ X₃} {δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  (n : ℤ)
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h₁LE : h.t.IsLE X₁ n) (h₁GE : h.t.IsGE X₁ n) (h₂LE : h.t.IsLE X₂ n)
  (h₂GE : h.t.IsGE X₂ n) (h₃LE : h.t.IsLE X₃ n) (h₃GE : h.t.IsGE X₃ n) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C h
      X₂ =
    CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj C
        h X₁ +
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h X₃
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj_triangle_of_pure_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]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  [CategoryTheory.IsTriangulated C]
  {X₁ X₂ X₃ : C} {f : X₁ ⟶ X₂}
  {g : X₂ ⟶ X₃}
  {δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X₁}
  (n : ℤ)
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h₁LE : h.t.IsLE X₁ n)
  (h₁GE : h.t.IsGE X₁ n)
  (h₂LE : h.t.IsLE X₂ n)
  (h₂GE : h.t.IsGE X₂ n)
  (h₃LE : h.t.IsLE X₃ n)
  (h₃GE : h.t.IsGE X₃ n) :
  CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
      C h X₂ =
    CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h X₁ +
      CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h X₃

Something wrong, better idea? Suggest a change

12.7.52. eulerZObj_triangle_of_pure_distTriang🔗

For a distinguished triangle concentrated in a single degree n, the Euler-form central charge satisfies the triangle relation: \texttt{eulerZObj}(X_2) = \texttt{eulerZObj}(X_1) + \texttt{eulerZObj}(X_3).

Proof: Applies Z_{K_0} to the heart-K_0 relation \texttt{heartK0\_relation\_of\_pure\_distTriang}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_triangle_of_pure_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]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  [CategoryTheory.IsTriangulated C] {X₁ X₂ X₃ : C} {f : X₁ ⟶ X₂}
  {g : X₂ ⟶ X₃} {δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  (n : ℤ)
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h₁LE : h.t.IsLE X₁ n) (h₁GE : h.t.IsGE X₁ n) (h₂LE : h.t.IsLE X₂ n)
  (h₂GE : h.t.IsGE X₂ n) (h₃LE : h.t.IsLE X₃ n) (h₃GE : h.t.IsGE X₃ n) :
  CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h X₂ =
    CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h X₁ +
      CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h X₃
CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_triangle_of_pure_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]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  [CategoryTheory.IsTriangulated C]
  {X₁ X₂ X₃ : C} {f : X₁ ⟶ X₂}
  {g : X₂ ⟶ X₃}
  {δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X₁}
  (n : ℤ)
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h₁LE : h.t.IsLE X₁ n)
  (h₁GE : h.t.IsGE X₁ n)
  (h₂LE : h.t.IsLE X₂ n)
  (h₂GE : h.t.IsGE X₂ n)
  (h₃LE : h.t.IsLE X₃ n)
  (h₃GE : h.t.IsGE X₃ n) :
  CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
      C h X₂ =
    CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
        C h X₁ +
      CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
        C h X₃

Something wrong, better idea? Suggest a change

12.7.53. eulerZObj_of_heart_shift🔗

For a heart object E and integer n, \texttt{eulerZObj}(E[-n]) = (-1)^{|n|} \cdot Z(E).

Proof: Uses \texttt{heartEulerClassObj\_of\_heart\_shift} and the definition of Z_{K_0} on \texttt{HeartK0}.

theorem

CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_of_heart_shift.{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) (n : ℤ) :
  CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h
      ((CategoryTheory.shiftFunctor C (-n)).obj E.obj) =
    (-1) ^ n.natAbs •
      CategoryTheory.Triangulated.HeartStabilityData.heartZObj C h E
CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_of_heart_shift.{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)
  (n : ℤ) :
  CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
      C h
      ((CategoryTheory.shiftFunctor C
            (-n)).obj
        E.obj) =
    (-1) ^ n.natAbs •
      CategoryTheory.Triangulated.HeartStabilityData.heartZObj
        C h E

Something wrong, better idea? Suggest a change

12.7.54. eulerZObj_additive_of_heart_shortExact🔗

The Euler-form central charge \texttt{eulerZObj} is additive over short exact sequences in the heart: for 0 \to A \to B \to Q \to 0, \texttt{eulerZObj}(B) = \texttt{eulerZObj}(A) + \texttt{eulerZObj}(Q).

Proof: Reduces to the linearity of Z_{K_0} over the heart Grothendieck group, using that \texttt{heartEulerClassObj} maps short exact sequences to the K_0 relation.

theorem

CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_additive_of_heart_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.HeartStabilityData.eulerZObj C h
      S.X₂.obj =
    CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h
        S.X₁.obj +
      CategoryTheory.Triangulated.HeartStabilityData.eulerZObj C h
        S.X₃.obj
CategoryTheory.Triangulated.HeartStabilityData.eulerZObj_additive_of_heart_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.HeartStabilityData.eulerZObj
      C h S.X₂.obj =
    CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
        C h S.X₁.obj +
      CategoryTheory.Triangulated.HeartStabilityData.eulerZObj
        C h S.X₃.obj

Something wrong, better idea? Suggest a change