Bridgeland Stability Conditions

9.2. Slicing: Defs🔗

9.2.1. HNFiltration🔗

[Definition 3.3] axiom (c): HN decomposition data for triangulated categories

A Harder–Narasimhan filtration of an object E in a triangulated category equipped with a slicing \mathcal{P} is a sequence of distinguished triangles 0 = E_0 \to E_1 \to \cdots \to E_n = E such that each successive quotient A_i = E_i / E_{i-1} lies in \mathcal{P}(\phi_i) for a strictly decreasing sequence of phases \phi_1 > \phi_2 > \cdots > \phi_n.

Construction: The structure carries the filtration length, the sequence of objects, the phase assignments, the distinguished triangle witnesses, and the strict monotonicity proof on the phases.

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

Constructor

CategoryTheory.Triangulated.HNFiltration.mk.{v, u}

Extends

Fields

n : ℕ
Inherited from
  1. CategoryTheory.Triangulated.PostnikovTower C E
chain : CategoryTheory.ComposableArrows C self.n
Inherited from
  1. CategoryTheory.Triangulated.PostnikovTower C E
triangle : Fin self.n → CategoryTheory.Pretriangulated.Triangle C
Inherited from
  1. CategoryTheory.Triangulated.PostnikovTower C E
triangle_dist : ∀ (i : Fin self.n), self.triangle i ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
Inherited from
  1. CategoryTheory.Triangulated.PostnikovTower C E
