Half-open boundary truncations for owner slicings

This module supplies the dual half-open truncation convention and packages both cutoff conventions as boundary triangles. These triangles are the geometric input for transporting skewed semistability between thin interval presentations.

theorem CategoryTheory.Triangulated.Slicing.exists_dual_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) (_ : geProp C s 0 X) (_ : ltProp 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 owner HN filtration into phases greater than or equal to zero and phases strictly below zero. This is the dual half-open convention to Slicing.exists_phase_truncation.

theorem CategoryTheory.Triangulated.Slicing.exists_upper_boundary_triangle (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 b₁ b₂ : ℝ} (hab₁ : a < b₁) {E : C} (hE : intervalProp C s a b₂ E) : ∃ (X : C) (Y : C) (f : X ⟶ E) (g : E ⟶ Y) (h : Y ⟶ (shiftFunctor C 1).obj X), Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles ∧ geProp C s b₁ X ∧ intervalProp C s a b₁ Y

Truncate an object at an upper endpoint, leaving the boundary phase in the first term.

theorem CategoryTheory.Triangulated.Slicing.exists_lower_boundary_triangle (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₁ a₂ b : ℝ} (ha₁ : a₁ < b) {E : C} (hE : intervalProp C s a₂ b E) : ∃ (X : C) (Y : C) (f : X ⟶ E) (g : E ⟶ Y) (h : Y ⟶ (shiftFunctor C 1).obj X), Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles ∧ intervalProp C s a₁ b X ∧ leProp C s a₁ Y

Truncate an object at a lower endpoint, leaving the boundary phase in the third term.

theorem CategoryTheory.Triangulated.Slicing.intervalProp_of_upper_boundary_triangle (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {a b₁ b₂ : ℝ} (hab₁ : a < b₁) (hab₂ : a < b₂) (hb₁ : b₁ ≤ a + 1) {E X Y : C} (hE : intervalProp C s a b₂ E) (hX : geProp C s b₁ X) (hY : intervalProp C s a b₁ Y) {f : X ⟶ E} {g : E ⟶ Y} {h : Y ⟶ (shiftFunctor C 1).obj X} (hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles) : intervalProp C s a b₂ X

The first term of an upper-boundary triangle remains in the original thin interval.

theorem CategoryTheory.Triangulated.Slicing.intervalProp_of_lower_boundary_triangle (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {a₁ a₂ b : ℝ} (ha₁ : a₁ < b) (ha : a₂ ≤ a₁) {E X Y : C} (hE : intervalProp C s a₂ b E) (hX : intervalProp C s a₁ b X) (hY : leProp C s a₁ Y) {f : X ⟶ E} {g : E ⟶ Y} {h : Y ⟶ (shiftFunctor C 1).obj X} (hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles) : intervalProp C s a₂ b Y

The third term of a lower-boundary triangle remains in the original thin interval.