Bridgeland Stability Conditions

12.3. HeartEquivalence: EulerLift🔗

12.3.1. heartCohClass🔗

The nth heart cohomology class of E, weighted by the parity sign: (-1)^{|n|} \cdot [H^n_t(E)] \in K_0(\operatorname{heart}).

Construction: Defined as the integer scalar (-1)^{|n|} applied to \texttt{HeartK0.of}(\texttt{heartCoh}(n, E)).

🔗def
CategoryTheory.Triangulated.HeartStabilityData.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.HeartK0 C h
CategoryTheory.Triangulated.HeartStabilityData.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.HeartK0 C h

Something wrong, better idea? Suggest a change

12.3.2. heartCohClass_eq_H0FunctorShift🔗

The heart cohomology class can equivalently be written using the shifted H^0 functor: \texttt{heartCohClass}(n, X) = (-1)^{|n|} \cdot [(H^0_t[n])(X)].

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

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_eq_H0FunctorShift.{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.heartCohClass C h n X =
    (-1) ^ n.natAbs •
      CategoryTheory.Triangulated.HeartK0.of C h
        (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
                  h).shift
              n).obj
          X)
CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_eq_H0FunctorShift.{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.heartCohClass
      C h n X =
    (-1) ^ n.natAbs •
      CategoryTheory.Triangulated.HeartK0.of
        C h
        (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor
                  C h).shift
              n).obj
          X)

Something wrong, better idea? Suggest a change

12.3.3. negOnePow_natAbs_succ🔗

(-1)^{|n+1|} = -(-1)^{|n|} for all n \in \mathbb{Z}.

Proof: Uses the standard identity (-1)^{n+1} = -(-1)^n from \texttt{Int.negOnePow\_succ}.

🔗theorem
CategoryTheory.Triangulated.negOnePow_natAbs_succ (n : ℤ) :
  (-1) ^ (n + 1).natAbs = -(-1) ^ n.natAbs
CategoryTheory.Triangulated.negOnePow_natAbs_succ
  (n : ℤ) :
  (-1) ^ (n + 1).natAbs = -(-1) ^ n.natAbs

Something wrong, better idea? Suggest a change

12.3.4. heartCohClass_five_term_relation🔗

The five-term relation for heart cohomology classes: for a distinguished triangle X_1 \to X_2 \to X_3 \to X_1[1], \texttt{heartCohClass}(n, X_2) - \texttt{heartCohClass}(n, X_3) - \texttt{heartCohClass}(n+1, X_1) equals a sum of two image terms.

Proof: Multiplies the H^0-functor five-term relation by (-1)^{|n|}, then distributes the sign using \texttt{negOnePow\_natAbs\_succ}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_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.HeartStabilityData.heartCohClass C h n
          T.obj₂ -
        CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h
          n T.obj₃ -
      CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h
        (n + 1) T.obj₁ =
    (-1) ^ n.natAbs •
        CategoryTheory.Triangulated.HeartK0.of C h
          (CategoryTheory.Limits.image
            (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor
                      C h).shift
                  n).map
              T.mor₁)) +
      (-1) ^ n.natAbs •
        CategoryTheory.Triangulated.HeartK0.of C h
          (CategoryTheory.Limits.image
            (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor
                      C h).shift
                  (n + 1)).map
              T.mor₁))
CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_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.HeartStabilityData.heartCohClass
          C h n T.obj₂ -
        CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
          C h n T.obj₃ -
      CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
        C h (n + 1) T.obj₁ =
    (-1) ^ n.natAbs •
        CategoryTheory.Triangulated.HeartK0.of
          C h
          (CategoryTheory.Limits.image
            (((CategoryTheory.Triangulated.HeartStabilityData.H0Functor
                      C h).shift
                  n).map
              T.mor₁)) +
      (-1) ^ n.natAbs •
        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

12.3.5. heartK0ToK0_heartCohClass🔗

The ambient image of the signed heart cohomology class is the class of the pure truncation: \texttt{heartK0ToK0}(\texttt{heartCohClass}(n, E)) = [\tau^{[n,n]} E] in K_0(\mathcal{C}).

Proof: Unfolds the definition, uses \texttt{map\_zsmul}, and identifies the heart object class with the shifted pure truncation class via the K_0-shift-parity formula.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0_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] (n : ℤ) (E : C) :
  (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0 C h)
      (CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h
        n E) =
    CategoryTheory.Triangulated.K₀.of C ((h.t.truncGELE n n).obj E)
CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0_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]
  (n : ℤ) (E : C) :
  (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0
        C h)
      (CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
        C h n E) =
    CategoryTheory.Triangulated.K₀.of C
      ((h.t.truncGELE n n).obj E)

Something wrong, better idea? Suggest a change

12.3.6. k0_truncLE_step🔗

One-step telescoping: [\tau^{\le n} E] = [\tau^{\le(n-1)} E] + \texttt{heartK0ToK0}(\texttt{heartCohClass}(n, E)) in K_0(\mathcal{C}).

Proof: The truncation triangle \tau^{<n} E \to \tau^{\le n} E \to \tau^{[n,n+1)} E gives a K_0 relation, and the right-hand term is identified with the heart cohomology class via \texttt{heartK0ToK0\_heartCohClass}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.k0_truncLE_step.{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] (n : ℤ) (E : C) :
  CategoryTheory.Triangulated.K₀.of C ((h.t.truncLE n).obj E) =
    CategoryTheory.Triangulated.K₀.of C ((h.t.truncLE (n - 1)).obj E) +
      (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0 C h)
        (CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C
          h n E)
CategoryTheory.Triangulated.HeartStabilityData.k0_truncLE_step.{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]
  (n : ℤ) (E : C) :
  CategoryTheory.Triangulated.K₀.of C
      ((h.t.truncLE n).obj E) =
    CategoryTheory.Triangulated.K₀.of C
        ((h.t.truncLE (n - 1)).obj E) +
      (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0
          C h)
        (CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
          C h n E)

