Owner-authored Harder--Narasimhan filtrations and slicings

These are the root data structures for the repository-owned stability API. They are deliberately small: operations on filtrations, interval categories, local finiteness, and stability conditions are migrated in later slices.

structure CategoryTheory.Triangulated.HNFiltration (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ℝ → ObjectProperty C) (E : C) extends CategoryTheory.Triangulated.PostnikovTower C E : Type (max u v)

A Harder--Narasimhan filtration: a Postnikov tower whose factors have strictly decreasing phases and lie in their corresponding phase slices.

• n : ℕ
• chain : ComposableArrows C self.n
• triangle : Fin self.n → Pretriangulated.Triangle C
• triangle_dist (i : Fin self.n) : self.triangle i ∈ Pretriangulated.distinguishedTriangles
• triangle_obj₁ (i : Fin self.n) : Nonempty ((self.triangle i).obj₁ ≅ self.chain.obj' ↑i ⋯)
• triangle_obj₂ (i : Fin self.n) : Nonempty ((self.triangle i).obj₂ ≅ self.chain.obj' (↑i + 1) ⋯)
• base_isZero : Limits.IsZero self.chain.left
• top_iso : Nonempty (self.chain.right ≅ E)
• φ : Fin self.n → ℝ

  Phase of each factor.

• hφ : StrictAnti self.φ

  Factor phases are strictly decreasing.

• semistable (j : Fin self.n) : P (self.φ j) (self.factor j)

  Each factor belongs to its recorded phase slice.

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

A Bridgeland slicing on a pretriangulated category.

• P : ℝ → ObjectProperty C

  Semistable objects of phase φ.

• closedUnderIso (φ : ℝ) : (self.P φ).IsClosedUnderIsomorphisms

  Phase slices are invariant under isomorphism.

• zero_mem (φ : ℝ) : self.P φ 0

  The zero object belongs to every phase slice.

• shift_iff (φ : ℝ) (X : C) : self.P φ X ↔ self.P (φ + 1) ((shiftFunctor C 1).obj X)

  Shifting by one increases phase by one.

• hom_vanishing (φ₁ φ₂ : ℝ) (A B : C) : φ₂ < φ₁ → self.P φ₁ A → self.P φ₂ B → ∀ (f : A ⟶ B), f = 0

  Morphisms from higher phase to lower phase vanish.

• hn_exists (E : C) : Nonempty (HNFiltration C self.P E)

  Every object admits an HN filtration.

theorem CategoryTheory.Triangulated.Slicing.ext (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {s t : Slicing C} (hP : s.P = t.P) : s = t

theorem CategoryTheory.Triangulated.Slicing.ext_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {s t : Slicing C} : s = t ↔ s.P = t.P

theorem CategoryTheory.Triangulated.Slicing.zero_mem_of_isZero (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (φ : ℝ) (X : C) (hX : Limits.IsZero X) : s.P φ X

A zero object belongs to every phase slice, not only the chosen zero object used by the structure field.

theorem CategoryTheory.Triangulated.Slicing.shift (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (φ : ℝ) (X : C) (h : s.P φ X) : s.P (φ + 1) ((shiftFunctor C 1).obj X)

Forward form of the shift axiom.

theorem CategoryTheory.Triangulated.Slicing.unshift (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (φ : ℝ) (X : C) (h : s.P (φ + 1) ((shiftFunctor C 1).obj X)) : s.P φ X

Backward form of the shift axiom.

theorem CategoryTheory.Triangulated.Slicing.shift_nat (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (φ : ℝ) (X : C) (n : ℕ) : s.P φ X → s.P (φ + ↑n) ((shiftFunctor C ↑n).obj X)

Iterating the slicing axiom shifts a semistable object by a natural number and adds that number to its phase.

theorem CategoryTheory.Triangulated.Slicing.unshift_nat (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (φ : ℝ) (X : C) (n : ℕ) : s.P (φ + ↑n) ((shiftFunctor C ↑n).obj X) → s.P φ X

Inverse form of Slicing.shift_nat.

theorem CategoryTheory.Triangulated.Slicing.shift_int (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (φ : ℝ) (X : C) (n : ℤ) : s.P φ X ↔ s.P (φ + ↑n) ((shiftFunctor C n).obj X)

Shifting by any integer adds that integer to the phase.