Bridgeland Stability Conditions

13.6. StabilityCondition: Seminorm🔗

13.6.1. slicingDist_self🔗

The Bridgeland generalized metric is zero on the diagonal: d(\mathcal{P}, \mathcal{P}) = 0.

Proof: Each phase difference is |\phi^\pm(E) - \phi^\pm(E)| = 0, so the supremum is 0.

🔗theorem
CategoryTheory.Triangulated.slicingDist_self.{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) :
  CategoryTheory.Triangulated.slicingDist C s s = 0
CategoryTheory.Triangulated.slicingDist_self.{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) :
  CategoryTheory.Triangulated.slicingDist
      C s s =
    0

Something wrong, better idea? Suggest a change

13.6.2. slicingDist_symm🔗

The Bridgeland generalized metric is symmetric: d(\mathcal{P}_1, \mathcal{P}_2) = d(\mathcal{P}_2, \mathcal{P}_1).

Proof: Follows from |a - b| = |b - a| applied to each phase difference.

🔗theorem
CategoryTheory.Triangulated.slicingDist_symm.{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₁ s₂ : CategoryTheory.Triangulated.Slicing C) :
  CategoryTheory.Triangulated.slicingDist C s₁ s₂ =
    CategoryTheory.Triangulated.slicingDist C s₂ s₁
CategoryTheory.Triangulated.slicingDist_symm.{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₁ s₂ :
    CategoryTheory.Triangulated.Slicing
      C) :
  CategoryTheory.Triangulated.slicingDist
      C s₁ s₂ =
    CategoryTheory.Triangulated.slicingDist
      C s₂ s₁

Something wrong, better idea? Suggest a change

13.6.3. slicingDist_triangle🔗

The Bridgeland generalized metric satisfies the triangle inequality: d(\mathcal{P}_1, \mathcal{P}_3) \leq d(\mathcal{P}_1, \mathcal{P}_2) + d(\mathcal{P}_2, \mathcal{P}_3).

Proof: For each nonzero E, applies the absolute value triangle inequality |a - c| \leq |a - b| + |b - c| to both \phi^+ and \phi^-, then takes the supremum.

🔗theorem
CategoryTheory.Triangulated.slicingDist_triangle.{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₁ s₂ s₃ : CategoryTheory.Triangulated.Slicing C) :
  CategoryTheory.Triangulated.slicingDist C s₁ s₃ ≤
    CategoryTheory.Triangulated.slicingDist C s₁ s₂ +
      CategoryTheory.Triangulated.slicingDist C s₂ s₃
CategoryTheory.Triangulated.slicingDist_triangle.{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₁ s₂ s₃ :
    CategoryTheory.Triangulated.Slicing
      C) :
  CategoryTheory.Triangulated.slicingDist
      C s₁ s₃ ≤
    CategoryTheory.Triangulated.slicingDist
        C s₁ s₂ +
      CategoryTheory.Triangulated.slicingDist
        C s₂ s₃

Something wrong, better idea? Suggest a change

13.6.4. instPseudoEMetricSpaceSlicing🔗

[Lemma 6.1] pseudo-emetric (not generalized metric: missing separation); Lean uses sup of phase differences, paper uses inf of containment radii — equivalence not proved

The space of slicings of \mathcal{C} carries a pseudo-extended-metric structure with distance d(\mathcal{P}, \mathcal{Q}) = \sup_{0 \neq E} \max(|\phi^+_{\mathcal{P}}(E) - \phi^+_{\mathcal{Q}}(E)|, |\phi^-_{\mathcal{P}}(E) - \phi^-_{\mathcal{Q}}(E)|), corresponding to Lemma 6.1 of Bridgeland.

Construction: The edist field is slicingDist; the three axioms (self-distance zero, symmetry, triangle inequality) are supplied by slicingDist_self, slicingDist_symm, and slicingDist_triangle. Note this is a pseudo-emetric (distances may be +\infty and distinct slicings may have distance zero), not a genuine metric.

🔗def
CategoryTheory.Triangulated.instPseudoEMetricSpaceSlicing.{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] :
  PseudoEMetricSpace (CategoryTheory.Triangulated.Slicing C)
