HN filtrations from phase-indexed induced t-structures

This file formalizes the finite phase-truncation argument in Corollary A.23 of arXiv:2607.28411v1. A target HN filtration is split into its highest-phase factor and tail. The t-structure supplied by formula (A.8) at that phase gives the corresponding source triangle. Uniqueness of t-structure truncation triangles identifies its image with the target head/tail triangle, and induction on the target filtration length terminates the construction.

theorem CategoryTheory.Triangulated.Slicing.InducedTStructures.isZero_of_map_isZero {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} (h : s.InducedTStructures F) {E : C} (hE : Limits.IsZero (F.obj E)) : Limits.IsZero E

Formula (A.8) reflects zero objects. This is the zero-length base case of the phase-truncation induction.

theorem CategoryTheory.Triangulated.Slicing.InducedTStructures.hn_exists {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated D] {s : Slicing D} {F : Functor C D} [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : s.InducedTStructures F) (E : C) : Nonempty (HNFiltration C (s.preimagePhase F) E)

The finite phase-truncation argument supplies the remaining HN field of Slicing.PreimageData.

theorem CategoryTheory.Triangulated.Slicing.InducedTStructures.preimageData {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated D] {s : Slicing D} {F : Functor C D} [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : s.InducedTStructures F) : s.PreimageData F

Formula (A.8), exactness of the detecting functor, and the target slicing construct the genuine preimage slicing data.