Bridgeland Stability Conditions

14.1. Deformation: BoundaryTriangle🔗

14.1.1. exists_upper_boundary_triangle🔗

Given a slicing, a cutoff b_1 > a, and an object Q \in \mathcal{P}((a, b_2)), there exists a distinguished triangle X \to Q \to Y \to X[1] with X \in \mathcal{P}(\ge b_1) and Y \in \mathcal{P}((a, b_1)). This is the upper boundary truncation.

Proof: Apply the t-structure truncation of the phase-shifted slicing at b_1 to separate the high-phase part X from the low-phase part Y. The interval bound on Y follows from the triangle and the phase bounds.

🔗theorem
CategoryTheory.Triangulated.exists_upper_boundary_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] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b₁ b₂ : ℝ}
  (hab₁ : a < b₁) {Q : C}
  (hQ : CategoryTheory.Triangulated.Slicing.intervalProp C s a b₂ Q) :
  ∃ X Y f g h,
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Triangulated.Slicing.geProp C s b₁ X ∧
        CategoryTheory.Triangulated.Slicing.intervalProp C s a b₁ Y
CategoryTheory.Triangulated.exists_upper_boundary_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]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b₁ b₂ : ℝ} (hab₁ : a < b₁) {Q : C}
  (hQ :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b₂ Q) :
  ∃ X Y f g h,
    CategoryTheory.Pretriangulated.Triangle.mk
          f g h ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Triangulated.Slicing.geProp
          C s b₁ X ∧
        CategoryTheory.Triangulated.Slicing.intervalProp
          C s a b₁ Y

Something wrong, better idea? Suggest a change

14.1.2. gtProp_of_geProp🔗

If E \in \mathcal{P}(\ge b) and a < b, then E \in \mathcal{P}(> a).

Proof: Immediate from the definitions: all phases \ge b > a.

🔗theorem
CategoryTheory.Triangulated.Slicing.gtProp_of_geProp.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b : ℝ} (hab : a < b)
  {E : C} (hE : CategoryTheory.Triangulated.Slicing.geProp C s b E) :
  CategoryTheory.Triangulated.Slicing.gtProp C s a E
CategoryTheory.Triangulated.Slicing.gtProp_of_geProp.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b : ℝ} (hab : a < b) {E : C}
  (hE :
    CategoryTheory.Triangulated.Slicing.geProp
      C s b E) :
  CategoryTheory.Triangulated.Slicing.gtProp
    C s a E

Something wrong, better idea? Suggest a change

14.1.3. wPhaseOf_gt_of_geProp_target🔗

If E \in \mathcal{P}((a, b)) is nonzero with \sigma-phases \ge \psi + \varepsilon_0, then the W-phase of E exceeds \psi.

Proof: All HN factors have phase \ge \psi + \varepsilon_0, so perturbation gives W-phase > \psi + \varepsilon_0 - \varepsilon_0 = \psi. Apply the K_0 imaginary-part summation and sin/Im conversion.

🔗theorem
CategoryTheory.Triangulated.wPhaseOf_gt_of_geProp_target.{v, u, u'}
  (C : Type u) [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b ψ ε₀ : ℝ} {E : C}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b E)
  (hEne : ¬CategoryTheory.Limits.IsZero E)
  (hGe :
    CategoryTheory.Triangulated.Slicing.geProp C σ.slicing (ψ + ε₀) E)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (henv_lo : a + ε₀ ≤ ψ)
  (henv_hi : ψ ≤ b - ε₀) (hthin : b - a + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀))) :
  ψ <
    CategoryTheory.Triangulated.wPhaseOf
      (W (CategoryTheory.Triangulated.cl C v E)) ((a + b) / 2)
CategoryTheory.Triangulated.wPhaseOf_gt_of_geProp_target.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b ψ ε₀ : ℝ} {E : C}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a b E)
  (hEne : ¬CategoryTheory.Limits.IsZero E)
  (hGe :
    CategoryTheory.Triangulated.Slicing.geProp
      C σ.slicing (ψ + ε₀) E)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (henv_lo : a + ε₀ ≤ ψ)
  (henv_hi : ψ ≤ b - ε₀)
  (hthin : b - a + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀))) :
  ψ <
    CategoryTheory.Triangulated.wPhaseOf
      (W
        (CategoryTheory.Triangulated.cl C
          v E))
      ((a + b) / 2)

Something wrong, better idea? Suggest a change

14.1.4. intervalProp_of_upper_boundary_triangle🔗

The low-phase vertex Y of an upper boundary triangle lies in \mathcal{P}((a, b_1)).

