Intrinsic phase bounds and interval membership

This module characterizes owner interval membership using intrinsic highest and lowest phases. It also supplies the interval-widening operations used by the deformed-slicing construction.

theorem CategoryTheory.Triangulated.Slicing.intervalProp_mono (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₁ a₂ b₁ b₂ : ℝ} (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : intervalProp C s a₁ b₁ ≤ intervalProp C s a₂ b₂

Enlarging both endpoints preserves owner interval membership.

theorem CategoryTheory.Triangulated.Slicing.intervalProp_widen (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} {φ ε δ : ℝ} (hE : intervalProp C s (φ - ε) (φ + ε) E) (hεδ : ε ≤ δ) : intervalProp C s (φ - δ) (φ + δ) E

A radius increase widens a centered owner interval.

theorem CategoryTheory.Triangulated.Slicing.phiPlus_lt_of_intervalProp (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} (hE : ¬Limits.IsZero E) {a b : ℝ} (hI : intervalProp C s a b E) : phiPlus C s E hE < b

Interval membership bounds the intrinsic highest phase from above.

theorem CategoryTheory.Triangulated.Slicing.phiMinus_gt_of_intervalProp (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} (hE : ¬Limits.IsZero E) {a b : ℝ} (hI : intervalProp C s a b E) : a < phiMinus C s E hE

Interval membership bounds the intrinsic lowest phase from below.

theorem CategoryTheory.Triangulated.Slicing.phiPlus_gt_of_intervalProp (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} (hE : ¬Limits.IsZero E) {a b : ℝ} (hI : intervalProp C s a b E) : a < phiPlus C s E hE

Interval membership bounds the intrinsic highest phase from below.

theorem CategoryTheory.Triangulated.Slicing.phiMinus_lt_of_intervalProp (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} (hE : ¬Limits.IsZero E) {a b : ℝ} (hI : intervalProp C s a b E) : phiMinus C s E hE < b

Interval membership bounds the intrinsic lowest phase from above.

theorem CategoryTheory.Triangulated.Slicing.intervalProp_of_intrinsic_phases (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} (hE : ¬Limits.IsZero E) {a b : ℝ} (hminus : a < phiMinus C s E hE) (hplus : phiPlus C s E hE < b) : intervalProp C s a b E

Intrinsic phase bounds imply owner interval membership.

theorem CategoryTheory.Triangulated.Slicing.intervalProp_intersection (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 c d : ℝ} (hab : intervalProp C s a b E) (hcd : intervalProp C s c d E) : intervalProp C s (max a c) (min b d) E

Membership in two owner intervals implies membership in their intersection.

theorem CategoryTheory.Triangulated.Slicing.intervalProp_iff_intrinsic_phases (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} (hE : ¬Limits.IsZero E) {a b : ℝ} : intervalProp C s a b E ↔ a < phiMinus C s E hE ∧ phiPlus C s E hE < b

For a nonzero object, owner interval membership is equivalent to bounds on both intrinsic phase extrema.

theorem CategoryTheory.Triangulated.Slicing.intrinsic_phases_mem_interval (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} (hE : ¬Limits.IsZero E) {a b : ℝ} (hI : intervalProp C s a b E) : a < phiPlus C s E hE ∧ phiPlus C s E hE < b ∧ a < phiMinus C s E hE ∧ phiMinus C s E hE < b

All four intrinsic extrema of a nonzero interval object lie between the interval endpoints.

theorem CategoryTheory.Triangulated.Slicing.gtProp_of_phiMinus_gt (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} (hE : ¬Limits.IsZero E) {a : ℝ} (h : a < phiMinus C s E hE) : gtProp C s a E

A strict bound on the intrinsic lowest phase yields the corresponding strict lower phase cut.

theorem CategoryTheory.Triangulated.Slicing.geProp_of_phiMinus_ge (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} (hE : ¬Limits.IsZero E) {a : ℝ} (h : a ≤ phiMinus C s E hE) : geProp C s a E

A weak bound on the intrinsic lowest phase yields the corresponding weak lower phase cut.

theorem CategoryTheory.Triangulated.Slicing.leProp_of_phiPlus_le (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} (hE : ¬Limits.IsZero E) {b : ℝ} (h : phiPlus C s E hE ≤ b) : leProp C s b E

A weak bound on the intrinsic highest phase yields the corresponding weak upper phase cut.

theorem CategoryTheory.Triangulated.Slicing.ltProp_of_phiPlus_lt (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} (hE : ¬Limits.IsZero E) {b : ℝ} (h : phiPlus C s E hE < b) : ltProp C s b E

A strict bound on the intrinsic highest phase yields the corresponding strict upper phase cut.

theorem CategoryTheory.Triangulated.Slicing.phiMinus_gt_of_gtProp (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} (hE : ¬Limits.IsZero E) {a : ℝ} (h : gtProp C s a E) : a < phiMinus C s E hE

Membership in a strict lower phase cut bounds the intrinsic lowest phase.

theorem CategoryTheory.Triangulated.Slicing.phiMinus_ge_of_geProp (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} (hE : ¬Limits.IsZero E) {a : ℝ} (h : geProp C s a E) : a ≤ phiMinus C s E hE

Membership in a weak lower phase cut bounds the intrinsic lowest phase.

theorem CategoryTheory.Triangulated.Slicing.phiPlus_le_of_leProp (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} (hE : ¬Limits.IsZero E) {b : ℝ} (h : leProp C s b E) : phiPlus C s E hE ≤ b

Membership in a weak upper phase cut bounds the intrinsic highest phase.

theorem CategoryTheory.Triangulated.Slicing.phiPlus_lt_of_ltProp (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} (hE : ¬Limits.IsZero E) {b : ℝ} (h : ltProp C s b E) : phiPlus C s E hE < b

Membership in a strict upper phase cut bounds the intrinsic highest phase.

theorem CategoryTheory.Triangulated.Slicing.ltProp_of_leProp_of_lt (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 b : ℝ} (hab : a < b) : leProp C s a ≤ ltProp C s b

A weak upper phase bound becomes a strict upper phase bound after strictly enlarging its endpoint.

theorem CategoryTheory.Triangulated.Slicing.phiPlus_triangle_le (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} (hA : ¬Limits.IsZero A) (hE : ¬Limits.IsZero E) {a b : ℝ} (hab : b ≤ a + 1) (hA_int : intervalProp C s a b A) (hB_int : intervalProp C s a b B) {f : A ⟶ E} {g : E ⟶ B} {h : B ⟶ (shiftFunctor C 1).obj A} (hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles) : phiPlus C s A hA ≤ phiPlus C s E hE

In a distinguished triangle A → E → B → A[1] whose outer terms lie in an interval of width at most one, the highest phase of the first term is at most the highest phase of the middle term.

theorem CategoryTheory.Triangulated.Slicing.phiMinus_triangle_le (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} (hB : ¬Limits.IsZero B) (hE : ¬Limits.IsZero E) {a b : ℝ} (hab : b ≤ a + 1) (hA_int : intervalProp C s a b A) (hB_int : intervalProp C s a b B) {f : A ⟶ E} {g : E ⟶ B} {h : B ⟶ (shiftFunctor C 1).obj A} (hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles) : phiMinus C s E hE ≤ phiMinus C s B hB

In a distinguished triangle A → E → B → A[1] whose outer terms lie in an interval of width at most one, the lowest phase of the middle term is at most the lowest phase of the third term.

theorem CategoryTheory.Triangulated.Slicing.phiPlus_lt_of_triangle_with_leProp (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {K E Q : C} (hK : ¬Limits.IsZero K) {b : ℝ} (hE_lt : ∀ (hE : ¬Limits.IsZero E), phiPlus C s E hE < b) {c : ℝ} (hQ_le : leProp C s c Q) (hcb : c < b + 1) {f₁ : K ⟶ E} {f₂ : E ⟶ Q} {f₃ : Q ⟶ (shiftFunctor C 1).obj K} (hT : Pretriangulated.Triangle.mk f₁ f₂ f₃ ∈ Pretriangulated.distinguishedTriangles) : phiPlus C s K hK < b

In a distinguished triangle K → E → Q → K[1], an upper phase bound on E and a compatible weak upper bound on Q bound K from above.

theorem CategoryTheory.Triangulated.Slicing.phiMinus_gt_of_triangle_with_gtProp (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {K E Q : C} (hQ : ¬Limits.IsZero Q) {a : ℝ} (hE_gt : ∀ (hE : ¬Limits.IsZero E), a < phiMinus C s E hE) {c : ℝ} (hK_gt : gtProp C s c K) (hca : a < c + 1) {f₁ : K ⟶ E} {f₂ : E ⟶ Q} {f₃ : Q ⟶ (shiftFunctor C 1).obj K} (hT : Pretriangulated.Triangle.mk f₁ f₂ f₃ ∈ Pretriangulated.distinguishedTriangles) : a < phiMinus C s Q hQ

In a distinguished triangle K → E → Q → K[1], a lower phase bound on E and a compatible strict lower bound on K bound Q from below.

theorem CategoryTheory.Triangulated.Slicing.first_intervalProp_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 b : ℝ} (hab : a < b) {K E Q : C} (hE : intervalProp C s a b E) (hQ_le : leProp C s (a + 1) Q) (hK_gt : gtProp C s a K) {f₁ : K ⟶ E} {f₂ : E ⟶ Q} {f₃ : Q ⟶ (shiftFunctor C 1).obj K} (hT : Pretriangulated.Triangle.mk f₁ f₂ f₃ ∈ Pretriangulated.distinguishedTriangles) : intervalProp C s a b K

The first vertex of a distinguished triangle stays in an open phase interval when its middle vertex is in that interval and the first and third vertices satisfy the one-sided bounds supplied by a common heart.

theorem CategoryTheory.Triangulated.Slicing.intervalProp_of_gtProp_ltProp (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 : ℝ} (hgt : gtProp C s a E) (hlt : ltProp C s b E) : intervalProp C s a b E

The intersection of strict lower and upper owner cuts is the corresponding open owner phase interval.

theorem CategoryTheory.Triangulated.Slicing.intervalProp_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} {a b : ℝ} (hA : intervalProp C s a b A) (hB : intervalProp C s a b B) {f : A ⟶ E} {g : E ⟶ B} {h : B ⟶ (shiftFunctor C 1).obj A} (hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles) : intervalProp C s a b E

Open owner phase intervals are extension-closed along distinguished triangles.

theorem CategoryTheory.Triangulated.Slicing.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), intervalProp C s a b (P.factor i)) (k : ℕ) (hk : k ≤ P.n) : intervalProp C s a b (P.chain.obj' k hk)

Every intermediate chain object belongs to an extension-closed slicing interval when all factors of the Postnikov tower do.

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

An owner Postnikov tower whose factors lie in a slicing interval has its total object in that interval.

theorem CategoryTheory.Triangulated.Slicing.semistable_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} (φ : ℝ) (hA : s.P φ A) (hB : s.P φ B) {f : A ⟶ E} {g : E ⟶ B} {h : B ⟶ (shiftFunctor C 1).obj A} (hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles) : s.P φ E

Semistable slices are extension-closed.

theorem CategoryTheory.Triangulated.Slicing.semistable_of_HN_all_eq (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} {φ : ℝ} (F : HNFiltration C s.P E) (hall : ∀ (i : Fin F.n), F.φ i = φ) : s.P φ E

If every factor of an owner HN filtration has the same phase, then the ambient object lies in that semistable slice.