Placing thin owner intervals in shifted hearts

Objects whose intrinsic phases lie in an interval of length at most one belong to a real phase-shifted owner heart. These lemmas provide the categorical bridge used by the small-gap part of deformed hom-vanishing.

theorem CategoryTheory.Triangulated.Slicing.mem_phaseShiftHeart_of_intrinsic_bounds (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {E : C} (hE : ¬Limits.IsZero E) {t : ℝ} (hminus : t < phiMinus C s E hE) (hplus : phiPlus C s E hE ≤ t + 1) : (toTStructure C (phaseShift C s t)).heart E

Intrinsic phases in (t,t+1] place an object in the heart of the slicing shifted by t.

theorem CategoryTheory.Triangulated.Slicing.mem_phaseShiftHeart_of_intervalProp (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {E : C} {a b : ℝ} (hI : intervalProp C s a b E) (hwidth : b ≤ a + 1) : (toTStructure C (phaseShift C s a)).heart E

Every object in an open interval of width at most one lies in the heart based at its lower endpoint.

theorem CategoryTheory.Triangulated.Slicing.gtProp_leProp_of_phaseShiftHeart (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {E : C} {a u : ℝ} (hHeart : (toTStructure C (phaseShift C s a)).heart E) (hE : ¬Limits.IsZero E) (hu : phiPlus C s E hE ≤ u) : gtProp C s a E ∧ leProp C s u E

A shifted-heart object lies above the heart cutoff and below any supplied upper intrinsic-phase bound.

theorem CategoryTheory.Triangulated.Slicing.geProp_leProp_of_phaseShiftHeart (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {E : C} {a l : ℝ} (hHeart : (toTStructure C (phaseShift C s a)).heart E) (hE : ¬Limits.IsZero E) (hl : l ≤ phiMinus C s E hE) : geProp C s l E ∧ leProp C s (a + 1) E

A shifted-heart object lies below the upper heart cutoff and above any supplied lower intrinsic-phase bound.

theorem CategoryTheory.Triangulated.Slicing.gtProp_leProp_of_intrinsic_bounds (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) : gtProp C s a E ∧ leProp C s b E

An intrinsic phase window also gives simultaneous old lower and upper phase-cut membership.