CategoryTheory.Triangulated.instPseudoEMetricSpaceSlicing.{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] :
  PseudoEMetricSpace
    (CategoryTheory.Triangulated.Slicing
      C)

Something wrong, better idea? Suggest a change

13.6.5. phiPlus_sub_lt_of_slicingDist🔗

If d(\mathcal{P}_1, \mathcal{P}_2) < \varepsilon, then |\phi_1^+(E) - \phi_2^+(E)| < \varepsilon for every nonzero E. This is one direction of Lemma 6.1.

Proof: Contrapositive: if |\phi_1^+(E) - \phi_2^+(E)| \geq \varepsilon, then the supremum defining d is at least \varepsilon.

🔗theorem
CategoryTheory.Triangulated.phiPlus_sub_lt_of_slicingDist.{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₁ s₂ : CategoryTheory.Triangulated.Slicing C) {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E) {ε : ℝ}
  (hd :
    CategoryTheory.Triangulated.slicingDist C s₁ s₂ <
      ENNReal.ofReal ε) :
  |CategoryTheory.Triangulated.Slicing.phiPlus C s₁ E hE -
        CategoryTheory.Triangulated.Slicing.phiPlus C s₂ E hE| <
    ε
CategoryTheory.Triangulated.phiPlus_sub_lt_of_slicingDist.{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₁ s₂ :
    CategoryTheory.Triangulated.Slicing C)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {ε : ℝ}
  (hd :
    CategoryTheory.Triangulated.slicingDist
        C s₁ s₂ <
      ENNReal.ofReal ε) :
  |CategoryTheory.Triangulated.Slicing.phiPlus
          C s₁ E hE -
        CategoryTheory.Triangulated.Slicing.phiPlus
          C s₂ E hE| <
    ε

Something wrong, better idea? Suggest a change

13.6.6. phiMinus_sub_lt_of_slicingDist🔗

If d(\mathcal{P}_1, \mathcal{P}_2) < \varepsilon, then |\phi_1^-(E) - \phi_2^-(E)| < \varepsilon for every nonzero E. This is the \phi^- direction of Lemma 6.1.

Proof: Identical to phiPlus_sub_lt_of_slicingDist using the \phi^- component of the maximum.

🔗theorem
CategoryTheory.Triangulated.phiMinus_sub_lt_of_slicingDist.{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₁ s₂ : CategoryTheory.Triangulated.Slicing C) {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E) {ε : ℝ}
  (hd :
    CategoryTheory.Triangulated.slicingDist C s₁ s₂ <
      ENNReal.ofReal ε) :
  |CategoryTheory.Triangulated.Slicing.phiMinus C s₁ E hE -
        CategoryTheory.Triangulated.Slicing.phiMinus C s₂ E hE| <
    ε
CategoryTheory.Triangulated.phiMinus_sub_lt_of_slicingDist.{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₁ s₂ :
    CategoryTheory.Triangulated.Slicing C)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {ε : ℝ}
  (hd :
    CategoryTheory.Triangulated.slicingDist
        C s₁ s₂ <
      ENNReal.ofReal ε) :
  |CategoryTheory.Triangulated.Slicing.phiMinus
          C s₁ E hE -
        CategoryTheory.Triangulated.Slicing.phiMinus
          C s₂ E hE| <
    ε

Something wrong, better idea? Suggest a change

13.6.7. intervalProp_of_semistable_slicingDist🔗

Lemma 6.1 (one direction). If d(\mathcal{P}_1, \mathcal{P}_2) < \varepsilon and E is \mathcal{P}_2-semistable of phase \phi, then \phi_1^+(E), \phi_1^-(E) \in (\phi - \varepsilon, \phi + \varepsilon). In words: the HN phases of a semistable object with respect to one slicing are controlled by the slicing distance.

Proof: Uses phiPlus_eq_phiMinus_of_semistable to replace both \phi_2^\pm(E) by \phi, then applies the phase difference bounds.

