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.
🔗structureCategoryTheory.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)
Fields
chain : CategoryTheory.ComposableArrows C self.n
triangle : Fin self.n → CategoryTheory.Pretriangulated.Triangle C
triangle_dist : ∀ (i : Fin self.n), self.triangle i ∈ CategoryTheory.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 : CategoryTheory.Limits.IsZero self.chain.left
top_iso : Nonempty (self.chain.right ≅ E)
zero_isZero : self.n = 0 → CategoryTheory.Limits.IsZero 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.
🔗structureCategoryTheory.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
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.
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.
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.
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.
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.
Something wrong, better idea? Suggest a change
9.2.8. P_containsZero🔗
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.
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.
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.
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.
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.
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.
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.
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.
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.
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}.
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.
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.
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.
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).
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.
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.
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.
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.
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.
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.
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.
Something wrong, better idea? Suggest a change