Bridgeland Stability Conditions

12.6. HeartEquivalence: H0Homological🔗

12.6.1. truncGEObjShiftIso🔗

Shifting \tau^{\ge n} X by n identifies it with \tau^{\ge 0}(X[n]).

Construction: Constructed by comparing the shifted truncation triangle of X at level n with the truncation triangle of X[n] at level 0, using the uniqueness of the truncation up to a triangle isomorphism.

🔗def
CategoryTheory.Triangulated.TStructure.truncGEObjShiftIso.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) :
  (CategoryTheory.shiftFunctor C n).obj ((t.truncGE n).obj X) ≅
    (t.truncGE 0).obj ((CategoryTheory.shiftFunctor C n).obj X)
CategoryTheory.Triangulated.TStructure.truncGEObjShiftIso.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t :
    CategoryTheory.Triangulated.TStructure
      C)
  (n : ℤ) (X : C) :
  (CategoryTheory.shiftFunctor C n).obj
      ((t.truncGE n).obj X) ≅
    (t.truncGE 0).obj
      ((CategoryTheory.shiftFunctor C
            n).obj
        X)

Something wrong, better idea? Suggest a change

12.6.2. truncLEObjShiftIso🔗

Shifting \tau^{\le n} X by n identifies it with \tau^{\le 0}(X[n]).

Construction: Analogous to \texttt{truncGEObjShiftIso}: compares the shifted \le-truncation triangle with the \le 0-truncation of X[n].

🔗def
CategoryTheory.Triangulated.TStructure.truncLEObjShiftIso.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) :
  (CategoryTheory.shiftFunctor C n).obj ((t.truncLE n).obj X) ≅
    (t.truncLE 0).obj ((CategoryTheory.shiftFunctor C n).obj X)
CategoryTheory.Triangulated.TStructure.truncLEObjShiftIso.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t :
    CategoryTheory.Triangulated.TStructure
      C)
  (n : ℤ) (X : C) :
  (CategoryTheory.shiftFunctor C n).obj
      ((t.truncLE n).obj X) ≅
    (t.truncLE 0).obj
      ((CategoryTheory.shiftFunctor C
            n).obj
        X)

Something wrong, better idea? Suggest a change

12.6.3. truncGELEObjShiftIso🔗

Shifting the pure truncation \tau^{[n,n]} X by n identifies it with \tau^{[0,0]}(X[n]).

Construction: Composes the \ge-shift isomorphism applied to \tau^{\le n} X with the functorial image of the \le-shift isomorphism under \tau^{\ge 0}.

🔗def
CategoryTheory.Triangulated.TStructure.truncGELEObjShiftIso.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) :
  (CategoryTheory.shiftFunctor C n).obj ((t.truncGELE n n).obj X) ≅
    (t.truncGELE 0 0).obj ((CategoryTheory.shiftFunctor C n).obj X)
CategoryTheory.Triangulated.TStructure.truncGELEObjShiftIso.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t :
    CategoryTheory.Triangulated.TStructure
      C)
  (n : ℤ) (X : C) :
  (CategoryTheory.shiftFunctor C n).obj
      ((t.truncGELE n n).obj X) ≅
    (t.truncGELE 0 0).obj
      ((CategoryTheory.shiftFunctor C
            n).obj
        X)

Something wrong, better idea? Suggest a change

12.6.4. H0FunctorShiftObjIsoHeartCoh🔗

The shifted H^0_t object of X agrees with the degree-n heart cohomology object \texttt{heartCoh}(n, X).

Construction: Composes the tautological shift-sequence isomorphism with the shift-by-zero and pure-truncation-shift identifications.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.H0FunctorShiftObjIsoHeartCoh.{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 : ℤ)
  (X : C) :
  ((CategoryTheory.Triangulated.HeartStabilityData.H0Functor C h).shift
          n).obj
      X ≅
    CategoryTheory.Triangulated.HeartStabilityData.heartCoh C h n X
CategoryTheory.Triangulated.HeartStabilityData.H0FunctorShiftObjIsoHeartCoh.{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 : ℤ) (X : C) :
  ((CategoryTheory.Triangulated.HeartStabilityData.H0Functor
              C h).shift
          n).obj
      X ≅
    CategoryTheory.Triangulated.HeartStabilityData.heartCoh
      C h n X

Something wrong, better idea? Suggest a change

12.6.5. isIso_truncLT_pred_map_of_isGE🔗

If A \in \mathcal{C}^{\ge a} and A \to Z \to X_3 \to A[1] is distinguished, then \tau^{<a-1}(m_3) is an isomorphism.

Proof: The rotated triangle places A[1] \in \mathcal{C}^{\ge a-1}, so the \tau^{<a-1} functor kills the first vertex and the isomorphism follows from the induced two-term exact sequence.

🔗theorem
CategoryTheory.Triangulated.TStructure.isIso_truncLT_pred_map_of_isGE.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {a : ℤ} {A Z X₃ : C}
  [t.IsGE A a] {m₁ : A ⟶ Z} {m₃ : Z ⟶ X₃}
  {δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj A}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃ δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.IsIso ((t.truncLT (a - 1)).map m₃)
CategoryTheory.Triangulated.TStructure.isIso_truncLT_pred_map_of_isGE.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (t :
    CategoryTheory.Triangulated.TStructure
      C)
  {a : ℤ} {A Z X₃ : C} [t.IsGE A a]
  {m₁ : A ⟶ Z} {m₃ : Z ⟶ X₃}
  {δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        A}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        m₁ m₃ δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.IsIso
    ((t.truncLT (a - 1)).map m₃)

Something wrong, better idea? Suggest a change

12.6.6. exists_truncLT_octahedral_split🔗

For any distinguished triangle X_1 \to X_2 \to X_3 \to X_1[1] and integer a, the octahedral axiom produces a factorization through the truncation \tau^{\ge a} X_1.

Proof: Applies the octahedral axiom to the composition \tau^{<a} X_1 \hookrightarrow X_1 \to X_2, yielding an intermediate object Z and two new distinguished triangles relating Z to \tau^{\ge a} X_1 and X_3.