Proof: The lower phase bound comes from the triangle: \phi^-(Y) > a since Q \in \mathcal{P}((a, b_2)) and X \in \mathcal{P}(\ge b_1). The upper bound \phi^+(Y) < b_1 comes from the t-structure truncation.

🔗theorem
CategoryTheory.Triangulated.intervalProp_of_upper_boundary_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]
  (s : CategoryTheory.Triangulated.Slicing C) {a b₁ b₂ : ℝ}
  (hab₁ : a < b₁) (hab₂ : a < b₂) (hb₁ : b₁ ≤ a + 1) {Q X Y : C}
  (hQ : CategoryTheory.Triangulated.Slicing.intervalProp C s a b₂ Q)
  (hX_ge : CategoryTheory.Triangulated.Slicing.geProp C s b₁ X)
  (hY : CategoryTheory.Triangulated.Slicing.intervalProp C s a b₁ Y)
  {f : X ⟶ Q} {g : Q ⟶ Y}
  {h : Y ⟶ (CategoryTheory.shiftFunctor C 1).obj X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.Slicing.intervalProp C s a b₂ X
CategoryTheory.Triangulated.intervalProp_of_upper_boundary_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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b₁ b₂ : ℝ} (hab₁ : a < b₁)
  (hab₂ : a < b₂) (hb₁ : b₁ ≤ a + 1)
  {Q X Y : C}
  (hQ :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b₂ Q)
  (hX_ge :
    CategoryTheory.Triangulated.Slicing.geProp
      C s b₁ X)
  (hY :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b₁ Y)
  {f : X ⟶ Q} {g : Q ⟶ Y}
  {h :
    Y ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.Slicing.intervalProp
    C s a b₂ X

Something wrong, better idea? Suggest a change

14.1.5. wPhaseOf_gt_of_upper_boundary_triangle🔗

The W-phase of the high-phase vertex in an upper boundary triangle exceeds \psi.

Proof: The high-phase vertex has all \sigma-phases \ge \psi + \varepsilon_0, so wPhaseOf_gt_of_geProp_target applies.

🔗theorem
CategoryTheory.Triangulated.wPhaseOf_gt_of_upper_boundary_triangle.{v,
    u, u'}
  (C : Type u) [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b₁ b₂ ψ ε₀ : ℝ} (hab₁ : a < b₁) (hab₂ : a < b₂) (hb : b₁ ≤ b₂)
  {Q X Y : C}
  (hQ :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b₂ Q)
  (hX_ge : CategoryTheory.Triangulated.Slicing.geProp C σ.slicing b₁ X)
  (hY :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b₁ Y)
  (hXne : ¬CategoryTheory.Limits.IsZero X) (hε₀ : 0 < ε₀)
  (hε₀2 : ε₀ < 1 / 4) (henv_lo : a + ε₀ ≤ ψ) (henv_hi : ψ ≤ b₁ - ε₀)
  (hthin : b₂ - a + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀)))
  {f : X ⟶ Q} {g : Q ⟶ Y}
  {h : Y ⟶ (CategoryTheory.shiftFunctor C 1).obj X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  ψ <
    CategoryTheory.Triangulated.wPhaseOf
      (W (CategoryTheory.Triangulated.cl C v X)) ((a + b₂) / 2)
CategoryTheory.Triangulated.wPhaseOf_gt_of_upper_boundary_triangle.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b₁ b₂ ψ ε₀ : ℝ} (hab₁ : a < b₁)
  (hab₂ : a < b₂) (hb : b₁ ≤ b₂)
  {Q X Y : C}
  (hQ :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a b₂ Q)
  (hX_ge :
    CategoryTheory.Triangulated.Slicing.geProp
      C σ.slicing b₁ X)
  (hY :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a b₁ Y)
  (hXne : ¬CategoryTheory.Limits.IsZero X)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (henv_lo : a + ε₀ ≤ ψ)
  (henv_hi : ψ ≤ b₁ - ε₀)
  (hthin : b₂ - a + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀)))
  {f : X ⟶ Q} {g : Q ⟶ Y}
  {h :
    Y ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  ψ <
    CategoryTheory.Triangulated.wPhaseOf
      (W
        (CategoryTheory.Triangulated.cl C
          v X))
      ((a + b₂) / 2)

Something wrong, better idea? Suggest a change

14.1.6. wPhaseOf_gt_of_upper_source_boundary_target🔗

Given a distinguished triangle X \to Q \to Y \to X[1] with Q \in \mathcal{P}((\psi-\varepsilon_0, \phi+\varepsilon_0)), X \in \mathcal{P}(\geq \psi+\varepsilon_0), Y \in \mathcal{P}((\psi-\varepsilon_0, \psi+\varepsilon_0)), \phi - \varepsilon_0 < \psi \leq \phi, and W sufficiently close to Z, then \psi < \mathrm{wPhaseOf}(W([X]), \tfrac{\psi-\varepsilon_0+\phi+\varepsilon_0}{2}).

Proof: The interval \mathcal{P}((\psi-\varepsilon_0, \phi+\varepsilon_0)) is thin (width < 1), and the boundary triangle places X in that interval with \phi^-(X) \geq \psi + \varepsilon_0, so wPhaseOf_gt_of_upper_boundary_triangle applies directly.

🔗theorem
CategoryTheory.Triangulated.wPhaseOf_gt_of_upper_source_boundary_target.{v,
    u, u'}
  (C : Type u) [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {φ ψ ε₀ : ℝ} {Q X Y : C}
  (hQ :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing
      (ψ - ε₀) (φ + ε₀) Q)
  (hX_ge :
    CategoryTheory.Triangulated.Slicing.geProp C σ.slicing (ψ + ε₀) X)
  (hY :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing
      (ψ - ε₀) (ψ + ε₀) Y)
  (hXne : ¬CategoryTheory.Limits.IsZero X) (hε₀ : 0 < ε₀)
  (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8) (hψ_lo : φ - ε₀ < ψ)
  (hψ_le : ψ ≤ φ)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀)))
  {f : X ⟶ Q} {g : Q ⟶ Y}
  {h : Y ⟶ (CategoryTheory.shiftFunctor C 1).obj X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  ψ <
    CategoryTheory.Triangulated.wPhaseOf
      (W (CategoryTheory.Triangulated.cl C v X))
      ((ψ - ε₀ + (φ + ε₀)) / 2)
CategoryTheory.Triangulated.wPhaseOf_gt_of_upper_source_boundary_target.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {φ ψ ε₀ : ℝ} {Q X Y : C}
  (hQ :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing (ψ - ε₀) (φ + ε₀) Q)
  (hX_ge :
    CategoryTheory.Triangulated.Slicing.geProp
      C σ.slicing (ψ + ε₀) X)
  (hY :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing (ψ - ε₀) (ψ + ε₀) Y)
  (hXne : ¬CategoryTheory.Limits.IsZero X)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (hε₀8 : ε₀ < 1 / 8) (hψ_lo : φ - ε₀ < ψ)
  (hψ_le : ψ ≤ φ)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀)))
  {f : X ⟶ Q} {g : Q ⟶ Y}
  {h :
    Y ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  ψ <
    CategoryTheory.Triangulated.wPhaseOf
      (W
        (CategoryTheory.Triangulated.cl C
          v X))
      ((ψ - ε₀ + (φ + ε₀)) / 2)

Something wrong, better idea? Suggest a change

14.1.7. wPhaseOf_gt_of_upper_source_boundary_P_phi🔗

Given a distinguished triangle X \to Q \to Y \to X[1] with Q \in \mathcal{P}((\psi-\varepsilon_0, \phi+\varepsilon_0)), X \in \mathcal{P}(\geq \psi+\varepsilon_0), and Y \in \mathcal{P}(\phi), if \phi - \varepsilon_0 < \psi \leq \phi and W is sufficiently close to Z, then the W-phase of X satisfies \psi < \mathrm{wPhaseOf}(W([X]), \tfrac{\psi-\varepsilon_0+\phi+\varepsilon_0}{2}).

Proof: The \mathcal{P}(\phi)-semistability of Y is used to place Y in the thin interval \mathcal{P}((\psi-\varepsilon_0, \psi+\varepsilon_0)), reducing the statement to wPhaseOf_gt_of_upper_source_boundary_target.

🔗theorem
CategoryTheory.Triangulated.wPhaseOf_gt_of_upper_source_boundary_P_phi.{v,
    u, u'}
  (C : Type u) [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {φ ψ ε₀ : ℝ} {Q X Y : C}
  (hQ :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing
      (ψ - ε₀) (φ + ε₀) Q)
  (hX_ge :
    CategoryTheory.Triangulated.Slicing.geProp C σ.slicing (ψ + ε₀) X)
  (hY_Pφ : σ.slicing.P φ Y) (hXne : ¬CategoryTheory.Limits.IsZero X)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8)
  (hψ_lo : φ - ε₀ < ψ) (hψ_hi : ψ < φ + ε₀) (hψ_le : ψ ≤ φ)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀)))
  {f : X ⟶ Q} {g : Q ⟶ Y}
  {h : Y ⟶ (CategoryTheory.shiftFunctor C 1).obj X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  ψ <
    CategoryTheory.Triangulated.wPhaseOf
      (W (CategoryTheory.Triangulated.cl C v X))
      ((ψ - ε₀ + (φ + ε₀)) / 2)
CategoryTheory.Triangulated.wPhaseOf_gt_of_upper_source_boundary_P_phi.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {φ ψ ε₀ : ℝ} {Q X Y : C}
  (hQ :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing (ψ - ε₀) (φ + ε₀) Q)
  (hX_ge :
    CategoryTheory.Triangulated.Slicing.geProp
      C σ.slicing (ψ + ε₀) X)
  (hY_Pφ : σ.slicing.P φ Y)
  (hXne : ¬CategoryTheory.Limits.IsZero X)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (hε₀8 : ε₀ < 1 / 8) (hψ_lo : φ - ε₀ < ψ)
  (hψ_hi : ψ < φ + ε₀) (hψ_le : ψ ≤ φ)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀)))
  {f : X ⟶ Q} {g : Q ⟶ Y}
  {h :
    Y ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  ψ <
    CategoryTheory.Triangulated.wPhaseOf
      (W
        (CategoryTheory.Triangulated.cl C
          v X))
      ((ψ - ε₀ + (φ + ε₀)) / 2)

Something wrong, better idea? Suggest a change

14.1.8. wPhaseOf_lt_of_leProp_source🔗

If E \in \mathcal{P}((a,b)) is nonzero with E \in \mathcal{P}(\leq \psi - \varepsilon_0), the interval (a,b) is thin (b - a + 2\varepsilon_0 < 1), a + \varepsilon_0 \leq \psi \leq b - \varepsilon_0, and W is sufficiently close to Z, then \mathrm{wPhaseOf}(W([E]), \tfrac{a+b}{2}) < \psi.

Proof: All HN phases of E are bounded above by \psi - \varepsilon_0. After rotating W([E]) by e^{-i\pi\psi} and decomposing via the HN filtration, the imaginary part is shown to be negative using the perturbation bounds on each semistable factor, which forces the W-phase below \psi.

🔗theorem
CategoryTheory.Triangulated.wPhaseOf_lt_of_leProp_source.{v, u, u'}
  (C : Type u) [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b ψ ε₀ : ℝ} {E : C}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b E)
  (hEne : ¬CategoryTheory.Limits.IsZero E)
  (hLe :
    CategoryTheory.Triangulated.Slicing.leProp C σ.slicing (ψ - ε₀) E)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (henv_lo : a + ε₀ ≤ ψ)
  (henv_hi : ψ ≤ b - ε₀) (hthin : b - a + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀))) :
  CategoryTheory.Triangulated.wPhaseOf
      (W (CategoryTheory.Triangulated.cl C v E)) ((a + b) / 2) <
    ψ
