Bridgeland Stability Conditions

14.15. Deformation: PhaseConfinement🔗

14.15.1. perturb_gt_of_perturb🔗

Shift per-factor perturbation bounds \phi - \varepsilon_0 < w < \phi + \varepsilon_0 to the lower endpoint: a - \varepsilon_0 < w < a - \varepsilon_0 + 1. Used by all phase confinement arguments.

Proof: Immediate arithmetic from the per-factor bounds and the thinness constraint b - a + 2\varepsilon_0 < 1.

🔗theorem
CategoryTheory.Triangulated.perturb_gt_of_perturb.{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)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a
      b}
  {ε₀ : ℝ}
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ → φ < b → φ - ε₀ < ssf.wPhase F ∧ ssf.wPhase F < φ + ε₀)
  (hthin : b - a + 2 * ε₀ < 1) (F : C) (φ : ℝ) (hP : σ.slicing.P φ F)
  (hFne : ¬CategoryTheory.Limits.IsZero F) (haφ : a < φ) (hφb : φ < b) :
  a - ε₀ < ssf.wPhase F ∧ ssf.wPhase F < a - ε₀ + 1
CategoryTheory.Triangulated.perturb_gt_of_perturb.{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)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v σ.slicing a b}
  {ε₀ : ℝ}
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b →
              φ - ε₀ < ssf.wPhase F ∧
                ssf.wPhase F < φ + ε₀)
  (hthin : b - a + 2 * ε₀ < 1) (F : C)
  (φ : ℝ) (hP : σ.slicing.P φ F)
  (hFne : ¬CategoryTheory.Limits.IsZero F)
  (haφ : a < φ) (hφb : φ < b) :
  a - ε₀ < ssf.wPhase F ∧
    ssf.wPhase F < a - ε₀ + 1

Something wrong, better idea? Suggest a change

14.15.2. perturb_lt_of_perturb🔗

Shift per-factor perturbation bounds to the upper endpoint: b + \varepsilon_0 - 1 < w < b + \varepsilon_0.

Proof: Symmetric arithmetic manipulation of the per-factor bounds.

🔗theorem
CategoryTheory.Triangulated.perturb_lt_of_perturb.{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)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a
      b}
  {ε₀ : ℝ}
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ → φ < b → φ - ε₀ < ssf.wPhase F ∧ ssf.wPhase F < φ + ε₀)
  (hthin : b - a + 2 * ε₀ < 1) (F : C) (φ : ℝ) (hP : σ.slicing.P φ F)
  (hFne : ¬CategoryTheory.Limits.IsZero F) (haφ : a < φ) (hφb : φ < b) :
  b + ε₀ - 1 < ssf.wPhase F ∧ ssf.wPhase F < b + ε₀
CategoryTheory.Triangulated.perturb_lt_of_perturb.{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)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v σ.slicing a b}
  {ε₀ : ℝ}
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b →
              φ - ε₀ < ssf.wPhase F ∧
                ssf.wPhase F < φ + ε₀)
  (hthin : b - a + 2 * ε₀ < 1) (F : C)
  (φ : ℝ) (hP : σ.slicing.P φ F)
  (hFne : ¬CategoryTheory.Limits.IsZero F)
  (haφ : a < φ) (hφb : φ < b) :
  b + ε₀ - 1 < ssf.wPhase F ∧
    ssf.wPhase F < b + ε₀

Something wrong, better idea? Suggest a change

14.15.3. phiPlus_lt_of_wSemistable🔗

Bridgeland's Lemma 7.3 (upper bound). If E is W-semistable of W-phase \psi in \mathcal{P}((a, b)) with the interval thin enough (b - a + 2\varepsilon_0 < 1) and each nonzero semistable factor has W-phase within \varepsilon_0 of its \sigma-phase, then \sigma.\phi^+(E) < \psi + \varepsilon_0.

Proof: By contradiction: assume \phi^+(E) \ge \psi + \varepsilon_0. Split E at the gap below \phi = \phi^+(E) in the HN filtration. The resulting top-phase subobject K \in \mathcal{P}(\phi) has \operatorname{wPhaseOf}(W(K)) > \phi - \varepsilon_0 \ge \psi, contradicting W-semistability.

🔗theorem
CategoryTheory.Triangulated.phiPlus_lt_of_wSemistable.{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)
  {E : C} {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a
      b}
  {ψ : ℝ}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
      E ψ)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hthin : b - a + 2 * ε₀ < 1)
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b → φ - ε₀ < ssf.wPhase F ∧ ssf.wPhase F < φ + ε₀) :
  CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing E ⋯ < ψ + ε₀
CategoryTheory.Triangulated.phiPlus_lt_of_wSemistable.{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)
  {E : C} {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v σ.slicing a b}
  {ψ : ℝ}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C ssf E ψ)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀)
  (hthin : b - a + 2 * ε₀ < 1)
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b →
              φ - ε₀ < ssf.wPhase F ∧
                ssf.wPhase F < φ + ε₀) :
  CategoryTheory.Triangulated.Slicing.phiPlus
      C σ.slicing E ⋯ <
    ψ + ε₀

