Bridgeland Stability Conditions

12.8. HeartEquivalence: Reverse🔗

12.8.1. stabilityFunctionOnHeart_hasHN_local🔗

The heart stability function induced by a stability condition \sigma has the Harder--Narasimhan property: every nonzero heart object admits an HN filtration.

Proof: By strong induction on the length of the slicing HN filtration F of E in \mathcal{C}. If F has a single factor, E \in \mathcal{P}(\varphi) and is already semistable in the heart. Otherwise, split F into the prefix (an object with fewer HN factors) and the last semistable factor. The prefix lies in the heart by the phase bounds, and has an abelian HN filtration by the inductive hypothesis. The last factor is semistable in the heart by \texttt{stabilityFunctionOnHeart\_isSemistable\_of\_mem\_P\_phi}. Appending via \texttt{append\_hn\_filtration\_of\_mono} gives the desired filtration of E.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart_hasHN_local.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (σ : CategoryTheory.Triangulated.StabilityCondition C) :
  (CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart
      C σ).HasHNProperty
CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart_hasHN_local.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition
      C) :
  (CategoryTheory.Triangulated.StabilityCondition.stabilityFunctionOnHeart
      C σ).HasHNProperty

Something wrong, better idea? Suggest a change

12.8.2. StabilityCondition.toHeartStabilityData🔗

[Proposition 5.3] forward: stability condition → heart stability data

Proposition 5.3a / forward direction. Every stability condition \sigma determines heart stability data: the t-structure is \sigma.\mathrm{slicing}.\mathrm{toTStructure}, boundedness follows from the HN filtration axiom, the stability function is Z restricted to the heart, and the HN property comes from \texttt{stabilityFunctionOnHeart\_hasHN\_local}.

Construction: Packages the four fields: t-structure, boundedness proof, restricted stability function, and HN property proof.

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

  1. The t-structure is σ.slicing.toTStructure.

  2. Boundedness follows from the HN filtration axiom.

  3. The stability function on the heart P((0, 1]) is the restriction of Z.

  4. The HN property on the heart is obtained by taking the slicing HN filtration of a heart object and reading it as an abelian HN filtration, exactly as in Bridgeland's proof of Proposition 5.3.

Something wrong, better idea? Suggest a change

12.8.3. phaseBase🔗

Normalize a real phase \varphi into the standard Bridgeland interval (0, 1].

Construction: Defined as \texttt{toIocMod} with period 1 and base point 0.

🔗def
CategoryTheory.Triangulated.phaseBase (φ : ℝ) : ℝ
CategoryTheory.Triangulated.phaseBase
  (φ : ℝ) : ℝ

Something wrong, better idea? Suggest a change

12.8.4. phaseIndex🔗

The integral shift needed to move a phase into (0, 1]: \varphi = \texttt{phaseBase}(\varphi) + \texttt{phaseIndex}(\varphi).

Construction: Defined as \texttt{toIocDiv} with period 1 and base point 0.

🔗def
CategoryTheory.Triangulated.phaseIndex (φ : ℝ) : ℤ
CategoryTheory.Triangulated.phaseIndex
  (φ : ℝ) : ℤ

Something wrong, better idea? Suggest a change

12.8.5. phaseBase_mem🔗

\texttt{phaseBase}(\varphi) \in (0, 1] for all \varphi \in \mathbb{R}.

Proof: Immediate from the modular arithmetic property of \texttt{toIocMod}.

🔗theorem
CategoryTheory.Triangulated.phaseBase_mem (φ : ℝ) :
  CategoryTheory.Triangulated.phaseBase φ ∈ Set.Ioc 0 1
CategoryTheory.Triangulated.phaseBase_mem
  (φ : ℝ) :
  CategoryTheory.Triangulated.phaseBase
      φ ∈
    Set.Ioc 0 1

Something wrong, better idea? Suggest a change

12.8.6. phaseBase_add_phaseIndex🔗

\texttt{phaseBase}(\varphi) + \texttt{phaseIndex}(\varphi) = \varphi.

Proof: The defining identity of the floor-mod decomposition.

🔗theorem
CategoryTheory.Triangulated.phaseBase_add_phaseIndex (φ : ℝ) :
  CategoryTheory.Triangulated.phaseBase φ +
      ↑(CategoryTheory.Triangulated.phaseIndex φ) =
    φ
