14.19. Deformation: PhiPlusReduction🔗

14.19.1. phiPlus_bound_of_destabilizing_subobject🔗

\varphi^+ bound on destabilizing subobjects (Bridgeland p.23). If Y \in \operatorname{IntervalCat}(a,b) with \varphi^+(Y) \le \psi(Y) + \varepsilon and \psi(Y) < b - 3\varepsilon, and A is a W-semistable strict subobject with \psi(A) > \psi(Y), then \psi(A) < b - \varepsilon.

Proof: phiPlus_triangle_le gives \varphi^+(A) \le \varphi^+(Y). Phase confinement gives \psi(A) - \varepsilon < \varphi^-(A) \le \varphi^+(A). Combining: \psi(A) < \varphi^+(Y) + \varepsilon \le \psi(Y) + 2\varepsilon < b - \varepsilon.

theorem

CategoryTheory.Triangulated.phiPlus_bound_of_destabilizing_subobject.{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 : ℝ} (hab : a < b) [Fact (a < b)] [Fact (b - a ≤ 1)] {ε : ℝ}
  (hε : 0 < ε) (hε2 : ε < 1 / 4) (hthin : b - a + 2 * ε < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε)))
  {Y : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  (hYne : ¬CategoryTheory.Limits.IsZero Y.obj)
  (hphiPlus :
    CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing Y.obj hYne ≤
      CategoryTheory.Triangulated.wPhaseOf
          (W (CategoryTheory.Triangulated.cl C v Y.obj)) ((a + b) / 2) +
        ε)
  (hψ_upper :
    CategoryTheory.Triangulated.wPhaseOf
        (W (CategoryTheory.Triangulated.cl C v Y.obj)) ((a + b) / 2) <
      b - 3 * ε)
  {A : CategoryTheory.Subobject Y}
  (hA_ss :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab)
      (CategoryTheory.Subobject.underlying.obj A).obj
      (CategoryTheory.Triangulated.wPhaseOf
        (W
          (CategoryTheory.Triangulated.cl C v
            (CategoryTheory.Subobject.underlying.obj A).obj))
        ((a + b) / 2)))
  (hA_strict : CategoryTheory.IsStrictMono A.arrow) :
  CategoryTheory.Triangulated.wPhaseOf
      (W
        (CategoryTheory.Triangulated.cl C v
          (CategoryTheory.Subobject.underlying.obj A).obj))
      ((a + b) / 2) <
    b - ε
CategoryTheory.Triangulated.phiPlus_bound_of_destabilizing_subobject.{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 : ℝ} (hab : a < b) [Fact (a < b)]
  [Fact (b - a ≤ 1)] {ε : ℝ} (hε : 0 < ε)
  (hε2 : ε < 1 / 4)
  (hthin : b - a + 2 * ε < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε)))
  {Y :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  (hYne :
    ¬CategoryTheory.Limits.IsZero Y.obj)
  (hphiPlus :
    CategoryTheory.Triangulated.Slicing.phiPlus
        C σ.slicing Y.obj hYne ≤
      CategoryTheory.Triangulated.wPhaseOf
          (W
            (CategoryTheory.Triangulated.cl
              C v Y.obj))
          ((a + b) / 2) +
        ε)
  (hψ_upper :
    CategoryTheory.Triangulated.wPhaseOf
        (W
          (CategoryTheory.Triangulated.cl
            C v Y.obj))
        ((a + b) / 2) <
      b - 3 * ε)
  {A : CategoryTheory.Subobject Y}
  (hA_ss :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab)
      (CategoryTheory.Subobject.underlying.obj
          A).obj
      (CategoryTheory.Triangulated.wPhaseOf
        (W
          (CategoryTheory.Triangulated.cl
            C v
            (CategoryTheory.Subobject.underlying.obj
                A).obj))
        ((a + b) / 2)))
  (hA_strict :
    CategoryTheory.IsStrictMono A.arrow) :
  CategoryTheory.Triangulated.wPhaseOf
      (W
        (CategoryTheory.Triangulated.cl C
          v
          (CategoryTheory.Subobject.underlying.obj
              A).obj))
      ((a + b) / 2) <
    b - ε

Something wrong, better idea? Suggest a change

14.19.2. hom_eq_zero_of_enveloped_semistable🔗

Hom vanishing for two \operatorname{ssf}-semistable objects whose W-phases are both in [a + \varepsilon, b - \varepsilon]. Converts both to deformedPred using (a, b) as the witness interval, then applies hom_eq_zero_of_deformedPred. This is the localized version of hHom that avoids the universal quantifier problem.

