Order relations on slicings

This file introduces the strict and weak relations on slicings used by both arXiv:2601.22994, Definition 2.1, and arXiv:2607.28411v1, Definition 3.12. They compare the phase of an object in the first slicing with the upper HN phase of the same object in the second slicing.

The source papers use different symbols for the same relations. The named predicates here keep that comparison independent of notation and of any central charge or geometric realization.

def CategoryTheory.Triangulated.Slicing.Precedes (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) : Prop

The strict order on slicings: every object of phase phi for s has all HN phases strictly below phi for t.

This is P_s(phi) ⊆ P_t(< phi) in arXiv:2601.22994, Definition 2.1, and P_s ≺ P_t in arXiv:2607.28411v1, Definition 3.12.

Equations

• CategoryTheory.Triangulated.Slicing.Precedes C s t = ∀ (phi : ℝ), s.P phi ≤ CategoryTheory.Triangulated.Slicing.ltProp C t phi

def CategoryTheory.Triangulated.Slicing.PrecedesWeak (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) : Prop

The weak order on slicings: every object of phase phi for s has all HN phases at most phi for t.

This is P_s(phi) ⊆ P_t(≤ phi) in both source papers.

Equations

• CategoryTheory.Triangulated.Slicing.PrecedesWeak C s t = ∀ (phi : ℝ), s.P phi ≤ CategoryTheory.Triangulated.Slicing.leProp C t phi

@[reducible, inline]

abbrev CategoryTheory.Triangulated.Slicing.LiPrecedes (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) : Prop

Li's strict order notation, retained as a source-facing alias of the canonical strict slicing order.

Equations

• CategoryTheory.Triangulated.Slicing.LiPrecedes C s t = CategoryTheory.Triangulated.Slicing.Precedes C s t

@[reducible, inline]

abbrev CategoryTheory.Triangulated.Slicing.LiPrecedesWeak (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) : Prop

Li's weak order notation, retained as a source-facing alias of the canonical weak slicing order.

Equations

• CategoryTheory.Triangulated.Slicing.LiPrecedesWeak C s t = CategoryTheory.Triangulated.Slicing.PrecedesWeak C s t

theorem CategoryTheory.Triangulated.Slicing.liPrecedes_iff_precedes (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) : LiPrecedes C s t ↔ Precedes C s t

The strict relation of arXiv:2601.22994, Definition 2.1, is exactly the strict relation of arXiv:2607.28411v1, Definition 3.12.

theorem CategoryTheory.Triangulated.Slicing.liPrecedesWeak_iff_precedesWeak (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) : LiPrecedesWeak C s t ↔ PrecedesWeak C s t

The weak relation of arXiv:2601.22994, Definition 2.1, is exactly the weak relation of arXiv:2607.28411v1, Definition 3.12.

theorem CategoryTheory.Triangulated.Slicing.precedes_iff_phiPlus_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} {phi : ℝ}, s.P phi E → ∀ (hE0 : ¬Limits.IsZero E), phiPlus C t E hE0 < phi

The strict slicing order is equivalent to its upper-phase formulation on nonzero objects semistable for the left-hand slicing.

theorem CategoryTheory.Triangulated.Slicing.precedesWeak_iff_phiPlus_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} {phi : ℝ}, s.P phi E → ∀ (hE0 : ¬Limits.IsZero E), phiPlus C t E hE0 ≤ phi

The weak slicing order is equivalent to its upper-phase formulation on nonzero objects semistable for the left-hand slicing.

theorem CategoryTheory.Triangulated.Slicing.Precedes.weak (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} (h : Precedes C s t) : PrecedesWeak C s t

A strict comparison is, in particular, a weak comparison.

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

The weak slicing order is reflexive.

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

Shifting all phases down by one strictly increases a slicing in the order: P ≺ P[1], where P[1](phi) = P(phi + 1).

theorem CategoryTheory.Triangulated.Slicing.phaseShift_phiPlus (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (t : ℝ) (E : C) (hE0 : ¬Limits.IsZero E) : phiPlus C (phaseShift C s t) E hE0 = phiPlus C s E hE0 - t

Shifting a slicing down by t subtracts t from the highest phase of a nonzero object.

theorem CategoryTheory.Triangulated.Slicing.phaseShift_phiMinus (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (t : ℝ) (E : C) (hE0 : ¬Limits.IsZero E) : phiMinus C (phaseShift C s t) E hE0 = phiMinus C s E hE0 - t

Shifting a slicing down by t subtracts t from the lowest phase of a nonzero object.