🔗theorem
CategoryTheory.Triangulated.TStructure.exists_truncLT_octahedral_split.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X₁ X₂ X₃ : C}
  {f : X₁ ⟶ X₂} {g : X₂ ⟶ X₃}
  {δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (a : ℤ) :
  ∃ Z v w m₁ m₃,
    CategoryTheory.Pretriangulated.Triangle.mk
          (CategoryTheory.CategoryStruct.comp ((t.truncLTι a).app X₁) f)
          v w ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃
            (CategoryTheory.CategoryStruct.comp δ
              ((CategoryTheory.shiftFunctor C 1).map
                ((t.truncGEπ a).app X₁))) ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles ∧
        CategoryTheory.CategoryStruct.comp ((t.truncGEπ a).app X₁) m₁ =
            CategoryTheory.CategoryStruct.comp f v ∧
          CategoryTheory.CategoryStruct.comp m₁ w =
              (t.truncGEδLT a).app X₁ ∧
            CategoryTheory.CategoryStruct.comp v m₃ = g
CategoryTheory.Triangulated.TStructure.exists_truncLT_octahedral_split.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (t :
    CategoryTheory.Triangulated.TStructure
      C)
  {X₁ X₂ X₃ : C} {f : X₁ ⟶ X₂}
  {g : X₂ ⟶ X₃}
  {δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X₁}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (a : ℤ) :
  ∃ Z v w m₁ m₃,
    CategoryTheory.Pretriangulated.Triangle.mk
          (CategoryTheory.CategoryStruct.comp
            ((t.truncLTι a).app X₁) f)
          v w ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Pretriangulated.Triangle.mk
            m₁ m₃
            (CategoryTheory.CategoryStruct.comp
              δ
              ((CategoryTheory.shiftFunctor
                    C 1).map
                ((t.truncGEπ a).app
                  X₁))) ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles ∧
        CategoryTheory.CategoryStruct.comp
              ((t.truncGEπ a).app X₁) m₁ =
            CategoryTheory.CategoryStruct.comp
              f v ∧
          CategoryTheory.CategoryStruct.comp
                m₁ w =
              (t.truncGEδLT a).app X₁ ∧
            CategoryTheory.CategoryStruct.comp
                v m₃ =
              g

Something wrong, better idea? Suggest a change

12.6.7. shortComplexOfDistTriangle_map_truncGEIsoOfSplit🔗

Given an octahedral splitting with \tau^{\ge 0}(v) an isomorphism, the \tau^{\ge 0}-images of the two short complexes (original and split) are isomorphic.

Construction: Builds a \texttt{ShortComplex.isoMk} from the isomorphism \tau^{\ge 0}(X_1) \cong \tau^{\ge 0}(\tau^{\ge 0}(X_1)) (idempotency) and \tau^{\ge 0}(v) (hypothesis), with commutativity checked from \texttt{hm_1} and \texttt{hm_3}.

🔗def
CategoryTheory.Triangulated.TStructure.shortComplexOfDistTriangle_map_truncGEIsoOfSplit.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C)
  [CategoryTheory.IsTriangulated C] {X₁ X₂ X₃ Z : C} {f : X₁ ⟶ X₂}
  {g : X₂ ⟶ X₃} {δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {v : X₂ ⟶ Z} {m₁ : (t.truncGE 0).obj X₁ ⟶ Z} {m₃ : Z ⟶ X₃}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT' :
    CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃
        (CategoryTheory.CategoryStruct.comp δ
          ((CategoryTheory.shiftFunctor C 1).map
            ((t.truncGEπ 0).app X₁))) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hm₁ :
    CategoryTheory.CategoryStruct.comp ((t.truncGEπ 0).app X₁) m₁ =
      CategoryTheory.CategoryStruct.comp f v)
  (hm₃ : CategoryTheory.CategoryStruct.comp v m₃ = g)
  (hvIso : CategoryTheory.IsIso ((t.truncGE 0).map v)) :
  (CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
          (CategoryTheory.Pretriangulated.Triangle.mk f g δ) hT).map
      (t.truncGE 0) ≅
    (CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
          (CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃
            (CategoryTheory.CategoryStruct.comp δ
              ((CategoryTheory.shiftFunctor C 1).map
                ((t.truncGEπ 0).app X₁))))
          hT').map
      (t.truncGE 0)
CategoryTheory.Triangulated.TStructure.shortComplexOfDistTriangle_map_truncGEIsoOfSplit.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t :
    CategoryTheory.Triangulated.TStructure
      C)
  [CategoryTheory.IsTriangulated C]
  {X₁ X₂ X₃ Z : C} {f : X₁ ⟶ X₂}
  {g : X₂ ⟶ X₃}
  {δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X₁}
  {v : X₂ ⟶ Z}
  {m₁ : (t.truncGE 0).obj X₁ ⟶ Z}
  {m₃ : Z ⟶ X₃}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT' :
    CategoryTheory.Pretriangulated.Triangle.mk
        m₁ m₃
        (CategoryTheory.CategoryStruct.comp
          δ
          ((CategoryTheory.shiftFunctor C
                1).map
            ((t.truncGEπ 0).app X₁))) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hm₁ :
    CategoryTheory.CategoryStruct.comp
        ((t.truncGEπ 0).app X₁) m₁ =
      CategoryTheory.CategoryStruct.comp f
        v)
  (hm₃ :
    CategoryTheory.CategoryStruct.comp v
        m₃ =
      g)
  (hvIso :
    CategoryTheory.IsIso
      ((t.truncGE 0).map v)) :
  (CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
          (CategoryTheory.Pretriangulated.Triangle.mk
            f g δ)
          hT).map
      (t.truncGE 0) ≅
    (CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
          (CategoryTheory.Pretriangulated.Triangle.mk
            m₁ m₃
            (CategoryTheory.CategoryStruct.comp
              δ
              ((CategoryTheory.shiftFunctor
                    C 1).map
                ((t.truncGEπ 0).app X₁))))
          hT').map
      (t.truncGE 0)

Something wrong, better idea? Suggest a change

12.6.8. truncGE_preadditiveCoyoneda_exact_iff_of_split🔗

For an octahedral splitting of a distinguished triangle, exactness of the \tau^{\ge 0}-coyoneda complex on the original triangle is equivalent to exactness on the split triangle.

Proof: Applies \texttt{shortComplexOfDistTriangle\_map\_truncGEIsoOfSplit} to get a comparison isomorphism, then uses \texttt{ShortComplex.exact\_iff\_of\_iso}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.truncGE_preadditiveCoyoneda_exact_iff_of_split.{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₃ Z : C} {f : X₁ ⟶ X₂}
  {g : X₂ ⟶ X₃} {δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {v : X₂ ⟶ Z} {m₁ : (h.t.truncGE 0).obj X₁ ⟶ Z} {m₃ : Z ⟶ X₃}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT' :
    CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃
        (CategoryTheory.CategoryStruct.comp δ
          ((CategoryTheory.shiftFunctor C 1).map
            ((h.t.truncGEπ 0).app X₁))) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hm₁ :
    CategoryTheory.CategoryStruct.comp ((h.t.truncGEπ 0).app X₁) m₁ =
      CategoryTheory.CategoryStruct.comp f v)
  (hm₃ : CategoryTheory.CategoryStruct.comp v m₃ = g)
  (hvIso : CategoryTheory.IsIso ((h.t.truncGE 0).map v))
  (E : h.t.heart.FullSubcategory) :
  ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
            (CategoryTheory.Pretriangulated.Triangle.mk f g δ) hT).map
        ((h.t.truncGE 0).comp
          (CategoryTheory.preadditiveCoyoneda.obj
            (Opposite.op E.obj)))).Exact ↔
    ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
            (CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃
              (CategoryTheory.CategoryStruct.comp δ
                ((CategoryTheory.shiftFunctor C 1).map
                  ((h.t.truncGEπ 0).app X₁))))
            hT').map
        ((h.t.truncGE 0).comp
          (CategoryTheory.preadditiveCoyoneda.obj
            (Opposite.op E.obj)))).Exact