Proof: Both objects are semistable with phases in [a + \varepsilon, b - \varepsilon], so each is a deformedPred object witnessed by (a, b). Apply the sharp Hom vanishing hom_eq_zero_of_deformedPred (Lemma 7.6, sorry-free).

theorem

CategoryTheory.Triangulated.hom_eq_zero_of_enveloped_semistable.{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 : ℝ} (hab : a < b) {ε : ℝ} (hε : 0 < ε) (hε2 : ε < 1 / 4)
  (hε8 : ε < 1 / 8) (hthin : b - a + 2 * ε < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε)))
  {E F : C}
  (hE :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab)
      E
      (CategoryTheory.Triangulated.wPhaseOf
        (W (CategoryTheory.Triangulated.cl C v E)) ((a + b) / 2)))
  (hF :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab)
      F
      (CategoryTheory.Triangulated.wPhaseOf
        (W (CategoryTheory.Triangulated.cl C v F)) ((a + b) / 2)))
  (hgap :
    CategoryTheory.Triangulated.wPhaseOf
        (W (CategoryTheory.Triangulated.cl C v F)) ((a + b) / 2) <
      CategoryTheory.Triangulated.wPhaseOf
        (W (CategoryTheory.Triangulated.cl C v E)) ((a + b) / 2))
  (hE_lo :
    a + ε ≤
      CategoryTheory.Triangulated.wPhaseOf
        (W (CategoryTheory.Triangulated.cl C v E)) ((a + b) / 2))
  (hE_hi :
    CategoryTheory.Triangulated.wPhaseOf
        (W (CategoryTheory.Triangulated.cl C v E)) ((a + b) / 2) ≤
      b - ε)
  (hF_lo :
    a + ε ≤
      CategoryTheory.Triangulated.wPhaseOf
        (W (CategoryTheory.Triangulated.cl C v F)) ((a + b) / 2))
  (hF_hi :
    CategoryTheory.Triangulated.wPhaseOf
        (W (CategoryTheory.Triangulated.cl C v F)) ((a + b) / 2) ≤
      b - ε)
  (f : E ⟶ F) : f = 0
CategoryTheory.Triangulated.hom_eq_zero_of_enveloped_semistable.{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 : ℝ} (hab : a < b) {ε : ℝ}
  (hε : 0 < ε) (hε2 : ε < 1 / 4)
  (hε8 : ε < 1 / 8)
  (hthin : b - a + 2 * ε < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε)))
  {E F : C}
  (hE :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab)
      E
      (CategoryTheory.Triangulated.wPhaseOf
        (W
          (CategoryTheory.Triangulated.cl
            C v E))
        ((a + b) / 2)))
  (hF :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW hab)
      F
      (CategoryTheory.Triangulated.wPhaseOf
        (W
          (CategoryTheory.Triangulated.cl
            C v F))
        ((a + b) / 2)))
  (hgap :
    CategoryTheory.Triangulated.wPhaseOf
        (W
          (CategoryTheory.Triangulated.cl
            C v F))
        ((a + b) / 2) <
      CategoryTheory.Triangulated.wPhaseOf
        (W
          (CategoryTheory.Triangulated.cl
            C v E))
        ((a + b) / 2))
  (hE_lo :
    a + ε ≤
      CategoryTheory.Triangulated.wPhaseOf
        (W
          (CategoryTheory.Triangulated.cl
            C v E))
        ((a + b) / 2))
  (hE_hi :
    CategoryTheory.Triangulated.wPhaseOf
        (W
          (CategoryTheory.Triangulated.cl
            C v E))
        ((a + b) / 2) ≤
      b - ε)
  (hF_lo :
    a + ε ≤
      CategoryTheory.Triangulated.wPhaseOf
        (W
          (CategoryTheory.Triangulated.cl
            C v F))
        ((a + b) / 2))
  (hF_hi :
    CategoryTheory.Triangulated.wPhaseOf
        (W
          (CategoryTheory.Triangulated.cl
            C v F))
        ((a + b) / 2) ≤
      b - ε)
  (f : E ⟶ F) : f = 0

Something wrong, better idea? Suggest a change

14.19.3. comp_of_destabilizing_with_quotient_bound🔗

MDQ composition with quotient-bound Hom vanishing (Bridgeland p.23). Same as comp_of_destabilizing_semistable_subobject but replaces the universal hHom with a quotient lower bound: all W-semistable strict quotients of X have \psi > t_{\mathrm{lo}}. Combined with \psi(A) < U_{\mathrm{hom}}, both objects are in [a + \varepsilon, b - \varepsilon], enabling hom_eq_zero_of_deformedPred.