Something wrong, better idea? Suggest a change

12.3.7. heartCohClassSum🔗

The finite alternating sum \sum_{j=0}^{n} \texttt{heartCohClass}(b+j, E) of heart cohomology classes from degrees b to b+n.

Construction: A Finset sum over \texttt{Finset.range}(n+1).

🔗def
CategoryTheory.Triangulated.HeartStabilityData.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) (b : ℤ) (n : ℕ)
  (E : C) : CategoryTheory.Triangulated.HeartK0 C h
CategoryTheory.Triangulated.HeartStabilityData.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)
  (b : ℤ) (n : ℕ) (E : C) :
  CategoryTheory.Triangulated.HeartK0 C h

Something wrong, better idea? Suggest a change

12.3.8. heartCohClassSum_succ🔗

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

Proof: Immediate from \texttt{Finset.sum\_range\_succ}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_succ.{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) (b : ℤ) (n : ℕ)
  (E : C) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h b
      (n + 1) E =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C h
        b n E +
      CategoryTheory.Triangulated.HeartStabilityData.heartCohClass C h
        (b + ↑(n + 1)) E
CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum_succ.{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)
  (b : ℤ) (n : ℕ) (E : C) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
      C h b (n + 1) E =
    CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
        C h b n E +
      CategoryTheory.Triangulated.HeartStabilityData.heartCohClass
        C h (b + ↑(n + 1)) E

Something wrong, better idea? Suggest a change

12.3.9. heartK0ToK0_heartCohClassSum_truncLE🔗

Telescoping formula: if E \in \mathcal{C}^{\ge b}, then \texttt{heartK0ToK0}(\texttt{heartCohClassSum}(b, n, E)) = [\tau^{\le(b+n)} E].

Proof: Induction on n. The base case uses the vanishing of \tau^{\le(b-1)} E for E \in \mathcal{C}^{\ge b}. The inductive step applies \texttt{k0\_truncLE\_step}.

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

Something wrong, better idea? Suggest a change

12.3.10. heartK0ToK0_heartCohClassSum🔗

The canonical bounded interval sum maps to [E] in ambient K_0: \texttt{heartK0ToK0}(\sum_{j=b}^{a} (-1)^{|j|} [H^j_t(E)]) = [E]. This is the usual formula [E] = \sum_n (-1)^n [H^n_t(E)].

Proof: Applies the telescoping formula \texttt{heartK0ToK0\_heartCohClassSum\_truncLE} up to degree a, then uses the fact that \tau^{\le a} E \cong E for E \in \mathcal{C}^{\le a}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0_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)
  [CategoryTheory.IsTriangulated C] {E : C} (a b : ℤ) (hab : b ≤ a)
  (hLE : h.t.IsLE E a) (hGE : h.t.IsGE E b) :
  (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0 C h)
      (CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum C
        h b (a - b).toNat E) =
    CategoryTheory.Triangulated.K₀.of C E
CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0_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)
  [CategoryTheory.IsTriangulated C]
  {E : C} (a b : ℤ) (hab : b ≤ a)
  (hLE : h.t.IsLE E a)
  (hGE : h.t.IsGE E b) :
  (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0
        C h)
      (CategoryTheory.Triangulated.HeartStabilityData.heartCohClassSum
        C h b (a - b).toNat E) =
    CategoryTheory.Triangulated.K₀.of C E

Something wrong, better idea? Suggest a change

12.3.11. upperBound🔗

A classical choice of an upper bound a such that E \in \mathcal{C}^{\le a}, for the bounded t-structure.