CategoryTheory.Triangulated.wPhaseOf_lt_of_leProp_source.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b ψ ε₀ : ℝ} {E : C}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a b E)
  (hEne : ¬CategoryTheory.Limits.IsZero E)
  (hLe :
    CategoryTheory.Triangulated.Slicing.leProp
      C σ.slicing (ψ - ε₀) E)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (henv_lo : a + ε₀ ≤ ψ)
  (henv_hi : ψ ≤ b - ε₀)
  (hthin : b - a + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀))) :
  CategoryTheory.Triangulated.wPhaseOf
      (W
        (CategoryTheory.Triangulated.cl C
          v E))
      ((a + b) / 2) <
    ψ

Something wrong, better idea? Suggest a change

14.1.9. exists_lower_boundary_triangle🔗

Dual of exists_upper_boundary_triangle: there exists a distinguished triangle X \to Q \to Y with Y \in \mathcal{P}(\le a_1) and X \in \mathcal{P}((a_1, b)).

Proof: Apply the dual t-structure truncation at a_1.

🔗theorem
CategoryTheory.Triangulated.exists_lower_boundary_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] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a₁ a₂ b : ℝ}
  (ha₁ : a₁ < b) {K : C}
  (hK : CategoryTheory.Triangulated.Slicing.intervalProp C s a₂ b K) :
  ∃ X Y f g h,
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Triangulated.Slicing.intervalProp C s a₁ b X ∧
        CategoryTheory.Triangulated.Slicing.leProp C s a₁ Y