🔗theorem
CategoryTheory.Triangulated.intervalProp_of_semistable_slicingDist.{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₁ s₂ : CategoryTheory.Triangulated.Slicing C) {E : C} {φ : ℝ}
  (hE : ¬CategoryTheory.Limits.IsZero E) (hS : s₂.P φ E) {ε : ℝ}
  (hd :
    CategoryTheory.Triangulated.slicingDist C s₁ s₂ <
      ENNReal.ofReal ε) :
  CategoryTheory.Triangulated.Slicing.phiPlus C s₁ E hE ∈
      Set.Ioo (φ - ε) (φ + ε) ∧
    CategoryTheory.Triangulated.Slicing.phiMinus C s₁ E hE ∈
      Set.Ioo (φ - ε) (φ + ε)
CategoryTheory.Triangulated.intervalProp_of_semistable_slicingDist.{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₁ s₂ :
    CategoryTheory.Triangulated.Slicing C)
  {E : C} {φ : ℝ}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hS : s₂.P φ E) {ε : ℝ}
  (hd :
    CategoryTheory.Triangulated.slicingDist
        C s₁ s₂ <
      ENNReal.ofReal ε) :
  CategoryTheory.Triangulated.Slicing.phiPlus
        C s₁ E hE ∈
      Set.Ioo (φ - ε) (φ + ε) ∧
    CategoryTheory.Triangulated.Slicing.phiMinus
        C s₁ E hE ∈
      Set.Ioo (φ - ε) (φ + ε)

Something wrong, better idea? Suggest a change

13.6.8. slicingDist_le_of_phase_bounds🔗

Converse direction: if |\phi_1^+(E) - \phi_2^+(E)| \leq \varepsilon and |\phi_1^-(E) - \phi_2^-(E)| \leq \varepsilon for all nonzero E, then d(\mathcal{P}_1, \mathcal{P}_2) \leq \varepsilon.

Proof: Takes the supremum of the pointwise bounds.

🔗theorem
CategoryTheory.Triangulated.slicingDist_le_of_phase_bounds.{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₁ s₂ : CategoryTheory.Triangulated.Slicing C) {ε : ℝ}
  (hP :
    ∀ (E : C) (hE : ¬CategoryTheory.Limits.IsZero E),
      |CategoryTheory.Triangulated.Slicing.phiPlus C s₁ E hE -
            CategoryTheory.Triangulated.Slicing.phiPlus C s₂ E hE| ≤
        ε)
  (hM :
    ∀ (E : C) (hE : ¬CategoryTheory.Limits.IsZero E),
      |CategoryTheory.Triangulated.Slicing.phiMinus C s₁ E hE -
            CategoryTheory.Triangulated.Slicing.phiMinus C s₂ E hE| ≤
        ε) :
  CategoryTheory.Triangulated.slicingDist C s₁ s₂ ≤ ENNReal.ofReal ε
CategoryTheory.Triangulated.slicingDist_le_of_phase_bounds.{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₁ s₂ :
    CategoryTheory.Triangulated.Slicing C)
  {ε : ℝ}
  (hP :
    ∀ (E : C)
      (hE :
        ¬CategoryTheory.Limits.IsZero E),
      |CategoryTheory.Triangulated.Slicing.phiPlus
              C s₁ E hE -
            CategoryTheory.Triangulated.Slicing.phiPlus
              C s₂ E hE| ≤
        ε)
  (hM :
    ∀ (E : C)
      (hE :
        ¬CategoryTheory.Limits.IsZero E),
      |CategoryTheory.Triangulated.Slicing.phiMinus
              C s₁ E hE -
            CategoryTheory.Triangulated.Slicing.phiMinus
              C s₂ E hE| ≤
        ε) :
  CategoryTheory.Triangulated.slicingDist
      C s₁ s₂ ≤
    ENNReal.ofReal ε

Something wrong, better idea? Suggest a change

13.6.9. stabSeminorm_nonneg🔗

The Bridgeland seminorm is nonnegative: \|U\|_\sigma \geq 0. Trivially true since \|U\|_\sigma \in \mathbb{R}_{\geq 0}^\infty.

Proof: Immediate from the definition of \mathbb{R}_{\geq 0}^\infty.