Construction: If E is in the heart, returns 0; otherwise applies \texttt{Classical.choose} to the boundedness hypothesis.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.upperBound.{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.upperBound.{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.3.12. lowerBound🔗

A classical choice of a lower bound b such that E \in \mathcal{C}^{\ge b}, for the bounded t-structure.

Construction: If E is in the heart, returns 0; otherwise applies \texttt{Classical.choose} twice to the boundedness hypothesis.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.lowerBound.{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.lowerBound.{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.3.13. isLE_upperBound🔗

E \in \mathcal{C}^{\le \texttt{upperBound}(E)}.

Proof: Case split on whether E is in the heart; in each case the bound is witnessed by the heart membership or the classical choice.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.isLE_upperBound.{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) :
  h.t.IsLE E
    (CategoryTheory.Triangulated.HeartStabilityData.upperBound C h E)
CategoryTheory.Triangulated.HeartStabilityData.isLE_upperBound.{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) :
  h.t.IsLE E
    (CategoryTheory.Triangulated.HeartStabilityData.upperBound
      C h E)

Something wrong, better idea? Suggest a change

12.3.14. isGE_lowerBound🔗

E \in \mathcal{C}^{\ge \texttt{lowerBound}(E)}.

Proof: Analogous to \texttt{isLE\_upperBound}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.isGE_lowerBound.{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) :
  h.t.IsGE E
    (CategoryTheory.Triangulated.HeartStabilityData.lowerBound C h E)
CategoryTheory.Triangulated.HeartStabilityData.isGE_lowerBound.{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) :
  h.t.IsGE E
    (CategoryTheory.Triangulated.HeartStabilityData.lowerBound
      C h E)

Something wrong, better idea? Suggest a change

12.3.15. lowerBound_le_upperBound🔗

\texttt{lowerBound}(E) \le \texttt{upperBound}(E) for every object E.

Proof: If the inequality fails, E would be zero, hence in the heart with both bounds equal to 0, contradicting the assumption.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.lowerBound_le_upperBound.{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.lowerBound C h E ≤
    CategoryTheory.Triangulated.HeartStabilityData.upperBound C h E
CategoryTheory.Triangulated.HeartStabilityData.lowerBound_le_upperBound.{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.lowerBound
      C h E ≤
    CategoryTheory.Triangulated.HeartStabilityData.upperBound
      C h E

Something wrong, better idea? Suggest a change

12.3.16. heartEulerClassObj🔗

The canonical object-level lift of [E] to K_0(\operatorname{heart}), given by the alternating sum of the chosen bounded heart cohomology classes.

Construction: Computes \texttt{heartCohClassSum}(b, \mathrm{toNat}(a - b), E) where a = \texttt{upperBound}(E) and b = \texttt{lowerBound}(E), or 0 if the bounds are reversed.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj.{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.HeartK0 C h
CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj.{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.HeartK0 C h

Something wrong, better idea? Suggest a change

12.3.17. heartK0ToK0_heartEulerClassObj🔗

The canonical object-level lift maps to the ambient Grothendieck-group class: \texttt{heartK0ToK0}(\texttt{heartEulerClassObj}(E)) = [E].

Proof: Delegates to \texttt{heartK0ToK0\_heartCohClassSum} with the chosen bounds, or handles the degenerate zero case.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0_heartEulerClassObj.{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) :
  (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0 C h)
      (CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E) =
    CategoryTheory.Triangulated.K₀.of C E
CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0_heartEulerClassObj.{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) :
  (CategoryTheory.Triangulated.HeartStabilityData.heartK0ToK0
        C h)
      (CategoryTheory.Triangulated.HeartStabilityData.heartEulerClassObj
        C h E) =
    CategoryTheory.Triangulated.K₀.of C E

Something wrong, better idea? Suggest a change

12.3.18. H0FunctorObjIsoOfHeart🔗

On objects already in the heart, the H^0 functor restricts to the identity: H^0_t(E) \cong E for E \in \operatorname{heart}(t).

Construction: Composes the isomorphisms from \tau^{\le 0} E \cong E and E \cong \tau^{\ge 0} E (both isomorphisms because E is in the heart) with the shift-by-zero identification.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.H0FunctorObjIsoOfHeart.{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.H0Functor C h).obj
      E.obj ≅
    E
CategoryTheory.Triangulated.HeartStabilityData.H0FunctorObjIsoOfHeart.{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.H0Functor
          C h).obj
      E.obj ≅
    E

Something wrong, better idea? Suggest a change

12.3.19. H0primeObjIsoOfHeart🔗

The primed H^0{}' restricts to the identity on heart objects.

Construction: Composes the inverse of \texttt{H0ObjIsoH0prime} with \texttt{H0FunctorObjIsoOfHeart}.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoOfHeart.{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.H0prime C h E.obj ≅ E
CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoOfHeart.{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.H0prime
      C h E.obj ≅
    E

Something wrong, better idea? Suggest a change

12.3.20. H0primeObjIsoOfHeart_inv_hom_comp_truncLEι🔗

The composite of the inverse of \texttt{H0primeObjIsoOfHeart} with the \tau^{\le 0}-inclusion equals the \tau^{\ge 0}-projection.

Proof: A direct computation using the definition of \texttt{H0primeObjIsoOfHeart} and the \texttt{H0ObjIsoH0prime} composition rules.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoOfHeart_inv_hom_comp_truncLEι.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  [CategoryTheory.IsTriangulated C] (E : h.t.heart.FullSubcategory) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoOfHeart
            C h E).inv.hom
      ((h.t.truncLEι 0).app ((h.t.truncGE 0).obj E.obj)) =
    (h.t.truncGEπ 0).app E.obj
CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoOfHeart_inv_hom_comp_truncLEι.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  [CategoryTheory.IsTriangulated C]
  (E : h.t.heart.FullSubcategory) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoOfHeart
            C h E).inv.hom
      ((h.t.truncLEι 0).app
        ((h.t.truncGE 0).obj E.obj)) =
    (h.t.truncGEπ 0).app E.obj

Something wrong, better idea? Suggest a change

12.3.21. H0primeObjIsoOfHeart_inv_hom_comp_truncLEι_assoc🔗

Associativity-reassociated form of \texttt{H0primeObjIsoOfHeart\_inv\_hom\_comp\_truncLE\iota}.

Proof: Obtained from the non-assoc version by \texttt{reassoc}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoOfHeart_inv_hom_comp_truncLEι_assoc.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  [CategoryTheory.IsTriangulated C] (E : h.t.heart.FullSubcategory)
  {Z : C} (h✝ : (h.t.truncGE 0).obj E.obj ⟶ Z) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoOfHeart
            C h E).inv.hom
      (CategoryTheory.CategoryStruct.comp
        ((h.t.truncLEι 0).app ((h.t.truncGE 0).obj E.obj)) h✝) =
    CategoryTheory.CategoryStruct.comp ((h.t.truncGEπ 0).app E.obj) h✝
CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoOfHeart_inv_hom_comp_truncLEι_assoc.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  [CategoryTheory.IsTriangulated C]
  (E : h.t.heart.FullSubcategory) {Z : C}
  (h✝ : (h.t.truncGE 0).obj E.obj ⟶ Z) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoOfHeart
            C h E).inv.hom
      (CategoryTheory.CategoryStruct.comp
        ((h.t.truncLEι 0).app
          ((h.t.truncGE 0).obj E.obj))
        h✝) =
    CategoryTheory.CategoryStruct.comp
      ((h.t.truncGEπ 0).app E.obj) h✝

Something wrong, better idea? Suggest a change

12.3.22. heartSourceH0primeShortComplex🔗

The short complex in the heart obtained by applying H^0{}' to the first two morphisms of a distinguished triangle whose source lies in the heart.

Construction: Built as the \texttt{ShortComplex.mk} of the maps \texttt{toH0primeHom}(A, f) and (H^0{}'(g)), with the zero-composite verified from the triangle relation f \circ g = 0.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex.{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 : h.t.heart.FullSubcategory) {X₂ X₃ : C} (f : A.obj ⟶ X₂)
  (g : X₂ ⟶ X₃) (hfg : CategoryTheory.CategoryStruct.comp f g = 0) :
  CategoryTheory.ShortComplex h.t.heart.FullSubcategory
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex.{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 : h.t.heart.FullSubcategory)
  {X₂ X₃ : C} (f : A.obj ⟶ X₂)
  (g : X₂ ⟶ X₃)
  (hfg :
    CategoryTheory.CategoryStruct.comp f
        g =
      0) :
  CategoryTheory.ShortComplex
    h.t.heart.FullSubcategory

Something wrong, better idea? Suggest a change

12.3.23. heartSourceH0primeShortComplex_f_eq_toH0primeHom🔗

The first map of the heart-source H^0{}' short complex equals the canonical lift \texttt{toH0primeHom}(A, f).

Proof: Follows from the private lemma \texttt{H0primeObjIsoOfHeart\_inv\_comp\_H0primeFunctor\_map}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_f_eq_toH0primeHom.{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 : h.t.heart.FullSubcategory)
  {X₂ X₃ : C} (f : A.obj ⟶ X₂) (g : X₂ ⟶ X₃)
  (hfg : CategoryTheory.CategoryStruct.comp f g = 0) :
  (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
        C h A f g hfg).f =
    CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom C h A f
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_f_eq_toH0primeHom.{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 : h.t.heart.FullSubcategory)
  {X₂ X₃ : C} (f : A.obj ⟶ X₂)
  (g : X₂ ⟶ X₃)
  (hfg :
    CategoryTheory.CategoryStruct.comp f
        g =
      0) :
  (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
        C h A f g hfg).f =
    CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom
      C h A f

Something wrong, better idea? Suggest a change

12.3.24. heartSourceH0primeShortComplexIso🔗

Comparison isomorphism between the heart-source H^0{}' short complex and the image of the ambient distinguished-triangle short complex under H^0{}'.

Construction: A \texttt{ShortComplex.isoMk} whose first component is (\texttt{H0primeObjIsoOfHeart}(A))^{-1} and second is the identity, with commutativity checked using \texttt{H0primeObjIsoOfHeart\_inv\_comp\_H0primeFunctor\_map}.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplexIso.{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 : 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) :
  CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
      C h A f g ⋯ ≅
    (CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
          (CategoryTheory.Pretriangulated.Triangle.mk f g δ) hT).map
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
        h)
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplexIso.{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 : 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) :
  CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
      C h A f g ⋯ ≅
    (CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
          (CategoryTheory.Pretriangulated.Triangle.mk
            f g δ)
          hT).map
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
        C h)

Something wrong, better idea? Suggest a change

12.3.25. heartSourceH0primeShortComplex_preadditiveCoyoneda_exact_iff🔗

For a distinguished triangle with heart source and a heart object E, exactness of the ambient short complex after applying H^0{}' and the preadditive coyoneda is equivalent to exactness of the heart-source short complex after applying coyoneda.

Proof: Uses the comparison isomorphism \texttt{heartSourceH0primeShortComplexIso} and \texttt{ShortComplex.exact\_iff\_of\_iso} to transfer exactness.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_preadditiveCoyoneda_exact_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)
  (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.heartSourceH0primeShortComplex
            C h A f g ⋯).map
        (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op E))).Exact
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_preadditiveCoyoneda_exact_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)
  (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.heartSourceH0primeShortComplex
            C h A f g ⋯).map
        (CategoryTheory.preadditiveCoyoneda.obj
          (Opposite.op E))).Exact