triangle_obj₁ : ∀ (i : Fin self.n), Nonempty ((self.triangle i).obj₁ ≅ self.chain.obj' ↑i ⋯)
Inherited from
  1. CategoryTheory.Triangulated.PostnikovTower C E
triangle_obj₂ : ∀ (i : Fin self.n), Nonempty ((self.triangle i).obj₂ ≅ self.chain.obj' (↑i + 1) ⋯)
Inherited from
  1. CategoryTheory.Triangulated.PostnikovTower C E
base_isZero : CategoryTheory.Limits.IsZero self.chain.left
Inherited from
  1. CategoryTheory.Triangulated.PostnikovTower C E
top_iso : Nonempty (self.chain.right ≅ E)
Inherited from
  1. CategoryTheory.Triangulated.PostnikovTower C E
zero_isZero : self.n = 0 → CategoryTheory.Limits.IsZero E
Inherited from
  1. CategoryTheory.Triangulated.PostnikovTower C E
φ : Fin self.n → ℝ

The phases of the semistable factors, in strictly decreasing order.

hφ : StrictAnti self.φ

The phases are strictly decreasing (higher phase factors appear first).

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

Each factor is semistable of the given phase.

Something wrong, better idea? Suggest a change

9.2.2. Slicing🔗

[Definition 3.3]

A slicing \mathcal{P} of a triangulated category \mathcal{T} assigns to each \phi \in \mathbb{R} a full additive subcategory \mathcal{P}(\phi) \subseteq \mathcal{T} satisfying: (1) \mathcal{P}(\phi + 1) = \mathcal{P}(\phi)[1], (2) if \phi_1 > \phi_2 and A_i \in \mathcal{P}(\phi_i) then \operatorname{Hom}(A_1, A_2) = 0, and (3) every nonzero object admits a Harder–Narasimhan filtration. This is Definition 3.3 of Bridgeland (2007).

Construction: The structure bundles a predicate mem : ℝ → C → Prop with proofs of the shift compatibility, Hom-vanishing, and HN existence axioms.

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

Constructor

CategoryTheory.Triangulated.Slicing.mk.{v, u}

Fields

P : ℝ → CategoryTheory.ObjectProperty C

For each phase φ ∈ ℝ, the property of semistable objects of phase φ.

closedUnderIso : ∀ (φ : ℝ), (self.P φ).IsClosedUnderIsomorphisms

Each phase slice is closed under isomorphisms.

zero_mem : ∀ (φ : ℝ), self.P φ 0

The zero object satisfies every phase predicate.

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

Shifting by [1] increases the phase by 1, and conversely.

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

Morphisms from higher-phase to lower-phase nonzero semistable objects vanish.

hn_exists : ∀ (E : C), Nonempty (CategoryTheory.Triangulated.HNFiltration C self.P E)

Every object has a Harder-Narasimhan filtration.

Something wrong, better idea? Suggest a change

9.2.3. ext🔗

Two slicings are equal if and only if their underlying phase predicates \mathcal{P} agree.

Proof: All fields of Slicing other than P are propositions or data determined by P, so equality of P implies equality of the whole structure by cases and simp.

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

Something wrong, better idea? Suggest a change

9.2.4. ext_iff🔗

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

Something wrong, better idea? Suggest a change

9.2.5. zero_mem'🔗

Any object isomorphic to zero belongs to every phase slice \mathcal{P}(\phi).

Proof: The zero object lies in \mathcal{P}(\phi) by Slicing.zero_mem; any object isomorphic to zero is therefore in \mathcal{P}(\phi) since each slice is closed under isomorphisms.

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

Something wrong, better idea? Suggest a change

9.2.6. shift🔗

If X \in \mathcal{P}(\phi) then X[1] \in \mathcal{P}(\phi + 1); this is the forward direction of the shift axiom.

Proof: Immediate from the mp direction of shift_iff.

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

Something wrong, better idea? Suggest a change

9.2.7. shift_inv🔗

If X[1] \in \mathcal{P}(\phi + 1) then X \in \mathcal{P}(\phi); this is the backward direction of the shift axiom.

Proof: Immediate from the mpr direction of shift_iff.

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

Something wrong, better idea? Suggest a change

9.2.8. instContainsZeroP🔗

Each phase slice \mathcal{P}(\phi) of a slicing contains the zero object, as required by the ContainsZero typeclass.

Construction: The witness is 0 \in \mathcal{C} together with isZero_zero and Slicing.zero_mem.

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

Something wrong, better idea? Suggest a change

9.2.9. shift_nat🔗

If X \in \mathcal{P}(\phi) then X[n] \in \mathcal{P}(\phi + n) for any natural number n; obtained by iterating the basic shift axiom.

Proof: By induction on n: the base case n = 0 uses the shift-by-zero isomorphism; the inductive step applies shift_iff once more and uses shiftFunctorAdd' to combine the shifts.

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

Something wrong, better idea? Suggest a change

9.2.10. unshift_nat🔗

If X[n] \in \mathcal{P}(\phi + n) for a natural number n then X \in \mathcal{P}(\phi); the inverse of shift_nat.

Proof: By induction on n, using the mpr direction of shift_iff and shiftFunctorAdd' to decompose the shift.

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

Something wrong, better idea? Suggest a change

9.2.11. shift_int🔗

The generalized shift: for any integer n, X \in \mathcal{P}(\phi) if and only if X[n] \in \mathcal{P}(\phi + n).

Proof: For n \geq 0 this follows from iterated application of shift_nat/unshift_nat; for n < 0 one uses shiftFunctorAdd' to rewrite the negative shift as a composite and reduces to the positive case.

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

Something wrong, better idea? Suggest a change

9.2.12. HNFiltration.phiPlus🔗

The highest HN phase \phi^+(E) = \phi_0 extracted from a given filtration, defined as the phase of the first (highest-phase) semistable factor.

Construction: Defined as F.\phi\langle 0, h\rangle, the value of the phase function at the first index.

🔗def
CategoryTheory.Triangulated.HNFiltration.phiPlus.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P : ℝ → CategoryTheory.ObjectProperty C} {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C P E) (h : 0 < F.n) : ℝ
CategoryTheory.Triangulated.HNFiltration.phiPlus.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P :
    ℝ → CategoryTheory.ObjectProperty C}
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C P E)
  (h : 0 < F.n) : ℝ

Something wrong, better idea? Suggest a change

9.2.13. HNFiltration.phiMinus🔗

The lowest HN phase \phi^-(E) = \phi_{n-1} extracted from a given filtration, defined as the phase of the last (lowest-phase) semistable factor.