CategoryTheory.Triangulated.exists_lower_boundary_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]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a₁ a₂ b : ℝ} (ha₁ : a₁ < b) {K : C}
  (hK :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a₂ b K) :
  ∃ X Y f g h,
    CategoryTheory.Pretriangulated.Triangle.mk
          f g h ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles ∧
      CategoryTheory.Triangulated.Slicing.intervalProp
          C s a₁ b X ∧
        CategoryTheory.Triangulated.Slicing.leProp
          C s a₁ Y

Something wrong, better idea? Suggest a change

14.1.10. intervalProp_of_lower_boundary_triangle🔗

If K \in \mathcal{P}((a_2, b)), X \in \mathcal{P}((a_1, b)), and Y \in \mathcal{P}(\leq a_1) fit into a distinguished triangle X \to K \to Y \to X[1] with a_2 \leq a_1 < b, then Y \in \mathcal{P}((a_2, b)).

Proof: The upper phase bound for Y comes from \phi^+(Y) \leq a_1 < b. The lower bound a_2 < \phi^-(Y) follows from \phi^-(K) being bounded below (using that K \in \mathcal{P}((a_2,b))) and propagation through the triangle via X \in \mathcal{P}(\geq a_1).

🔗theorem
CategoryTheory.Triangulated.intervalProp_of_lower_boundary_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]
  (s : CategoryTheory.Triangulated.Slicing C) {a₁ a₂ b : ℝ}
  (ha₁ : a₁ < b) (ha : a₂ ≤ a₁) {K X Y : C}
  (hK : CategoryTheory.Triangulated.Slicing.intervalProp C s a₂ b K)
  (hX : CategoryTheory.Triangulated.Slicing.intervalProp C s a₁ b X)
  (hY_le : CategoryTheory.Triangulated.Slicing.leProp C s a₁ Y)
  {f : X ⟶ K} {g : K ⟶ Y}
  {h : Y ⟶ (CategoryTheory.shiftFunctor C 1).obj X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.Slicing.intervalProp C s a₂ b Y
CategoryTheory.Triangulated.intervalProp_of_lower_boundary_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]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a₁ a₂ b : ℝ} (ha₁ : a₁ < b)
  (ha : a₂ ≤ a₁) {K X Y : C}
  (hK :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a₂ b K)
  (hX :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a₁ b X)
  (hY_le :
    CategoryTheory.Triangulated.Slicing.leProp
      C s a₁ Y)
  {f : X ⟶ K} {g : K ⟶ Y}
  {h :
    Y ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.Slicing.intervalProp
    C s a₂ b Y

Something wrong, better idea? Suggest a change

14.1.11. wPhaseOf_lt_of_lower_boundary_triangle🔗

Given a distinguished triangle X \to K \to Y \to X[1] with K \in \mathcal{P}((a_2,b)), X \in \mathcal{P}((a_1,b)), Y \in \mathcal{P}(\leq a_1) (with a_2 \leq a_1 < b), and Y nonzero, if W is sufficiently close to Z and a_1 + \varepsilon_0 \leq \psi \leq b - \varepsilon_0, then \mathrm{wPhaseOf}(W([Y]), \tfrac{a_2+b}{2}) < \psi.

Proof: First Y \in \mathcal{P}((a_2,b)) is established by intervalProp_of_lower_boundary_triangle, and then Y \in \mathcal{P}(\leq \psi - \varepsilon_0) is inherited from the \mathcal{P}(\leq a_1) bound; finally wPhaseOf_lt_of_leProp_source applies.

🔗theorem
CategoryTheory.Triangulated.wPhaseOf_lt_of_lower_boundary_triangle.{v,
    u, u'}
  (C : Type u) [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a₁ a₂ b ψ ε₀ : ℝ} (ha₁ : a₁ < b) (ha : a₂ ≤ a₁) {K X Y : C}
  (hK :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a₂ b K)
  (hX :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a₁ b X)
  (hY_le : CategoryTheory.Triangulated.Slicing.leProp C σ.slicing a₁ Y)
  (hYne : ¬CategoryTheory.Limits.IsZero Y) (hε₀ : 0 < ε₀)
  (hε₀2 : ε₀ < 1 / 4) (henv_lo : a₁ + ε₀ ≤ ψ) (henv_hi : ψ ≤ b - ε₀)
  (hthin : b - a₂ + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀)))
  {f : X ⟶ K} {g : K ⟶ Y}
  {h : Y ⟶ (CategoryTheory.shiftFunctor C 1).obj X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.wPhaseOf
      (W (CategoryTheory.Triangulated.cl C v Y)) ((a₂ + b) / 2) <
    ψ
CategoryTheory.Triangulated.wPhaseOf_lt_of_lower_boundary_triangle.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a₁ a₂ b ψ ε₀ : ℝ} (ha₁ : a₁ < b)
  (ha : a₂ ≤ a₁) {K X Y : C}
  (hK :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a₂ b K)
  (hX :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a₁ b X)
  (hY_le :
    CategoryTheory.Triangulated.Slicing.leProp
      C σ.slicing a₁ Y)
  (hYne : ¬CategoryTheory.Limits.IsZero Y)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (henv_lo : a₁ + ε₀ ≤ ψ)
  (henv_hi : ψ ≤ b - ε₀)
  (hthin : b - a₂ + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀)))
  {f : X ⟶ K} {g : K ⟶ Y}
  {h :
    Y ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.wPhaseOf
      (W
        (CategoryTheory.Triangulated.cl C
          v Y))
      ((a₂ + b) / 2) <
    ψ

Something wrong, better idea? Suggest a change

14.1.12. wPhaseOf_lt_of_lower_source_boundary_target🔗

Given a distinguished triangle X \to K \to Y \to X[1] with K \in \mathcal{P}((\phi-\varepsilon_0, \psi+\varepsilon_0)), X \in \mathcal{P}((\psi-\varepsilon_0, \psi+\varepsilon_0)), Y \in \mathcal{P}(\leq \psi-\varepsilon_0) nonzero, \phi \leq \psi < \phi + \varepsilon_0, and W sufficiently close to Z, then \mathrm{wPhaseOf}(W([Y]), \tfrac{\phi-\varepsilon_0+\psi+\varepsilon_0}{2}) < \psi.

Proof: The interval (\phi-\varepsilon_0, \psi+\varepsilon_0) is thin by the hypothesis \varepsilon_0 < 1/8 and \psi < \phi + \varepsilon_0; then wPhaseOf_lt_of_lower_boundary_triangle applies with a_1 = \psi - \varepsilon_0, a_2 = \phi - \varepsilon_0, b = \psi + \varepsilon_0.

🔗theorem
CategoryTheory.Triangulated.wPhaseOf_lt_of_lower_source_boundary_target.{v,
    u, u'}
  (C : Type u) [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {φ ψ ε₀ : ℝ} {K X Y : C}
  (hK :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing
      (φ - ε₀) (ψ + ε₀) K)
  (hX :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing
      (ψ - ε₀) (ψ + ε₀) X)
  (hY_le :
    CategoryTheory.Triangulated.Slicing.leProp C σ.slicing (ψ - ε₀) Y)
  (hYne : ¬CategoryTheory.Limits.IsZero Y) (hε₀ : 0 < ε₀)
  (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8) (hψ_hi : ψ < φ + ε₀)
  (hφ_le : φ ≤ ψ)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀)))
  {f : X ⟶ K} {g : K ⟶ Y}
  {h : Y ⟶ (CategoryTheory.shiftFunctor C 1).obj X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.wPhaseOf
      (W (CategoryTheory.Triangulated.cl C v Y))
      ((φ - ε₀ + (ψ + ε₀)) / 2) <
    ψ
CategoryTheory.Triangulated.wPhaseOf_lt_of_lower_source_boundary_target.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {φ ψ ε₀ : ℝ} {K X Y : C}
  (hK :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing (φ - ε₀) (ψ + ε₀) K)
  (hX :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing (ψ - ε₀) (ψ + ε₀) X)
  (hY_le :
    CategoryTheory.Triangulated.Slicing.leProp
      C σ.slicing (ψ - ε₀) Y)
  (hYne : ¬CategoryTheory.Limits.IsZero Y)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (hε₀8 : ε₀ < 1 / 8) (hψ_hi : ψ < φ + ε₀)
  (hφ_le : φ ≤ ψ)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀)))
  {f : X ⟶ K} {g : K ⟶ Y}
  {h :
    Y ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.wPhaseOf
      (W
        (CategoryTheory.Triangulated.cl C
          v Y))
      ((φ - ε₀ + (ψ + ε₀)) / 2) <
    ψ

Something wrong, better idea? Suggest a change

14.1.13. wPhaseOf_lt_of_lower_source_boundary_P_phi🔗

Given a distinguished triangle X \to K \to Y \to X[1] with K \in \mathcal{P}((\phi-\varepsilon_0, \psi+\varepsilon_0)), X \in \mathcal{P}(\phi) (the semistable slice), Y \in \mathcal{P}(\leq \psi-\varepsilon_0) nonzero, \phi \leq \psi < \phi + \varepsilon_0, and W sufficiently close to Z, then \mathrm{wPhaseOf}(W([Y]), \tfrac{\phi-\varepsilon_0+\psi+\varepsilon_0}{2}) < \psi.

Proof: The \mathcal{P}(\phi)-semistability of X places X in the thin interval \mathcal{P}((\psi-\varepsilon_0, \psi+\varepsilon_0)), then wPhaseOf_lt_of_lower_source_boundary_target applies.

🔗theorem
CategoryTheory.Triangulated.wPhaseOf_lt_of_lower_source_boundary_P_phi.{v,
    u, u'}
  (C : Type u) [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {φ ψ ε₀ : ℝ} {K X Y : C}
  (hK :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing
      (φ - ε₀) (ψ + ε₀) K)
  (hX_Pφ : σ.slicing.P φ X)
  (hY_le :
    CategoryTheory.Triangulated.Slicing.leProp C σ.slicing (ψ - ε₀) Y)
  (hYne : ¬CategoryTheory.Limits.IsZero Y) (hε₀ : 0 < ε₀)
  (hε₀2 : ε₀ < 1 / 4) (hε₀8 : ε₀ < 1 / 8) (hψ_hi : ψ < φ + ε₀)
  (hφ_le : φ ≤ ψ)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀)))
  {f : X ⟶ K} {g : K ⟶ Y}
  {h : Y ⟶ (CategoryTheory.shiftFunctor C 1).obj X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.wPhaseOf
      (W (CategoryTheory.Triangulated.cl C v Y))
      ((φ - ε₀ + (ψ + ε₀)) / 2) <
    ψ
CategoryTheory.Triangulated.wPhaseOf_lt_of_lower_source_boundary_P_phi.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {φ ψ ε₀ : ℝ} {K X Y : C}
  (hK :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing (φ - ε₀) (ψ + ε₀) K)
  (hX_Pφ : σ.slicing.P φ X)
  (hY_le :
    CategoryTheory.Triangulated.Slicing.leProp
      C σ.slicing (ψ - ε₀) Y)
  (hYne : ¬CategoryTheory.Limits.IsZero Y)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (hε₀8 : ε₀ < 1 / 8) (hψ_hi : ψ < φ + ε₀)
  (hφ_le : φ ≤ ψ)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀)))
  {f : X ⟶ K} {g : K ⟶ Y}
  {h :
    Y ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        X}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  CategoryTheory.Triangulated.wPhaseOf
      (W
        (CategoryTheory.Triangulated.cl C
          v Y))
      ((φ - ε₀ + (ψ + ε₀)) / 2) <
    ψ