Something wrong, better idea? Suggest a change

12.3.26. heartSourceH0primeShortComplex_preadditiveCoyoneda_exact_of_f_is_kernel🔗

If the first map of the heart-source short complex is a kernel, then the short complex is exact after applying the preadditive coyoneda.

Proof: Delegates directly to \texttt{ShortComplex.preadditiveCoyoneda\_exact\_of\_f\_is\_kernel}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_preadditiveCoyoneda_exact_of_f_is_kernel.{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 : h.t.heart.FullSubcategory) {X₂ X₃ : C} {f : A.obj ⟶ X₂}
  {g : X₂ ⟶ X₃} (hfg : CategoryTheory.CategoryStruct.comp f g = 0)
  (hKer :
    CategoryTheory.Limits.IsLimit
      (CategoryTheory.Limits.KernelFork.ofι
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
            C h A f g hfg).f
        ⋯))
  (E : h.t.heart.FullSubcategory) :
  ((CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
          C h A f g hfg).map
      (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op E))).Exact
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_preadditiveCoyoneda_exact_of_f_is_kernel.{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 : h.t.heart.FullSubcategory)
  {X₂ X₃ : C} {f : A.obj ⟶ X₂}
  {g : X₂ ⟶ X₃}
  (hfg :
    CategoryTheory.CategoryStruct.comp f
        g =
      0)
  (hKer :
    CategoryTheory.Limits.IsLimit
      (CategoryTheory.Limits.KernelFork.ofι
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
            C h A f g hfg).f
        ⋯))
  (E : h.t.heart.FullSubcategory) :
  ((CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
          C h A f g hfg).map
      (CategoryTheory.preadditiveCoyoneda.obj
        (Opposite.op E))).Exact

Something wrong, better idea? Suggest a change

12.3.27. heartSourceH0primeShortComplex_cokernelDesc🔗

The canonical map from the cokernel of the heart-source H^0{}' short complex to H^0{}'(X_3), given by the descent of the second map g through the cokernel.

