Global HN filtrations for the owner deformed slices

The global cut triangles are iterated across a finite phase interval. This file first records the exact orthogonality of the provisional cuts and a normalization lemma which discards the parts of a local filtration lying outside a prescribed cut window.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.hom_eq_zero_of_deformedGtLe (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ε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hε8 : ε < 1 / 8) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) {t : ℝ} {E F : C} (hE : deformedGtPred C σ W hr0 hr1 hW ε t E) (hF : deformedLePred C σ W hr0 hr1 hW ε t F) (f : E ⟶ F) : f = 0

The two provisional cuts at the same phase are orthogonal.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.isZero_of_deformedGtLe (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ε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hε8 : ε < 1 / 8) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) {t : ℝ} {E : C} (hGt : deformedGtPred C σ W hr0 hr1 hW ε t E) (hLe : deformedLePred C σ W hr0 hr1 hW ε t E) : Limits.IsZero E

An object lying in both provisional cuts at the same phase is zero.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedHN_of_cut_window (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ε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hε8 : ε < 1 / 8) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) {a b : ℝ} {E : C} (G : HNFiltration C (deformedPred C σ W hr0 hr1 hW ε) E) (hGt : deformedGtPred C σ W hr0 hr1 hW ε a E) (hLe : deformedLePred C σ W hr0 hr1 hW ε b E) : ∃ (G' : HNFiltration C (deformedPred C σ W hr0 hr1 hW ε) E), (∀ (j : Fin G'.n), a < G'.φ j) ∧ ∀ (j : Fin G'.n), G'.φ j ≤ b

Restrict a deformed HN filtration to the open-closed phase window forced by cut membership of its target.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedHN_exists_in_cut_strip (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ε₀16 : ε₀ < 1 / 16) (hWide : WeakStabilityCondition.StabilityCondition.Deformation.WideSectorFiniteLength C σ ε₀) {ε : ℝ} (hε : 0 < ε) (hεhalf : ε < ε₀ / 2) (hε2 : ε ≤ 1 / 2) (hε8 : ε < 1 / 8) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) {E : C} (t : ℝ) (hGt : deformedGtPred C σ W hr0 hr1 hW ε (t - ε₀) E) (hLe : deformedLePred C σ W hr0 hr1 hW ε t E) : ∃ (G : HNFiltration C (deformedPred C σ W hr0 hr1 hW ε) E), (∀ (j : Fin G.n), t - ε₀ < G.φ j) ∧ ∀ (j : Fin G.n), G.φ j ≤ t

A single strip between consecutive global cuts has a deformed HN filtration whose phases lie in exactly that strip.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedHN_exists_of_bounded_cuts (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ε₀ : 0 < ε₀) (hε₀16 : ε₀ < 1 / 16) (hWide : WeakStabilityCondition.StabilityCondition.Deformation.WideSectorFiniteLength C σ ε₀) {ε : ℝ} (hε : 0 < ε) (hεhalf : ε < ε₀ / 2) (hε2 : ε ≤ 1 / 2) (hε8 : ε < 1 / 8) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) (n : ℕ) (t : ℝ) (E : C) (hGt : deformedGtPred C σ W hr0 hr1 hW ε (t - ↑n * ε₀) E) (hLe : deformedLePred C σ W hr0 hr1 hW ε t E) : ∃ (G : HNFiltration C (deformedPred C σ W hr0 hr1 hW ε) E), (∀ (j : Fin G.n), t - ↑n * ε₀ < G.φ j) ∧ ∀ (j : Fin G.n), G.φ j ≤ t

Iterating consecutive cut strips produces an HN filtration on every object already bounded by two provisional cuts.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedHN_exists (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ε₀ : 0 < ε₀) (hε₀16 : ε₀ < 1 / 16) (hWide : WeakStabilityCondition.StabilityCondition.Deformation.WideSectorFiniteLength C σ ε₀) {ε : ℝ} (hε : 0 < ε) (hεhalf : ε < ε₀ / 2) (hε2 : ε ≤ 1 / 2) (hε8 : ε < 1 / 8) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) (E : C) : Nonempty (HNFiltration C (deformedPred C σ W hr0 hr1 hW ε) E)

Every object has an HN filtration for the repository-owned deformed phase predicate.