🔗theorem
CategoryTheory.Triangulated.stabSeminorm_nonneg.{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] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (U : Λ →+ ℂ) : 0 ≤ CategoryTheory.Triangulated.stabSeminorm C σ U
CategoryTheory.Triangulated.stabSeminorm_nonneg.{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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (U : Λ →+ ℂ) :
  0 ≤
    CategoryTheory.Triangulated.stabSeminorm
      C σ U

Something wrong, better idea? Suggest a change

13.6.10. stabSeminorm_zero🔗

The seminorm at zero is zero: \|0\|_\sigma = 0.

Proof: Each term in the supremum is \|0\| / \|Z([E])\| = 0.

🔗theorem
CategoryTheory.Triangulated.stabSeminorm_zero.{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] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) :
  CategoryTheory.Triangulated.stabSeminorm C σ 0 = 0
CategoryTheory.Triangulated.stabSeminorm_zero.{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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v) :
  CategoryTheory.Triangulated.stabSeminorm
      C σ 0 =
    0

Something wrong, better idea? Suggest a change

13.6.11. finiteSeminormSubgroup🔗

The finite seminorm subgroup V(\sigma) = \{\, U \in \operatorname{Hom}(\Lambda, \mathbb{C}) : \|U\|_\sigma < \infty \,\}. On a connected component of \operatorname{Stab}(\mathcal{D}), this subgroup is independent of the chosen \sigma (by Lemma 6.2).

Construction: Defined as the AddSubgroup of \Lambda \to \mathbb{C} consisting of those U with finite Bridgeland seminorm. Closure under addition uses the seminorm triangle inequality; closure under negation uses \|-U\|_\sigma = \|U\|_\sigma.

🔗def
CategoryTheory.Triangulated.finiteSeminormSubgroup.{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] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) :
  AddSubgroup (Λ →+ ℂ)
CategoryTheory.Triangulated.finiteSeminormSubgroup.{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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v) :
  AddSubgroup (Λ →+ ℂ)

Something wrong, better idea? Suggest a change

13.6.12. sector_bound🔗

Sector bound (Lemma 6.2 core). For a stability condition \sigma = (Z, \mathcal{P}) and U \colon \Lambda \to \mathbb{C}, if \|U([A])\| \leq M \cdot \|Z([A])\| for every semistable factor A, then for any object E with HN phase width at most \eta < 1, \|U([E])\| \leq \frac{M}{\cos(\pi\eta/2)} \cdot \|Z([E])\|. This is the quantitative heart of Bridgeland's seminorm comparison theory.

Proof: Decomposes U([E]) = \sum U([F_i]) and Z([E]) = \sum Z([F_i]) via the HN filtration and K_0 additivity. Bounds \sum \|U([F_i])\| \leq M \sum \|Z([F_i])\| pointwise, then applies the sector estimate \cos(\pi\eta/2) \cdot \sum \|Z([F_i])\| \leq \|Z([E])\|.

🔗theorem
CategoryTheory.Triangulated.sector_bound.{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] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (U : Λ →+ ℂ) {E : C}
  (F : CategoryTheory.Triangulated.HNFiltration C σ.slicing.P E)
  (hn : 0 < F.n) {η : ℝ} (hη : 0 ≤ η) (hη1 : η < 1)
  (hwidth : F.φ ⟨0, hn⟩ - F.φ ⟨F.n - 1, ⋯⟩ ≤ η) {M : ℝ} (hM0 : 0 ≤ M)
  (hM :
    ∀ (A : C) (φ : ℝ),
      σ.slicing.P φ A →
        ¬CategoryTheory.Limits.IsZero A →
          ‖U (CategoryTheory.Triangulated.cl C v A)‖ ≤
            M * ‖σ.charge A‖) :
  ‖U (CategoryTheory.Triangulated.cl C v E)‖ ≤
    M / Real.cos (Real.pi * η / 2) * ‖σ.charge E‖
CategoryTheory.Triangulated.sector_bound.{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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (U : Λ →+ ℂ) {E : C}
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C σ.slicing.P E)
  (hn : 0 < F.n) {η : ℝ} (hη : 0 ≤ η)
  (hη1 : η < 1)
  (hwidth :
    F.φ ⟨0, hn⟩ - F.φ ⟨F.n - 1, ⋯⟩ ≤ η)
  {M : ℝ} (hM0 : 0 ≤ M)
  (hM :
    ∀ (A : C) (φ : ℝ),
      σ.slicing.P φ A →
        ¬CategoryTheory.Limits.IsZero A →
          ‖U
                (CategoryTheory.Triangulated.cl
                  C v A)‖ ≤
            M * ‖σ.charge A‖) :
  ‖U
        (CategoryTheory.Triangulated.cl C
          v E)‖ ≤
    M / Real.cos (Real.pi * η / 2) *
      ‖σ.charge E‖