CategoryTheory.Triangulated.phaseBase_add_phaseIndex
  (φ : ℝ) :
  CategoryTheory.Triangulated.phaseBase
        φ +
      ↑(CategoryTheory.Triangulated.phaseIndex
          φ) =
    φ

Something wrong, better idea? Suggest a change

12.8.7. phaseBase_add_one🔗

\texttt{phaseBase}(\varphi + 1) = \texttt{phaseBase}(\varphi).

Proof: Adding the period does not change the mod-representative.

🔗theorem
CategoryTheory.Triangulated.phaseBase_add_one (φ : ℝ) :
  CategoryTheory.Triangulated.phaseBase (φ + 1) =
    CategoryTheory.Triangulated.phaseBase φ
CategoryTheory.Triangulated.phaseBase_add_one
  (φ : ℝ) :
  CategoryTheory.Triangulated.phaseBase
      (φ + 1) =
    CategoryTheory.Triangulated.phaseBase
      φ

Something wrong, better idea? Suggest a change

12.8.8. phaseIndex_add_one🔗

\texttt{phaseIndex}(\varphi + 1) = \texttt{phaseIndex}(\varphi) + 1.

Proof: Adding the period increments the floor by one.

🔗theorem
CategoryTheory.Triangulated.phaseIndex_add_one (φ : ℝ) :
  CategoryTheory.Triangulated.phaseIndex (φ + 1) =
    CategoryTheory.Triangulated.phaseIndex φ + 1
CategoryTheory.Triangulated.phaseIndex_add_one
  (φ : ℝ) :
  CategoryTheory.Triangulated.phaseIndex
      (φ + 1) =
    CategoryTheory.Triangulated.phaseIndex
        φ +
      1

Something wrong, better idea? Suggest a change

12.8.9. phaseBase_eq_of_mem_Ioc🔗

If \varphi \in (0, 1], then \texttt{phaseBase}(\varphi) = \varphi.

Proof: The mod operation fixes elements already in the fundamental domain.

🔗theorem
CategoryTheory.Triangulated.phaseBase_eq_of_mem_Ioc {φ : ℝ}
  (hφ : φ ∈ Set.Ioc 0 1) : CategoryTheory.Triangulated.phaseBase φ = φ
CategoryTheory.Triangulated.phaseBase_eq_of_mem_Ioc
  {φ : ℝ} (hφ : φ ∈ Set.Ioc 0 1) :
  CategoryTheory.Triangulated.phaseBase
      φ =
    φ

Something wrong, better idea? Suggest a change

12.8.10. phaseIndex_eq_zero_of_mem_Ioc🔗

If \varphi \in (0, 1], then \texttt{phaseIndex}(\varphi) = 0.

Proof: If \varphi is already in the fundamental domain, no shift is needed.

🔗theorem
CategoryTheory.Triangulated.phaseIndex_eq_zero_of_mem_Ioc {φ : ℝ}
  (hφ : φ ∈ Set.Ioc 0 1) : CategoryTheory.Triangulated.phaseIndex φ = 0
CategoryTheory.Triangulated.phaseIndex_eq_zero_of_mem_Ioc
  {φ : ℝ} (hφ : φ ∈ Set.Ioc 0 1) :
  CategoryTheory.Triangulated.phaseIndex
      φ =
    0

Something wrong, better idea? Suggest a change

12.8.11. HeartSemistable🔗

Semistability in the heart with respect to the heart stability function.

Construction: An abbreviation: \texttt{StabilityFunction.IsSemistable} applied to h.Z and a heart object E.

🔗def
CategoryTheory.Triangulated.HeartSemistable.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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) : Prop
CategoryTheory.Triangulated.HeartSemistable.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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) : Prop

Something wrong, better idea? Suggest a change

12.8.12. HeartPhase🔗

The phase of a heart object measured by the heart stability function.

Construction: An abbreviation: \texttt{StabilityFunction.phase} applied to h.Z and a heart object E.

🔗def
CategoryTheory.Triangulated.HeartPhase.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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.HeartPhase.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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) : ℝ

Something wrong, better idea? Suggest a change