Construction: Defined as F.\phi\langle n-1, \cdot\rangle, the value of the phase function at the last index.

🔗def
CategoryTheory.Triangulated.HNFiltration.phiMinus.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P : ℝ → CategoryTheory.ObjectProperty C} {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C P E) (h : 0 < F.n) : ℝ
CategoryTheory.Triangulated.HNFiltration.phiMinus.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P :
    ℝ → CategoryTheory.ObjectProperty C}
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C P E)
  (h : 0 < F.n) : ℝ

Something wrong, better idea? Suggest a change

9.2.14. intervalProp🔗

The interval subcategory predicate \mathcal{P}((a,b)): an object E belongs to \mathcal{P}((a,b)) if it is zero or admits an HN filtration all of whose phases lie in the open interval (a, b).

Construction: Defined as the ObjectProperty sending E to \mathrm{IsZero}(E) \lor \exists F : \mathrm{HNFiltration}, \forall i,\; a < F.\phi_i \wedge F.\phi_i < b.

🔗def
CategoryTheory.Triangulated.Slicing.intervalProp.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) (a b : ℝ) :
  CategoryTheory.ObjectProperty C
CategoryTheory.Triangulated.Slicing.intervalProp.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (a b : ℝ) :
  CategoryTheory.ObjectProperty C

Something wrong, better idea? Suggest a change

9.2.15. prefix🔗

Extracts the first k factors of an HN filtration, yielding an HN filtration of the intermediate object E_k with phases \phi_0 > \cdots > \phi_{k-1}.

Construction: The prefix filtration restricts the chain, triangles, and phase data to indices 0, \ldots, k-1; top_iso is the identity since E_k is by definition the k-th chain object.

🔗def
CategoryTheory.Triangulated.HNFiltration.prefix.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P : ℝ → CategoryTheory.ObjectProperty C} {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C P E) (k : ℕ)
  (hk : k ≤ F.n) (hk0 : 0 < k) :
  CategoryTheory.Triangulated.HNFiltration C P (F.chain.obj ⟨k, ⋯⟩)
CategoryTheory.Triangulated.HNFiltration.prefix.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P :
    ℝ → CategoryTheory.ObjectProperty C}
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C P E)
  (k : ℕ) (hk : k ≤ F.n) (hk0 : 0 < k) :
  CategoryTheory.Triangulated.HNFiltration
    C P (F.chain.obj ⟨k, ⋯⟩)

Something wrong, better idea? Suggest a change

9.2.16. prefix_φ🔗

The phases of the prefix filtration agree with those of the original: (F.\mathrm{prefix}\, k).\phi_j = F.\phi_j for all j < k.

Proof: This holds by reflexivity from the definition of prefix.

🔗theorem
CategoryTheory.Triangulated.HNFiltration.prefix_φ.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P : ℝ → CategoryTheory.ObjectProperty C} {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C P E) (k : ℕ)
  (hk : k ≤ F.n) (hk0 : 0 < k) (j : Fin k) :
  (CategoryTheory.Triangulated.HNFiltration.prefix C F k hk hk0).φ j =
    F.φ ⟨↑j, ⋯⟩
CategoryTheory.Triangulated.HNFiltration.prefix_φ.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P :
    ℝ → CategoryTheory.ObjectProperty C}
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C P E)
  (k : ℕ) (hk : k ≤ F.n) (hk0 : 0 < k)
  (j : Fin k) :
  (CategoryTheory.Triangulated.HNFiltration.prefix
          C F k hk hk0).φ
      j =
    F.φ ⟨↑j, ⋯⟩

Something wrong, better idea? Suggest a change

9.2.17. ofIso🔗

Transports an HN filtration of E along an isomorphism E \cong E', producing an HN filtration of E' with the same length, chain, phases, and semistable factors.

Construction: All fields are copied unchanged from the original filtration; top_iso is updated by composing the old isomorphism with e : E \xrightarrow{\sim} E', and zero_isZero is transported along e^{-1}.