CategoryTheory.Triangulated.HeartStabilityData.truncGE_preadditiveCoyoneda_exact_iff_of_split.{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₃ Z : C} {f : X₁ ⟶ X₂}
  {g : X₂ ⟶ X₃}
  {δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X₁}
  {v : X₂ ⟶ Z}
  {m₁ : (h.t.truncGE 0).obj X₁ ⟶ Z}
  {m₃ : Z ⟶ X₃}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT' :
    CategoryTheory.Pretriangulated.Triangle.mk
        m₁ m₃
        (CategoryTheory.CategoryStruct.comp
          δ
          ((CategoryTheory.shiftFunctor C
                1).map
            ((h.t.truncGEπ 0).app X₁))) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hm₁ :
    CategoryTheory.CategoryStruct.comp
        ((h.t.truncGEπ 0).app X₁) m₁ =
      CategoryTheory.CategoryStruct.comp f
        v)
  (hm₃ :
    CategoryTheory.CategoryStruct.comp v
        m₃ =
      g)
  (hvIso :
    CategoryTheory.IsIso
      ((h.t.truncGE 0).map v))
  (E : h.t.heart.FullSubcategory) :
  ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
            (CategoryTheory.Pretriangulated.Triangle.mk
              f g δ)
            hT).map
        ((h.t.truncGE 0).comp
          (CategoryTheory.preadditiveCoyoneda.obj
            (Opposite.op E.obj)))).Exact ↔
    ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
            (CategoryTheory.Pretriangulated.Triangle.mk
              m₁ m₃
              (CategoryTheory.CategoryStruct.comp
                δ
                ((CategoryTheory.shiftFunctor
                      C 1).map
                  ((h.t.truncGEπ 0).app
                    X₁))))
            hT').map
        ((h.t.truncGE 0).comp
          (CategoryTheory.preadditiveCoyoneda.obj
            (Opposite.op E.obj)))).Exact

Something wrong, better idea? Suggest a change

12.6.9. H0primeFunctor_preadditiveCoyoneda_exact_iff_octahedral_split🔗

For any distinguished triangle T and heart object E, exactness of H^0{}'-coyoneda on T is equivalent to exactness on the octahedral-split triangle; the octahedral split data exists for any T.

Proof: Applies \texttt{exists\_truncLT\_octahedral\_split} at level 0 to produce the split, checks that \tau^{\ge 0}(v) is an isomorphism (making the split exact condition transferable), and translates between the two exactness conditions via \texttt{H0primeFunctor\_preadditiveCoyoneda\_exact\_iff\_truncGE} and \texttt{truncGE\_preadditiveCoyoneda\_exact\_iff\_of\_split}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_preadditiveCoyoneda_exact_iff_octahedral_split.{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]
  (T : CategoryTheory.Pretriangulated.Triangle C)
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (E : h.t.heart.FullSubcategory) :
  ∃ Z v w m₁ m₃,
    ∃ (_ :
      CategoryTheory.Pretriangulated.Triangle.mk
          (CategoryTheory.CategoryStruct.comp
            ((h.t.truncLTι 0).app T.obj₁) T.mor₁)
          v w ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles)
      (h23 :
      CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃
          (CategoryTheory.CategoryStruct.comp T.mor₃
            ((CategoryTheory.shiftFunctor C 1).map
              ((h.t.truncGEπ 0).app T.obj₁))) ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles),
      CategoryTheory.CategoryStruct.comp ((h.t.truncGEπ 0).app T.obj₁)
            m₁ =
          CategoryTheory.CategoryStruct.comp T.mor₁ v ∧
        CategoryTheory.CategoryStruct.comp m₁ w =
            (h.t.truncGEδLT 0).app T.obj₁ ∧
          CategoryTheory.CategoryStruct.comp v m₃ = T.mor₂ ∧
            (((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
                      T hT).map
                  ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
                        C h).comp
                    (CategoryTheory.preadditiveCoyoneda.obj
                      (Opposite.op E)))).Exact ↔
              ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
                      (CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃
                        (CategoryTheory.CategoryStruct.comp T.mor₃
                          ((CategoryTheory.shiftFunctor C 1).map
                            ((h.t.truncGEπ 0).app T.obj₁))))
                      h23).map
                  ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
                        C h).comp
                    (CategoryTheory.preadditiveCoyoneda.obj
                      (Opposite.op E)))).Exact)
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_preadditiveCoyoneda_exact_iff_octahedral_split.{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]
  (T :
    CategoryTheory.Pretriangulated.Triangle
      C)
  (hT :
    T ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (E : h.t.heart.FullSubcategory) :
  ∃ Z v w m₁ m₃,
    ∃ (_ :
      CategoryTheory.Pretriangulated.Triangle.mk
          (CategoryTheory.CategoryStruct.comp
            ((h.t.truncLTι 0).app T.obj₁)
            T.mor₁)
          v w ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles)
      (h23 :
      CategoryTheory.Pretriangulated.Triangle.mk
          m₁ m₃
          (CategoryTheory.CategoryStruct.comp
            T.mor₃
            ((CategoryTheory.shiftFunctor
                  C 1).map
              ((h.t.truncGEπ 0).app
                T.obj₁))) ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles),
      CategoryTheory.CategoryStruct.comp
            ((h.t.truncGEπ 0).app T.obj₁)
            m₁ =
          CategoryTheory.CategoryStruct.comp
            T.mor₁ v ∧
        CategoryTheory.CategoryStruct.comp
              m₁ w =
            (h.t.truncGEδLT 0).app
              T.obj₁ ∧
          CategoryTheory.CategoryStruct.comp
                v m₃ =
              T.mor₂ ∧
            (((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
                      T hT).map
                  ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
                        C h).comp
                    (CategoryTheory.preadditiveCoyoneda.obj
                      (Opposite.op
                        E)))).Exact ↔
              ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
                      (CategoryTheory.Pretriangulated.Triangle.mk
                        m₁ m₃
                        (CategoryTheory.CategoryStruct.comp
                          T.mor₃
                          ((CategoryTheory.shiftFunctor
                                C 1).map
                            ((h.t.truncGEπ
                                  0).app
                              T.obj₁))))
                      h23).map
                  ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
                        C h).comp
                    (CategoryTheory.preadditiveCoyoneda.obj
                      (Opposite.op
                        E)))).Exact)

Something wrong, better idea? Suggest a change

12.6.10. exists_toH0primeHom_eq_of_obstruction_zero🔗

If \beta.\mathrm{hom} \circ \iota_{\le 0} \circ (\tau^{\ge 0} \to X)_{\mathrm{conn}} = 0 (the obstruction vanishes), then \beta = \texttt{toH0primeHom}(f) for some f : E_{\mathrm{obj}} \to X.

Proof: Lifts \beta.\mathrm{hom} \circ \iota_{\le 0} to a morphism into X via the exactness of the \tau^{\ge 0}-triangle and the vanishing obstruction, then identifies the lift with \texttt{toH0primeHom}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.exists_toH0primeHom_eq_of_obstruction_zero.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X : C}
  (β : E ⟶ CategoryTheory.Triangulated.HeartStabilityData.H0prime C h X)
  (hβ :
    CategoryTheory.CategoryStruct.comp β.hom
        (CategoryTheory.CategoryStruct.comp
          ((h.t.truncLEι 0).app ((h.t.truncGE 0).obj X))
          ((h.t.truncGEδLT 0).app X)) =
      0) :
  ∃ f,
    β =
      CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom C h E
        f