12.8.13. shiftedHeartSemistable🔗

Bridgeland's reverse-direction phase slices: objects whose [-n]-shift lies in the heart and is semistable there of phase \psi, together with zero objects.

Construction: An \texttt{ObjectProperty} on \mathcal{C}: X satisfies \texttt{shiftedHeartSemistable}(\psi, n) iff X is zero, or X[-n] \in \operatorname{heart}(t) with heart-semistable phase \psi.

🔗def
CategoryTheory.Triangulated.shiftedHeartSemistable.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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 : ℤ) : CategoryTheory.ObjectProperty C
CategoryTheory.Triangulated.shiftedHeartSemistable.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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 : ℤ) :
  CategoryTheory.ObjectProperty C

Something wrong, better idea? Suggest a change

12.8.14. phasePredicate🔗

The ambient phase predicate attached to heart stability data: normalize the phase into (0, 1], then shift the object back by the corresponding integer.

Construction: Defined as \texttt{shiftedHeartSemistable}(\texttt{phaseBase}(\varphi), \texttt{phaseIndex}(\varphi)).

🔗def
CategoryTheory.Triangulated.phasePredicate.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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.ObjectProperty C
CategoryTheory.Triangulated.phasePredicate.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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.ObjectProperty C

Something wrong, better idea? Suggest a change

12.8.15. shiftedHeartSemistable_zero_iff🔗

X belongs to \texttt{shiftedHeartSemistable}(h, \psi, 0) if and only if X is zero or X itself (without any shift) is a heart object that is semistable of phase \psi.

Proof: Both directions transfer the heart-membership and stability data along the canonical isomorphism X[0] \cong X using \texttt{prop\_of\_iso} and \texttt{isSemistable\_of\_iso}.

🔗theorem
CategoryTheory.Triangulated.shiftedHeartSemistable_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) (ψ : ℝ)
  (X : C) :
  CategoryTheory.Triangulated.shiftedHeartSemistable C h ψ 0 X ↔
    CategoryTheory.Limits.IsZero X ∨
      ∃ (hX : h.t.heart X),
        have XH := { obj := X, property := hX };
        CategoryTheory.Triangulated.HeartSemistable C h XH ∧
          CategoryTheory.Triangulated.HeartPhase C h XH = ψ
CategoryTheory.Triangulated.shiftedHeartSemistable_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)
  (ψ : ℝ) (X : C) :
  CategoryTheory.Triangulated.shiftedHeartSemistable
      C h ψ 0 X ↔
    CategoryTheory.Limits.IsZero X ∨
      ∃ (hX : h.t.heart X),
        have XH :=
          { obj := X, property := hX };
        CategoryTheory.Triangulated.HeartSemistable
            C h XH ∧
          CategoryTheory.Triangulated.HeartPhase
              C h XH =
            ψ

Something wrong, better idea? Suggest a change

12.8.16. phasePredicate_iff_of_mem_Ioc🔗

For \varphi \in (0, 1], \texttt{phasePredicate}(\varphi, X) iff X is zero or X lies in the heart with heart-semistable phase \varphi.

Proof: Since \texttt{phaseBase}(\varphi) = \varphi and \texttt{phaseIndex}(\varphi) = 0, the shifted heart condition reduces to the unshifted one.

🔗theorem
CategoryTheory.Triangulated.phasePredicate_iff_of_mem_Ioc.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) {φ : ℝ}
  (hφ : φ ∈ Set.Ioc 0 1) (X : C) :
  CategoryTheory.Triangulated.phasePredicate C h φ X ↔
    CategoryTheory.Limits.IsZero X ∨
      ∃ (hX : h.t.heart X),
        have XH := { obj := X, property := hX };
        CategoryTheory.Triangulated.HeartSemistable C h XH ∧
          CategoryTheory.Triangulated.HeartPhase C h XH = φ
CategoryTheory.Triangulated.phasePredicate_iff_of_mem_Ioc.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {φ : ℝ} (hφ : φ ∈ Set.Ioc 0 1) (X : C) :
  CategoryTheory.Triangulated.phasePredicate
      C h φ X ↔
    CategoryTheory.Limits.IsZero X ∨
      ∃ (hX : h.t.heart X),
        have XH :=
          { obj := X, property := hX };
        CategoryTheory.Triangulated.HeartSemistable
            C h XH ∧
          CategoryTheory.Triangulated.HeartPhase
              C h XH =
            φ

