Owner deformed HN existence

This file upgrades the strict MDQ recursion to the enveloped HN existence statements used to assemble the deformed slicing.

theorem CategoryTheory.Triangulated.HNFiltration.firstFactor_phiPlus_le_target (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {P : ℝ → ObjectProperty C} {E : C} (G : HNFiltration C P E) (hn : 0 < G.n) (hE : ¬Limits.IsZero E) (hfirst : ¬Limits.IsZero (G.factor ⟨0, hn⟩)) {a b : ℝ} (hab : b ≤ a + 1) (hfactors : ∀ (i : Fin G.n), Slicing.intervalProp C s a b (G.factor i)) : Slicing.phiPlus C s (G.factor ⟨0, hn⟩) hfirst ≤ Slicing.phiPlus C s E hE

The first factor of a Postnikov filtration whose factors lie in a common thin old interval cannot have old highest phase above that of the total object.

theorem CategoryTheory.Triangulated.HNFiltration.target_phiMinus_le_lastFactor (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {P : ℝ → ObjectProperty C} {E : C} (G : HNFiltration C P E) (hn : 0 < G.n) (hE : ¬Limits.IsZero E) (hlast : ¬Limits.IsZero (G.factor ⟨G.n - 1, ⋯⟩)) {a b : ℝ} (hab : b ≤ a + 1) (hfactors : ∀ (i : Fin G.n), Slicing.intervalProp C s a b (G.factor i)) : Slicing.phiMinus C s E hE ≤ Slicing.phiMinus C s (G.factor ⟨G.n - 1, ⋯⟩) hlast

The last factor of a Postnikov filtration whose factors lie in a common thin old interval cannot have old lowest phase below that of the total object.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.interior_has_enveloped_HN_skewed (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) (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 : C} (hE : ¬Limits.IsZero E) (hInner : Slicing.intervalProp C σ.slicing (a + 2 * ε) (b - 4 * ε) E) : have F := WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab; ∃ (G : HNFiltration C (fun (ψ : ℝ) (X : C) => F.IsSemistable X ψ) E), ∀ (j : Fin G.n), a + ε < G.φ j ∧ G.φ j < b - ε

Every nonzero object in the interior of a thin finite-length interval has an HN filtration by skewed-semistable factors whose phases are enveloped by the ambient interval.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.interior_has_enveloped_HN (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) (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 : C} (hE : ¬Limits.IsZero E) (hInner : Slicing.intervalProp C σ.slicing (a + 2 * ε) (b - 4 * ε) E) : ∃ (G : HNFiltration C (deformedPred C σ W hr0 hr1 hW ε) E), (∀ (j : Fin G.n), a + ε < G.φ j ∧ G.φ j < b - ε) ∧ ∀ (j : Fin G.n), ¬Limits.IsZero (G.factor j)

Interior HN existence in the repository-owned deformed slice predicate.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.semistable_has_deformedHN (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) {ε₀ : ℝ} (hε₀10 : ε₀ < 1 / 10) (hWide : WeakStabilityCondition.StabilityCondition.Deformation.WideSectorFiniteLength C σ ε₀) {ε : ℝ} (hε : 0 < ε) (hεε₀ : ε < ε₀) (hε2 : ε ≤ 1 / 2) (hε8 : ε < 1 / 8) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) {E : C} {φ : ℝ} (hP : σ.slicing.P φ E) (hE : ¬Limits.IsZero E) : ∃ (G : HNFiltration C (deformedPred C σ W hr0 hr1 hW ε) E), (∀ (j : Fin G.n), φ - 4 * ε₀ + ε < G.φ j ∧ G.φ j < φ + 4 * ε₀ - ε) ∧ ∀ (j : Fin G.n), ¬Limits.IsZero (G.factor j)

Every nonzero old semistable object admits an owner deformed HN filtration. The wide local-finiteness sector is used directly, avoiding any change-of-interval chain-condition assumption.