Something wrong, better idea? Suggest a change

14.1.14. exists_upper_boundary_strictShortExact🔗

In a thin interval subcategory \mathcal{P}((a, b_2)) (with b_2 - a \le 1), given a < b_1 \le b_2 and Q \in \mathcal{P}((a, b_2)), there exists a strict short exact sequence 0 \to X_1 \to Q \to X_3 \to 0 in \mathcal{P}((a, b_2)) with X_1 \in \mathcal{P}(\ge b_1) and X_3 \in \mathcal{P}((a, b_1)).

Proof: Apply exists_upper_boundary_triangle to obtain the distinguished triangle, then use strictShortExact_of_distTriang to package it as a strict short exact sequence in the thin interval category.

🔗theorem
CategoryTheory.Triangulated.exists_upper_boundary_strictShortExact.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a b₁ b₂ : ℝ}
  [Fact (a < b₂)] [Fact (b₂ - a ≤ 1)] (hab₁ : a < b₁) (hb : b₁ ≤ b₂)
  {Q : C}
  (hQ : CategoryTheory.Triangulated.Slicing.intervalProp C s a b₂ Q) :
  ∃ S,
    CategoryTheory.StrictShortExact S ∧
      S.X₂ = { obj := Q, property := hQ } ∧
        CategoryTheory.Triangulated.Slicing.geProp C s b₁ S.X₁.obj ∧
          CategoryTheory.Triangulated.Slicing.intervalProp C s a b₁
            S.X₃.obj