Something wrong, better idea? Suggest a change

12.8.17. arg_add_lt_max_local🔗

For two complex numbers z_1, z_2 in the upper half-plane union with distinct arguments, the argument of their sum is strictly less than the maximum of their arguments.

Proof: Delegates directly to the general \texttt{arg\_add\_lt\_max} lemma.

🔗theorem
CategoryTheory.Triangulated.arg_add_lt_max_local {z₁ z₂ : ℂ}
  (h₁ : z₁ ∈ CategoryTheory.upperHalfPlaneUnion)
  (h₂ : z₂ ∈ CategoryTheory.upperHalfPlaneUnion)
  (hne : z₁.arg ≠ z₂.arg) : (z₁ + z₂).arg < max z₁.arg z₂.arg
CategoryTheory.Triangulated.arg_add_lt_max_local
  {z₁ z₂ : ℂ}
  (h₁ :
    z₁ ∈
      CategoryTheory.upperHalfPlaneUnion)
  (h₂ :
    z₂ ∈
      CategoryTheory.upperHalfPlaneUnion)
  (hne : z₁.arg ≠ z₂.arg) :
  (z₁ + z₂).arg < max z₁.arg z₂.arg

Something wrong, better idea? Suggest a change

12.8.18. heart_phase_le_of_epi🔗

If p : E \to Q is an epimorphism in the heart with E semistable and Q nonzero, then \mathrm{phase}(E) \le \mathrm{phase}(Q).

Proof: Delegates to the general result \texttt{phase\_le\_of\_epi} applied to h.Z.

🔗theorem
CategoryTheory.Triangulated.heart_phase_le_of_epi.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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 Q : h.t.heart.FullSubcategory} (p : E ⟶ Q) [CategoryTheory.Epi p]
  (hss : CategoryTheory.Triangulated.HeartSemistable C h E)
  (hQ : ¬CategoryTheory.Limits.IsZero Q) :
  CategoryTheory.Triangulated.HeartPhase C h E ≤
    CategoryTheory.Triangulated.HeartPhase C h Q
CategoryTheory.Triangulated.heart_phase_le_of_epi.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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 Q : h.t.heart.FullSubcategory}
  (p : E ⟶ Q) [CategoryTheory.Epi p]
  (hss :
    CategoryTheory.Triangulated.HeartSemistable
      C h E)
  (hQ : ¬CategoryTheory.Limits.IsZero Q) :
  CategoryTheory.Triangulated.HeartPhase C
      h E ≤
    CategoryTheory.Triangulated.HeartPhase
      C h Q

Something wrong, better idea? Suggest a change

12.8.19. heart_hom_zero_of_semistable_phase_gt🔗

If E and F are heart-semistable with \mathrm{phase}(F) < \mathrm{phase}(E), then every morphism f : E \to F in the heart is zero.

Proof: Delegates to the general stability-function result \texttt{hom\_zero\_of\_semistable\_phase\_gt} applied to the heart stability function h.Z.

🔗theorem
CategoryTheory.Triangulated.heart_hom_zero_of_semistable_phase_gt.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  {E F : h.t.heart.FullSubcategory}
  (hE : CategoryTheory.Triangulated.HeartSemistable C h E)
  (hF : CategoryTheory.Triangulated.HeartSemistable C h F)
  (hph :
    CategoryTheory.Triangulated.HeartPhase C h F <
      CategoryTheory.Triangulated.HeartPhase C h E)
  (f : E ⟶ F) : f = 0
CategoryTheory.Triangulated.heart_hom_zero_of_semistable_phase_gt.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {E F : h.t.heart.FullSubcategory}
  (hE :
    CategoryTheory.Triangulated.HeartSemistable
      C h E)
  (hF :
    CategoryTheory.Triangulated.HeartSemistable
      C h F)
  (hph :
    CategoryTheory.Triangulated.HeartPhase
        C h F <
      CategoryTheory.Triangulated.HeartPhase
        C h E)
  (f : E ⟶ F) : f = 0

Something wrong, better idea? Suggest a change