CategoryTheory.Triangulated.HeartStabilityData.exists_toH0primeHom_eq_of_obstruction_zero.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) {X : C}
  (β :
    E ⟶
      CategoryTheory.Triangulated.HeartStabilityData.H0prime
        C h X)
  (hβ :
    CategoryTheory.CategoryStruct.comp
        β.hom
        (CategoryTheory.CategoryStruct.comp
          ((h.t.truncLEι 0).app
            ((h.t.truncGE 0).obj X))
          ((h.t.truncGEδLT 0).app X)) =
      0) :
  ∃ f,
    β =
      CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom
        C h E f

Something wrong, better idea? Suggest a change

12.6.11. comp_H0primeFunctor_map_eq_zero_iff🔗

A morphism \beta \circ H^0{}'(g) = 0 in the heart if and only if \beta.\mathrm{hom} \circ \iota_{\le 0} \circ \tau^{\ge 0}(g) = 0 in \mathcal{C}.

Proof: Both directions use naturality of \iota_{\le 0} and \texttt{hom\_ext\_toH0prime} to pass between the heart and ambient-category conditions.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.comp_H0primeFunctor_map_eq_zero_iff.{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) {X Y : C}
  (β : E ⟶ CategoryTheory.Triangulated.HeartStabilityData.H0prime C h X)
  (g : X ⟶ Y) :
  CategoryTheory.CategoryStruct.comp β
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).map
          g) =
      0 ↔
    CategoryTheory.CategoryStruct.comp β.hom
        (CategoryTheory.CategoryStruct.comp
          ((h.t.truncLEι 0).app ((h.t.truncGE 0).obj X))
          ((h.t.truncGE 0).map g)) =
      0
CategoryTheory.Triangulated.HeartStabilityData.comp_H0primeFunctor_map_eq_zero_iff.{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)
  {X Y : C}
  (β :
    E ⟶
      CategoryTheory.Triangulated.HeartStabilityData.H0prime
        C h X)
  (g : X ⟶ Y) :
  CategoryTheory.CategoryStruct.comp β
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).map
          g) =
      0 ↔
    CategoryTheory.CategoryStruct.comp
        β.hom
        (CategoryTheory.CategoryStruct.comp
          ((h.t.truncLEι 0).app
            ((h.t.truncGE 0).obj X))
          ((h.t.truncGE 0).map g)) =
      0

Something wrong, better idea? Suggest a change

12.6.12. toH0primeHom_eq_zero_iff🔗

The canonical lift \texttt{toH0primeHom}(f) = 0 if and only if f \circ \pi_{\ge 0} = 0.

Proof: Both directions use \texttt{hom\_ext\_toH0prime} together with \texttt{toH0primeHom\_hom}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_eq_zero_iff.{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) {X : C} (f : E.obj ⟶ X) :
  CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom C h E f =
      0 ↔
    CategoryTheory.CategoryStruct.comp f ((h.t.truncGEπ 0).app X) = 0
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_eq_zero_iff.{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) {X : C}
  (f : E.obj ⟶ X) :
  CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom
        C h E f =
      0 ↔
    CategoryTheory.CategoryStruct.comp f
        ((h.t.truncGEπ 0).app X) =
      0

Something wrong, better idea? Suggest a change

12.6.13. isZero_H0prime_of_isGE_one🔗

For X \in \mathcal{C}^{\ge 1}, the object H^0{}'(X) is zero.

Proof: The underlying object \tau^{\le 0}(\tau^{\ge 0}(X)) vanishes because \tau^{\ge 0}(X) \in \mathcal{C}^{\ge 0} and \tau^{\le 0} of an object in \mathcal{C}^{\ge 1} is zero.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.isZero_H0prime_of_isGE_one.{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)
  [inst : CategoryTheory.IsTriangulated C] {X : C} [h.t.IsGE X 1] :
  CategoryTheory.Limits.IsZero
    (CategoryTheory.Triangulated.HeartStabilityData.H0prime C h X)
CategoryTheory.Triangulated.HeartStabilityData.isZero_H0prime_of_isGE_one.{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)
  [inst : CategoryTheory.IsTriangulated C]
  {X : C} [h.t.IsGE X 1] :
  CategoryTheory.Limits.IsZero
    (CategoryTheory.Triangulated.HeartStabilityData.H0prime
      C h X)

Something wrong, better idea? Suggest a change

12.6.14. H0primeFunctor_preadditiveCoyoneda_exact_of_isIso_truncLT_map🔗

If \tau^{<0}(m_3) is an isomorphism in a distinguished triangle A \to Z \to X_3, then the H^0{}'-coyoneda short complex on the triangle is exact.

Proof: Using the isomorphism of \tau^{<0}(m_3), lifts a kernel element \beta (with \beta \circ H^0{}'(m_3) = 0) to a morphism f : E \to Z via the obstruction-zero lifting lemma \texttt{exists\_toH0primeHom\_eq\_of\_obstruction\_zero}, then constructs a preimage via \texttt{Triangle.coyoneda\_exact}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_preadditiveCoyoneda_exact_of_isIso_truncLT_map.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) {A Z X₃ : C}
  {m₁ : A ⟶ Z} {m₃ : Z ⟶ X₃}
  {δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj A}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃ δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hm₃LT : CategoryTheory.IsIso ((h.t.truncLT 0).map m₃))
  (E : h.t.heart.FullSubcategory) :
  ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
          (CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃ δ) hT).map
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
            h).comp
        (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op E)))).Exact
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_preadditiveCoyoneda_exact_of_isIso_truncLT_map.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {A Z X₃ : C} {m₁ : A ⟶ Z} {m₃ : Z ⟶ X₃}
  {δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        A}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        m₁ m₃ δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hm₃LT :
    CategoryTheory.IsIso
      ((h.t.truncLT 0).map m₃))
  (E : h.t.heart.FullSubcategory) :
  ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
          (CategoryTheory.Pretriangulated.Triangle.mk
            m₁ m₃ δ)
          hT).map
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
            C h).comp
        (CategoryTheory.preadditiveCoyoneda.obj
          (Opposite.op E)))).Exact

Something wrong, better idea? Suggest a change

12.6.15. H0primeFunctor_preadditiveCoyoneda_exact_of_isGE_one🔗

For a distinguished triangle with first vertex A \in \mathcal{C}^{\ge 1}, the short complex obtained by applying H^0{}' and the preadditive coyoneda is exact.

