7. Slicing.Defs
Module BridgelandStability.Slicing.Defs — 5 declarations (Structure, Definition)
7.1. CategoryTheory.Triangulated.HNFiltration
Structure | BridgelandStability.Slicing.Defs | Source | Open Issue
/-- A Harder-Narasimhan (HN) filtration of an object `E` with respect to a phase
predicate `P`. This extends a `PostnikovTower` with phase data: each factor is
semistable with a given phase, and the phases are strictly decreasing. -/
@[informal "Definition 3.3" "axiom (c): HN decomposition data for triangulated categories"]
structure HNFiltration (P : ℝ → ObjectProperty C) (E : C) extends PostnikovTower C E where
/-- The phases of the semistable factors, in strictly decreasing order. -/
φ : Fin n → ℝ
/-- The phases are strictly decreasing (higher phase factors appear first). -/
hφ : StrictAnti φ
/-- Each factor is semistable of the given phase. -/
semistable : ∀ j, (P (φ j)) (toPostnikovTower.factor j)
7.2. CategoryTheory.Triangulated.Slicing
Structure | BridgelandStability.Slicing.Defs | Source | Open Issue
/-- A slicing of a pretriangulated category `C`, as defined in
Bridgeland (2007), Definition 5.1. A slicing assigns to each real number `φ`
a full subcategory of semistable objects `P(φ)` (as an `ObjectProperty`),
subject to shift, Hom-vanishing, and Harder-Narasimhan existence axioms.
Each `P(φ)` is an `ObjectProperty C`, enabling use of the `ObjectProperty` API
(e.g. `FullSubcategory`, shift stability, closure properties). -/
@[informal "Definition 3.3" complete]
structure Slicing where
/-- For each phase `φ ∈ ℝ`, the property of semistable objects of phase `φ`. -/
P : ℝ → ObjectProperty C
/-- Each phase slice is closed under isomorphisms. -/
closedUnderIso : ∀ (φ : ℝ), (P φ).IsClosedUnderIsomorphisms
/-- The zero object satisfies every phase predicate. -/
zero_mem : ∀ (φ : ℝ), (P φ) (0 : C)
/-- Shifting by `[1]` increases the phase by 1, and conversely. -/
shift_iff : ∀ (φ : ℝ) (X : C), (P φ) X ↔ (P (φ + 1)) (X⟦(1 : ℤ)⟧)
/-- Morphisms from higher-phase to lower-phase nonzero semistable objects vanish. -/
hom_vanishing : ∀ (φ₁ φ₂ : ℝ) (A B : C),
φ₂ < φ₁ → (P φ₁) A → (P φ₂) B → ∀ (f : A ⟶ B), f = 0
/-- Every object has a Harder-Narasimhan filtration. -/
hn_exists : ∀ (E : C), Nonempty (HNFiltration C P E)
7.3. CategoryTheory.Triangulated.Slicing.intervalProp
Definition | BridgelandStability.Slicing.Defs | Source | Open Issue
/-- The interval subcategory predicate `P((a,b))`: an object `E` belongs to the
interval subcategory if it is zero or all phases in its HN filtration lie in `(a,b)`. -/
def Slicing.intervalProp (s : Slicing C) (a b : ℝ) : ObjectProperty C :=
fun E ↦ IsZero E ∨ ∃ (F : HNFiltration C s.P E), ∀ i, a < F.φ i ∧ F.φ i < b
7.4. CategoryTheory.Triangulated.Slicing.phiPlus
Definition | BridgelandStability.Slicing.Defs | Source | Open Issue
/-- The intrinsic highest phase of a nonzero object with respect to a slicing.
This is the phase of the first factor in any HN filtration with nonzero first factor.
Well-defined by `phiPlus_eq_of_nonzero_factors`. -/
noncomputable def Slicing.phiPlus (s : Slicing C) (E : C) (hE : ¬IsZero E) : ℝ :=
let F := (HNFiltration.exists_nonzero_first C s hE).choose
let hn := (HNFiltration.exists_nonzero_first C s hE).choose_spec.choose
F.φ ⟨0, hn⟩
7.5. CategoryTheory.Triangulated.Slicing.phiMinus
Definition | BridgelandStability.Slicing.Defs | Source | Open Issue
/-- The intrinsic lowest phase of a nonzero object with respect to a slicing.
This is the phase of the last factor in any HN filtration with nonzero last factor.
Well-defined by `phiMinus_eq_of_nonzero_last_factors`. -/
noncomputable def Slicing.phiMinus (s : Slicing C) (E : C) (hE : ¬IsZero E) : ℝ :=
let F := (HNFiltration.exists_nonzero_last C s hE).choose
let hn : 0 < F.n := (HNFiltration.exists_nonzero_last C s hE).choose_spec.choose
F.φ ⟨F.n - 1, Nat.sub_one_lt_of_le hn le_rfl⟩