Something wrong, better idea? Suggest a change

13.6.13. sector_bound'🔗

Variant of the sector bound using the intrinsic phase width \phi^+(E) - \phi^-(E) \leq \eta.

Proof: Reduces to sector_bound by extracting the canonical HN filtration and its intrinsic width.

🔗theorem
CategoryTheory.Triangulated.sector_bound'.{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] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (U : Λ →+ ℂ) {E : C} (hE : ¬CategoryTheory.Limits.IsZero E) {η : ℝ}
  (hη : 0 ≤ η) (hη1 : η < 1)
  (hwidth :
    CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing E hE -
        CategoryTheory.Triangulated.Slicing.phiMinus C σ.slicing E hE ≤
      η)
  {M : ℝ} (hM0 : 0 ≤ M)
  (hM :
    ∀ (A : C) (φ : ℝ),
      σ.slicing.P φ A →
        ¬CategoryTheory.Limits.IsZero A →
          ‖U (CategoryTheory.Triangulated.cl C v A)‖ ≤
            M * ‖σ.charge A‖) :
  ‖U (CategoryTheory.Triangulated.cl C v E)‖ ≤
    M / Real.cos (Real.pi * η / 2) * ‖σ.charge E‖
CategoryTheory.Triangulated.sector_bound'.{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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (U : Λ →+ ℂ) {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {η : ℝ} (hη : 0 ≤ η) (hη1 : η < 1)
  (hwidth :
    CategoryTheory.Triangulated.Slicing.phiPlus
          C σ.slicing E hE -
        CategoryTheory.Triangulated.Slicing.phiMinus
          C σ.slicing E hE ≤
      η)
  {M : ℝ} (hM0 : 0 ≤ M)
  (hM :
    ∀ (A : C) (φ : ℝ),
      σ.slicing.P φ A →
        ¬CategoryTheory.Limits.IsZero A →
          ‖U
                (CategoryTheory.Triangulated.cl
                  C v A)‖ ≤
            M * ‖σ.charge A‖) :
  ‖U
        (CategoryTheory.Triangulated.cl C
          v E)‖ ≤
    M / Real.cos (Real.pi * η / 2) *
      ‖σ.charge E‖

Something wrong, better idea? Suggest a change

13.6.14. norm_Z_le_of_tau_semistable🔗

For a \tau-semistable nonzero object E with d(\sigma, \tau) < \varepsilon < 1/2 and \|\tau.Z - \sigma.Z\|_\sigma \leq M, one has (1 - M/\cos(\pi\varepsilon)) \cdot \|\sigma.Z([E])\| \leq \|\tau.Z([E])\|. This controls \|Z([E])\| by \|W([E])\| via the reverse triangle inequality and the sector bound.

Proof: The \sigma-HN width of E is less than 2\varepsilon (from semistability and the metric bound). Applies the sector bound with \eta = 2\varepsilon and U = \tau.Z - \sigma.Z, then uses the reverse triangle inequality.

🔗theorem
CategoryTheory.Triangulated.norm_Z_le_of_tau_semistable.{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] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {E : C} {φ : ℝ} (hE : ¬CategoryTheory.Limits.IsZero E)
  (hS : τ.slicing.P φ E) {ε : ℝ} (hε : 0 < ε) (hε1 : ε < 1 / 2)
  (hd :
    CategoryTheory.Triangulated.slicingDist C σ.slicing τ.slicing <
      ENNReal.ofReal ε)
  {M : ℝ} (hM0 : 0 ≤ M)
  (hM_bound :
    ∀ (A : C) (ψ : ℝ),
      σ.slicing.P ψ A →
        ¬CategoryTheory.Limits.IsZero A →
          ‖(τ.Z - σ.Z) (CategoryTheory.Triangulated.cl C v A)‖ ≤
            M * ‖σ.charge A‖) :
  (1 - M / Real.cos (Real.pi * ε)) * ‖σ.charge E‖ ≤ ‖τ.charge E‖