🔗def
CategoryTheory.Triangulated.HNFiltration.ofIso.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P : ℝ → CategoryTheory.ObjectProperty C} {E E' : C}
  (F : CategoryTheory.Triangulated.HNFiltration C P E) (e : E ≅ E') :
  CategoryTheory.Triangulated.HNFiltration C P E'
CategoryTheory.Triangulated.HNFiltration.ofIso.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P :
    ℝ → CategoryTheory.ObjectProperty C}
  {E E' : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C P E)
  (e : E ≅ E') :
  CategoryTheory.Triangulated.HNFiltration
    C P E'

Something wrong, better idea? Suggest a change

9.2.18. shiftHN🔗

Shifts an HN filtration of E by an integer a \in \mathbb{Z}, producing an HN filtration of E[a] with shifted phases \phi_i + a. The semistability of each shifted factor follows from the axiom \mathcal{P}(\phi)[a] = \mathcal{P}(\phi + a).

Construction: The chain is precomposed with the shift functor [a]; each phase is increased by a (cast to \mathbb{R}); semistability is verified using Slicing.shift_int.

🔗def
CategoryTheory.Triangulated.HNFiltration.shiftHN.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C s.P E) (a : ℤ) :
  CategoryTheory.Triangulated.HNFiltration C s.P
    ((CategoryTheory.shiftFunctor C a).obj E)
CategoryTheory.Triangulated.HNFiltration.shiftHN.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (a : ℤ) :
  CategoryTheory.Triangulated.HNFiltration
    C s.P
    ((CategoryTheory.shiftFunctor C a).obj
      E)

Something wrong, better idea? Suggest a change

9.2.19. shiftHN_phiMinus🔗

Shifting an HN filtration by a increases \phi^- by a: (F.\mathrm{shiftHN}\, a).\phi^- = F.\phi^- + a.

Proof: This holds by rfl from the definition of shiftHN and phiMinus.

🔗theorem
CategoryTheory.Triangulated.HNFiltration.shiftHN_phiMinus.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C s.P E) (a : ℤ)
  (h : 0 < F.n) :
  CategoryTheory.Triangulated.HNFiltration.phiMinus C
      (CategoryTheory.Triangulated.HNFiltration.shiftHN C s F a) h =
    CategoryTheory.Triangulated.HNFiltration.phiMinus C F h + ↑a
CategoryTheory.Triangulated.HNFiltration.shiftHN_phiMinus.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (a : ℤ) (h : 0 < F.n) :
  CategoryTheory.Triangulated.HNFiltration.phiMinus
      C
      (CategoryTheory.Triangulated.HNFiltration.shiftHN
        C s F a)
      h =
    CategoryTheory.Triangulated.HNFiltration.phiMinus
        C F h +
      ↑a

Something wrong, better idea? Suggest a change

9.2.20. shiftHN_phiPlus🔗

Shifting an HN filtration by a increases \phi^+ by a: (F.\mathrm{shiftHN}\, a).\phi^+ = F.\phi^+ + a.

Proof: This holds by rfl from the definition of shiftHN and phiPlus.

🔗theorem
CategoryTheory.Triangulated.HNFiltration.shiftHN_phiPlus.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C s.P E) (a : ℤ)
  (h : 0 < F.n) :
  CategoryTheory.Triangulated.HNFiltration.phiPlus C
      (CategoryTheory.Triangulated.HNFiltration.shiftHN C s F a) h =
    CategoryTheory.Triangulated.HNFiltration.phiPlus C F h + ↑a
CategoryTheory.Triangulated.HNFiltration.shiftHN_phiPlus.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C s.P E)
  (a : ℤ) (h : 0 < F.n) :
  CategoryTheory.Triangulated.HNFiltration.phiPlus
      C
      (CategoryTheory.Triangulated.HNFiltration.shiftHN
        C s F a)
      h =
    CategoryTheory.Triangulated.HNFiltration.phiPlus
        C F h +
      ↑a

Something wrong, better idea? Suggest a change

9.2.21. n_pos🔗