Construction: Defined as \texttt{cokernel.desc} applied to the second map g of the heart-source short complex.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_cokernelDesc.{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 : h.t.heart.FullSubcategory) {X₂ X₃ : C} (f : A.obj ⟶ X₂)
  (g : X₂ ⟶ X₃) (hfg : CategoryTheory.CategoryStruct.comp f g = 0) :
  CategoryTheory.Limits.cokernel
      (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
          C h A f g hfg).f ⟶
    CategoryTheory.Triangulated.HeartStabilityData.H0prime C h X₃
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_cokernelDesc.{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 : h.t.heart.FullSubcategory)
  {X₂ X₃ : C} (f : A.obj ⟶ X₂)
  (g : X₂ ⟶ X₃)
  (hfg :
    CategoryTheory.CategoryStruct.comp f
        g =
      0) :
  CategoryTheory.Limits.cokernel
      (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
          C h A f g hfg).f ⟶
    CategoryTheory.Triangulated.HeartStabilityData.H0prime
      C h X₃

Something wrong, better idea? Suggest a change

12.3.28. heartSourceH0primeShortComplex_cokernelπ_comp_cokernelDesc🔗

The cokernel projection followed by the canonical descent map equals the second map of the heart-source short complex.

Proof: This is the defining property \pi \circ \texttt{desc} = g of the cokernel universal property.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_cokernelπ_comp_cokernelDesc.{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 : h.t.heart.FullSubcategory) {X₂ X₃ : C} (f : A.obj ⟶ X₂)
  (g : X₂ ⟶ X₃) (hfg : CategoryTheory.CategoryStruct.comp f g = 0) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.cokernel.π
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
            C h A f g hfg).f)
      (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_cokernelDesc
        C h A f g hfg) =
    (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
        C h A f g hfg).g
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_cokernelπ_comp_cokernelDesc.{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 : h.t.heart.FullSubcategory)
  {X₂ X₃ : C} (f : A.obj ⟶ X₂)
  (g : X₂ ⟶ X₃)
  (hfg :
    CategoryTheory.CategoryStruct.comp f
        g =
      0) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.cokernel.π
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
            C h A f g hfg).f)
      (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_cokernelDesc
        C h A f g hfg) =
    (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
        C h A f g hfg).g

Something wrong, better idea? Suggest a change

12.3.29. heartSourceH0primeShortComplex_cokernelπ_comp_cokernelDesc_assoc🔗

Associativity-reassociated form of \texttt{heartSourceH0primeShortComplex\_cokernelπ\_comp\_cokernelDesc}.

Proof: Obtained by \texttt{reassoc} from the non-assoc version.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_cokernelπ_comp_cokernelDesc_assoc.{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 : h.t.heart.FullSubcategory) {X₂ X₃ : C} (f : A.obj ⟶ X₂)
  (g : X₂ ⟶ X₃) (hfg : CategoryTheory.CategoryStruct.comp f g = 0)
  {Z : h.t.heart.FullSubcategory}
  (h✝ :
    CategoryTheory.Triangulated.HeartStabilityData.H0prime C h X₃ ⟶ Z) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.cokernel.π
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
            C h A f g hfg).f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_cokernelDesc
          C h A f g hfg)
        h✝) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
          C h A f g hfg).g
      h✝
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_cokernelπ_comp_cokernelDesc_assoc.{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 : h.t.heart.FullSubcategory)
  {X₂ X₃ : C} (f : A.obj ⟶ X₂)
  (g : X₂ ⟶ X₃)
  (hfg :
    CategoryTheory.CategoryStruct.comp f
        g =
      0)
  {Z : h.t.heart.FullSubcategory}
  (h✝ :
    CategoryTheory.Triangulated.HeartStabilityData.H0prime
        C h X₃ ⟶
      Z) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.cokernel.π
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
            C h A f g hfg).f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_cokernelDesc
          C h A f g hfg)
        h✝) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
          C h A f g hfg).g
      h✝

Something wrong, better idea? Suggest a change

12.3.30. heartSourceH0primeShortComplex_f_is_kernel_of_distTriang🔗

In the heart-source H^0{}' short complex induced by a distinguished triangle, the first map is a kernel.

Construction: Uses \texttt{TStructure.heartFullSubcategory\_shortExact\_of\_distTriang} to obtain a short exact sequence in the heart, then reads off the kernel property from \texttt{ShortExact.fIsKernel}.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_f_is_kernel_of_distTriang.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (A : h.t.heart.FullSubcategory) {X₂ X₃ : C} {f : A.obj ⟶ X₂}
  {g : X₂ ⟶ X₃} (hfg : CategoryTheory.CategoryStruct.comp f g = 0)
  {δ :
    (CategoryTheory.Triangulated.HeartStabilityData.H0prime C h
          X₃).obj ⟶
      (CategoryTheory.shiftFunctor C 1).obj A.obj}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
              C h A f g hfg).f.hom
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
              C h A f g hfg).g.hom
        δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Limits.IsLimit
    (CategoryTheory.Limits.KernelFork.ofι
      (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
          C h A f g hfg).f
      ⋯)
CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex_f_is_kernel_of_distTriang.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (A : h.t.heart.FullSubcategory)
  {X₂ X₃ : C} {f : A.obj ⟶ X₂}
  {g : X₂ ⟶ X₃}
  (hfg :
    CategoryTheory.CategoryStruct.comp f
        g =
      0)
  {δ :
    (CategoryTheory.Triangulated.HeartStabilityData.H0prime
          C h X₃).obj ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        A.obj}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
              C h A f g hfg).f.hom
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
              C h A f g hfg).g.hom
        δ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Limits.IsLimit
    (CategoryTheory.Limits.KernelFork.ofι
      (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
          C h A f g hfg).f
      ⋯)

Something wrong, better idea? Suggest a change

12.3.31. H0Functor_isHomological_of_eval_of_heartSourceH0primeShortComplex🔗

If the heart-source H^0{}' short complex is exact for every heart source and every representable, then H^0_t is a homological functor.