Something wrong, better idea? Suggest a change

14.15.4. phiMinus_gt_of_wSemistable🔗

Bridgeland's Lemma 7.3 (lower bound). If E is W-semistable of W-phase \psi in \mathcal{P}((a, b)), then \psi - \varepsilon_0 < \sigma.\phi^-(E).

Proof: Split E at cutoff \psi - \varepsilon_0. The quotient Y (with \sigma-phases \le \psi - \varepsilon_0) has \operatorname{Im}(W(Y) \cdot e^{-i\pi\psi}) < 0 via the sin/Im argument. Combined with \operatorname{Im}(W(E) \cdot e^{-i\pi\psi}) = 0, this gives \operatorname{Im}(W(K) \cdot e^{-i\pi\psi}) > 0, hence \operatorname{wPhaseOf}(W(K)) > \psi, contradicting W-semistability.

🔗theorem
CategoryTheory.Triangulated.phiMinus_gt_of_wSemistable.{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)
  {E : C} {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a
      b}
  {ψ : ℝ}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
      E ψ)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hthin : b - a + 2 * ε₀ < 1)
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b → φ - ε₀ < ssf.wPhase F ∧ ssf.wPhase F < φ + ε₀) :
  ψ - ε₀ < CategoryTheory.Triangulated.Slicing.phiMinus C σ.slicing E ⋯
CategoryTheory.Triangulated.phiMinus_gt_of_wSemistable.{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)
  {E : C} {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v σ.slicing a b}
  {ψ : ℝ}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C ssf E ψ)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀)
  (hthin : b - a + 2 * ε₀ < 1)
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b →
              φ - ε₀ < ssf.wPhase F ∧
                ssf.wPhase F < φ + ε₀) :
  ψ - ε₀ <
    CategoryTheory.Triangulated.Slicing.phiMinus
      C σ.slicing E ⋯

Something wrong, better idea? Suggest a change

14.15.5. phase_confinement_of_wSemistable🔗

Bridgeland's Lemma 7.3 (phase confinement). If E is W-semistable of W-phase \psi in \mathcal{P}((a, b)) and the interval is thin enough, then \psi - \varepsilon_0 < \sigma.\phi^-(E) and \sigma.\phi^+(E) < \psi + \varepsilon_0.

Proof: Combines phiMinus_gt_of_wSemistable and phiPlus_lt_of_wSemistable.

🔗theorem
CategoryTheory.Triangulated.phase_confinement_of_wSemistable.{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)
  {E : C} {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a
      b}
  {ψ : ℝ}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
      E ψ)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hthin : b - a + 2 * ε₀ < 1)
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b → φ - ε₀ < ssf.wPhase F ∧ ssf.wPhase F < φ + ε₀) :
  ψ - ε₀ <
      CategoryTheory.Triangulated.Slicing.phiMinus C σ.slicing E ⋯ ∧
    CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing E ⋯ < ψ + ε₀
CategoryTheory.Triangulated.phase_confinement_of_wSemistable.{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)
  {E : C} {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v σ.slicing a b}
  {ψ : ℝ}
  (hSS :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C ssf E ψ)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀)
  (hthin : b - a + 2 * ε₀ < 1)
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b →
              φ - ε₀ < ssf.wPhase F ∧
                ssf.wPhase F < φ + ε₀) :
  ψ - ε₀ <
      CategoryTheory.Triangulated.Slicing.phiMinus
        C σ.slicing E ⋯ ∧
    CategoryTheory.Triangulated.Slicing.phiPlus
        C σ.slicing E ⋯ <
      ψ + ε₀

Something wrong, better idea? Suggest a change

14.15.6. hom_eq_zero_of_wSemistable_gap🔗

Weak hom-vanishing for W-semistable objects. If E is W-semistable of phase \psi_1 and F is W-semistable of phase \psi_2 with \psi_1 > \psi_2 + 2\varepsilon_0, then \operatorname{Hom}(E, F) = 0.

Proof: Phase confinement puts E and F in disjoint \sigma-intervals: E \in \mathcal{P}((\psi_1 - \varepsilon_0 - \delta, \psi_1 + \varepsilon_0 + \delta)) and F \in \mathcal{P}((\psi_2 - \varepsilon_0 - \delta, \psi_2 + \varepsilon_0 + \delta)). For small enough \delta, these are disjoint, so interval hom-vanishing applies.

🔗theorem
CategoryTheory.Triangulated.hom_eq_zero_of_wSemistable_gap.{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)
  {E F : C} {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a
      b}
  {ψ₁ ψ₂ : ℝ}
  (hE :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
      E ψ₁)
  (hF :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
      F ψ₂)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hthin : b - a + 2 * ε₀ < 1)
  (hperturb :
    ∀ (G : C) (φ : ℝ),
      σ.slicing.P φ G →
        ¬CategoryTheory.Limits.IsZero G →
          a < φ → φ < b → φ - ε₀ < ssf.wPhase G ∧ ssf.wPhase G < φ + ε₀)
  (hgap : ψ₁ > ψ₂ + 2 * ε₀) (f : E ⟶ F) : f = 0