Proof: The map \tau^{<0}(m_3) is an isomorphism because A[1] \in \mathcal{C}^{\ge 0} forces the rotated-triangle first vertex to be in \mathcal{C}^{\ge 0}. The result follows from \texttt{H0primeFunctor\_preadditiveCoyoneda\_exact\_of\_isIso\_truncLT\_map}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_preadditiveCoyoneda_exact_of_isGE_one.{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] {A Z X₃ : C} [h.t.IsGE A 1]
  {m₁ : A ⟶ Z} {m₃ : Z ⟶ X₃}
  {δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj A}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃ δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (E : h.t.heart.FullSubcategory) :
  ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
          (CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃ δ) hT).map
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
            h).comp
        (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op E)))).Exact
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_preadditiveCoyoneda_exact_of_isGE_one.{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]
  {A Z X₃ : C} [h.t.IsGE A 1] {m₁ : A ⟶ Z}
  {m₃ : Z ⟶ X₃}
  {δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        A}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        m₁ m₃ δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (E : h.t.heart.FullSubcategory) :
  ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
          (CategoryTheory.Pretriangulated.Triangle.mk
            m₁ m₃ δ)
          hT).map
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
            C h).comp
        (CategoryTheory.preadditiveCoyoneda.obj
          (Opposite.op E)))).Exact

Something wrong, better idea? Suggest a change

12.6.16. H0primeFunctor_preadditiveCoyoneda_exact_of_split_one🔗

Given an octahedral split of a distinguished triangle at level 1, if the short triangle from \tau^{<1}(A) gives an exact H^0{}'-coyoneda complex, then so does the original triangle.

Proof: The split triangle with first vertex \tau^{\ge 1}(A) is exact by \texttt{H0primeFunctor\_preadditiveCoyoneda\_exact\_of\_isGE\_one}. Combines both exactness statements to lift kernel elements in the original complex.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_preadditiveCoyoneda_exact_of_split_one.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) {A X₂ X₃ Z : C}
  {f : A ⟶ X₂} {g : X₂ ⟶ X₃}
  {δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj A} {v : X₂ ⟶ Z}
  {w :
    Z ⟶ (CategoryTheory.shiftFunctor C 1).obj ((h.t.truncLT 1).obj A)}
  {m₁ : (h.t.truncGE 1).obj A ⟶ Z} {m₃ : Z ⟶ X₃}
  (E : h.t.heart.FullSubcategory)
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h13 :
    CategoryTheory.Pretriangulated.Triangle.mk
        (CategoryTheory.CategoryStruct.comp ((h.t.truncLTι 1).app A) f)
        v w ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h23 :
    CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃
        (CategoryTheory.CategoryStruct.comp δ
          ((CategoryTheory.shiftFunctor C 1).map
            ((h.t.truncGEπ 1).app A))) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hm₃ : CategoryTheory.CategoryStruct.comp v m₃ = g)
  (hex13 :
    ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
            (CategoryTheory.Pretriangulated.Triangle.mk
              (CategoryTheory.CategoryStruct.comp
                ((h.t.truncLTι 1).app A) f)
              v w)
            h13).map
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).comp
          (CategoryTheory.preadditiveCoyoneda.obj
            (Opposite.op E)))).Exact) :
  ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
          (CategoryTheory.Pretriangulated.Triangle.mk f g δ) hT).map
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
            h).comp
        (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op E)))).Exact
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_preadditiveCoyoneda_exact_of_split_one.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {A X₂ X₃ Z : C} {f : A ⟶ X₂}
  {g : X₂ ⟶ X₃}
  {δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        A}
  {v : X₂ ⟶ Z}
  {w :
    Z ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        ((h.t.truncLT 1).obj A)}
  {m₁ : (h.t.truncGE 1).obj A ⟶ Z}
  {m₃ : Z ⟶ X₃}
  (E : h.t.heart.FullSubcategory)
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h13 :
    CategoryTheory.Pretriangulated.Triangle.mk
        (CategoryTheory.CategoryStruct.comp
          ((h.t.truncLTι 1).app A) f)
        v w ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h23 :
    CategoryTheory.Pretriangulated.Triangle.mk
        m₁ m₃
        (CategoryTheory.CategoryStruct.comp
          δ
          ((CategoryTheory.shiftFunctor C
                1).map
            ((h.t.truncGEπ 1).app A))) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hm₃ :
    CategoryTheory.CategoryStruct.comp v
        m₃ =
      g)
  (hex13 :
    ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
            (CategoryTheory.Pretriangulated.Triangle.mk
              (CategoryTheory.CategoryStruct.comp
                ((h.t.truncLTι 1).app A)
                f)
              v w)
            h13).map
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).comp
          (CategoryTheory.preadditiveCoyoneda.obj
            (Opposite.op E)))).Exact) :
  ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
          (CategoryTheory.Pretriangulated.Triangle.mk
            f g δ)
          hT).map
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
            C h).comp
        (CategoryTheory.preadditiveCoyoneda.obj
          (Opposite.op E)))).Exact

Something wrong, better idea? Suggest a change

12.6.17. H0primeFunctor_preadditiveCoyoneda_exact_of_isGE_zero_of_heart_case🔗

For a distinguished triangle with first vertex A \in \mathcal{C}^{\ge 0}, if exactness holds for all heart-source triangles, then the H^0{}'-coyoneda short complex is exact.

Proof: Applies the octahedral split at level 1 to reduce to a heart-source triangle (via \tau^{<1}(A) \in \operatorname{heart}) and a triangle with first vertex \tau^{\ge 1}(A) \in \mathcal{C}^{\ge 1}, then combines via \texttt{H0primeFunctor\_preadditiveCoyoneda\_exact\_of\_split\_one}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_preadditiveCoyoneda_exact_of_isGE_zero_of_heart_case.{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] {A X₂ X₃ : C} [h.t.IsGE A 0]
  {f : A ⟶ X₂} {g : X₂ ⟶ X₃}
  {δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj A}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (E : h.t.heart.FullSubcategory)
  (hHeart :
    ∀ (A0 : h.t.heart.FullSubcategory) {Y₂ Y₃ : C} {f0 : A0.obj ⟶ Y₂}
      {g0 : Y₂ ⟶ Y₃}
      {δ0 : Y₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj A0.obj}
      (hT0 :
        CategoryTheory.Pretriangulated.Triangle.mk f0 g0 δ0 ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles),
      ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
              (CategoryTheory.Pretriangulated.Triangle.mk f0 g0 δ0)
              hT0).map
          ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
                C h).comp
            (CategoryTheory.preadditiveCoyoneda.obj
              (Opposite.op E)))).Exact) :
  ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
          (CategoryTheory.Pretriangulated.Triangle.mk f g δ) hT).map
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
            h).comp
        (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op E)))).Exact
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_preadditiveCoyoneda_exact_of_isGE_zero_of_heart_case.{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]
  {A X₂ X₃ : C} [h.t.IsGE A 0]
  {f : A ⟶ X₂} {g : X₂ ⟶ X₃}
  {δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        A}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (E : h.t.heart.FullSubcategory)
  (hHeart :
    ∀ (A0 : h.t.heart.FullSubcategory)
      {Y₂ Y₃ : C} {f0 : A0.obj ⟶ Y₂}
      {g0 : Y₂ ⟶ Y₃}
      {δ0 :
        Y₃ ⟶
          (CategoryTheory.shiftFunctor C
                1).obj
            A0.obj}
      (hT0 :
        CategoryTheory.Pretriangulated.Triangle.mk
            f0 g0 δ0 ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles),
      ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
              (CategoryTheory.Pretriangulated.Triangle.mk
                f0 g0 δ0)
              hT0).map
          ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
                C h).comp
            (CategoryTheory.preadditiveCoyoneda.obj
              (Opposite.op E)))).Exact) :
  ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
          (CategoryTheory.Pretriangulated.Triangle.mk
            f g δ)
          hT).map
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
            C h).comp
        (CategoryTheory.preadditiveCoyoneda.obj
          (Opposite.op E)))).Exact

