Highest-phase reduction for owner deformation HN recursion

This file packages the two estimates used to keep the recursive strict-MDQ construction inside a phase-enveloping interval. It is the owner-native version of the phiPlus reduction in Bridgeland's deformation proof.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.phase_lt_upper_of_destabilizing_subobject (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) (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 * ε))) [Fact (a < b)] [Fact (b - a ≤ 1)] {Y : Slicing.IntervalCat C σ.slicing a b} (hY : ¬Limits.IsZero Y.obj) (hplus : Slicing.phiPlus C σ.slicing Y.obj hY ≤ (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase Y.obj + ε) (hupper : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase Y.obj < b - 3 * ε) {A : Subobject Y} (hA : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).IsSemistable (Subobject.underlying.obj A).obj ((WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase (Subobject.underlying.obj A).obj)) (hAstrict : IsStrictMono A.arrow) : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase (Subobject.underlying.obj A).obj < b - ε

If the highest old phase of Y is controlled by its skewed phase, then every skewed-semistable strict subobject of Y stays below the upper deformation boundary.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.hom_eq_zero_of_enveloped_semistable (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) (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 * ε))) {E F : C} (hE : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).IsSemistable E ((WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase E)) (hF : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).IsSemistable F ((WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase F)) (hgap : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase F < (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase E) (hElo : a + ε ≤ (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase E) (hEhi : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase E ≤ b - ε) (hFlo : a + ε ≤ (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase F) (hFhi : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase F ≤ b - ε) (f : E ⟶ F) : f = 0

Sharp Hom-vanishing for two skewed-semistable objects whose phases are enveloped by their common thin interval.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.comp_mdq_of_destabilizing_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 * ε))) {t : ℝ} (ht : a + ε ≤ t) {X : Slicing.IntervalCat C σ.slicing a b} (hXlo : t < (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase X.obj) (hQuotLo : ∀ {G : Slicing.IntervalCat C σ.slicing a b} (p : X ⟶ G), IsStrictEpi p → ¬Limits.IsZero G.obj → (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).IsSemistable G.obj ((WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase G.obj) → t < (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase G.obj) {A : Subobject X} (hA : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).IsSemistable (Subobject.underlying.obj A).obj ((WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase (Subobject.underlying.obj A).obj)) (hAstrict : IsStrictMono A.arrow) (hAphase : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase X.obj < (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase (Subobject.underlying.obj A).obj) (hAtop : A ≠ ⊤) (hAupper : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase (Subobject.underlying.obj A).obj < b - ε) {Q : Slicing.IntervalCat C σ.slicing a b} {q : Limits.cokernel A.arrow ⟶ Q} (hq : WeakStabilityCondition.StabilityCondition.Deformation.IsStrictMDQ C σ (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab) q) : WeakStabilityCondition.StabilityCondition.Deformation.IsStrictMDQ C σ (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab) (CategoryStruct.comp (Limits.cokernel.π A.arrow) q)

Compose an MDQ across a destabilizing strict subobject when all semistable strict quotients of the ambient object have a common lower phase bound. That lower bound and the highest-phase estimate put the two objects in the enveloped range needed for sharp Hom-vanishing.