Proof: Reduces to the heart-case exactness criterion for the H^0{}' functor by the comparison isomorphism between H^0 and H^0{}'.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_isHomological_of_eval_of_heartSourceH0primeShortComplex.{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)
  (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.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
              C h A f g ⋯).map
          (CategoryTheory.preadditiveCoyoneda.obj
            (Opposite.op E))).Exact) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
      h).IsHomological
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_isHomological_of_eval_of_heartSourceH0primeShortComplex.{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)
  (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.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
              C h A f g ⋯).map
          (CategoryTheory.preadditiveCoyoneda.obj
            (Opposite.op E))).Exact) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor
      C h).IsHomological

Something wrong, better idea? Suggest a change

12.3.32. H0Functor_isHomological_of_heartSourceH0primeShortComplex_f_is_kernel🔗

If for every distinguished triangle with heart source the first map of the heart-source H^0{}' short complex is a kernel, then H^0_t is a homological functor.

Proof: Applies \texttt{heartSourceH0primeShortComplex\_preadditiveCoyoneda\_exact\_of\_f\_is\_kernel} to each representable and then uses \texttt{H0Functor\_isHomological\_of\_eval\_of\_heartSourceH0primeShortComplex}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_isHomological_of_heartSourceH0primeShortComplex_f_is_kernel.{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)
  (hKer :
    (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) →
                CategoryTheory.Limits.IsLimit
                  (CategoryTheory.Limits.KernelFork.ofι
                    (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
                        C h A f g ⋯).f
                    ⋯)) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
      h).IsHomological
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_isHomological_of_heartSourceH0primeShortComplex_f_is_kernel.{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)
  (hKer :
    (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) →
                CategoryTheory.Limits.IsLimit
                  (CategoryTheory.Limits.KernelFork.ofι
                    (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
                        C h A f g ⋯).f
                    ⋯)) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor
      C h).IsHomological

Something wrong, better idea? Suggest a change

12.3.33. H0Functor_isHomological_of_heartSourceH0primeShortComplex_distTriang🔗

If for every distinguished triangle with heart source the induced H^0{}' short complex admits a compatible distinguished triangle, then H^0_t is a homological functor.

Proof: Produces the required kernel witness from the distinguished triangle assumption via \texttt{heartSourceH0primeShortComplex\_f\_is\_kernel\_of\_distTriang}, then applies \texttt{H0Functor\_isHomological\_of\_heartSourceH0primeShortComplex\_f\_is\_kernel}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_isHomological_of_heartSourceH0primeShortComplex_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)
  (hTri :
    (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) →
                (δ' :
                  (CategoryTheory.Triangulated.HeartStabilityData.H0prime
                        C h X₃).obj ⟶
                    (CategoryTheory.shiftFunctor C 1).obj A.obj) ×'
                  CategoryTheory.Pretriangulated.Triangle.mk
                      (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
                            C h A f g ⋯).f.hom
                      (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
                            C h A f g ⋯).g.hom
                      δ' ∈
                    CategoryTheory.Pretriangulated.distinguishedTriangles) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
      h).IsHomological
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_isHomological_of_heartSourceH0primeShortComplex_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)
  (hTri :
    (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) →
                (δ' :
                  (CategoryTheory.Triangulated.HeartStabilityData.H0prime
                        C h X₃).obj ⟶
                    (CategoryTheory.shiftFunctor
                          C 1).obj
                      A.obj) ×'
                  CategoryTheory.Pretriangulated.Triangle.mk
                      (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
                            C h A f g
                            ⋯).f.hom
                      (CategoryTheory.Triangulated.HeartStabilityData.heartSourceH0primeShortComplex
                            C h A f g
                            ⋯).g.hom
                      δ' ∈
                    CategoryTheory.Pretriangulated.distinguishedTriangles) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor
      C h).IsHomological

Something wrong, better idea? Suggest a change

12.3.34. heartSourceNegOneToAShiftHom🔗

The morphism from the (-1,0)-truncation of X_3 to A[1] induced by a morphism \delta : X_3 \to A[1] with A in the heart.

Construction: Lifts (\iota_{<0})_{X_3} \circ \delta through the truncation triangle \tau^{(-1,0)}(X_3) using the Yoneda exactness \texttt{Triangle.yoneda\_exact} after checking the vanishing condition.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.heartSourceNegOneToAShiftHom.{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 : h.t.heart.FullSubcategory) {X₃ : C}
  (δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj A.obj) :
  (h.t.truncGELT (-1) 0).obj X₃ ⟶
    (CategoryTheory.shiftFunctor C 1).obj A.obj
CategoryTheory.Triangulated.HeartStabilityData.heartSourceNegOneToAShiftHom.{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 : h.t.heart.FullSubcategory) {X₃ : C}
  (δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        A.obj) :
  (h.t.truncGELT (-1) 0).obj X₃ ⟶
    (CategoryTheory.shiftFunctor C 1).obj
      A.obj

Something wrong, better idea? Suggest a change

12.3.35. truncLT_map_truncGEπ_comp_heartSourceNegOneToAShiftHom🔗

The \tau^{\ge(-1)}-projection on \tau^{<0}(X_3) followed by \texttt{heartSourceNegOneToAShiftHom} equals (\iota_{<0})_{X_3} \circ \delta.

Proof: Reads off the defining property of the chosen lift from the Yoneda exactness calculation.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.truncLT_map_truncGEπ_comp_heartSourceNegOneToAShiftHom.{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 : h.t.heart.FullSubcategory) {X₃ : C}
  (δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj A.obj) :
  CategoryTheory.CategoryStruct.comp
      ((h.t.truncGEπ (-1)).app ((h.t.truncLT 0).obj X₃))
      (CategoryTheory.Triangulated.HeartStabilityData.heartSourceNegOneToAShiftHom
        C h A δ) =
    CategoryTheory.CategoryStruct.comp ((h.t.truncLTι 0).app X₃) δ