CategoryTheory.Triangulated.exists_upper_boundary_strictShortExact.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a b₁ b₂ : ℝ} [Fact (a < b₂)]
  [Fact (b₂ - a ≤ 1)] (hab₁ : a < b₁)
  (hb : b₁ ≤ b₂) {Q : C}
  (hQ :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b₂ Q) :
  ∃ S,
    CategoryTheory.StrictShortExact S ∧
      S.X₂ =
          { obj := Q, property := hQ } ∧
        CategoryTheory.Triangulated.Slicing.geProp
            C s b₁ S.X₁.obj ∧
          CategoryTheory.Triangulated.Slicing.intervalProp
            C s a b₁ S.X₃.obj

Something wrong, better idea? Suggest a change

14.1.15. exists_lower_boundary_strictShortExact🔗

In a finite-length interval subcategory, lower boundary truncation yields a strict short exact sequence.

Proof: Dual of exists_upper_boundary_strictShortExact using the lower boundary triangle.

🔗theorem
CategoryTheory.Triangulated.exists_lower_boundary_strictShortExact.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {a₁ a₂ b : ℝ}
  [Fact (a₂ < b)] [Fact (b - a₂ ≤ 1)] (ha₁ : a₁ < b) (ha : a₂ ≤ a₁)
  {K : C}
  (hK : CategoryTheory.Triangulated.Slicing.intervalProp C s a₂ b K) :
  ∃ S,
    CategoryTheory.StrictShortExact S ∧
      S.X₂ = { obj := K, property := hK } ∧
        CategoryTheory.Triangulated.Slicing.intervalProp C s a₁ b
            S.X₁.obj ∧
          CategoryTheory.Triangulated.Slicing.leProp C s a₁ S.X₃.obj
