Phase truncations and the t-structure interface

This file isolates the final input needed to construct a t-structure from an owner slicing: a distinguished triangle separating positive from nonpositive HN phases. The structure construction itself is proved here from that input; the canonical decomposition supplied by an HN filtration is developed next.

theorem CategoryTheory.Triangulated.Slicing.exists_phase_truncation (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (A : C) (F : HNFiltration C s.P A) : ∃ (X : C) (Y : C) (_ : gtProp C s 0 X) (_ : leProp C s 0 Y) (f : X ⟶ A) (g : A ⟶ Y) (h : Y ⟶ (shiftFunctor C 1).obj X), Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles

Split an HN filtration at phase zero. The proof removes the final factor, recursively truncates the prefix, and uses an octahedron to attach a nonpositive last factor to the lower-phase side.

theorem CategoryTheory.Triangulated.Slicing.exists_phase_truncation_zero (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (A : C) : ∃ (X : C) (Y : C) (_ : gtProp C s 0 X) (_ : leProp C s 0 Y) (f : X ⟶ A) (g : A ⟶ Y) (h : Y ⟶ (shiftFunctor C 1).obj X), Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles

Distinguished phase truncations at the boundary 0. This is the precise decomposition datum required by the half-open t-structure convention, and it is available for every owner slicing from its Harder--Narasimhan filtrations.

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

An owner slicing determines a t-structure. Its heart uses the half-open convention P((0, 1]).

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.Slicing.toTStructure_heart_iff (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (E : C) : (toTStructure C s).heart E ↔ gtProp C s 0 E ∧ leProp C s 1 E

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

The t-structure determined by a slicing is bounded.