CategoryTheory.Triangulated.hom_eq_zero_of_wSemistable_gap.{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)
  {E F : C} {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v σ.slicing a b}
  {ψ₁ ψ₂ : ℝ}
  (hE :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C ssf E ψ₁)
  (hF :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C ssf F ψ₂)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀)
  (hthin : b - a + 2 * ε₀ < 1)
  (hperturb :
    ∀ (G : C) (φ : ℝ),
      σ.slicing.P φ G →
        ¬CategoryTheory.Limits.IsZero G →
          a < φ →
            φ < b →
              φ - ε₀ < ssf.wPhase G ∧
                ssf.wPhase G < φ + ε₀)
  (hgap : ψ₁ > ψ₂ + 2 * ε₀) (f : E ⟶ F) :
  f = 0

Something wrong, better idea? Suggest a change

14.15.7. phase_le_of_triangle_quotient🔗

A nonzero quotient in a distinguished triangle K \to E \to Q \to K[1] of a W-semistable object E has W-phase \ge \psi, provided both K, Q \in \mathcal{P}((a, b)).

Proof: If K = 0, then Q \cong E and the result is trivial. Otherwise, W-semistability gives \operatorname{wPhaseOf}(W(K)) \le \psi. The K_0 identity W(E) = W(K) + W(Q) and the phase see-saw lemma give \operatorname{wPhaseOf}(W(Q)) \ge \psi.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.phase_le_of_triangle_quotient.{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)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a
      b}
  {X K Y : C} {f₁ : K ⟶ X} {f₂ : X ⟶ Y}
  {f₃ : Y ⟶ (CategoryTheory.shiftFunctor C 1).obj K} {ψ ε₀ : ℝ}
  (hX :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
      X ψ)
  (hε₀ : 0 < ε₀) (hthin : b - a + 2 * ε₀ < 1)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F)
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ → φ < b → φ - ε₀ < ssf.wPhase F ∧ ssf.wPhase F < φ + ε₀)
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hKI :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b K)
  (hYI :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b Y)
  (hY : ¬CategoryTheory.Limits.IsZero Y) : ψ ≤ ssf.wPhase Y
CategoryTheory.Triangulated.SkewedStabilityFunction.phase_le_of_triangle_quotient.{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)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v σ.slicing a b}
  {X K Y : C} {f₁ : K ⟶ X} {f₂ : X ⟶ Y}
  {f₃ :
    Y ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        K}
  {ψ ε₀ : ℝ}
  (hX :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C ssf X ψ)
  (hε₀ : 0 < ε₀)
  (hthin : b - a + 2 * ε₀ < 1)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F)
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b →
              φ - ε₀ < ssf.wPhase F ∧
                ssf.wPhase F < φ + ε₀)
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hKI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a b K)
  (hYI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a b Y)
  (hY : ¬CategoryTheory.Limits.IsZero Y) :
  ψ ≤ ssf.wPhase Y

Something wrong, better idea? Suggest a change

14.15.8. phase_le_of_strictQuotient🔗

A nonzero strict quotient of a W-semistable interval object has W-phase at least \psi. Delegates to phase_le_of_triangle_quotient after extracting the distinguished triangle from the strict short exact sequence.

Proof: Lift the strict epimorphism E \twoheadrightarrow Y to a short exact sequence in the abelian heart, extract the corresponding distinguished triangle, then apply phase_le_of_triangle_quotient.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.phase_le_of_strictQuotient.{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)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a
      b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {ψ ε₀ : ℝ}
  (hX :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
      X.obj ψ)
  (hε₀ : 0 < ε₀) (hthin : b - a + 2 * ε₀ < 1)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F)
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ → φ < b → φ - ε₀ < ssf.wPhase F ∧ ssf.wPhase F < φ + ε₀)
  (p : X ⟶ Y) (hp : CategoryTheory.IsStrictEpi p)
  (hY : ¬CategoryTheory.Limits.IsZero Y.obj) : ψ ≤ ssf.wPhase Y.obj
CategoryTheory.Triangulated.SkewedStabilityFunction.phase_le_of_strictQuotient.{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)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v σ.slicing a b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  {X Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {ψ ε₀ : ℝ}
  (hX :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C ssf X.obj ψ)
  (hε₀ : 0 < ε₀)
  (hthin : b - a + 2 * ε₀ < 1)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F)
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b →
              φ - ε₀ < ssf.wPhase F ∧
                ssf.wPhase F < φ + ε₀)
  (p : X ⟶ Y)
  (hp : CategoryTheory.IsStrictEpi p)
  (hY :
    ¬CategoryTheory.Limits.IsZero Y.obj) :
  ψ ≤ ssf.wPhase Y.obj

Something wrong, better idea? Suggest a change