Deformation of Stability Conditions — Lemma77

Paper-facing HN existence and Postnikov extension closure (Lemma 7.7)

theorem CategoryTheory.Triangulated.SkewedStabilityFunction.hn_exists_in_thin_interval_of_quotientLowerBound (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 Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {a b : ℝ} {ssf : SkewedStabilityFunction C v σ.slicing a b} [Fact (a < b)] [Fact (b - a ≤ 1)] (hFiniteLength : ThinFiniteLengthInInterval C σ a b) (hW_interval : ∀ {F : C}, Slicing.intervalProp C σ.slicing a b F → ¬Limits.IsZero F → ssf.wNe F) {L U : ℝ} (hWindow : ∀ {F : C}, Slicing.intervalProp C σ.slicing a b F → ¬Limits.IsZero F → L < ssf.wPhase F ∧ ssf.wPhase F < U) (hWidth : U - L < 1) {U_hom : ℝ} (hHom : ∀ {E F : Slicing.IntervalCat C σ.slicing a b}, Semistable C ssf E.obj (ssf.wPhase E.obj) → Semistable C ssf F.obj (ssf.wPhase F.obj) → ssf.wPhase F.obj < ssf.wPhase E.obj → ssf.wPhase E.obj < U_hom → ∀ (f : E ⟶ F), f = 0) (hDestabBound : ∀ {Y : Slicing.IntervalCat C σ.slicing a b}, ¬Limits.IsZero Y → ∀ {A : Subobject Y}, Semistable C ssf (Subobject.underlying.obj A).obj (ssf.wPhase (Subobject.underlying.obj A).obj) → IsStrictMono A.arrow → ssf.wPhase Y.obj < ssf.wPhase (Subobject.underlying.obj A).obj → ssf.wPhase (Subobject.underlying.obj A).obj < U_hom) (t : ℝ) (X : Slicing.IntervalCat C σ.slicing a b) (hX : ¬Limits.IsZero X) : (∀ (A : Subobject X), A ≠ ⊤ → IsStrictMono A.arrow → t < ssf.wPhase (Limits.cokernel A.arrow).obj) → have Psem := fun (ψ : ℝ) (E : C) => Semistable C ssf E ψ; ∃ (G : HNFiltration C Psem X.obj), ∀ (j : Fin G.n), t < G.φ j ∧ G.φ j < U

theorem CategoryTheory.Triangulated.SkewedStabilityFunction.hn_exists_in_thin_interval (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 Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {a b : ℝ} {ssf : SkewedStabilityFunction C v σ.slicing a b} [Fact (a < b)] [Fact (b - a ≤ 1)] (hFiniteLength : ThinFiniteLengthInInterval C σ a b) (hW_interval : ∀ {F : C}, Slicing.intervalProp C σ.slicing a b F → ¬Limits.IsZero F → ssf.wNe F) {L U : ℝ} (hWindow : ∀ {F : C}, Slicing.intervalProp C σ.slicing a b F → ¬Limits.IsZero F → L < ssf.wPhase F ∧ ssf.wPhase F < U) (hWidth : U - L < 1) {U_hom : ℝ} (hHom : ∀ {E F : Slicing.IntervalCat C σ.slicing a b}, Semistable C ssf E.obj (ssf.wPhase E.obj) → Semistable C ssf F.obj (ssf.wPhase F.obj) → ssf.wPhase F.obj < ssf.wPhase E.obj → ssf.wPhase E.obj < U_hom → ∀ (f : E ⟶ F), f = 0) (hDestabBound : ∀ {Y : Slicing.IntervalCat C σ.slicing a b}, ¬Limits.IsZero Y → ∀ {A : Subobject Y}, Semistable C ssf (Subobject.underlying.obj A).obj (ssf.wPhase (Subobject.underlying.obj A).obj) → IsStrictMono A.arrow → ssf.wPhase Y.obj < ssf.wPhase (Subobject.underlying.obj A).obj → ssf.wPhase (Subobject.underlying.obj A).obj < U_hom) (X : Slicing.IntervalCat C σ.slicing a b) (hX : ¬Limits.IsZero X) : have Psem := fun (ψ : ℝ) (E : C) => Semistable C ssf E ψ; ∃ (G : HNFiltration C Psem X.obj), ∀ (j : Fin G.n), L < G.φ j ∧ G.φ j < U

theorem CategoryTheory.Triangulated.SkewedStabilityFunction.hn_exists_in_thin_interval_of_strictQuotientLowerBound (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 Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {a b : ℝ} {ssf : SkewedStabilityFunction C v σ.slicing a b} [Fact (a < b)] [Fact (b - a ≤ 1)] (hFiniteLength : ThinFiniteLengthInInterval C σ a b) (hW_interval : ∀ {F : C}, Slicing.intervalProp C σ.slicing a b F → ¬Limits.IsZero F → ssf.wNe F) {L U : ℝ} (hWindow : ∀ {F : C}, Slicing.intervalProp C σ.slicing a b F → ¬Limits.IsZero F → L < ssf.wPhase F ∧ ssf.wPhase F < U) (hWidth : U - L < 1) {U_hom : ℝ} (hHom : ∀ {E F : Slicing.IntervalCat C σ.slicing a b}, Semistable C ssf E.obj (ssf.wPhase E.obj) → Semistable C ssf F.obj (ssf.wPhase F.obj) → ssf.wPhase F.obj < ssf.wPhase E.obj → ssf.wPhase E.obj < U_hom → ∀ (f : E ⟶ F), f = 0) (hDestabBound : ∀ {Y : Slicing.IntervalCat C σ.slicing a b}, ¬Limits.IsZero Y → ∀ {A : Subobject Y}, Semistable C ssf (Subobject.underlying.obj A).obj (ssf.wPhase (Subobject.underlying.obj A).obj) → IsStrictMono A.arrow → ssf.wPhase Y.obj < ssf.wPhase (Subobject.underlying.obj A).obj → ssf.wPhase (Subobject.underlying.obj A).obj < U_hom) (t : ℝ) (X : Slicing.IntervalCat C σ.slicing a b) (hX : ¬Limits.IsZero X) (hquot : ∀ {B : Slicing.IntervalCat C σ.slicing a b} (q : X ⟶ B), IsStrictEpi q → ¬Limits.IsZero B.obj → t < ssf.wPhase B.obj) : have Psem := fun (ψ : ℝ) (E : C) => Semistable C ssf E ψ; ∃ (G : HNFiltration C Psem X.obj), ∀ (j : Fin G.n), t < G.φ j ∧ G.φ j < U

Extension-closure of intervalProp over Postnikov towers

theorem CategoryTheory.Triangulated.intervalProp_chain_of_postnikovTower (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {E : C} {a b : ℝ} (P : PostnikovTower C E) (hfactors : ∀ (i : Fin P.n), Slicing.intervalProp C s a b (P.factor i)) (k : ℕ) (hk : k ≤ P.n) : Slicing.intervalProp C s a b (P.chain.obj' k ⋯)

All intermediate chain objects of a PostnikovTower satisfy intervalProp when all factors do. This is the induction underlying intervalProp_of_postnikovTower, extracted so that it can be applied to intermediate chain objects (e.g., for Lemma 3.4 arguments on PostnikovTower triangles).

theorem CategoryTheory.Triangulated.intervalProp_of_postnikovTower (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {E : C} {a b : ℝ} (P : PostnikovTower C E) (hfactors : ∀ (i : Fin P.n), Slicing.intervalProp C s a b (P.factor i)) : Slicing.intervalProp C s a b E

Extension-closure of intervalProp over Postnikov towers: if all factors of a Postnikov tower have HN phases in (a, b), then the total object does too.

This follows by induction on the tower length, applying intervalProp_of_triangle at each step.

theorem CategoryTheory.Triangulated.gtProp_of_postnikovTower (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {E : C} {t : ℝ} (P : PostnikovTower C E) (hfactors : ∀ (i : Fin P.n), Slicing.gtProp C s t (P.factor i)) : Slicing.gtProp C s t E

Extension-closure of gtProp over Postnikov towers.

theorem CategoryTheory.Triangulated.ltProp_of_postnikovTower (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {E : C} {t : ℝ} (P : PostnikovTower C E) (hfactors : ∀ (i : Fin P.n), Slicing.ltProp C s t (P.factor i)) : Slicing.ltProp C s t E

Extension-closure of ltProp over Postnikov towers.