9. IntervalCategory.Basic
Module BridgelandStability.IntervalCategory.Basic — 1 declarations (Definition)
9.1. CategoryTheory.Triangulated.Slicing.IntervalCat
Definition | BridgelandStability.IntervalCategory.Basic | Source | Open Issue
/-- The interval subcategory `P((a, b))` of a slicing, defined as the full subcategory
on objects whose HN phases all lie in `(a, b)`. An object `E` belongs to `P((a, b))` if
it is zero or admits an HN filtration with all phases in `(a, b)`.
This is **Bridgeland's Definition 4.1** specialized to open intervals. -/
abbrev Slicing.IntervalCat (s : Slicing C) (a b : ℝ) :=
(s.intervalProp C a b).FullSubcategory