Owner maximal destabilizing quotients for deformation #
This is the two-branch MDQ recursion in Bridgeland's deformation argument.
The controlled φ⁺ branch uses the sharp deformed Hom-vanishing theorem;
the complementary branch splits the old HN filtration at ψ + ε.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_strictMDQ_with_quotient_bound
(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)]
(hFinite : WeakStabilityCondition.StabilityCondition.Deformation.ThinStrictFiniteLength C σ a b)
{L U : ℝ}
(hWindow :
∀ (Y : Slicing.IntervalCat C σ.slicing a b),
¬Limits.IsZero Y.obj →
L < (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).phase
Y.obj ∧ (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).phase
Y.obj < U)
(hWidth : U - L < 1)
(hε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hε8 : ε < 1 / 8)
(hthin : b - a + 2 * ε < 1)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
(hL_a : a ≤ L + ε)
{t : ℝ}
(ht : a + ε ≤ t)
{X : Slicing.IntervalCat C σ.slicing a b}
(hX : ¬Limits.IsZero X)
(hQuotLo :
∀ {B' : Slicing.IntervalCat C σ.slicing a b} (q' : X ⟶ B'),
IsStrictEpi q' →
¬Limits.IsZero B'.obj →
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).IsSemistable
B'.obj
((WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1
hW hab).phase
B'.obj) →
t < (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1
hW hab).phase
B'.obj)
(hXupper :
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).phase
X.obj < b - 3 * ε)
:
∃ (B : Slicing.IntervalCat C σ.slicing a b) (q : X ⟶ B),
WeakStabilityCondition.StabilityCondition.Deformation.IsStrictMDQ C σ
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab)
q
A nonzero thin-interval object admits a strict MDQ while all semistable strict quotients are constrained above a common lower phase cutoff.