Something wrong, better idea? Suggest a change

12.6.18. isIso_truncLT_negOne_map_of_heart_source🔗

For a distinguished triangle A \to X_2 \to X_3 with A in the heart, the map \tau^{<(-1)}(g) is an isomorphism.

Proof: The connecting morphism in the rotated triangle lies in \mathcal{C}^{\ge -1} (since A[1] \in \mathcal{C}^{\ge -1}), so \texttt{isIso₁\_truncLT\_map\_of\_isGE} applies to give the isomorphism.

🔗theorem
CategoryTheory.Triangulated.TStructure.isIso_truncLT_negOne_map_of_heart_source.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C)
  (A : t.heart.FullSubcategory) {X₂ X₃ : C} {f : A.obj ⟶ X₂}
  {g : X₂ ⟶ X₃} {δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj A.obj}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.IsIso ((t.truncLT (-1)).map g)
CategoryTheory.Triangulated.TStructure.isIso_truncLT_negOne_map_of_heart_source.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (t :
    CategoryTheory.Triangulated.TStructure
      C)
  (A : t.heart.FullSubcategory)
  {X₂ X₃ : C} {f : A.obj ⟶ X₂}
  {g : X₂ ⟶ X₃}
  {δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        A.obj}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.IsIso
    ((t.truncLT (-1)).map g)

Something wrong, better idea? Suggest a change

12.6.19. isZero_H0Functor_shift_obj_of_lt_bound🔗

H^m_t(X) = 0 when m < n and X \in \mathcal{C}^{\ge n}.

Proof: The pure truncation \tau^{[m,m]} X vanishes because \tau^{\le m} X = 0 for m < n when X \in \mathcal{C}^{\ge n}. The heart cohomology object, being a shift of this zero object, is also zero.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.isZero_H0Functor_shift_obj_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)
  [inst : CategoryTheory.IsTriangulated C] {X : C} {m n : ℤ}
  (hmn : m < n) (hGE : h.t.IsGE X n) :
  CategoryTheory.Limits.IsZero
    (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
              h).shift
          m).obj
      X)
CategoryTheory.Triangulated.HeartStabilityData.isZero_H0Functor_shift_obj_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)
  [inst : CategoryTheory.IsTriangulated C]
  {X : C} {m n : ℤ} (hmn : m < n)
  (hGE : h.t.IsGE X n) :
  CategoryTheory.Limits.IsZero
    (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor
              C h).shift
          m).obj
      X)

Something wrong, better idea? Suggest a change

12.6.20. isZero_H0Functor_shift_obj_of_gt_bound🔗

H^m_t(X) = 0 when m > n and X \in \mathcal{C}^{\le n}.

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 when X \in \mathcal{C}^{\le n}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.isZero_H0Functor_shift_obj_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)
  [inst : CategoryTheory.IsTriangulated C] {X : C} {m n : ℤ}
  (hmn : n < m) (hLE : h.t.IsLE X n) :
  CategoryTheory.Limits.IsZero
    (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
              h).shift
          m).obj
      X)
CategoryTheory.Triangulated.HeartStabilityData.isZero_H0Functor_shift_obj_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)
  [inst : CategoryTheory.IsTriangulated C]
  {X : C} {m n : ℤ} (hmn : n < m)
  (hLE : h.t.IsLE X n) :
  CategoryTheory.Limits.IsZero
    (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor
              C h).shift
          m).obj
      X)

Something wrong, better idea? Suggest a change

12.6.21. eq_zero_congr_hasZeroMorphisms🔗

The vanishing of a morphism f = 0 is independent of the choice of \texttt{HasZeroMorphisms} instance, since there is at most one such instance.

Proof: Uses \texttt{Subsingleton.elim} to unify the two zero-morphism structures.

🔗theorem
CategoryTheory.Triangulated.eq_zero_congr_hasZeroMorphisms.{u_1, u_2}
  {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D]
  (I J : CategoryTheory.Limits.HasZeroMorphisms D) {X Y : D} {f : X ⟶ Y}
  (h : f = 0) : f = 0
CategoryTheory.Triangulated.eq_zero_congr_hasZeroMorphisms.{u_1,
    u_2}
  {D : Type u_1}
  [CategoryTheory.Category.{u_2, u_1} D]
  (I J :
    CategoryTheory.Limits.HasZeroMorphisms
      D)
  {X Y : D} {f : X ⟶ Y} (h : f = 0) :
  f = 0

Something wrong, better idea? Suggest a change

12.6.22. shortComplex_exact_congr_hasZeroMorphisms🔗

Exactness of a short complex is independent of the choice of \texttt{HasZeroMorphisms} instance.

Proof: Uses \texttt{Subsingleton.elim} to unify the two instances, then the zero-composite witnesses.

🔗theorem
CategoryTheory.Triangulated.shortComplex_exact_congr_hasZeroMorphisms.{u_1,
    u_2}
  {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D]
  (I J : CategoryTheory.Limits.HasZeroMorphisms D) {X₁ X₂ X₃ : D}
  {f : X₁ ⟶ X₂} {g : X₂ ⟶ X₃}
  {wI : CategoryTheory.CategoryStruct.comp f g = 0}
  {wJ : CategoryTheory.CategoryStruct.comp f g = 0}
  (h :
    { X₁ := X₁, X₂ := X₂, X₃ := X₃, f := f, g := g,
        zero := wI }.Exact) :
  { X₁ := X₁, X₂ := X₂, X₃ := X₃, f := f, g := g, zero := wJ }.Exact
CategoryTheory.Triangulated.shortComplex_exact_congr_hasZeroMorphisms.{u_1,
    u_2}
  {D : Type u_1}
  [CategoryTheory.Category.{u_2, u_1} D]
  (I J :
    CategoryTheory.Limits.HasZeroMorphisms
      D)
  {X₁ X₂ X₃ : D} {f : X₁ ⟶ X₂}
  {g : X₂ ⟶ X₃}
  {wI :
    CategoryTheory.CategoryStruct.comp f
        g =
      0}
  {wJ :
    CategoryTheory.CategoryStruct.comp f
        g =
      0}
  (h :
    { X₁ := X₁, X₂ := X₂, X₃ := X₃,
        f := f, g := g,
        zero := wI }.Exact) :
  { X₁ := X₁, X₂ := X₂, X₃ := X₃, f := f,
      g := g, zero := wJ }.Exact

Something wrong, better idea? Suggest a change

12.6.23. exact_of_eval🔗

A short complex S of functors J \to A (with A abelian) is exact if and only if for every object j \in J the evaluation S_j is exact.

Proof: Reduces to checking that the kernel lift is epi on each evaluation using \texttt{NatTrans.epi\_iff\_epi\_app}, the kernel comparison isomorphism, and the given evaluation exactness.

