Preimage transfer of slicings

For a functor F : C ⥤ D and a slicing s on D, the raw phase collection

P_F(phi)(E) := s.P phi (F.obj E)

is the common categorical core of both constructions in arXiv:2607.28411v1, Definitions 3.1 and 3.6. Remarks 3.2 and 3.7 explicitly warn that this raw collection need not be a slicing, even when F is conservative. Accordingly, Slicing.PreimageData records precisely the two slicing axioms which do not follow formally from functoriality and shift compatibility: Hom-vanishing and HN existence.

This factorization is deliberately honest about the theorem boundary. The geometric inducing results (Propositions 3.3 and 3.8, via Appendix A) are expected to construct PreimageData; bare adjunction and conservativity do not.

Main definitions

• Slicing.preimagePhase, Slicing.PreimageData, Slicing.preimage: the raw phase collection, its two non-formal axioms, and the slicing they produce.
• Slicing.pullback, Slicing.pushforward: the source-facing names of Definitions 3.1 and 3.6.

Main results

• Slicing.preimage_id, Slicing.preimage_comp, Slicing.preimage_iso, Slicing.preimage_square: the preimage slicing is functorial in the detecting functor up to natural isomorphism; the square is the shape of Lemma 3.10(1.b)/(2.b).

References

• arXiv:2607.28411v1, Definitions 3.1 and 3.6, Remarks 3.2 and 3.7, Lemma 3.10.

def CategoryTheory.Triangulated.Slicing.preimagePhase {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (s : Slicing D) (F : Functor C D) (phi : ℝ) : ObjectProperty C

The raw inverse-image phase collection along a functor.

It is intentionally only an ObjectProperty, not a Slicing: conservativity alone does not supply Hom-vanishing or HN filtrations.

Equations

• s.preimagePhase F phi E = s.P phi (F.obj E)

@[reducible, inline]

abbrev CategoryTheory.Triangulated.Slicing.pullbackPhaseCollection {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (s : Slicing D) (push : Functor C D) (phi : ℝ) : ObjectProperty C

Source-facing name for Definition 3.1 of arXiv:2607.28411v1. A geometric pullback slicing is computed using the direct-image functor.

Equations

• s.pullbackPhaseCollection push = s.preimagePhase push

@[reducible, inline]

abbrev CategoryTheory.Triangulated.Slicing.pushforwardPhaseCollection {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (s : Slicing D) (pull : Functor C D) (phi : ℝ) : ObjectProperty C

Source-facing name for Definition 3.6 of arXiv:2607.28411v1. A geometric pushforward slicing is computed using the inverse-image functor.

Equations

• s.pushforwardPhaseCollection pull = s.preimagePhase pull

structure CategoryTheory.Triangulated.Slicing.PreimageData {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] (s : Slicing D) (F : Functor C D) : Prop

The genuinely missing axioms for turning the raw inverse-image phase collection into a slicing.

Closure under isomorphisms, zero membership, and the shift law follow from s and F.CommShift. The two fields here are exactly what remains.

• hom_vanishing (phi₁ phi₂ : ℝ) (A B : C) : phi₂ < phi₁ → s.P phi₁ (F.obj A) → s.P phi₂ (F.obj B) → ∀ (g : A ⟶ B), g = 0

  Hom-vanishing for objects whose images lie in separated phase slices.

• hn_exists (E : C) : Nonempty (HNFiltration C (s.preimagePhase F) E)

  HN filtrations in the source with factors detected by F.

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

The identity functor satisfies the two non-formal preimage axioms.

def CategoryTheory.Triangulated.Slicing.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] (s : Slicing D) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : s.PreimageData F) : Slicing C

Construct the genuine inverse-image slicing once the two non-formal axioms have been supplied.

Equations

• s.preimage F h = { P := s.preimagePhase F, closedUnderIso := ⋯, zero_mem := ⋯, shift_iff := ⋯, hom_vanishing := ⋯, hn_exists := ⋯ }

theorem CategoryTheory.Triangulated.Slicing.PreimageData.comp {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] {E : Type u₃} [Category.{v₃, u₃} E] [Limits.HasZeroObject E] [HasShift E ℤ] [Preadditive E] [∀ (n : ℤ), (shiftFunctor E n).Additive] [Pretriangulated E] {s : Slicing E} {G : Functor D E} [G.Additive] [G.CommShift ℤ] [G.IsTriangulated] (hG : s.PreimageData G) {F : Functor C D} (hF : (s.preimage G hG).PreimageData F) : s.PreimageData (F.comp G)

Preimage witnesses compose in the same contravariant order as their functors. The second witness is measured against the slicing constructed by the first stage, so its HN filtrations already have exactly the phases needed for the composite.

theorem CategoryTheory.Triangulated.Slicing.PreimageData.ofIso {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] {s : Slicing D} {F G : Functor C D} (hF : s.PreimageData F) (e : F ≅ G) : s.PreimageData G

A natural isomorphism of detecting functors transports the two non-formal preimage axioms. In particular, the HN factors are unchanged because phase membership is invariant under the component isomorphisms.

@[simp]

theorem CategoryTheory.Triangulated.Slicing.preimage_P {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] (s : Slicing D) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : s.PreimageData F) (phi : ℝ) (E : C) : (s.preimage F h).P phi E ↔ s.P phi (F.obj E)