12.8.20. phasePredicate_hom_zero_of_mem_Ioc🔗

For \varphi_1, \varphi_2 \in (0, 1] with \varphi_2 < \varphi_1, every morphism f : E \to F with E \in P(\varphi_1) and F \in P(\varphi_2) is zero.

Proof: Reduces to Hom vanishing between heart-semistable objects of decreasing phase via \texttt{heart\_hom\_zero\_of\_semistable\_phase\_gt}.

🔗theorem
CategoryTheory.Triangulated.phasePredicate_hom_zero_of_mem_Ioc.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) {φ₁ φ₂ : ℝ}
  (hφ₁ : φ₁ ∈ Set.Ioc 0 1) (hφ₂ : φ₂ ∈ Set.Ioc 0 1) {E F : C}
  (hE : CategoryTheory.Triangulated.phasePredicate C h φ₁ E)
  (hF : CategoryTheory.Triangulated.phasePredicate C h φ₂ F)
  (hgap : φ₂ < φ₁) (f : E ⟶ F) : f = 0
CategoryTheory.Triangulated.phasePredicate_hom_zero_of_mem_Ioc.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {φ₁ φ₂ : ℝ} (hφ₁ : φ₁ ∈ Set.Ioc 0 1)
  (hφ₂ : φ₂ ∈ Set.Ioc 0 1) {E F : C}
  (hE :
    CategoryTheory.Triangulated.phasePredicate
      C h φ₁ E)
  (hF :
    CategoryTheory.Triangulated.phasePredicate
      C h φ₂ F)
  (hgap : φ₂ < φ₁) (f : E ⟶ F) : f = 0

Something wrong, better idea? Suggest a change

12.8.21. shiftedHeartSemistable_closedUnderIso🔗

The shifted heart semistability predicate is closed under isomorphism.

Proof: An isomorphism X \cong Y induces an isomorphism X[-n] \cong Y[-n] in the heart, preserving semistability and phase.

🔗theorem
CategoryTheory.Triangulated.shiftedHeartSemistable_closedUnderIso.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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 : ℤ) :
  (CategoryTheory.Triangulated.shiftedHeartSemistable C h ψ
      n).IsClosedUnderIsomorphisms
CategoryTheory.Triangulated.shiftedHeartSemistable_closedUnderIso.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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 : ℤ) :
  (CategoryTheory.Triangulated.shiftedHeartSemistable
      C h ψ n).IsClosedUnderIsomorphisms

Something wrong, better idea? Suggest a change

12.8.22. phasePredicate_closedUnderIso🔗

The phase predicate P(\varphi) is closed under isomorphism.

Proof: Follows from \texttt{shiftedHeartSemistable\_closedUnderIso}.

🔗theorem
CategoryTheory.Triangulated.phasePredicate_closedUnderIso.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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.phasePredicate C h
      φ).IsClosedUnderIsomorphisms
CategoryTheory.Triangulated.phasePredicate_closedUnderIso.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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.phasePredicate
      C h φ).IsClosedUnderIsomorphisms

Something wrong, better idea? Suggest a change

12.8.23. phasePredicate_instClosedUnderIso🔗

Instance: P(\varphi) is closed under isomorphism.

Proof: Delegates to \texttt{phasePredicate\_closedUnderIso}.

🔗theorem
CategoryTheory.Triangulated.phasePredicate_instClosedUnderIso.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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.phasePredicate C h
      φ).IsClosedUnderIsomorphisms
CategoryTheory.Triangulated.phasePredicate_instClosedUnderIso.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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.phasePredicate
      C h φ).IsClosedUnderIsomorphisms

Something wrong, better idea? Suggest a change

12.8.24. shiftedHeartSemistable_shift_iff🔗

X belongs to \texttt{shiftedHeartSemistable}(h, \psi, n) if and only if X[1] belongs to \texttt{shiftedHeartSemistable}(h, \psi, n+1).

Proof: Both directions transfer data along the canonical isomorphism (X[1])[-(n+1)] \cong X[-n] given by the shift-addition law, using \texttt{prop\_of\_iso} and \texttt{isSemistable\_of\_iso}.