🔗theorem
CategoryTheory.Triangulated.ShortComplex.exact_of_eval.{u_1, u_2, u_3,
    u_4}
  {J : Type u_1} [CategoryTheory.Category.{u_3, u_1} J] {A : Type u_2}
  [CategoryTheory.Category.{u_4, u_2} A] [CategoryTheory.Abelian A]
  (S : CategoryTheory.ShortComplex (CategoryTheory.Functor J A))
  (hS :
    ∀ (j : J), (S.map ((CategoryTheory.evaluation J A).obj j)).Exact) :
  S.Exact
CategoryTheory.Triangulated.ShortComplex.exact_of_eval.{u_1,
    u_2, u_3, u_4}
  {J : Type u_1}
  [CategoryTheory.Category.{u_3, u_1} J]
  {A : Type u_2}
  [CategoryTheory.Category.{u_4, u_2} A]
  [CategoryTheory.Abelian A]
  (S :
    CategoryTheory.ShortComplex
      (CategoryTheory.Functor J A))
  (hS :
    ∀ (j : J),
      (S.map
          ((CategoryTheory.evaluation J
                A).obj
            j)).Exact) :
  S.Exact

Something wrong, better idea? Suggest a change

12.6.24. preadditiveCoyoneda_exact_of_f_is_kernel🔗

If the first map of a short complex S in a preadditive category is a kernel, then the complex is exact after applying the preadditive coyoneda functor.

Proof: Given a kernel element \beta with \beta \circ S.g = 0, lifts \beta through the kernel universal property and checks the factorization.

🔗theorem
CategoryTheory.Triangulated.ShortComplex.preadditiveCoyoneda_exact_of_f_is_kernel.{u_1,
    u_2}
  {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D]
  [CategoryTheory.Preadditive D] {S : CategoryTheory.ShortComplex D}
  (hS :
    CategoryTheory.Limits.IsLimit
      (CategoryTheory.Limits.KernelFork.ofι S.f ⋯))
  (E : D) :
  (S.map (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op E))).Exact
CategoryTheory.Triangulated.ShortComplex.preadditiveCoyoneda_exact_of_f_is_kernel.{u_1,
    u_2}
  {D : Type u_1}
  [CategoryTheory.Category.{u_2, u_1} D]
  [CategoryTheory.Preadditive D]
  {S : CategoryTheory.ShortComplex D}
  (hS :
    CategoryTheory.Limits.IsLimit
      (CategoryTheory.Limits.KernelFork.ofι
        S.f ⋯))
  (E : D) :
  (S.map
      (CategoryTheory.preadditiveCoyoneda.obj
        (Opposite.op E))).Exact

Something wrong, better idea? Suggest a change

12.6.25. H0primeFunctor_comp_preadditiveYoneda_eval🔗

The composite H^0{}' followed by the preadditive Yoneda, evaluated at a heart object E, is the same as H^0{}' followed by the preadditive coyoneda at E.

Proof: This is a definitional equality (\texttt{rfl}).

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_comp_preadditiveYoneda_eval.{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.H0primeFunctor C
              h).comp
          CategoryTheory.preadditiveYoneda).comp
      ((CategoryTheory.evaluation h.t.heart.FullSubcategoryᵒᵖ
            AddCommGrpCat).obj
        (Opposite.op E)) =
    (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
          h).comp
      (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op E))
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_comp_preadditiveYoneda_eval.{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.H0primeFunctor
              C h).comp
          CategoryTheory.preadditiveYoneda).comp
      ((CategoryTheory.evaluation
            h.t.heart.FullSubcategoryᵒᵖ
            AddCommGrpCat).obj
        (Opposite.op E)) =
    (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
          C h).comp
      (CategoryTheory.preadditiveCoyoneda.obj
        (Opposite.op E))

Something wrong, better idea? Suggest a change

12.6.26. H0primeFunctor_preadditiveYoneda_isHomological_of_eval🔗

If for every distinguished triangle and every heart object the H^0{}'-coyoneda complex is exact, then H^0{}' composed with the preadditive Yoneda is a homological functor.

Proof: Reduces to checking exactness on each evaluation functor \mathcal{C} \to \mathbf{Ab} via \texttt{ShortComplex.exact\_of\_eval} and the provided hypothesis.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_preadditiveYoneda_isHomological_of_eval.{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)
  (hExact :
    ∀ (T : CategoryTheory.Pretriangulated.Triangle C)
      (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
      (E : h.t.heart.FullSubcategory),
      ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T
              hT).map
          ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
                C h).comp
            (CategoryTheory.preadditiveCoyoneda.obj
              (Opposite.op E)))).Exact) :
  ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
          h).comp
      CategoryTheory.preadditiveYoneda).IsHomological
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_preadditiveYoneda_isHomological_of_eval.{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)
  (hExact :
    ∀
      (T :
        CategoryTheory.Pretriangulated.Triangle
          C)
      (hT :
        T ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles)
      (E : h.t.heart.FullSubcategory),
      ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
              T hT).map
          ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
                C h).comp
            (CategoryTheory.preadditiveCoyoneda.obj
              (Opposite.op E)))).Exact) :
  ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
          C h).comp
      CategoryTheory.preadditiveYoneda).IsHomological

Something wrong, better idea? Suggest a change

12.6.27. H0primeFunctor_isHomological_of_preadditiveYoneda🔗

If H^0{}' composed with the preadditive Yoneda is a homological functor, then H^0{}' itself is homological.

Proof: The preadditive Yoneda is faithful, so exact sequences are reflected; applies \texttt{Functor.reflects\_exact\_of\_faithful}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_isHomological_of_preadditiveYoneda.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  [CategoryTheory.IsTriangulated C]
  [((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
            h).comp
        CategoryTheory.preadditiveYoneda).IsHomological] :
  (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
      h).IsHomological
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_isHomological_of_preadditiveYoneda.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  [CategoryTheory.IsTriangulated C]
  [((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
            C h).comp
        CategoryTheory.preadditiveYoneda).IsHomological] :
  (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
      C h).IsHomological

Something wrong, better idea? Suggest a change

12.6.28. H0Functor_isHomological_of_H0primeFunctor🔗

If H^0{}' is a homological functor, then so is H^0_t (via the natural isomorphism H^0_t \cong H^0{}').

Proof: Applies \texttt{Functor.IsHomological.of\_iso} to the inverse of \texttt{H0FunctorIsoH0primeFunctor}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_isHomological_of_H0primeFunctor.{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.HeartStabilityData.H0primeFunctor C
        h).IsHomological] :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
      h).IsHomological
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_isHomological_of_H0primeFunctor.{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.HeartStabilityData.H0primeFunctor
        C h).IsHomological] :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor
      C h).IsHomological

Something wrong, better idea? Suggest a change

12.6.29. H0Functor_isHomological_of_eval🔗

If the preadditive-coyoneda evaluations of H^0{}' are all exact on distinguished triangles, then H^0_t is a homological functor.