@[simp]

theorem CategoryTheory.Triangulated.Slicing.preimage_id {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) : s.preimage (Functor.id C) ⋯ = s

@[simp]

theorem CategoryTheory.Triangulated.Slicing.preimage_comp {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] {E : Type u₃} [Category.{v₃, u₃} E] [Limits.HasZeroObject E] [HasShift E ℤ] [Preadditive E] [∀ (n : ℤ), (shiftFunctor E n).Additive] [Pretriangulated E] (s : Slicing E) (G : Functor D E) [G.Additive] [G.CommShift ℤ] [G.IsTriangulated] (hG : s.PreimageData G) (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (hF : (s.preimage G hG).PreimageData F) : s.preimage (F.comp G) ⋯ = (s.preimage G hG).preimage F hF

Constructing a preimage slicing in two stages agrees with constructing it along the composite functor. The statement is independent of the proof terms used to witness the slicing axioms.

theorem CategoryTheory.Triangulated.Slicing.preimage_iso {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] (s : Slicing D) (F G : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] [G.Additive] [G.CommShift ℤ] [G.IsTriangulated] (hF : s.PreimageData F) (e : F ≅ G) : s.preimage G ⋯ = s.preimage F hF

Preimage slicings are invariant under a natural isomorphism of the detecting functors.

theorem CategoryTheory.Triangulated.Slicing.preimageData_equivalence {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] (s : Slicing D) (e : C ≌ D) [e.inverse.Additive] [e.functor.CommShift ℤ] [e.inverse.CommShift ℤ] [e.functor.IsTriangulated] [e.inverse.IsTriangulated] : s.PreimageData e.functor

A triangulated equivalence supplies the two non-formal preimage axioms.

Unlike Slicing.mapEquiv, this theorem allows the source and target categories to differ. HN filtrations are transported through the inverse functor and then identified with the original object by the unit isomorphism.

theorem CategoryTheory.Triangulated.Slicing.preimage_equivalence_P {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] (s : Slicing D) (e : C ≌ D) [e.functor.Additive] [e.inverse.Additive] [e.functor.CommShift ℤ] [e.inverse.CommShift ℤ] [e.functor.IsTriangulated] [e.inverse.IsTriangulated] (phi : ℝ) (X : C) : (s.preimage e.functor ⋯).P phi X ↔ s.P phi (e.functor.obj X)

The preimage slicing along a triangulated equivalence is detected exactly by the equivalence functor.

def CategoryTheory.Triangulated.Slicing.PreimageData.ofFaithful {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] (s : Slicing D) (F : Functor C D) [F.Additive] [F.Faithful] (hn : ∀ (E : C), Nonempty (HNFiltration C (s.preimagePhase F) E)) : s.PreimageData F

For a faithful functor, target Hom-vanishing supplies the Hom component of PreimageData; only HN existence remains to be proved.

Equations

• ⋯ = ⋯

def CategoryTheory.Triangulated.Slicing.PreimageData.phaseShift {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] {s : Slicing D} {F : Functor C D} [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : s.PreimageData F) (t : ℝ) : (Slicing.phaseShift D s t).PreimageData F

The preimage lifting criterion is stable under a uniform translation of all phases.

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev CategoryTheory.Triangulated.Slicing.pullback {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] (s : Slicing D) (push : Functor C D) [push.Additive] [push.CommShift ℤ] [push.IsTriangulated] (h : s.PreimageData push) : Slicing C

Source-facing genuine pullback name. Its explicit PreimageData argument is the formal reminder that conservativity alone is insufficient.

Equations

• s.pullback push h = s.preimage push h

@[reducible, inline]

abbrev CategoryTheory.Triangulated.Slicing.pushforward {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] (s : Slicing D) (pull : Functor C D) [pull.Additive] [pull.CommShift ℤ] [pull.IsTriangulated] (h : s.PreimageData pull) : Slicing C

Source-facing genuine pushforward name.

Equations

• s.pushforward pull h = s.preimage pull h

theorem CategoryTheory.Triangulated.Slicing.preimage_square {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] {E : Type u₃} [Category.{v₃, u₃} E] [Limits.HasZeroObject E] [HasShift E ℤ] [Preadditive E] [∀ (n : ℤ), (shiftFunctor E n).Additive] [Pretriangulated E] {C' : Type u₄} [Category.{v₄, u₄} C'] [Limits.HasZeroObject C'] [HasShift C' ℤ] [Preadditive C'] [∀ (n : ℤ), (shiftFunctor C' n).Additive] [Pretriangulated C'] (s : Slicing E) {F₁ : Functor C D} {G₂ : Functor D E} {G₁ : Functor C C'} {F₂ : Functor C' E} [F₁.Additive] [F₁.CommShift ℤ] [F₁.IsTriangulated] [G₂.Additive] [G₂.CommShift ℤ] [G₂.IsTriangulated] [G₁.Additive] [G₁.CommShift ℤ] [G₁.IsTriangulated] [F₂.Additive] [F₂.CommShift ℤ] [F₂.IsTriangulated] (e : F₁.comp G₂ ≅ G₁.comp F₂) (hG₂ : s.PreimageData G₂) (hF₁ : (s.preimage G₂ hG₂).PreimageData F₁) (hF₂ : s.PreimageData F₂) (hG₁ : (s.preimage F₂ hF₂).PreimageData G₁) : (s.preimage G₂ hG₂).preimage F₁ hF₁ = (s.preimage F₂ hF₂).preimage G₁ hG₁

Two-step preimage slicings around a commuting square of detecting functors agree: the slicing pulled back along G₂ and then along F₁ is the slicing pulled back along F₂ and then along G₁, when F₁ ⋙ G₂ ≅ G₁ ⋙ F₂. This is the shape of Lemma 3.10(1.b) and (2.b) of arXiv:2607.28411v1, the compatibility of pullback and pushforward of slicings with base change along a field extension: base change and the geometric transfer are the two ways around the square, and the slicing does not see which is taken first. Here F₁ : C ⥤ D and F₂ : C' ⥤ E are the transfer functors (f_{ℓ*}, f_* for (1.b); f_ℓ^*, f^* for (2.b)) and G₁, G₂ the base-change direct images π_*; all four run between bounded categories carrying slicings, which is the finite-extension case. For an infinite extension the base-change slicing is not the preimage of a Slicing along π_*, whose target is the Ind-extension in Dqc, and only the shape is captured here.