Proof: For a competitor q' : X \to B' with \psi(B') \le \psi(B): the quotient lower bound gives \psi(B') \ge a + \varepsilon, the destabilizing subobject has \psi(A) < b - \varepsilon, and the phase gap \psi(B') < \psi(A) enables hom_eq_zero_of_enveloped_semistable to show A \to B' = 0. Hence q' factors through \operatorname{coker}(A), reducing to the MDQ minimality on the cokernel.

theorem

CategoryTheory.Triangulated.comp_of_destabilizing_with_quotient_bound.{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)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧ ssf.wPhase F < U)
  (hWidth : U - L < 1) (W : Λ →+ ℂ)
  (hW_stab :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε : ℝ} (hε : 0 < ε) (hε2 : ε < 1 / 4) (hε8 : ε < 1 / 8) (hab : a < b)
  (hthin : b - a + 2 * ε < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε)))
  (hssf :
    ssf =
      CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW_stab hab)
  {t_lo : ℝ} (ht_lo : a + ε ≤ t_lo)
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  (hψ_X_lo : t_lo < ssf.wPhase X.obj)
  (hQuotLo :
    ∀
      {B' :
        CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
      (q' : X ⟶ B'),
      CategoryTheory.IsStrictEpi q' →
        ¬CategoryTheory.Limits.IsZero B'.obj →
          CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
              C ssf B'.obj (ssf.wPhase B'.obj) →
            t_lo < ssf.wPhase B'.obj)
  {A : CategoryTheory.Subobject X}
  (hA_ss :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
      (CategoryTheory.Subobject.underlying.obj A).obj
      (ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj))
  (hA_strict : CategoryTheory.IsStrictMono A.arrow)
  (hA_phase :
    ssf.wPhase X.obj <
      ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj)
  (hA_top : A ≠ ⊤)
  (hA_phase_upper :
    ssf.wPhase (CategoryTheory.Subobject.underlying.obj A).obj < b - ε)
  {B : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {q : CategoryTheory.Limits.cokernel A.arrow ⟶ B}
  (hq : CategoryTheory.Triangulated.IsStrictMDQ C σ ssf q) :
  CategoryTheory.Triangulated.IsStrictMDQ C σ ssf
    (CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.cokernel.π A.arrow) q)
CategoryTheory.Triangulated.comp_of_destabilizing_with_quotient_bound.{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)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval
      C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧
            ssf.wPhase F < U)
  (hWidth : U - L < 1) (W : Λ →+ ℂ)
  (hW_stab :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε : ℝ} (hε : 0 < ε) (hε2 : ε < 1 / 4)
  (hε8 : ε < 1 / 8) (hab : a < b)
  (hthin : b - a + 2 * ε < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε)))
  (hssf :
    ssf =
      CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW_stab hab)
  {t_lo : ℝ} (ht_lo : a + ε ≤ t_lo)
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  (hψ_X_lo : t_lo < ssf.wPhase X.obj)
  (hQuotLo :
    ∀
      {B' :
        CategoryTheory.Triangulated.Slicing.IntervalCat
          C σ.slicing a b}
      (q' : X ⟶ B'),
      CategoryTheory.IsStrictEpi q' →
        ¬CategoryTheory.Limits.IsZero
              B'.obj →
          CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
              C ssf B'.obj
              (ssf.wPhase B'.obj) →
            t_lo < ssf.wPhase B'.obj)
  {A : CategoryTheory.Subobject X}
  (hA_ss :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C ssf
      (CategoryTheory.Subobject.underlying.obj
          A).obj
      (ssf.wPhase
        (CategoryTheory.Subobject.underlying.obj
            A).obj))
  (hA_strict :
    CategoryTheory.IsStrictMono A.arrow)
  (hA_phase :
    ssf.wPhase X.obj <
      ssf.wPhase
        (CategoryTheory.Subobject.underlying.obj
            A).obj)
  (hA_top : A ≠ ⊤)
  (hA_phase_upper :
    ssf.wPhase
        (CategoryTheory.Subobject.underlying.obj
            A).obj <
      b - ε)
  {B :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {q :
    CategoryTheory.Limits.cokernel
        A.arrow ⟶
      B}
  (hq :
    CategoryTheory.Triangulated.IsStrictMDQ
      C σ ssf q) :
  CategoryTheory.Triangulated.IsStrictMDQ
    C σ ssf
    (CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.cokernel.π
        A.arrow)
      q)

Something wrong, better idea? Suggest a change

14.19.4. mdq_of_sigma_phase_split🔗

MDQ lifting through \sigma-phase split (Bridgeland p.23). Given a strict SES 0 \to X_{\mathrm{hi}} \to E \to E_{\mathrm{lo}} \to 0 from the \sigma-phase split at cutoff t_{\mathrm{cut}}, where X_{\mathrm{hi}} \in \operatorname{geProp}(t_{\mathrm{cut}}) and an MDQ q : E_{\mathrm{lo}} \to B for E_{\mathrm{lo}}, the composite E \twoheadrightarrow E_{\mathrm{lo}} \twoheadrightarrow B is an MDQ for E.

Proof: For any W-semistable quotient p : E \to B' with \psi(B') \le \psi(B): phase confinement gives \varphi^+(B') < \psi(B') + \varepsilon \le \psi(B) + \varepsilon. Since B is a quotient of E_{\mathrm{lo}} (all \sigma-phases \le t_{\mathrm{cut}}), the seesaw gives \psi(B) \le \psi(E), hence \varphi^+(B') < t_{\mathrm{cut}}. So B' \in \operatorname{ltProp}(t_{\mathrm{cut}}) while X_{\mathrm{hi}} \in \operatorname{geProp}(t_{\mathrm{cut}}), giving \operatorname{Hom}(X_{\mathrm{hi}}, B') = 0. Hence E \to B' factors through E \to E_{\mathrm{lo}} \to B'.

theorem

CategoryTheory.Triangulated.mdq_of_sigma_phase_split.{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)]
  {E X_hi E_lo :
    CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {p_hi : X_hi ⟶ E} {p_lo : E ⟶ E_lo}
  (hp_lo : CategoryTheory.IsStrictEpi p_lo) {t_cut : ℝ}
  (hX_hi_ge :
    CategoryTheory.Triangulated.Slicing.geProp C σ.slicing t_cut
      X_hi.obj)
  (hcokernel :
    ∀
      {D :
        CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
      (f : E ⟶ D),
      CategoryTheory.CategoryStruct.comp p_hi f = 0 →
        ∃ r, f = CategoryTheory.CategoryStruct.comp p_lo r)
  {B : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  {q : E_lo ⟶ B}
  (hq : CategoryTheory.Triangulated.IsStrictMDQ C σ ssf q)
  (hPhaseConf :
    ∀
      {F :
        CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a
          b},
      CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C
          ssf F.obj (ssf.wPhase F.obj) →
        ssf.wPhase F.obj ≤ ssf.wPhase B.obj →
          CategoryTheory.Triangulated.Slicing.ltProp C σ.slicing t_cut
            F.obj) :
  CategoryTheory.Triangulated.IsStrictMDQ C σ ssf
    (CategoryTheory.CategoryStruct.comp p_lo q)
CategoryTheory.Triangulated.mdq_of_sigma_phase_split.{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)]
  {E X_hi E_lo :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {p_hi : X_hi ⟶ E} {p_lo : E ⟶ E_lo}
  (hp_lo :
    CategoryTheory.IsStrictEpi p_lo)
  {t_cut : ℝ}
  (hX_hi_ge :
    CategoryTheory.Triangulated.Slicing.geProp
      C σ.slicing t_cut X_hi.obj)
  (hcokernel :
    ∀
      {D :
        CategoryTheory.Triangulated.Slicing.IntervalCat
          C σ.slicing a b}
      (f : E ⟶ D),
      CategoryTheory.CategoryStruct.comp
            p_hi f =
          0 →
        ∃ r,
          f =
            CategoryTheory.CategoryStruct.comp
              p_lo r)
  {B :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  {q : E_lo ⟶ B}
  (hq :
    CategoryTheory.Triangulated.IsStrictMDQ
      C σ ssf q)
  (hPhaseConf :
    ∀
      {F :
        CategoryTheory.Triangulated.Slicing.IntervalCat
          C σ.slicing a b},
      CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
          C ssf F.obj (ssf.wPhase F.obj) →
        ssf.wPhase F.obj ≤
            ssf.wPhase B.obj →
          CategoryTheory.Triangulated.Slicing.ltProp
            C σ.slicing t_cut F.obj) :
  CategoryTheory.Triangulated.IsStrictMDQ
    C σ ssf
    (CategoryTheory.CategoryStruct.comp
      p_lo q)

Something wrong, better idea? Suggest a change