Bridgeland Stability Conditions

7.1. IntervalCategory: Basic🔗

7.1.1. IntervalCat🔗

The interval subcategory \mathcal{P}((a, b)) of a slicing \mathcal{P} on a pretriangulated category \mathcal{C} is the full subcategory on objects E that are either zero or admit an HN filtration whose phases all lie in the open interval (a, b) \subset \mathbb{R}. This is Bridgeland's Definition 4.1 specialized to open intervals.

Construction: Defined as the full subcategory on the object property s.intervalProp C a b, which is the disjunction: E is zero, or E has an HN filtration with all phases in (a, b).

🔗def
CategoryTheory.Triangulated.Slicing.IntervalCat.{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 : ℝ) : Type u
CategoryTheory.Triangulated.Slicing.IntervalCat.{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 : ℝ) : Type u

Something wrong, better idea? Suggest a change

7.1.2. ι🔗

The inclusion functor \iota : \mathcal{P}((a, b)) \hookrightarrow \mathcal{C} from the interval subcategory into the ambient category.

Construction: The forgetful functor from the full subcategory to the ambient category, given by ObjectProperty.ι.

🔗def
CategoryTheory.Triangulated.Slicing.IntervalCat.ι.{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.Functor
    (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b) C
CategoryTheory.Triangulated.Slicing.IntervalCat.ι.{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.Functor
    (CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b)
    C

Something wrong, better idea? Suggest a change

7.1.3. intervalProp_of_isZero🔗

Any zero object lies in every interval subcategory \mathcal{P}((a, b)).

Proof: Immediate from the left disjunct of the interval property definition.

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalProp_of_isZero.{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) (a b : ℝ) :
  CategoryTheory.Triangulated.Slicing.intervalProp C s a b E
CategoryTheory.Triangulated.Slicing.intervalProp_of_isZero.{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)
  (a b : ℝ) :
  CategoryTheory.Triangulated.Slicing.intervalProp
    C s a b E

Something wrong, better idea? Suggest a change

7.1.4. intervalProp_containsZero🔗

The interval property \mathcal{P}((a, b)) contains the zero object, witnessed by the canonical zero of \mathcal{C}.

Proof: Applies intervalProp_of_isZero to the canonical zero object.

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalProp_containsZero.{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.Triangulated.Slicing.intervalProp C s a
      b).ContainsZero
CategoryTheory.Triangulated.Slicing.intervalProp_containsZero.{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.Triangulated.Slicing.intervalProp
      C s a b).ContainsZero

Something wrong, better idea? Suggest a change

7.1.5. isZero_of_obj_isZero🔗

If the underlying object of an interval subcategory element X \in \mathcal{P}((a, b)) is zero in \mathcal{C}, then X is zero in \mathcal{P}((a, b)).

Proof: Constructs an isomorphism between X and the zero object of \mathcal{P}((a, b)) by lifting the isomorphism of their underlying objects.

🔗theorem
CategoryTheory.Triangulated.Slicing.IntervalCat.isZero_of_obj_isZero.{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 : ℝ}
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C s a b}
  (hX : CategoryTheory.Limits.IsZero X.obj) :
  CategoryTheory.Limits.IsZero X
CategoryTheory.Triangulated.Slicing.IntervalCat.isZero_of_obj_isZero.{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 : ℝ}
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b}
  (hX :
    CategoryTheory.Limits.IsZero X.obj) :
  CategoryTheory.Limits.IsZero X

Something wrong, better idea? Suggest a change

7.1.6. intervalFiniteLength🔗

For an object E \in \mathcal{P}((a, b)) with b - a \le 2\eta, if every object in each \eta-interval subcategory has a finite subobject lattice, then E has a finite subobject lattice.

Proof: Choose t = (a + b)/2. Then (a, b) \subseteq (t - \eta, t + \eta), so E lies in the \eta-interval centered at t, where the hypothesis provides finiteness.

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalFiniteLength.{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 : ℝ} {E : C}
  (hI : CategoryTheory.Triangulated.Slicing.intervalProp C s a b E)
  {η : ℝ} :
  b - a ≤ 2 * η →
    (∀ (t : ℝ) (F : C),
        CategoryTheory.Triangulated.Slicing.intervalProp C s (t - η)
            (t + η) F →
          Finite (CategoryTheory.Subobject F)) →
      Finite (CategoryTheory.Subobject E)