CategoryTheory.Triangulated.norm_Z_le_of_tau_semistable.{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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {E : C} {φ : ℝ}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hS : τ.slicing.P φ E) {ε : ℝ}
  (hε : 0 < ε) (hε1 : ε < 1 / 2)
  (hd :
    CategoryTheory.Triangulated.slicingDist
        C σ.slicing τ.slicing <
      ENNReal.ofReal ε)
  {M : ℝ} (hM0 : 0 ≤ M)
  (hM_bound :
    ∀ (A : C) (ψ : ℝ),
      σ.slicing.P ψ A →
        ¬CategoryTheory.Limits.IsZero A →
          ‖(τ.Z - σ.Z)
                (CategoryTheory.Triangulated.cl
                  C v A)‖ ≤
            M * ‖σ.charge A‖) :
  (1 - M / Real.cos (Real.pi * ε)) *
      ‖σ.charge E‖ ≤
    ‖τ.charge E‖

Something wrong, better idea? Suggest a change

13.6.15. stabSeminorm_bound_real🔗

For \sigma-semistable nonzero A of phase \psi, the ratio \|U([A])\| / \|Z([A])\| is bounded by the toReal of the Bridgeland seminorm \|U\|_\sigma.

Proof: The ratio is one term in the supremum defining \|U\|_\sigma, so it is at most the supremum. Converts via ENNReal.toReal_mono and clears the division.

🔗theorem
CategoryTheory.Triangulated.stabSeminorm_bound_real.{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] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (U : Λ →+ ℂ)
  (hfin : CategoryTheory.Triangulated.stabSeminorm C σ U ≠ ⊤) {A : C}
  {ψ : ℝ} (hP : σ.slicing.P ψ A)
  (hA : ¬CategoryTheory.Limits.IsZero A) :
  ‖U (CategoryTheory.Triangulated.cl C v A)‖ ≤
    (CategoryTheory.Triangulated.stabSeminorm C σ U).toReal *
      ‖σ.charge A‖