CategoryTheory.Triangulated.exists_lower_boundary_strictShortExact.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {a₁ a₂ b : ℝ} [Fact (a₂ < b)]
  [Fact (b - a₂ ≤ 1)] (ha₁ : a₁ < b)
  (ha : a₂ ≤ a₁) {K : C}
  (hK :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a₂ b K) :
  ∃ S,
    CategoryTheory.StrictShortExact S ∧
      S.X₂ =
          { obj := K, property := hK } ∧
        CategoryTheory.Triangulated.Slicing.intervalProp
            C s a₁ b S.X₁.obj ∧
          CategoryTheory.Triangulated.Slicing.leProp
            C s a₁ S.X₃.obj

Something wrong, better idea? Suggest a change

14.1.16. intervalProp_of_wSemistable_upper_target🔗

If E is W-semistable of phase \psi in \mathcal{P}((a, b)) and has \sigma-phases confined by Lemma 7.3, then E \in \mathcal{P}((a, \psi + \varepsilon_0)).

Proof: Phase confinement gives \phi^+(E) < \psi + \varepsilon_0 and \phi^-(E) > a (from interval membership), so all HN phases lie in (a, \psi + \varepsilon_0).

🔗theorem
CategoryTheory.Triangulated.intervalProp_of_wSemistable_upper_target.{v,
    u, u'}
  (C : Type u) [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b₁ b₂ ψ ε₀ : ℝ} (hab₁ : a < b₁) (hab₂ : a < b₂) (hb : b₁ ≤ b₂)
  {E : C}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab₂)
      E ψ)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (henv_lo : a + ε₀ ≤ ψ)
  (henv_hi : ψ ≤ b₁ - ε₀) (hthin₂ : b₂ - a + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀))) :
  CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b₁ E