CategoryTheory.Triangulated.HeartStabilityData.truncLT_map_truncGEπ_comp_heartSourceNegOneToAShiftHom.{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 : h.t.heart.FullSubcategory) {X₃ : C}
  (δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        A.obj) :
  CategoryTheory.CategoryStruct.comp
      ((h.t.truncGEπ (-1)).app
        ((h.t.truncLT 0).obj X₃))
      (CategoryTheory.Triangulated.HeartStabilityData.heartSourceNegOneToAShiftHom
        C h A δ) =
    CategoryTheory.CategoryStruct.comp
      ((h.t.truncLTι 0).app X₃) δ

Something wrong, better idea? Suggest a change

12.3.36. truncLT_map_truncGEπ_comp_heartSourceNegOneToAShiftHom_assoc🔗

Associativity-reassociated form of \texttt{truncLT\_map\_truncGEπ\_comp\_heartSourceNegOneToAShiftHom}.

Proof: Obtained by \texttt{reassoc} from the non-assoc version.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.truncLT_map_truncGEπ_comp_heartSourceNegOneToAShiftHom_assoc.{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 : h.t.heart.FullSubcategory) {X₃ : C}
  (δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj A.obj) {Z : C}
  (h✝ : (CategoryTheory.shiftFunctor C 1).obj A.obj ⟶ Z) :
  CategoryTheory.CategoryStruct.comp
      ((h.t.truncGEπ (-1)).app ((h.t.truncLT 0).obj X₃))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceNegOneToAShiftHom
          C h A δ)
        h✝) =
    CategoryTheory.CategoryStruct.comp ((h.t.truncLTι 0).app X₃)
      (CategoryTheory.CategoryStruct.comp δ h✝)
CategoryTheory.Triangulated.HeartStabilityData.truncLT_map_truncGEπ_comp_heartSourceNegOneToAShiftHom_assoc.{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 : h.t.heart.FullSubcategory) {X₃ : C}
  (δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        A.obj)
  {Z : C}
  (h✝ :
    (CategoryTheory.shiftFunctor C 1).obj
        A.obj ⟶
      Z) :
  CategoryTheory.CategoryStruct.comp
      ((h.t.truncGEπ (-1)).app
        ((h.t.truncLT 0).obj X₃))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceNegOneToAShiftHom
          C h A δ)
        h✝) =
    CategoryTheory.CategoryStruct.comp
      ((h.t.truncLTι 0).app X₃)
      (CategoryTheory.CategoryStruct.comp
        δ h✝)

Something wrong, better idea? Suggest a change

12.3.37. heartSourceNegOneToAHom🔗

After shifting back by -1, the morphism \texttt{heartSourceNegOneToAShiftHom} becomes a morphism H^{-1}_t(X_3) \to A in the heart.

Construction: Composes the shift-by-(-1) of \texttt{heartSourceNegOneToAShiftHom} with the isomorphism \texttt{truncGELEIsoTruncGELT} and the canonical A[1][-1] \cong A isomorphism.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.heartSourceNegOneToAHom.{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 : h.t.heart.FullSubcategory) {X₃ : C}
  (δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj A.obj) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCoh C h (-1) X₃ ⟶
    A
CategoryTheory.Triangulated.HeartStabilityData.heartSourceNegOneToAHom.{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 : h.t.heart.FullSubcategory) {X₃ : C}
  (δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        A.obj) :
  CategoryTheory.Triangulated.HeartStabilityData.heartCoh
      C h (-1) X₃ ⟶
    A

Something wrong, better idea? Suggest a change

12.3.38. exists_heartSourceNegOneToAShiftHom_comp_shift_map_factor🔗

The composite \texttt{heartSourceNegOneToAShiftHom}(\delta) \circ f[1] factors through the connecting morphism of the (-1,0)-truncation triangle.

Proof: Checks the vanishing condition using the triangle relation \delta \circ f = 0 and \texttt{truncLT\_map\_truncGEπ\_comp\_heartSourceNegOneToAShiftHom}, then applies the Yoneda exactness of the truncation triangle.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.exists_heartSourceNegOneToAShiftHom_comp_shift_map_factor.{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 : 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) :
  ∃ φ,
    CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceNegOneToAShiftHom
          C h A δ)
        ((CategoryTheory.shiftFunctor C 1).map f) =
      CategoryTheory.CategoryStruct.comp
        ((h.t.truncGELTδLT (-1) 0).app X₃) φ
CategoryTheory.Triangulated.HeartStabilityData.exists_heartSourceNegOneToAShiftHom_comp_shift_map_factor.{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 : 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) :
  ∃ φ,
    CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceNegOneToAShiftHom
          C h A δ)
        ((CategoryTheory.shiftFunctor C
              1).map
          f) =
      CategoryTheory.CategoryStruct.comp
        ((h.t.truncGELTδLT (-1) 0).app X₃)
        φ

Something wrong, better idea? Suggest a change

12.3.39. exists_comp_heartSourceNegOneToAShiftHom_eq_of_comp_truncGEπ_zero🔗

If m \circ \pi_{\ge 0} = 0, then there exists u : E \to \tau^{(-1,0)}(X_3) such that u \circ \texttt{heartSourceNegOneToAShiftHom} = m \circ \delta.

Proof: Lifts m through the \tau^{<0}-truncation triangle using \texttt{Triangle.coyoneda\_exact}, then computes the composite with \texttt{truncGE}(-1)-projection using \texttt{truncLT\_map\_truncGEπ\_comp\_heartSourceNegOneToAShiftHom}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.exists_comp_heartSourceNegOneToAShiftHom_eq_of_comp_truncGEπ_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 A : h.t.heart.FullSubcategory) {X₃ : C}
  (δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj A.obj)
  (m : E.obj ⟶ X₃)
  (hm :
    CategoryTheory.CategoryStruct.comp m ((h.t.truncGEπ 0).app X₃) =
      0) :
  ∃ u,
    CategoryTheory.CategoryStruct.comp u
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceNegOneToAShiftHom
          C h A δ) =
      CategoryTheory.CategoryStruct.comp m δ