CategoryTheory.Triangulated.Slicing.intervalFiniteLength.{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 : ℝ} {E : C}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b E)
  {η : ℝ} :
  b - a ≤ 2 * η →
    (∀ (t : ℝ) (F : C),
        CategoryTheory.Triangulated.Slicing.intervalProp
            C s (t - η) (t + η) F →
          Finite
            (CategoryTheory.Subobject
              F)) →
      Finite (CategoryTheory.Subobject E)

Something wrong, better idea? Suggest a change

7.1.7. intervalProp_of_semistable🔗

A \sigma-semistable object E \in \mathcal{P}(\phi) with phase \phi \in (a, b) lies in the interval subcategory \mathcal{P}((a, b)).

Proof: If E is zero this is trivial. Otherwise, semistability forces \phi^+(E) = \phi^-(E) = \phi, so all HN phases lie in (a, b) since a < \phi < b.

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalProp_of_semistable.{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} {φ : ℝ}
  (hP : s.P φ E) {a b : ℝ} (ha : a < φ) (hb : φ < b) :
  CategoryTheory.Triangulated.Slicing.intervalProp C s a b E
CategoryTheory.Triangulated.Slicing.intervalProp_of_semistable.{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} {φ : ℝ} (hP : s.P φ E) {a b : ℝ}
  (ha : a < φ) (hb : φ < b) :
  CategoryTheory.Triangulated.Slicing.intervalProp
    C s a b E

Something wrong, better idea? Suggest a change

7.1.8. intervalProp_mono🔗

Narrower intervals are contained in wider ones: if a' \le a and b \le b', then \mathcal{P}((a, b)) \subseteq \mathcal{P}((a', b')).

Proof: An HN filtration with all phases in (a, b) automatically has all phases in the larger interval (a', b').

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalProp_mono.{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} {a b a' b' : ℝ}
  (ha : a' ≤ a) (hb : b ≤ b')
  (hI : CategoryTheory.Triangulated.Slicing.intervalProp C s a b E) :
  CategoryTheory.Triangulated.Slicing.intervalProp C s a' b' E
