Conditional functoriality of the slicing orders

Remark 3.14(3) of arXiv:2607.28411v1 says the strict and weak orders are preserved by the paper's pullback and pushforward constructions, when those constructions are slicings. This repository does not yet have the geometric functors or the adjoint-pair API needed to define either construction.

SlicingOrderPreimageData isolates the exact categorical interface consumed by that observation. An operation on slicings is described objectwise by a map obj; membership in a phase slice and in the strict/weak upper phase windows is reflected along that same map. The two order-transport theorems then follow without importing schemes or manufacturing a fake pullback.

The future f_sharp and f^sharp constructions can instantiate this data; until then the result remains explicitly hypothesis-carrying, as required by destination issue #211 (transferred from source issue #141).

structure CategoryTheory.Triangulated.SlicingOrderPreimageData {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (op : Slicing C → Slicing D) (obj : D → C) : Prop

Objectwise preimage data sufficient to transport both slicing orders.

This is intentionally not a functor or a geometric pullback: it is the exact hypothesis package that a future pullback or pushforward construction must discharge.

• semistable_iff (s : Slicing C) (phi : ℝ) (E : D) : (op s).P phi E ↔ s.P phi (obj E)

  Phase-slice membership is computed on the chosen source object.

• ltProp_iff (s : Slicing C) (phi : ℝ) (E : D) : Slicing.ltProp D (op s) phi E ↔ Slicing.ltProp C s phi (obj E)

  The strict upper phase window is computed on the same source object.

• leProp_iff (s : Slicing C) (phi : ℝ) (E : D) : Slicing.leProp D (op s) phi E ↔ Slicing.leProp C s phi (obj E)

  The weak upper phase window is computed on the same source object.

theorem CategoryTheory.Triangulated.SlicingOrderPreimageData.precedes {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {op : Slicing C → Slicing D} {obj : D → C} (h : SlicingOrderPreimageData op obj) {s t : Slicing C} (hst : Slicing.Precedes C s t) : Slicing.Precedes D (op s) (op t)

Any slicing operation satisfying the preimage interface preserves the strict order. This is the hypothesis-carrying form of the strict pullback/pushforward clause in Remark 3.14(3).

theorem CategoryTheory.Triangulated.SlicingOrderPreimageData.precedesWeak {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {op : Slicing C → Slicing D} {obj : D → C} (h : SlicingOrderPreimageData op obj) {s t : Slicing C} (hst : Slicing.PrecedesWeak C s t) : Slicing.PrecedesWeak D (op s) (op t)

Any slicing operation satisfying the preimage interface preserves the weak order. This is the hypothesis-carrying form of the weak pullback/pushforward clause in Remark 3.14(3).

theorem CategoryTheory.Triangulated.Slicing.Precedes.pushforward_of_preimage {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (op : Slicing C → Slicing D) (obj : D → C) (h : SlicingOrderPreimageData op obj) {s t : Slicing C} (hst : Precedes C s t) : Precedes D (op s) (op t)

Source-facing strict pushforward wrapper. No pushforward is constructed: the caller supplies its preimage data explicitly.

theorem CategoryTheory.Triangulated.Slicing.PrecedesWeak.pushforward_of_preimage {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (op : Slicing C → Slicing D) (obj : D → C) (h : SlicingOrderPreimageData op obj) {s t : Slicing C} (hst : PrecedesWeak C s t) : PrecedesWeak D (op s) (op t)

Source-facing weak pushforward wrapper.

theorem CategoryTheory.Triangulated.Slicing.Precedes.pullback_of_preimage {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (op : Slicing C → Slicing D) (obj : D → C) (h : SlicingOrderPreimageData op obj) {s t : Slicing C} (hst : Precedes C s t) : Precedes D (op s) (op t)

Source-facing strict pullback wrapper. It is deliberately a second name for the same abstract interface: which geometric adjoint computes obj is a fact for the future pullback construction, not for the slicing-order layer.

theorem CategoryTheory.Triangulated.Slicing.PrecedesWeak.pullback_of_preimage {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (op : Slicing C → Slicing D) (obj : D → C) (h : SlicingOrderPreimageData op obj) {s t : Slicing C} (hst : PrecedesWeak C s t) : PrecedesWeak D (op s) (op t)

Source-facing weak pullback wrapper.