Bridgeland Stability Conditions

14.21. Deformation: Setup🔗

14.21.1. exists_epsilon0🔗

Given a stability condition \sigma, there exists a positive real \varepsilon_0 < 1/8 such that for all t \in \mathbb{R}, every object in the interval subcategory \mathcal{P}((t - 4\varepsilon_0, t + 4\varepsilon_0)) has strict finite length. The width 8\varepsilon_0 is chosen to fit inside the local finiteness parameter 2\eta.

Proof: Extract \eta > 0 from the local finiteness axiom and set \varepsilon_0 = \eta/4. Then 4\varepsilon_0 = \eta, so each window of radius 4\varepsilon_0 is exactly the local finiteness window of radius \eta.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_epsilon0.{v,
    u, 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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) :
  ∃ ε₀,
    ∃ (hε₀ : 0 < ε₀) (hε₀' : ε₀ < 1 / 8),
      ∀ (t : ℝ),
        let a := t - 4 * ε₀;
        let b := t + 4 * ε₀;
        ∀
          (E :
            CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing
              a b),
          CategoryTheory.IsStrictArtinianObject E ∧
            CategoryTheory.IsStrictNoetherianObject E
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_epsilon0.{v,
    u, 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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v) :
  ∃ ε₀,
    ∃ (hε₀ : 0 < ε₀) (hε₀' : ε₀ < 1 / 8),
      ∀ (t : ℝ),
        let a := t - 4 * ε₀;
        let b := t + 4 * ε₀;
        ∀
          (E :
            CategoryTheory.Triangulated.Slicing.IntervalCat
              C σ.slicing a b),
          CategoryTheory.IsStrictArtinianObject
              E ∧
            CategoryTheory.IsStrictNoetherianObject
              E

Something wrong, better idea? Suggest a change

14.21.2. exists_epsilon0_sector🔗

Variant of \varepsilon_0 extraction providing 2\varepsilon_0-intervals for the sector bound: there exists \varepsilon_0 < 1/4 such that every \mathcal{P}((t - 2\varepsilon_0, t + 2\varepsilon_0)) has strict finite length.

Proof: Set \varepsilon_0 = \eta/2 where \eta is the local finiteness parameter, so 2\varepsilon_0 = \eta.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_epsilon0_sector.{v,
    u, 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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) :
  ∃ ε₀,
    ∃ (hε₀ : 0 < ε₀) (hε₀' : ε₀ < 1 / 4),
      ∀ (t : ℝ),
        let a := t - 2 * ε₀;
        let b := t + 2 * ε₀;
        ∀
          (E :
            CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing
              a b),
          CategoryTheory.IsStrictArtinianObject E ∧
            CategoryTheory.IsStrictNoetherianObject E
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_epsilon0_sector.{v,
    u, 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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v) :
  ∃ ε₀,
    ∃ (hε₀ : 0 < ε₀) (hε₀' : ε₀ < 1 / 4),
      ∀ (t : ℝ),
        let a := t - 2 * ε₀;
        let b := t + 2 * ε₀;
        ∀
          (E :
            CategoryTheory.Triangulated.Slicing.IntervalCat
              C σ.slicing a b),
          CategoryTheory.IsStrictArtinianObject
              E ∧
            CategoryTheory.IsStrictNoetherianObject
              E

Something wrong, better idea? Suggest a change

14.21.3. SectorFiniteLength🔗

The predicate asserting that for a stability condition \sigma and parameter \varepsilon_0 > 0, every interval subcategory \mathcal{P}((t - 2\varepsilon_0, t + 2\varepsilon_0)) has strict finite length. This is the thin-sector hypothesis used to start the deformation argument.

Construction: A universal quantification over t \in \mathbb{R}: for each t, every object in \mathcal{P}((t - 2\varepsilon_0, t + 2\varepsilon_0)) is both strict Artinian and strict Noetherian.

🔗def
CategoryTheory.Triangulated.SectorFiniteLength.{v, u, 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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (ε₀ : ℝ) (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4) : Prop
CategoryTheory.Triangulated.SectorFiniteLength.{v,
    u, 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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (ε₀ : ℝ) (hε₀ : 0 < ε₀)
  (hε₀2 : ε₀ < 1 / 4) : Prop

Something wrong, better idea? Suggest a change

14.21.4. WideSectorFiniteLength🔗

The wide local-finiteness predicate: every interval of radius 4\varepsilon_0 has strict finite length. This is the witness needed to apply Lemma 7.7 in the windows \mathcal{P}((t - 3\varepsilon_0, t + 5\varepsilon_0)).

Construction: A universal quantification over t \in \mathbb{R}: for each t, every object in \mathcal{P}((t - 4\varepsilon_0, t + 4\varepsilon_0)) is both strict Artinian and strict Noetherian.

🔗def
CategoryTheory.Triangulated.WideSectorFiniteLength.{v, u, 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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (ε₀ : ℝ) (hε₀ : 0 < ε₀) (hε₀8 : ε₀ < 1 / 8) : Prop
CategoryTheory.Triangulated.WideSectorFiniteLength.{v,
    u, 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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (ε₀ : ℝ) (hε₀ : 0 < ε₀)
  (hε₀8 : ε₀ < 1 / 8) : Prop

Something wrong, better idea? Suggest a change

14.21.5. intervalProp_of_semistable_near🔗

Phase confinement. If d(\sigma.\mathcal{P}, \tau.\mathcal{P}) < \varepsilon and E is \tau-semistable of phase \phi, then E lies in the \sigma-interval subcategory \mathcal{P}((\phi - \varepsilon, \phi + \varepsilon)). This is the fundamental input for the deformation construction.

Proof: From the slicing distance bound, extract HN phase bounds \phi^+(E), \phi^-(E) \in (\phi - \varepsilon, \phi + \varepsilon). Each HN factor phase is then sandwiched between these bounds by monotonicity.

🔗theorem
CategoryTheory.Triangulated.intervalProp_of_semistable_near.{v, u, 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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {E : C} {φ ε : ℝ} (hE : ¬CategoryTheory.Limits.IsZero E)
  (hτ : τ.slicing.P φ E)
  (hd :
    CategoryTheory.Triangulated.slicingDist C σ.slicing τ.slicing <
      ENNReal.ofReal ε) :
  CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing (φ - ε)
    (φ + ε) E
CategoryTheory.Triangulated.intervalProp_of_semistable_near.{v,
    u, 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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {E : C} {φ ε : ℝ}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hτ : τ.slicing.P φ E)
  (hd :
    CategoryTheory.Triangulated.slicingDist
        C σ.slicing τ.slicing <
      ENNReal.ofReal ε) :
  CategoryTheory.Triangulated.Slicing.intervalProp
    C σ.slicing (φ - ε) (φ + ε) E

Something wrong, better idea? Suggest a change

14.21.6. intervalProp_widen🔗

Embedding an interval in a wider one centered at the same point: if E \in \mathcal{P}((\phi - \varepsilon, \phi + \varepsilon)) and \varepsilon \le \varepsilon', then E \in \mathcal{P}((\phi - \varepsilon', \phi + \varepsilon')).

Proof: Immediate from interval monotonicity: (\phi - \varepsilon, \phi + \varepsilon) \subseteq (\phi - \varepsilon', \phi + \varepsilon').

🔗theorem
CategoryTheory.Triangulated.intervalProp_widen.{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} {φ ε ε' : ℝ}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp C s (φ - ε) (φ + ε)
      E)
  (hle : ε ≤ ε') :
  CategoryTheory.Triangulated.Slicing.intervalProp C s (φ - ε') (φ + ε')
    E
CategoryTheory.Triangulated.intervalProp_widen.{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} {φ ε ε' : ℝ}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s (φ - ε) (φ + ε) E)
  (hle : ε ≤ ε') :
  CategoryTheory.Triangulated.Slicing.intervalProp
    C s (φ - ε') (φ + ε') E

Something wrong, better idea? Suggest a change

14.21.7. phiPlus_phiMinus_in_interval🔗

If E \in \mathcal{P}((\phi - \varepsilon, \phi + \varepsilon)) is nonzero, then both \phi^+(E) and \phi^-(E) lie in the open interval (\phi - \varepsilon, \phi + \varepsilon).

Proof: Combines the four existing lemmas phiPlus_gt/lt_of_intervalProp and phiMinus_gt/lt_of_intervalProp.

🔗theorem
CategoryTheory.Triangulated.phiPlus_phiMinus_in_interval.{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) {φ ε : ℝ}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp C s (φ - ε) (φ + ε)
      E) :
  φ - ε < CategoryTheory.Triangulated.Slicing.phiPlus C s E hE ∧
    CategoryTheory.Triangulated.Slicing.phiPlus C s E hE < φ + ε ∧
      φ - ε < CategoryTheory.Triangulated.Slicing.phiMinus C s E hE ∧
        CategoryTheory.Triangulated.Slicing.phiMinus C s E hE < φ + ε
CategoryTheory.Triangulated.phiPlus_phiMinus_in_interval.{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)
  {φ ε : ℝ}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C s (φ - ε) (φ + ε) E) :
  φ - ε <
      CategoryTheory.Triangulated.Slicing.phiPlus
        C s E hE ∧
    CategoryTheory.Triangulated.Slicing.phiPlus
          C s E hE <
        φ + ε ∧
      φ - ε <
          CategoryTheory.Triangulated.Slicing.phiMinus
            C s E hE ∧
        CategoryTheory.Triangulated.Slicing.phiMinus
            C s E hE <
          φ + ε

Something wrong, better idea? Suggest a change

14.21.8. phiPlus_phiMinus_near🔗

If d(\mathcal{P}, \mathcal{Q}) < \varepsilon and E is \tau-semistable of phase \phi, then both \sigma.\phi^+(E) and \sigma.\phi^-(E) lie in (\phi - \varepsilon, \phi + \varepsilon).

Proof: Compose intervalProp_of_semistable_near with phiPlus_phiMinus_in_interval.

🔗theorem
CategoryTheory.Triangulated.phiPlus_phiMinus_near.{v, u, 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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {E : C} {φ ε : ℝ} (hE : ¬CategoryTheory.Limits.IsZero E)
  (hτ : τ.slicing.P φ E)
  (hd :
    CategoryTheory.Triangulated.slicingDist C σ.slicing τ.slicing <
      ENNReal.ofReal ε) :
  φ - ε < CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing E hE ∧
    CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing E hE <
        φ + ε ∧
      φ - ε <
          CategoryTheory.Triangulated.Slicing.phiMinus C σ.slicing E
            hE ∧
        CategoryTheory.Triangulated.Slicing.phiMinus C σ.slicing E hE <
          φ + ε
CategoryTheory.Triangulated.phiPlus_phiMinus_near.{v,
    u, 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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {E : C} {φ ε : ℝ}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hτ : τ.slicing.P φ E)
  (hd :
    CategoryTheory.Triangulated.slicingDist
        C σ.slicing τ.slicing <
      ENNReal.ofReal ε) :
  φ - ε <
      CategoryTheory.Triangulated.Slicing.phiPlus
        C σ.slicing E hE ∧
    CategoryTheory.Triangulated.Slicing.phiPlus
          C σ.slicing E hE <
        φ + ε ∧
      φ - ε <
          CategoryTheory.Triangulated.Slicing.phiMinus
            C σ.slicing E hE ∧
        CategoryTheory.Triangulated.Slicing.phiMinus
            C σ.slicing E hE <
          φ + ε

Something wrong, better idea? Suggest a change

14.21.9. slicingDist_le_of_near🔗

If \sigma and \tau have pointwise phase bounds |\phi^+(E; \sigma) - \phi^+(E; \tau)| \le \varepsilon and |\phi^-(E; \sigma) - \phi^-(E; \tau)| \le \varepsilon for all nonzero E, then d(\mathcal{P}, \mathcal{Q}) \le \varepsilon.

Proof: Delegates to slicingDist_le_of_phase_bounds, which packages the pointwise bounds into the supremum definition of slicing distance.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.slicingDist_le_of_near.{v,
    u, 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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {ε : ℝ}
  (hP :
    ∀ (E : C) (hE : ¬CategoryTheory.Limits.IsZero E),
      |CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing E hE -
            CategoryTheory.Triangulated.Slicing.phiPlus C τ.slicing E
              hE| ≤
        ε)
  (hM :
    ∀ (E : C) (hE : ¬CategoryTheory.Limits.IsZero E),
      |CategoryTheory.Triangulated.Slicing.phiMinus C σ.slicing E hE -
            CategoryTheory.Triangulated.Slicing.phiMinus C τ.slicing E
              hE| ≤
        ε) :
  CategoryTheory.Triangulated.slicingDist C σ.slicing τ.slicing ≤
    ENNReal.ofReal ε
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.slicingDist_le_of_near.{v,
    u, 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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {ε : ℝ}
  (hP :
    ∀ (E : C)
      (hE :
        ¬CategoryTheory.Limits.IsZero E),
      |CategoryTheory.Triangulated.Slicing.phiPlus
              C σ.slicing E hE -
            CategoryTheory.Triangulated.Slicing.phiPlus
              C τ.slicing E hE| ≤
        ε)
  (hM :
    ∀ (E : C)
      (hE :
        ¬CategoryTheory.Limits.IsZero E),
      |CategoryTheory.Triangulated.Slicing.phiMinus
              C σ.slicing E hE -
            CategoryTheory.Triangulated.Slicing.phiMinus
              C τ.slicing E hE| ≤
        ε) :
  CategoryTheory.Triangulated.slicingDist
      C σ.slicing τ.slicing ≤
    ENNReal.ofReal ε

Something wrong, better idea? Suggest a change