CategoryTheory.Triangulated.Slicing.intervalProp_mono.{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} {a b a' b' : ℝ} (ha : a' ≤ a)
  (hb : b ≤ b')
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b E) :
  CategoryTheory.Triangulated.Slicing.intervalProp
    C s a' b' E

Something wrong, better idea? Suggest a change

7.1.9. inclusion🔗

The inclusion functor \mathcal{P}((a_1, b_1)) \hookrightarrow \mathcal{P}((a_2, b_2)) for nested intervals with a_2 \le a_1 and b_1 \le b_2.

Construction: Defined via ObjectProperty.ιOfLE using intervalProp_mono.

🔗def
CategoryTheory.Triangulated.Slicing.IntervalCat.inclusion.{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₁ a₂ b₂ : ℝ}
  (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) :
  CategoryTheory.Functor
    (CategoryTheory.Triangulated.Slicing.IntervalCat C s a₁ b₁)
    (CategoryTheory.Triangulated.Slicing.IntervalCat C s a₂ b₂)
CategoryTheory.Triangulated.Slicing.IntervalCat.inclusion.{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₁ a₂ b₂ : ℝ} (ha : a₂ ≤ a₁)
  (hb : b₁ ≤ b₂) :
  CategoryTheory.Functor
    (CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a₁ b₁)
    (CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a₂ b₂)

Something wrong, better idea? Suggest a change

7.1.10. intervalProp_closedUnderIso🔗

The interval property \mathcal{P}((a, b)) is closed under isomorphisms in \mathcal{C}.

Proof: A zero object remains zero under isomorphism; an HN filtration transfers across an isomorphism of the base object.

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalProp_closedUnderIso.{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.Triangulated.Slicing.intervalProp C s a
      b).IsClosedUnderIsomorphisms
CategoryTheory.Triangulated.Slicing.intervalProp_closedUnderIso.{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.Triangulated.Slicing.intervalProp
      C s a b).IsClosedUnderIsomorphisms

Something wrong, better idea? Suggest a change

7.1.11. intervalProp_stableUnderRetracts🔗

The interval property \mathcal{P}((a, b)) is stable under retracts: if X is a retract of Y \in \mathcal{P}((a, b)), then X \in \mathcal{P}((a, b)).

Proof: If X is zero, we are done. Otherwise, by contradiction: if \phi^+(X) \ge b, the top HN factor of X maps to zero through Y (by hom-vanishing since all phases of Y are < b), and composing with the retraction forces it to map to zero through X as well, contradicting non-triviality. A dual argument handles \phi^-(X) \le a.

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalProp_stableUnderRetracts.{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.Triangulated.Slicing.intervalProp C s a
      b).IsStableUnderRetracts
CategoryTheory.Triangulated.Slicing.intervalProp_stableUnderRetracts.{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.Triangulated.Slicing.intervalProp
      C s a b).IsStableUnderRetracts

Something wrong, better idea? Suggest a change

7.1.12. intervalProp_biprod🔗

The interval property \mathcal{P}((a, b)) is closed under binary biproducts: if X, Y \in \mathcal{P}((a, b)), then X \oplus Y \in \mathcal{P}((a, b)).

Proof: The binary biproduct triangle X \to X \oplus Y \to Y \to X[1] is distinguished, and the interval property is extension-closed.

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalProp_biprod.{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 : ℝ} {X Y : C}
  (hX : CategoryTheory.Triangulated.Slicing.intervalProp C s a b X)
  (hY : CategoryTheory.Triangulated.Slicing.intervalProp C s a b Y) :
  CategoryTheory.Triangulated.Slicing.intervalProp C s a b (X ⊞ Y)
CategoryTheory.Triangulated.Slicing.intervalProp_biprod.{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 : ℝ} {X Y : C}
  (hX :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b X)
  (hY :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a b Y) :
  CategoryTheory.Triangulated.Slicing.intervalProp
    C s a b (X ⊞ Y)

Something wrong, better idea? Suggest a change

7.1.13. intervalProp_closedUnderBinaryProducts🔗

The interval property \mathcal{P}((a, b)) is closed under binary products.

Proof: Follows from closure under binary biproducts via the isomorphism between categorical products and biproducts in a preadditive category.

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalProp_closedUnderBinaryProducts.{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.Triangulated.Slicing.intervalProp C s a
      b).IsClosedUnderBinaryProducts
CategoryTheory.Triangulated.Slicing.intervalProp_closedUnderBinaryProducts.{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.Triangulated.Slicing.intervalProp
      C s a b).IsClosedUnderBinaryProducts

Something wrong, better idea? Suggest a change

7.1.14. intervalProp_closedUnderFiniteProducts🔗

The interval property \mathcal{P}((a, b)) is closed under finite products.

Proof: Induction from closure under binary products and the zero object.

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalProp_closedUnderFiniteProducts.{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.Triangulated.Slicing.intervalProp C s a
      b).IsClosedUnderFiniteProducts
CategoryTheory.Triangulated.Slicing.intervalProp_closedUnderFiniteProducts.{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.Triangulated.Slicing.intervalProp
      C s a b).IsClosedUnderFiniteProducts

Something wrong, better idea? Suggest a change

7.1.15. intervalCat_hasFiniteProducts🔗

The thin interval subcategory \mathcal{P}((a, b)) has finite products.

Proof: Follows from having binary products and a terminal object.

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalCat_hasFiniteProducts.{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.Limits.HasFiniteProducts
    (CategoryTheory.Triangulated.Slicing.IntervalCat C s a b)
CategoryTheory.Triangulated.Slicing.intervalCat_hasFiniteProducts.{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.Limits.HasFiniteProducts
    (CategoryTheory.Triangulated.Slicing.IntervalCat
      C s a b)

Something wrong, better idea? Suggest a change

7.1.16. intervalHom_eq_zero🔗

Hom-vanishing between disjoint intervals. If A \in \mathcal{P}((a_1, b_1)) and B \in \mathcal{P}((a_2, b_2)) with b_2 \le a_1, then \operatorname{Hom}(A, B) = 0.

Proof: Every HN factor of A has phase > a_1 \ge b_2 and every HN factor of B has phase < b_2, so the slicing's hom-vanishing axiom kills each factor-to-factor component. The conclusion follows by induction on the filtration lengths.

🔗theorem
CategoryTheory.Triangulated.Slicing.intervalHom_eq_zero.{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 : C}
  {a₁ b₁ a₂ b₂ : ℝ}
  (hA : CategoryTheory.Triangulated.Slicing.intervalProp C s a₁ b₁ A)
  (hB : CategoryTheory.Triangulated.Slicing.intervalProp C s a₂ b₂ B)
  (hgap : b₂ ≤ a₁) (f : A ⟶ B) : f = 0
CategoryTheory.Triangulated.Slicing.intervalHom_eq_zero.{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 : C} {a₁ b₁ a₂ b₂ : ℝ}
  (hA :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a₁ b₁ A)
  (hB :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s a₂ b₂ B)
  (hgap : b₂ ≤ a₁) (f : A ⟶ B) : f = 0

Something wrong, better idea? Suggest a change