Phase-indexed induced t-structures

Corollary A.23 of arXiv:2607.28411v1 does not construct a preimage slicing directly from an adjunction. It first applies Theorem A.17 at every real phase and obtains a family of bounded t-structures on the source. Formula (A.8) recognizes their two halves by the target slicing:

• D_X,phi^{<= 0} consists of the objects whose image lies in P_Y(>= phi);
• D_X,phi^{>= 1} consists of the objects whose image lies in P_Y(< phi).

This file records that genuine intermediate output. It also proves the Hom-vanishing half of the preimage-slicing theorem from t-structure orthogonality. Constructing source HN filtrations by iterated phase truncation is deliberately a separate theorem boundary; it is not hidden in this structure.

structure CategoryTheory.Triangulated.Slicing.InducedTStructures {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) : Type u₁

The bounded output of applying the Polishchuk inducing theorem at every real phase, expressed by the recognition formulas (A.8).

This is output data, not a replacement for the large-category hypotheses of Theorem A.17. In particular, the structure contains neither an adjunction nor an HN-existence field.

• tStructure : ℝ → TStructure C

  The source t-structure induced at the phase phi.

• le_zero_iff (phi : ℝ) (E : C) : (self.tStructure phi).IsLE E 0 ↔ geProp D s phi (F.obj E)

  Formula (A.8), connective half.

• ge_one_iff (phi : ℝ) (E : C) : (self.tStructure phi).IsGE E 1 ↔ ltProp D s phi (F.obj E)

  Formula (A.8), coconnective half.

def CategoryTheory.Triangulated.Slicing.InducedTStructures.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} (h : s.InducedTStructures F) (e : F ≅ G) : s.InducedTStructures G

Phase-indexed recognition formulas are invariant under a natural isomorphism of the detecting functor.

Equations

• h.ofIso e = { tStructure := h.tStructure, le_zero_iff := ⋯, ge_one_iff := ⋯ }

theorem CategoryTheory.Triangulated.Slicing.InducedTStructures.hom_vanishing {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) (phi₁ phi₂ : ℝ) (A B : C) : phi₂ < phi₁ → s.P phi₁ (F.obj A) → s.P phi₂ (F.obj B) → ∀ (g : A ⟶ B), g = 0

Formula (A.8) supplies Hom-vanishing for the raw preimage phase collection. This is the first non-formal slicing axiom in Slicing.PreimageData.

theorem CategoryTheory.Triangulated.Slicing.InducedTStructures.toPreimageData {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) (hn : ∀ (E : C), Nonempty (HNFiltration C (s.preimagePhase F) E)) : s.PreimageData F

Once the finite phase-truncation argument has supplied source HN filtrations, the phase-indexed t-structures complete the genuine preimage slicing data. The only argument left explicit here is exactly the second field of Slicing.PreimageData, not a disguised copy of the whole output.

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

The identity functor gives an inhabited model of the phase-indexed recognition formulas. Its t-structure at phi is the dual half-open t-structure P([phi, phi + 1)).

Equations

• One or more equations did not get rendered due to their size.