Proof: Assembles the argument: first shows H^0{}' composed with the preadditive Yoneda is homological (via \texttt{H0primeFunctor\_preadditiveYoneda\_isHomological\_of\_eval}), then applies \texttt{H0primeFunctor\_isHomological\_of\_preadditiveYoneda} and \texttt{H0Functor\_isHomological\_of\_H0primeFunctor}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_isHomological_of_eval.{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]
  (hExact :
    ∀ (T : CategoryTheory.Pretriangulated.Triangle C)
      (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
      (E : h.t.heart.FullSubcategory),
      ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T
              hT).map
          ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
                C h).comp
            (CategoryTheory.preadditiveCoyoneda.obj
              (Opposite.op E)))).Exact) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
      h).IsHomological
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_isHomological_of_eval.{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]
  (hExact :
    ∀
      (T :
        CategoryTheory.Pretriangulated.Triangle
          C)
      (hT :
        T ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles)
      (E : h.t.heart.FullSubcategory),
      ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
              T hT).map
          ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
                C h).comp
            (CategoryTheory.preadditiveCoyoneda.obj
              (Opposite.op E)))).Exact) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor
      C h).IsHomological

Something wrong, better idea? Suggest a change

12.6.30. H0Functor_isHomological_of_eval_of_heart_case🔗

It suffices to verify exactness only for distinguished triangles whose first vertex lies in the heart: if those cases hold, then H^0_t is a homological functor.

Proof: Uses \texttt{H0primeFunctor\_preadditiveCoyoneda\_exact\_iff\_octahedral\_split} to reduce the general case to the heart-source case via the octahedral split, then applies \texttt{H0Functor\_isHomological\_of\_eval}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_isHomological_of_eval_of_heart_case.{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]
  (hHeart :
    ∀ (A : h.t.heart.FullSubcategory) {X₂ X₃ : C} {f : A.obj ⟶ X₂}
      {g : X₂ ⟶ X₃}
      {δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj A.obj}
      (hT :
        CategoryTheory.Pretriangulated.Triangle.mk f g δ ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles)
      (E : h.t.heart.FullSubcategory),
      ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
              (CategoryTheory.Pretriangulated.Triangle.mk f g δ) hT).map
          ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
                C h).comp
            (CategoryTheory.preadditiveCoyoneda.obj
              (Opposite.op E)))).Exact) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
      h).IsHomological
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_isHomological_of_eval_of_heart_case.{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]
  (hHeart :
    ∀ (A : h.t.heart.FullSubcategory)
      {X₂ X₃ : C} {f : A.obj ⟶ X₂}
      {g : X₂ ⟶ X₃}
      {δ :
        X₃ ⟶
          (CategoryTheory.shiftFunctor C
                1).obj
            A.obj}
      (hT :
        CategoryTheory.Pretriangulated.Triangle.mk
            f g δ ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles)
      (E : h.t.heart.FullSubcategory),
      ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
              (CategoryTheory.Pretriangulated.Triangle.mk
                f g δ)
              hT).map
          ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
                C h).comp
            (CategoryTheory.preadditiveCoyoneda.obj
              (Opposite.op E)))).Exact) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor
      C h).IsHomological

Something wrong, better idea? Suggest a change

12.6.31. mapHomologicalFunctor🔗

A homological functor F on a triangulated category \mathcal{C} maps a spectral object indexed by \iota to an abelian spectral object by applying the long exact cohomology sequence.

Construction: Sets H_n := \omega_1 \circ F[n] and the connecting maps from F's homology-sequence morphisms; exactness at each position follows from the three exactness axioms of a homological functor.

🔗def
CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctor.{v, u,
    u_1, u_2, u_3, u_4}
  (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] {ι : Type u_1}
  [CategoryTheory.Category.{u_3, u_1} ι] {A : Type u_2}
  [CategoryTheory.Category.{u_4, u_2} A] [CategoryTheory.Abelian A]
  (X : CategoryTheory.Triangulated.SpectralObject C ι)
  (F : CategoryTheory.Functor C A) [F.IsHomological]
  [F.ShiftSequence ℤ] : CategoryTheory.Abelian.SpectralObject A ι
CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctor.{v,
    u, u_1, u_2, u_3, u_4}
  (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]
  {ι : Type u_1}
  [CategoryTheory.Category.{u_3, u_1} ι]
  {A : Type u_2}
  [CategoryTheory.Category.{u_4, u_2} A]
  [CategoryTheory.Abelian A]
  (X :
    CategoryTheory.Triangulated.SpectralObject
      C ι)
  (F : CategoryTheory.Functor C A)
  [F.IsHomological] [F.ShiftSequence ℤ] :
  CategoryTheory.Abelian.SpectralObject A
    ι

Something wrong, better idea? Suggest a change

12.6.32. H0Functor_five_term_relation🔗

The five-term exact segment in the long exact sequence of the homological H^0_t yields: [H^n(X_2)] - [H^n(X_3)] + [H^{n+1}(X_1)] = [\operatorname{im}(H^n(f))] + [\operatorname{im}(H^{n+1}(f))] in K_0(\operatorname{heart}).

Proof: Applies \texttt{HeartK0.of\_exact\_five} to the five consecutive terms H^n(X_1) \to H^n(X_2) \to H^n(X_3) \to H^{n+1}(X_1) \to H^{n+1}(X_2) from the long exact cohomology sequence of the distinguished triangle.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_five_term_relation.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  [CategoryTheory.Abelian h.t.heart.FullSubcategory]
  [(CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
        h).IsHomological]
  (T : CategoryTheory.Pretriangulated.Triangle C)
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (n : ℤ) :
  CategoryTheory.Triangulated.HeartK0.of C h
          (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
                    h).shift
                n).obj
            T.obj₂) -
        CategoryTheory.Triangulated.HeartK0.of C h
          (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
                    h).shift
                n).obj
            T.obj₃) +
      CategoryTheory.Triangulated.HeartK0.of C h
        (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
                  h).shift
              (n + 1)).obj
          T.obj₁) =
    CategoryTheory.Triangulated.HeartK0.of C h
        (CategoryTheory.Limits.image
          (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
                    h).shift
                n).map
            T.mor₁)) +
      CategoryTheory.Triangulated.HeartK0.of C h
        (CategoryTheory.Limits.image
          (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
                    h).shift
                (n + 1)).map
            T.mor₁))
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_five_term_relation.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  [CategoryTheory.Abelian
      h.t.heart.FullSubcategory]
  [(CategoryTheory.Triangulated.HeartStabilityData.H0Functor
        C h).IsHomological]
  (T :
    CategoryTheory.Pretriangulated.Triangle
      C)
  (hT :
    T ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (n : ℤ) :
  CategoryTheory.Triangulated.HeartK0.of C
          h
          (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor
                    C h).shift
                n).obj
            T.obj₂) -
        CategoryTheory.Triangulated.HeartK0.of
          C h
          (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor
                    C h).shift
                n).obj
            T.obj₃) +
      CategoryTheory.Triangulated.HeartK0.of
        C h
        (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor
                  C h).shift
              (n + 1)).obj
          T.obj₁) =
    CategoryTheory.Triangulated.HeartK0.of
        C h
        (CategoryTheory.Limits.image
          (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor
                    C h).shift
                n).map
            T.mor₁)) +
      CategoryTheory.Triangulated.HeartK0.of
        C h
        (CategoryTheory.Limits.image
          (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor
                    C h).shift
                (n + 1)).map
            T.mor₁))

Something wrong, better idea? Suggest a change