🔗theorem
CategoryTheory.Triangulated.shiftedHeartSemistable_shift_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) (ψ : ℝ) (n : ℤ)
  (X : C) :
  CategoryTheory.Triangulated.shiftedHeartSemistable C h ψ n X ↔
    CategoryTheory.Triangulated.shiftedHeartSemistable C h ψ (n + 1)
      ((CategoryTheory.shiftFunctor C 1).obj X)
CategoryTheory.Triangulated.shiftedHeartSemistable_shift_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)
  (ψ : ℝ) (n : ℤ) (X : C) :
  CategoryTheory.Triangulated.shiftedHeartSemistable
      C h ψ n X ↔
    CategoryTheory.Triangulated.shiftedHeartSemistable
      C h ψ (n + 1)
      ((CategoryTheory.shiftFunctor C
            1).obj
        X)

Something wrong, better idea? Suggest a change

12.8.25. phasePredicate_shift_iff🔗

Shifting by [1] raises the phase by 1: X \in P(\varphi) iff X[1] \in P(\varphi + 1).

Proof: Uses \texttt{phaseBase\_add\_one} and \texttt{phaseIndex\_add\_one} to reduce to \texttt{shiftedHeartSemistable\_shift\_iff}.

🔗theorem
CategoryTheory.Triangulated.phasePredicate_shift_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) (φ : ℝ)
  (X : C) :
  CategoryTheory.Triangulated.phasePredicate C h φ X ↔
    CategoryTheory.Triangulated.phasePredicate C h (φ + 1)
      ((CategoryTheory.shiftFunctor C 1).obj X)
CategoryTheory.Triangulated.phasePredicate_shift_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)
  (φ : ℝ) (X : C) :
  CategoryTheory.Triangulated.phasePredicate
      C h φ X ↔
    CategoryTheory.Triangulated.phasePredicate
      C h (φ + 1)
      ((CategoryTheory.shiftFunctor C
            1).obj
        X)

Something wrong, better idea? Suggest a change

12.8.26. phasePredicate_shift_int🔗

Shifting by [n] raises the phase by n: X \in P(\varphi) iff X[n] \in P(\varphi + n).

Proof: Induction on n (positive and negative cases), using \texttt{phasePredicate\_shift\_iff} for each step.

🔗theorem
CategoryTheory.Triangulated.phasePredicate_shift_int.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) (φ : ℝ) (X : C)
  (n : ℤ) :
  CategoryTheory.Triangulated.phasePredicate C h φ X ↔
    CategoryTheory.Triangulated.phasePredicate C h (φ + ↑n)
      ((CategoryTheory.shiftFunctor C n).obj X)
CategoryTheory.Triangulated.phasePredicate_shift_int.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (φ : ℝ) (X : C) (n : ℤ) :
  CategoryTheory.Triangulated.phasePredicate
      C h φ X ↔
    CategoryTheory.Triangulated.phasePredicate
      C h (φ + ↑n)
      ((CategoryTheory.shiftFunctor C
            n).obj
        X)

Something wrong, better idea? Suggest a change

12.8.27. phaseIndex_lt_phase🔗

\texttt{phaseIndex}(\varphi) < \varphi for all \varphi \in \mathbb{R}.

Proof: Since \texttt{phaseBase}(\varphi) > 0 and \varphi = \texttt{phaseBase}(\varphi) + \texttt{phaseIndex}(\varphi), the strict positivity gives the inequality.

🔗theorem
CategoryTheory.Triangulated.phaseIndex_lt_phase (φ : ℝ) :
  ↑(CategoryTheory.Triangulated.phaseIndex φ) < φ
CategoryTheory.Triangulated.phaseIndex_lt_phase
  (φ : ℝ) :
  ↑(CategoryTheory.Triangulated.phaseIndex
        φ) <
    φ

Something wrong, better idea? Suggest a change

12.8.28. phase_le_phaseIndex_add_one🔗

\varphi \le \texttt{phaseIndex}(\varphi) + 1 for all \varphi \in \mathbb{R}.

Proof: Since \texttt{phaseBase}(\varphi) \le 1 and \varphi = \texttt{phaseBase}(\varphi) + \texttt{phaseIndex}(\varphi), the upper bound on the base gives the inequality.