CategoryTheory.Triangulated.intervalProp_of_wSemistable_upper_target.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b₁ b₂ ψ ε₀ : ℝ} (hab₁ : a < b₁)
  (hab₂ : a < b₂) (hb : b₁ ≤ b₂) {E : C}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab₂)
      E ψ)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (henv_lo : a + ε₀ ≤ ψ)
  (henv_hi : ψ ≤ b₁ - ε₀)
  (hthin₂ : b₂ - a + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀))) :
  CategoryTheory.Triangulated.Slicing.intervalProp
    C σ.slicing a b₁ E

Something wrong, better idea? Suggest a change

14.1.17. intervalProp_of_wSemistable_lower_target🔗

If E is W-semistable of phase \psi in \mathcal{P}((a, b)), then E \in \mathcal{P}((\psi - \varepsilon_0, b)).

Proof: Phase confinement gives \phi^-(E) > \psi - \varepsilon_0 and \phi^+(E) < b.

🔗theorem
CategoryTheory.Triangulated.intervalProp_of_wSemistable_lower_target.{v,
    u, u'}
  (C : Type u) [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  [CategoryTheory.IsTriangulated C] {a₁ a₂ b ψ ε₀ : ℝ} (ha₁ : a₁ < b)
  (ha₂ : a₂ < b) (ha : a₁ ≤ a₂) {E : C}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW ha₁)
      E ψ)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) (henv_lo : a₂ + ε₀ ≤ ψ)
  (henv_hi : ψ ≤ b - ε₀) (hthin₁ : b - a₁ + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀))) :
  CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a₂ b E
CategoryTheory.Triangulated.intervalProp_of_wSemistable_lower_target.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, 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'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  [CategoryTheory.IsTriangulated C]
  {a₁ a₂ b ψ ε₀ : ℝ} (ha₁ : a₁ < b)
  (ha₂ : a₂ < b) (ha : a₁ ≤ a₂) {E : C}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW ha₁)
      E ψ)
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (henv_lo : a₂ + ε₀ ≤ ψ)
  (henv_hi : ψ ≤ b - ε₀)
  (hthin₁ : b - a₁ + 2 * ε₀ < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀))) :
  CategoryTheory.Triangulated.Slicing.intervalProp
    C σ.slicing a₂ b E

Something wrong, better idea? Suggest a change