Highest-phase split for owner deformation HN recursion #
When an interval object's highest old phase lies above its skewed phase by more than the deformation tolerance, its old HN filtration supplies a proper strict subobject of larger skewed phase. This is the second branch of Bridgeland's maximal-destabilizing-quotient recursion.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_strictSubobject_of_phiPlus_gt
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{κ : K₀ C →+ Λ}
(σ : WithClassMap C κ)
(W : Λ →+ ℂ)
{r : ℝ}
(hr0 : 0 ≤ r)
(hr1 : r < 1)
(hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r)
{a b ε : ℝ}
(hab : a < b)
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{L U : ℝ}
(hWindow :
∀ (Z : Slicing.IntervalCat C σ.slicing a b),
¬Limits.IsZero Z.obj →
L < (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).phase
Z.obj ∧ (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).phase
Z.obj < U)
(hWidth : U - L < 1)
(hε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hthin : b - a + 2 * ε < 1)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
(hL_a : a ≤ L + ε)
{Y : Slicing.IntervalCat C σ.slicing a b}
(hY : ¬Limits.IsZero Y.obj)
(hplus :
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).phase
Y.obj + ε < Slicing.phiPlus C σ.slicing Y.obj hY)
:
∃ (A : Subobject Y),
A ≠ ⊥ ∧ A ≠ ⊤ ∧ IsStrictMono A.arrow ∧ (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).phase
Y.obj < (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1
hW hab).phase
(Subobject.underlying.obj A).obj ∧ Slicing.geProp C σ.slicing
((WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1
hW hab).phase
Y.obj + ε)
(Subobject.underlying.obj A).obj
If φ⁺(Y) > ψ(Y) + ε, splitting the old HN filtration at
ψ(Y) + ε produces a proper strict subobject whose skewed phase is larger
than that of Y. The subobject also retains the closed lower phase cut
used for the MDQ minimality argument.