🔗theorem
CategoryTheory.Triangulated.phase_le_phaseIndex_add_one (φ : ℝ) :
  φ ≤ ↑(CategoryTheory.Triangulated.phaseIndex φ) + 1
CategoryTheory.Triangulated.phase_le_phaseIndex_add_one
  (φ : ℝ) :
  φ ≤
    ↑(CategoryTheory.Triangulated.phaseIndex
          φ) +
      1

Something wrong, better idea? Suggest a change

12.8.29. phaseIndex_le_of_lt🔗

If \varphi_2 < \varphi_1, then \texttt{phaseIndex}(\varphi_2) \le \texttt{phaseIndex}(\varphi_1).

Proof: If the index were strictly larger, then \texttt{phaseIndex}(\varphi_1) + 1 \le \texttt{phaseIndex}(\varphi_2), giving \varphi_1 \ge \texttt{phaseIndex}(\varphi_1) + 1 > \varphi_2, a contradiction with \texttt{phaseIndex\_lt\_phase} and \texttt{phase\_le\_phaseIndex\_add\_one}.

🔗theorem
CategoryTheory.Triangulated.phaseIndex_le_of_lt {φ₁ φ₂ : ℝ}
  (hlt : φ₂ < φ₁) :
  CategoryTheory.Triangulated.phaseIndex φ₂ ≤
    CategoryTheory.Triangulated.phaseIndex φ₁
CategoryTheory.Triangulated.phaseIndex_le_of_lt
  {φ₁ φ₂ : ℝ} (hlt : φ₂ < φ₁) :
  CategoryTheory.Triangulated.phaseIndex
      φ₂ ≤
    CategoryTheory.Triangulated.phaseIndex
      φ₁

Something wrong, better idea? Suggest a change

12.8.30. phasePredicate_hom_zero🔗

For arbitrary phases \varphi_1 > \varphi_2, every morphism f : E \to F with E \in P(\varphi_1) and F \in P(\varphi_2) is zero.

Proof: If \texttt{phaseIndex}(\varphi_2) = \texttt{phaseIndex}(\varphi_1), both objects shift to the same heart and the result follows from heart Hom vanishing. Otherwise the index gap forces a nonzero t-amplitude mismatch between the shifted objects, and the morphism vanishes by the t-structure orthogonality \texttt{zero\_of\_isLE\_of\_isGE}.

🔗theorem
CategoryTheory.Triangulated.phasePredicate_hom_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 F : C} (hE : CategoryTheory.Triangulated.phasePredicate C h φ₁ E)
  (hF : CategoryTheory.Triangulated.phasePredicate C h φ₂ F)
  (hgap : φ₂ < φ₁) (f : E ⟶ F) : f = 0
CategoryTheory.Triangulated.phasePredicate_hom_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 F : C}
  (hE :
    CategoryTheory.Triangulated.phasePredicate
      C h φ₁ E)
  (hF :
    CategoryTheory.Triangulated.phasePredicate
      C h φ₂ F)
  (hgap : φ₂ < φ₁) (f : E ⟶ F) : f = 0

Something wrong, better idea? Suggest a change

12.8.31. PhasePackage🔗

A local reverse-direction package: the induced phase family from heart stability data, together with the isomorphism, shift, and Hom-vanishing axioms of a Bridgeland slicing.

Construction: Fields: the heart stability data, the phase predicate P : \mathbb{R} \to \texttt{ObjectProperty}\; \mathcal{C}, closure under isomorphism, zero membership, shift compatibility P(\varphi)(X) \Leftrightarrow P(\varphi+1)(X[1]), and Hom vanishing \varphi_2 < \varphi_1 \Rightarrow \operatorname{Hom}(P(\varphi_1), P(\varphi_2)) = 0.

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

Constructor

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

Fields

heartData : CategoryTheory.Triangulated.HeartStabilityData C

The heart-side input data of Proposition 5.3.

P : ℝ → CategoryTheory.ObjectProperty C

The induced phase predicate on the ambient triangulated category.

closedUnderIso : ∀ (φ : ℝ), (self.P φ).IsClosedUnderIsomorphisms

The phase predicates are closed under isomorphism.

zero_mem : ∀ (φ : ℝ), self.P φ 0

The zero object lies in every phase.