If E is nonzero then any HN filtration of E has at least one factor, i.e., n \geq 1. If n = 0 the empty filtration would give E \cong 0, contradicting the hypothesis.

Proof: If n = 0 then zero_isZero (applied with the inequality n \leq 0) yields E \cong 0, contradicting \neg\mathrm{IsZero}(E).

🔗theorem
CategoryTheory.Triangulated.HNFiltration.n_pos.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P : ℝ → CategoryTheory.ObjectProperty C} {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C P E)
  (hE : ¬CategoryTheory.Limits.IsZero E) : 0 < F.n
CategoryTheory.Triangulated.HNFiltration.n_pos.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P :
    ℝ → CategoryTheory.ObjectProperty C}
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C P E)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  0 < F.n

Something wrong, better idea? Suggest a change

9.2.22. exists_nonzero_factor🔗

For any HN filtration of a nonzero object E, at least one semistable factor is nonzero. If all factors were zero, a straightforward induction on the chain would show E \cong 0, a contradiction.

Proof: By induction on the chain length: if every factor A_i is zero then each E_i \cong E_{i-1} (since the triangle E_{i-1} \to E_i \to A_i with A_i = 0 gives an isomorphism on the first map), so E = E_n \cong E_0 = 0, contradicting E \neq 0.

🔗theorem
CategoryTheory.Triangulated.HNFiltration.exists_nonzero_factor.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P : ℝ → CategoryTheory.ObjectProperty C} {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C P E)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  ∃ i, ¬CategoryTheory.Limits.IsZero (F.triangle i).obj₃
CategoryTheory.Triangulated.HNFiltration.exists_nonzero_factor.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P :
    ℝ → CategoryTheory.ObjectProperty C}
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C P E)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  ∃ i,
    ¬CategoryTheory.Limits.IsZero
        (F.triangle i).obj₃

Something wrong, better idea? Suggest a change

9.2.23. dropFirst🔗

Given an HN filtration whose first factor A_0 = \mathrm{cone}(E_0 \to E_1)[-1] is zero, produces a new HN filtration of the same object E with the first factor removed, having n-1 factors with phases \phi_1 > \cdots > \phi_{n-1}. The zero first factor forces E_1 \cong 0, so the shortened chain still starts at zero.

Construction: The construction uses the fact that a zero factor forces E_1 \cong 0 (via the distinguished triangle), making the new chain (starting at E_1) a valid HN filtration with the same top object E.

🔗def
CategoryTheory.Triangulated.HNFiltration.dropFirst.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P : ℝ → CategoryTheory.ObjectProperty C} {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C P E) (hn : 1 < F.n)
  (hzero : CategoryTheory.Limits.IsZero (F.triangle ⟨0, ⋯⟩).obj₃) :
  CategoryTheory.Triangulated.HNFiltration C P E
CategoryTheory.Triangulated.HNFiltration.dropFirst.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P :
    ℝ → CategoryTheory.ObjectProperty C}
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C P E)
  (hn : 1 < F.n)
  (hzero :
    CategoryTheory.Limits.IsZero
      (F.triangle ⟨0, ⋯⟩).obj₃) :
  CategoryTheory.Triangulated.HNFiltration
    C P E

Something wrong, better idea? Suggest a change

9.2.24. exists_nonzero_first🔗

For any nonzero object E, there exists an HN filtration whose first factor is nonzero. This is obtained by repeatedly applying dropFirst to eliminate zero leading factors; the process terminates since each step strictly decreases the length n, and at least one factor must be nonzero by exists_nonzero_factor.

Proof: By well-founded induction on the length n: if the first factor of the current filtration is zero, invoke dropFirst (which decreases n by 1) and recurse; otherwise the current filtration witnesses the claim.

🔗theorem
CategoryTheory.Triangulated.HNFiltration.exists_nonzero_first.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  ∃ F,
    ∃ (hn : 0 < F.n),
      ¬CategoryTheory.Limits.IsZero (F.triangle ⟨0, hn⟩).obj₃
