Extension closure of owner slicing phase cuts

The four HN phase cuts are closed under distinguished extensions. The proof uses nonzero boundary factors, owner phase-gap Hom-vanishing, and the Yoneda exact sequences of a distinguished triangle.

Closure under a single extension propagates along any owner Postnikov tower through ExtensionClosure.le_of_closed, so each cut is also closed under towers whose factors satisfy it; this is how a condition stated on semistable objects extends to every object with HN phases on one side of the cut once an exact functor has been applied factorwise.

theorem CategoryTheory.Triangulated.Slicing.leProp_of_triangle (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {A E B : C} (t : ℝ) (hA : leProp C s t A) (hB : leProp C s t B) {f : A ⟶ E} {g : E ⟶ B} {h : B ⟶ (shiftFunctor C 1).obj A} (hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles) : leProp C s t E

The owner upper phase cut is closed under distinguished extensions.

theorem CategoryTheory.Triangulated.Slicing.ltProp_of_triangle (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {A E B : C} (t : ℝ) (hA : ltProp C s t A) (hB : ltProp C s t B) {f : A ⟶ E} {g : E ⟶ B} {h : B ⟶ (shiftFunctor C 1).obj A} (hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles) : ltProp C s t E

The owner strict upper phase cut is closed under distinguished extensions.

theorem CategoryTheory.Triangulated.Slicing.gtProp_of_triangle (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {A E B : C} (t : ℝ) (hA : gtProp C s t A) (hB : gtProp C s t B) {f : A ⟶ E} {g : E ⟶ B} {h : B ⟶ (shiftFunctor C 1).obj A} (hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles) : gtProp C s t E

The owner strict lower phase cut is closed under distinguished extensions.

theorem CategoryTheory.Triangulated.Slicing.geProp_of_triangle (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {A E B : C} (t : ℝ) (hA : geProp C s t A) (hB : geProp C s t B) {f : A ⟶ E} {g : E ⟶ B} {h : B ⟶ (shiftFunctor C 1).obj A} (hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles) : geProp C s t E

The owner weak lower phase cut is closed under distinguished extensions.

theorem CategoryTheory.Triangulated.Slicing.leProp_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), leProp C s t (P.factor i)) : leProp C s t E

An owner Postnikov tower whose factors satisfy the upper phase cut has its total object satisfying it.

theorem CategoryTheory.Triangulated.Slicing.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), ltProp C s t (P.factor i)) : ltProp C s t E

An owner Postnikov tower whose factors satisfy the strict upper phase cut has its total object satisfying it.

theorem CategoryTheory.Triangulated.Slicing.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), gtProp C s t (P.factor i)) : gtProp C s t E

An owner Postnikov tower whose factors satisfy the strict lower phase cut has its total object satisfying it.

theorem CategoryTheory.Triangulated.Slicing.geProp_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), geProp C s t (P.factor i)) : geProp C s t E

An owner Postnikov tower whose factors satisfy the lower phase cut has its total object satisfying it.