CategoryTheory.Triangulated.stabSeminorm_bound_real.{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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (U : Λ →+ ℂ)
  (hfin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ U ≠
      ⊤)
  {A : C} {ψ : ℝ} (hP : σ.slicing.P ψ A)
  (hA : ¬CategoryTheory.Limits.IsZero A) :
  ‖U
        (CategoryTheory.Triangulated.cl C
          v A)‖ ≤
    (CategoryTheory.Triangulated.stabSeminorm
          C σ U).toReal *
      ‖σ.charge A‖

Something wrong, better idea? Suggest a change

13.6.16. stabSeminorm_lt_top_of_same_Z🔗

Seminorm comparison for same central charge. If \sigma and \tau share the same Z and d(\mathcal{P}, \mathcal{Q}) < \varepsilon < 1/2, then \|U\|_\tau < \infty whenever \|U\|_\sigma < \infty. This shows V(\sigma) \subseteq V(\tau) for nearby conditions with the same charge.

Proof: Bounds each term in \|U\|_\tau using the sector bound: the \sigma-HN width of each \tau-semistable object is at most 2\varepsilon, so \|U([E])\| / \|\tau.Z([E])\| \leq M / \cos(\pi\varepsilon).

🔗theorem
CategoryTheory.Triangulated.stabSeminorm_lt_top_of_same_Z.{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] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (hZ : σ.Z = τ.Z) {ε : ℝ} (hε : 0 < ε) (hε1 : ε < 1 / 2)
  (hd :
    CategoryTheory.Triangulated.slicingDist C σ.slicing τ.slicing <
      ENNReal.ofReal ε)
  (U : Λ →+ ℂ)
  (hU : CategoryTheory.Triangulated.stabSeminorm C σ U < ⊤) :
  CategoryTheory.Triangulated.stabSeminorm C τ U < ⊤
CategoryTheory.Triangulated.stabSeminorm_lt_top_of_same_Z.{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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (hZ : σ.Z = τ.Z) {ε : ℝ} (hε : 0 < ε)
  (hε1 : ε < 1 / 2)
  (hd :
    CategoryTheory.Triangulated.slicingDist
        C σ.slicing τ.slicing <
      ENNReal.ofReal ε)
  (U : Λ →+ ℂ)
  (hU :
    CategoryTheory.Triangulated.stabSeminorm
        C σ U <
      ⊤) :
  CategoryTheory.Triangulated.stabSeminorm
      C τ U <
    ⊤

Something wrong, better idea? Suggest a change

13.6.17. finiteSeminormSubgroup_eq_of_same_Z🔗

Proposition 6.3 (same Z case). If \sigma.Z = \tau.Z and d(\mathcal{P}, \mathcal{Q}) < \varepsilon < 1/2, then V(\sigma) = V(\tau).

Proof: Applies stabSeminorm_lt_top_of_same_Z in both directions (swapping \sigma and \tau and using symmetry of the slicing distance).

🔗theorem
CategoryTheory.Triangulated.finiteSeminormSubgroup_eq_of_same_Z.{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] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (hZ : σ.Z = τ.Z) {ε : ℝ} (hε : 0 < ε) (hε1 : ε < 1 / 2)
  (hd :
    CategoryTheory.Triangulated.slicingDist C σ.slicing τ.slicing <
      ENNReal.ofReal ε) :
  CategoryTheory.Triangulated.finiteSeminormSubgroup C σ =
    CategoryTheory.Triangulated.finiteSeminormSubgroup C τ
CategoryTheory.Triangulated.finiteSeminormSubgroup_eq_of_same_Z.{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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (hZ : σ.Z = τ.Z) {ε : ℝ} (hε : 0 < ε)
  (hε1 : ε < 1 / 2)
  (hd :
    CategoryTheory.Triangulated.slicingDist
        C σ.slicing τ.slicing <
      ENNReal.ofReal ε) :
  CategoryTheory.Triangulated.finiteSeminormSubgroup
      C σ =
    CategoryTheory.Triangulated.finiteSeminormSubgroup
      C τ

Something wrong, better idea? Suggest a change

13.6.18. stabSeminorm_le_of_near🔗

General Lemma 6.2 (explicit seminorm bound). If d(\mathcal{P}, \mathcal{Q}) < \varepsilon < 1/2 and \|\tau.Z - \sigma.Z\|_\sigma < \cos(\pi\varepsilon), then \|U\|_\tau \leq \frac{\|U\|_\sigma}{\cos(\pi\varepsilon) - \|\tau.Z - \sigma.Z\|_\sigma}.

Proof: Uses the sector bound on each \tau-semistable object (HN width < 2\varepsilon) with the pointwise seminorm bound and the reverse triangle inequality estimate on \|Z([E])\|.

🔗theorem
CategoryTheory.Triangulated.stabSeminorm_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] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {ε : ℝ} (hε : 0 < ε) (hε1 : ε < 1 / 2)
  (hd :
    CategoryTheory.Triangulated.slicingDist C σ.slicing τ.slicing <
      ENNReal.ofReal ε)
  (hZdiff :
    CategoryTheory.Triangulated.stabSeminorm C σ (τ.Z - σ.Z) <
      ENNReal.ofReal (Real.cos (Real.pi * ε)))
  (U : Λ →+ ℂ)
  (hU : CategoryTheory.Triangulated.stabSeminorm C σ U ≠ ⊤) :
  CategoryTheory.Triangulated.stabSeminorm C τ U ≤
    ENNReal.ofReal
      ((CategoryTheory.Triangulated.stabSeminorm C σ U).toReal /
        (Real.cos (Real.pi * ε) -
          (CategoryTheory.Triangulated.stabSeminorm C σ
              (τ.Z - σ.Z)).toReal))
CategoryTheory.Triangulated.stabSeminorm_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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {ε : ℝ} (hε : 0 < ε) (hε1 : ε < 1 / 2)
  (hd :
    CategoryTheory.Triangulated.slicingDist
        C σ.slicing τ.slicing <
      ENNReal.ofReal ε)
  (hZdiff :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (τ.Z - σ.Z) <
      ENNReal.ofReal
        (Real.cos (Real.pi * ε)))
  (U : Λ →+ ℂ)
  (hU :
    CategoryTheory.Triangulated.stabSeminorm
        C σ U ≠
      ⊤) :
  CategoryTheory.Triangulated.stabSeminorm
      C τ U ≤
    ENNReal.ofReal
      ((CategoryTheory.Triangulated.stabSeminorm
            C σ U).toReal /
        (Real.cos (Real.pi * ε) -
          (CategoryTheory.Triangulated.stabSeminorm
              C σ (τ.Z - σ.Z)).toReal))

Something wrong, better idea? Suggest a change

13.6.19. stabSeminorm_lt_top_of_near🔗

General Lemma 6.2 (seminorm finiteness comparison). Under the hypotheses of stabSeminorm_le_of_near, \|U\|_\sigma < \infty implies \|U\|_\tau < \infty.

Proof: Immediate from stabSeminorm_le_of_near since the bound is finite.

🔗theorem
CategoryTheory.Triangulated.stabSeminorm_lt_top_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] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {ε : ℝ} (hε : 0 < ε) (hε1 : ε < 1 / 2)
  (hd :
    CategoryTheory.Triangulated.slicingDist C σ.slicing τ.slicing <
      ENNReal.ofReal ε)
  (hZdiff :
    CategoryTheory.Triangulated.stabSeminorm C σ (τ.Z - σ.Z) <
      ENNReal.ofReal (Real.cos (Real.pi * ε)))
  (U : Λ →+ ℂ)
  (hU : CategoryTheory.Triangulated.stabSeminorm C σ U < ⊤) :
  CategoryTheory.Triangulated.stabSeminorm C τ U < ⊤
CategoryTheory.Triangulated.stabSeminorm_lt_top_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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {ε : ℝ} (hε : 0 < ε) (hε1 : ε < 1 / 2)
  (hd :
    CategoryTheory.Triangulated.slicingDist
        C σ.slicing τ.slicing <
      ENNReal.ofReal ε)
  (hZdiff :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (τ.Z - σ.Z) <
      ENNReal.ofReal
        (Real.cos (Real.pi * ε)))
  (U : Λ →+ ℂ)
  (hU :
    CategoryTheory.Triangulated.stabSeminorm
        C σ U <
      ⊤) :
  CategoryTheory.Triangulated.stabSeminorm
      C τ U <
    ⊤

Something wrong, better idea? Suggest a change

13.6.20. finiteSeminormSubgroup_eq_of_basisNhd🔗

Proposition 6.3 (V equality for nearby stability conditions). If \tau \in B_\varepsilon(\sigma) with \varepsilon < 1/8, then V(\sigma) = V(\tau). The key inequality is \sin(\pi\varepsilon)(1 + \cos(\pi\varepsilon)) < \cos^2(\pi\varepsilon) for \varepsilon < 1/8, which ensures the reverse comparison \|\sigma.Z - \tau.Z\|_\tau < \cos(\pi\varepsilon).

Proof: Forward direction uses stabSeminorm_lt_top_of_near. Reverse direction bounds \|\sigma.Z - \tau.Z\|_\tau via the explicit seminorm comparison, then verifies M_Z / (c - M_Z) < c using the trigonometric inequality \sin(x)(1 + \cos(x)) < \cos^2(x) for x = \pi\varepsilon.

🔗theorem
CategoryTheory.Triangulated.finiteSeminormSubgroup_eq_of_basisNhd.{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] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {ε : ℝ} (hε : 0 < ε) (hε1 : ε < 1 / 8)
  (hd :
    CategoryTheory.Triangulated.slicingDist C σ.slicing τ.slicing <
      ENNReal.ofReal ε)
  (hZnorm :
    CategoryTheory.Triangulated.stabSeminorm C σ (τ.Z - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε))) :
  CategoryTheory.Triangulated.finiteSeminormSubgroup C σ =
    CategoryTheory.Triangulated.finiteSeminormSubgroup C τ
CategoryTheory.Triangulated.finiteSeminormSubgroup_eq_of_basisNhd.{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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {ε : ℝ} (hε : 0 < ε) (hε1 : ε < 1 / 8)
  (hd :
    CategoryTheory.Triangulated.slicingDist
        C σ.slicing τ.slicing <
      ENNReal.ofReal ε)
  (hZnorm :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (τ.Z - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε))) :
  CategoryTheory.Triangulated.finiteSeminormSubgroup
      C σ =
    CategoryTheory.Triangulated.finiteSeminormSubgroup
      C τ

Something wrong, better idea? Suggest a change