CategoryTheory.Triangulated.HNFiltration.exists_nonzero_first.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  ∃ F,
    ∃ (hn : 0 < F.n),
      ¬CategoryTheory.Limits.IsZero
          (F.triangle ⟨0, hn⟩).obj₃

Something wrong, better idea? Suggest a change

9.2.25. dropLast🔗

Given an HN filtration whose last factor A_{n-1} is zero, produces a new HN filtration of the same object E with the last factor removed, having n-1 factors with phases \phi_0 > \cdots > \phi_{n-2}. A zero last factor implies E_{n-1} \cong E_n = E via the distinguished triangle, so the prefix already filtrates E.

Construction: The construction reuses HNFiltration.prefix for the first n-1 steps and adjusts top_iso using the isomorphism E_{n-1} \cong E that results from the zero last factor.

🔗def
CategoryTheory.Triangulated.HNFiltration.dropLast.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P : ℝ → CategoryTheory.ObjectProperty C} {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C P E) (hn : 1 < F.n)
  (hzero :
    CategoryTheory.Limits.IsZero (F.triangle ⟨F.n - 1, ⋯⟩).obj₃) :
  CategoryTheory.Triangulated.HNFiltration C P E
CategoryTheory.Triangulated.HNFiltration.dropLast.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P :
    ℝ → CategoryTheory.ObjectProperty C}
  {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C P E)
  (hn : 1 < F.n)
  (hzero :
    CategoryTheory.Limits.IsZero
      (F.triangle ⟨F.n - 1, ⋯⟩).obj₃) :
  CategoryTheory.Triangulated.HNFiltration
    C P E

Something wrong, better idea? Suggest a change

9.2.26. exists_nonzero_last🔗

For any nonzero object E, there exists an HN filtration whose last factor is nonzero. This is the analogue of exists_nonzero_first, obtained by repeatedly applying dropLast.

Proof: By well-founded induction on n: if the last factor is zero, apply dropLast (decreasing n) and recurse; otherwise stop.

🔗theorem
CategoryTheory.Triangulated.HNFiltration.exists_nonzero_last.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  ∃ F,
    ∃ (hn : 0 < F.n),
      ¬CategoryTheory.Limits.IsZero (F.triangle ⟨F.n - 1, ⋯⟩).obj₃
CategoryTheory.Triangulated.HNFiltration.exists_nonzero_last.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  ∃ F,
    ∃ (hn : 0 < F.n),
      ¬CategoryTheory.Limits.IsZero
          (F.triangle ⟨F.n - 1, ⋯⟩).obj₃

Something wrong, better idea? Suggest a change

9.2.27. Slicing.phiPlus🔗

The intrinsic highest phase \phi^+(E) of a nonzero object E with respect to a slicing \mathcal{P}, defined as the phase of the first factor in an HN filtration chosen to have nonzero first factor.

Construction: Defined using exists_nonzero_first to choose an HN filtration F with nonzero first factor, then taking F.\phi_0; well-definedness is proved separately.

🔗def
CategoryTheory.Triangulated.Slicing.phiPlus.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) (E : C)
  (hE : ¬CategoryTheory.Limits.IsZero E) : ℝ
CategoryTheory.Triangulated.Slicing.phiPlus.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (E : C)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  ℝ

Something wrong, better idea? Suggest a change

9.2.28. Slicing.phiMinus🔗

The intrinsic lowest phase \phi^-(E) of a nonzero object E with respect to a slicing \mathcal{P}, defined as the phase of the last factor in an HN filtration chosen to have nonzero last factor.

Construction: Defined using exists_nonzero_last to choose an HN filtration F with nonzero last factor, then taking F.\phi_{n-1}; well-definedness (independence of the choice) is proved separately.

🔗def
CategoryTheory.Triangulated.Slicing.phiMinus.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s : CategoryTheory.Triangulated.Slicing C) (E : C)
  (hE : ¬CategoryTheory.Limits.IsZero E) : ℝ
CategoryTheory.Triangulated.Slicing.phiMinus.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (s :
    CategoryTheory.Triangulated.Slicing C)
  (E : C)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  ℝ

Something wrong, better idea? Suggest a change