shift_iff : ∀ (φ : ℝ) (X : C), self.P φ X ↔ self.P (φ + 1) ((CategoryTheory.shiftFunctor C 1).obj X)

Shifting by [1] raises the phase by 1.

hom_vanishing : ∀ (φ₁ φ₂ : ℝ) (A B : C), φ₂ < φ₁ → self.P φ₁ A → self.P φ₂ B → ∀ (f : A ⟶ B), f = 0

Morphisms from higher phase to lower phase vanish.

Something wrong, better idea? Suggest a change

12.8.32. PhasePackage.toHeartStabilityData🔗

Forget the reverse-direction phase package back to the original heart data.

Construction: Projects the \texttt{heartData} field.

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

Something wrong, better idea? Suggest a change

12.8.33. HeartStabilityData.toPhasePackage🔗

[Proposition 5.3] reverse: partial, missing central charge construction + HN existence

Proposition 5.3b / reverse direction. Heart stability data determines the ambient phase family P(\varphi) with the isomorphism, shift, and Hom-vanishing axioms.

Construction: Packages \texttt{phasePredicate} together with the proofs \texttt{phasePredicate\_closedUnderIso}, \texttt{phasePredicate\_shift\_iff}, and \texttt{phasePredicate\_hom\_zero}.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.toPhasePackage.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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.PhasePackage C
CategoryTheory.Triangulated.HeartStabilityData.toPhasePackage.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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.PhasePackage
    C

  1. constructing the ambient central charge K₀ C →+ ℂ;

  2. proving HN existence for the induced phase family.

Something wrong, better idea? Suggest a change

12.8.34. StabilityCondition.toPhasePackage🔗

The reverse-direction phase package extracted from a stability condition.

Construction: Composes \texttt{toHeartStabilityData} with \texttt{toPhasePackage}.

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

Something wrong, better idea? Suggest a change

12.8.35. StabilityCondition.roundtrip🔗

Proposition 5.3c / left inverse. Starting from \sigma, extracting heart data, and reconstructing the phase package agrees with the direct construction: (\sigma.\mathrm{toHeartStabilityData}).\mathrm{toPhasePackage} = \sigma.\mathrm{toPhasePackage}.

Proof: Definitional equality (\texttt{rfl}).

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.roundtrip.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (σ : CategoryTheory.Triangulated.StabilityCondition C) :
  CategoryTheory.Triangulated.HeartStabilityData.toPhasePackage C
      (CategoryTheory.Triangulated.StabilityCondition.toHeartStabilityData
        C σ) =
    CategoryTheory.Triangulated.StabilityCondition.toPhasePackage C σ
CategoryTheory.Triangulated.StabilityCondition.roundtrip.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition
      C) :
  CategoryTheory.Triangulated.HeartStabilityData.toPhasePackage
      C
      (CategoryTheory.Triangulated.StabilityCondition.toHeartStabilityData
        C σ) =
    CategoryTheory.Triangulated.StabilityCondition.toPhasePackage
      C σ

Something wrong, better idea? Suggest a change

12.8.36. HeartStabilityData.roundtrip🔗

Proposition 5.3c / right inverse. Forgetting the phase package back to heart data recovers the original input: (h.\mathrm{toPhasePackage}).\mathrm{toHeartStabilityData} = h.

Proof: Definitional equality (\texttt{rfl}).

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.roundtrip.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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.PhasePackage.toHeartStabilityData C
      (CategoryTheory.Triangulated.HeartStabilityData.toPhasePackage C
        h) =
    h
CategoryTheory.Triangulated.HeartStabilityData.roundtrip.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject 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.PhasePackage.toHeartStabilityData
      C
      (CategoryTheory.Triangulated.HeartStabilityData.toPhasePackage
        C h) =
    h

Something wrong, better idea? Suggest a change

12.8.37. heart_shortExact_triangle🔗

Given a short exact sequence 0 \to A \to B \to Q \to 0 with A, B, Q in the heart (as objects and morphisms in the ambient category), there exists a distinguished triangle A \to B \to Q \to A[1].

Proof: Lifts the given data to the heart full subcategory, applies \texttt{heartFullSubcategory\_shortExact\_triangle}, then transports the connecting morphism back to the ambient category.

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

Something wrong, better idea? Suggest a change