Intrinsic-phase characterizations of the slicing orders

The strict and weak slicing orders admit three useful descriptions: by the upper HN phase of objects semistable for the left slicing, by the lower HN phase of objects semistable for the right slicing, and by both intrinsic HN endpoints of every nonzero object. These are the four formulations in arXiv:2607.28411v1, Lemma 3.13. The weak form is also arXiv:2601.22994, Lemma 2.2; the strict form is obtained there by replacing every non-strict inequality with a strict one.

theorem CategoryTheory.Triangulated.Slicing.precedes_iff_lt_phiMinus (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s t : Slicing C) : Precedes C s t ↔ ∀ {E : C} {phi : ℝ}, t.P phi E → ∀ (hE0 : ¬Limits.IsZero E), phi < phiMinus C s E hE0

The strict order is equivalent to the lower-phase formulation on nonzero objects semistable for the right-hand slicing.

theorem CategoryTheory.Triangulated.Slicing.precedesWeak_iff_le_phiMinus (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s t : Slicing C) : PrecedesWeak C s t ↔ ∀ {E : C} {phi : ℝ}, t.P phi E → ∀ (hE0 : ¬Limits.IsZero E), phi ≤ phiMinus C s E hE0

The weak order is equivalent to the lower-phase formulation on nonzero objects semistable for the right-hand slicing.

theorem CategoryTheory.Triangulated.Slicing.precedes_iff_extreme_phases_lt (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s t : Slicing C) : Precedes C s t ↔ ∀ (E : C) (hE0 : ¬Limits.IsZero E), phiPlus C t E hE0 < phiPlus C s E hE0 ∧ phiMinus C t E hE0 < phiMinus C s E hE0

The strict order is equivalent to strict decrease of both intrinsic HN endpoints on every nonzero object.

theorem CategoryTheory.Triangulated.Slicing.precedesWeak_iff_extreme_phases_le (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s t : Slicing C) : PrecedesWeak C s t ↔ ∀ (E : C) (hE0 : ¬Limits.IsZero E), phiPlus C t E hE0 ≤ phiPlus C s E hE0 ∧ phiMinus C t E hE0 ≤ phiMinus C s E hE0

The weak order is equivalent to weak decrease of both intrinsic HN endpoints on every nonzero object.

theorem CategoryTheory.Triangulated.Slicing.Precedes.trans (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {s t u : Slicing C} (hst : Precedes C s t) (htu : Precedes C t u) : Precedes C s u

Transitivity of the strict slicing order.

theorem CategoryTheory.Triangulated.Slicing.PrecedesWeak.trans (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {s t u : Slicing C} (hst : PrecedesWeak C s t) (htu : PrecedesWeak C t u) : PrecedesWeak C s u

Transitivity of the weak slicing order.

theorem CategoryTheory.Triangulated.Slicing.Precedes.trans_weak (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {s t u : Slicing C} (hst : Precedes C s t) (htu : PrecedesWeak C t u) : Precedes C s u

A strict comparison followed by a weak one remains strict.

theorem CategoryTheory.Triangulated.Slicing.PrecedesWeak.trans_strict (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {s t u : Slicing C} (hst : PrecedesWeak C s t) (htu : Precedes C t u) : Precedes C s u

A weak comparison followed by a strict one remains strict.