CategoryTheory.Triangulated.HeartStabilityData.exists_comp_heartSourceNegOneToAShiftHom_eq_of_comp_truncGEπ_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 A : h.t.heart.FullSubcategory)
  {X₃ : C}
  (δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        A.obj)
  (m : E.obj ⟶ X₃)
  (hm :
    CategoryTheory.CategoryStruct.comp m
        ((h.t.truncGEπ 0).app X₃) =
      0) :
  ∃ u,
    CategoryTheory.CategoryStruct.comp u
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceNegOneToAShiftHom
          C h A δ) =
      CategoryTheory.CategoryStruct.comp m
        δ

Something wrong, better idea? Suggest a change

12.3.40. exists_comp_heartSourceNegOneToAShiftHom_eq_of_toH0prime_comp_kernel🔗

If the canonical lift \texttt{toH0prime}(f) \circ H^0{}'(g) = 0, then there exists u such that u \circ \texttt{heartSourceNegOneToAShiftHom} = f \circ g \circ \delta.

Proof: Reduces to \texttt{exists\_comp\_heartSourceNegOneToAShiftHom\_eq\_of\_comp\_truncGEπ\_zero} by converting the vanishing condition via \texttt{toH0primeHom\_eq\_zero\_iff}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.exists_comp_heartSourceNegOneToAShiftHom_eq_of_toH0prime_comp_kernel.{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 A : h.t.heart.FullSubcategory) {X₂ X₃ : C} (f : E.obj ⟶ X₂)
  (g : X₂ ⟶ X₃) {δ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj A.obj}
  (hfg :
    CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom C h
          E f)
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).map
          g) =
      0) :
  ∃ u,
    CategoryTheory.CategoryStruct.comp u
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceNegOneToAShiftHom
          C h A δ) =
      CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp g δ)
CategoryTheory.Triangulated.HeartStabilityData.exists_comp_heartSourceNegOneToAShiftHom_eq_of_toH0prime_comp_kernel.{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 A : h.t.heart.FullSubcategory)
  {X₂ X₃ : C} (f : E.obj ⟶ X₂)
  (g : X₂ ⟶ X₃)
  {δ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        A.obj}
  (hfg :
    CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom
          C h E f)
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).map
          g) =
      0) :
  ∃ u,
    CategoryTheory.CategoryStruct.comp u
        (CategoryTheory.Triangulated.HeartStabilityData.heartSourceNegOneToAShiftHom
          C h A δ) =
      CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp
          g δ)

Something wrong, better idea? Suggest a change

12.3.41. comp_shift_truncGEπ_zero_of_truncLT_negOne🔗

For any morphism \phi : (\tau^{<(-1)}(X_3))[1] \to X_2[1], the composite \phi \circ (\pi_{\ge 0})_{X_2}[1] vanishes.

Proof: The source lies in \mathcal{C}^{\le -2} (after shifting) while the target lies in \mathcal{C}^{\ge -1}, so the morphism vanishes by t-structure orthogonality.

🔗theorem
CategoryTheory.Triangulated.TStructure.comp_shift_truncGEπ_zero_of_truncLT_negOne.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X₂ X₃ : C}
  (φ :
    (CategoryTheory.shiftFunctor C 1).obj ((t.truncLT (-1)).obj X₃) ⟶
      (CategoryTheory.shiftFunctor C 1).obj X₂) :
  CategoryTheory.CategoryStruct.comp φ
      ((CategoryTheory.shiftFunctor C 1).map ((t.truncGEπ 0).app X₂)) =
    0
CategoryTheory.Triangulated.TStructure.comp_shift_truncGEπ_zero_of_truncLT_negOne.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t :
    CategoryTheory.Triangulated.TStructure
      C)
  {X₂ X₃ : C}
  (φ :
    (CategoryTheory.shiftFunctor C 1).obj
        ((t.truncLT (-1)).obj X₃) ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X₂) :
  CategoryTheory.CategoryStruct.comp φ
      ((CategoryTheory.shiftFunctor C
            1).map
        ((t.truncGEπ 0).app X₂)) =
    0

Something wrong, better idea? Suggest a change

12.3.42. heartCohObjIsoOfHeartShift🔗

For a heart object E and integer n, the underlying object of H^n_t(E[-n]) is canonically isomorphic to E.

Construction: Uses the isomorphisms \tau^{\le n}(E[-n]) \cong E[-n] and E[-n] \cong \tau^{\ge n}(E[-n]) (since E[-n] is concentrated in degree n), composed with a shift isomorphism.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.heartCohObjIsoOfHeartShift.{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.heartCoh C h n
        ((CategoryTheory.shiftFunctor C (-n)).obj E.obj)).obj ≅
    E.obj
CategoryTheory.Triangulated.HeartStabilityData.heartCohObjIsoOfHeartShift.{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.heartCoh
        C h n
        ((CategoryTheory.shiftFunctor C
              (-n)).obj
          E.obj)).obj ≅
    E.obj

Something wrong, better idea? Suggest a change

12.3.43. heartCohClass_zero_of_heart🔗

For a heart object E, the degree-0 heart cohomology class equals the class [E]: \texttt{heartCohClass}(0, E) = [E].

Proof: Simplifies using \texttt{heartCohClass}, \texttt{heartCoh}, and the isomorphism \texttt{H0FunctorObjIsoOfHeart}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_zero_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.heartCohClass C h 0
      E.obj =
    CategoryTheory.Triangulated.HeartK0.of C h E
CategoryTheory.Triangulated.HeartStabilityData.heartCohClass_zero_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.heartCohClass
      C h 0 E.obj =
    CategoryTheory.Triangulated.HeartK0.of
      C h E

Something wrong, better idea? Suggest a change