Bridgeland Stability Conditions

13.3. StabilityCondition: Deformation🔗

13.3.1. exists_eq_Z_and_mem_basisNhd_of_stabSeminorm_lt_sin🔗

Theorem 7.1 (local surjectivity). A small deformation of the central charge lifts to a stability condition inside B_\varepsilon(\sigma): if \|W - Z(\sigma)\|_\sigma < \sin(\pi\varepsilon) and the wide-sector finite length condition holds, then there exists \tau with \tau.Z = W and \tau \in B_\varepsilon(\sigma).

Proof: Invokes the deformation theorem to obtain \tau with \tau.Z = W and controlled slicing distance, then verifies both the seminorm and distance conditions for membership in B_\varepsilon(\sigma).

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_eq_Z_and_mem_basisNhd_of_stabSeminorm_lt_sin.{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)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  (ε₀ : ℝ) (hε₀ : 0 < ε₀) (hε₀10 : ε₀ < 1 / 10)
  (hWide :
    CategoryTheory.Triangulated.WideSectorFiniteLength C σ ε₀ hε₀ ⋯)
  (ε : ℝ) (hε : 0 < ε) (hεε₀ : ε < ε₀)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε))) :
  ∃ τ, τ.Z = W ∧ τ ∈ CategoryTheory.Triangulated.basisNhd C σ ε
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_eq_Z_and_mem_basisNhd_of_stabSeminorm_lt_sin.{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)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  (ε₀ : ℝ) (hε₀ : 0 < ε₀)
  (hε₀10 : ε₀ < 1 / 10)
  (hWide :
    CategoryTheory.Triangulated.WideSectorFiniteLength
      C σ ε₀ hε₀ ⋯)
  (ε : ℝ) (hε : 0 < ε) (hεε₀ : ε < ε₀)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε))) :
  ∃ τ,
    τ.Z = W ∧
      τ ∈
        CategoryTheory.Triangulated.basisNhd
          C σ ε

Something wrong, better idea? Suggest a change

13.3.2. wideSectorFiniteLength_mono🔗

Wide-sector finite length is monotone under shrinking \varepsilon_0: if the condition holds for \varepsilon_0, it holds for any \varepsilon_1 \leq \varepsilon_0.

Proof: The interval [t - 4\varepsilon_1, t + 4\varepsilon_1] is contained in [t - 4\varepsilon_0, t + 4\varepsilon_0], so any object in the smaller interval category embeds into the larger one, which has finite length by hypothesis.

🔗theorem
CategoryTheory.Triangulated.wideSectorFiniteLength_mono.{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)
  (hWide :
    CategoryTheory.Triangulated.WideSectorFiniteLength C σ ε₀ hε₀ hε₀8)
  (hε₁ : 0 < ε₁) (hε₁8 : ε₁ < 1 / 8) (hε₁ε₀ : ε₁ ≤ ε₀) :
  CategoryTheory.Triangulated.WideSectorFiniteLength C σ ε₁ hε₁ hε₁8
CategoryTheory.Triangulated.wideSectorFiniteLength_mono.{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)
  (hWide :
    CategoryTheory.Triangulated.WideSectorFiniteLength
      C σ ε₀ hε₀ hε₀8)
  (hε₁ : 0 < ε₁) (hε₁8 : ε₁ < 1 / 8)
  (hε₁ε₀ : ε₁ ≤ ε₀) :
  CategoryTheory.Triangulated.WideSectorFiniteLength
    C σ ε₁ hε₁ hε₁8

Something wrong, better idea? Suggest a change

13.3.3. exists_epsilon0_tenth🔗

Every stability condition admits a local \varepsilon_0 < 1/10 witness for Theorem 7.1, obtained by halving the standard exists_epsilon0 witness.

Proof: Takes the standard \varepsilon_1 < 1/8 from exists_epsilon0 and sets \varepsilon_0 = \varepsilon_1/2, applying wideSectorFiniteLength_mono.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_epsilon0_tenth.{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ε₀10 : ε₀ < 1 / 10),
      CategoryTheory.Triangulated.WideSectorFiniteLength C σ ε₀ hε₀ ⋯
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_epsilon0_tenth.{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ε₀10 :
      ε₀ < 1 / 10),
      CategoryTheory.Triangulated.WideSectorFiniteLength
        C σ ε₀ hε₀ ⋯

Something wrong, better idea? Suggest a change

13.3.4. deformation🔗

[Theorem 7.1]

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformation.{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) :
  ∃ ε₀,
    0 < ε₀ ∧
      ∀ (W : Λ →+ ℂ) (ε : ℝ),
        0 < ε →
          ε < ε₀ →
            CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
                ENNReal.ofReal (Real.sin (Real.pi * ε)) →
              ∃ τ,
                τ.Z = W ∧
                  CategoryTheory.Triangulated.slicingDist C σ.slicing
                      τ.slicing <
                    ENNReal.ofReal ε
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformation.{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) :
  ∃ ε₀,
    0 < ε₀ ∧
      ∀ (W : Λ →+ ℂ) (ε : ℝ),
        0 < ε →
          ε < ε₀ →
            CategoryTheory.Triangulated.stabSeminorm
                  C σ (W - σ.Z) <
                ENNReal.ofReal
                  (Real.sin
                    (Real.pi * ε)) →
              ∃ τ,
                τ.Z = W ∧
                  CategoryTheory.Triangulated.slicingDist
                      C σ.slicing
                      τ.slicing <
                    ENNReal.ofReal ε

Something wrong, better idea? Suggest a change

13.3.5. linearInterpolationZ🔗

The affine interpolation between the central charges of \sigma and \tau: Z_t = Z(\sigma) + t \cdot (Z(\tau) - Z(\sigma)) for t \in \mathbb{R}.

Construction: Defined as \sigma.Z + t \cdot (\tau.Z - \sigma.Z) using scalar multiplication on additive group homomorphisms.

🔗def
CategoryTheory.Triangulated.linearInterpolationZ.{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)
  (t : ℝ) : Λ →+ ℂ
CategoryTheory.Triangulated.linearInterpolationZ.{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)
  (t : ℝ) : Λ →+ ℂ

Something wrong, better idea? Suggest a change

13.3.6. linearInterpolationZ_zero🔗

Z_0 = Z(\sigma): the interpolation at t = 0 recovers the initial charge.

Proof: Immediate from 0 \cdot (\tau.Z - \sigma.Z) = 0.

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

Something wrong, better idea? Suggest a change

13.3.7. linearInterpolationZ_one🔗

Z_1 = Z(\tau): the interpolation at t = 1 recovers the target charge.

Proof: Immediate from \sigma.Z + 1 \cdot (\tau.Z - \sigma.Z) = \tau.Z.

🔗theorem
CategoryTheory.Triangulated.linearInterpolationZ_one.{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) :
  CategoryTheory.Triangulated.linearInterpolationZ C σ τ 1 = τ.Z
CategoryTheory.Triangulated.linearInterpolationZ_one.{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) :
  CategoryTheory.Triangulated.linearInterpolationZ
      C σ τ 1 =
    τ.Z

Something wrong, better idea? Suggest a change

13.3.8. linearInterpolationZ_sub🔗

Z_t - Z(\sigma) = t \cdot (Z(\tau) - Z(\sigma)).

Proof: Direct computation from the definition of the interpolation.

🔗theorem
CategoryTheory.Triangulated.linearInterpolationZ_sub.{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)
  (t : ℝ) :
  CategoryTheory.Triangulated.linearInterpolationZ C σ τ t - σ.Z =
    t • (τ.Z - σ.Z)
CategoryTheory.Triangulated.linearInterpolationZ_sub.{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)
  (t : ℝ) :
  CategoryTheory.Triangulated.linearInterpolationZ
        C σ τ t -
      σ.Z =
    t • (τ.Z - σ.Z)

Something wrong, better idea? Suggest a change

13.3.9. linearInterpolationZ_sub_sub🔗

Z_t - Z_s = (t - s) \cdot (Z(\tau) - Z(\sigma)).

Proof: Subtracts the two interpolation formulas and simplifies.

🔗theorem
CategoryTheory.Triangulated.linearInterpolationZ_sub_sub.{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)
  (s t : ℝ) :
  CategoryTheory.Triangulated.linearInterpolationZ C σ τ t -
      CategoryTheory.Triangulated.linearInterpolationZ C σ τ s =
    (t - s) • (τ.Z - σ.Z)
CategoryTheory.Triangulated.linearInterpolationZ_sub_sub.{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)
  (s t : ℝ) :
  CategoryTheory.Triangulated.linearInterpolationZ
        C σ τ t -
      CategoryTheory.Triangulated.linearInterpolationZ
        C σ τ s =
    (t - s) • (τ.Z - σ.Z)

Something wrong, better idea? Suggest a change

13.3.10. stabSeminorm_smul🔗

The Bridgeland seminorm is \mathbb{R}-homogeneous: \|t \cdot U\|_\sigma = |t| \cdot \|U\|_\sigma.

Proof: Pulls |t| out of each term \|tU([E])\| / \|Z([E])\| using \|tU([E])\| = |t| \cdot \|U([E])\|, then factors through the supremum.

🔗theorem
CategoryTheory.Triangulated.stabSeminorm_smul.{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)
  (U : Λ →+ ℂ) (t : ℝ) :
  CategoryTheory.Triangulated.stabSeminorm C σ (t • U) =
    ENNReal.ofReal |t| * CategoryTheory.Triangulated.stabSeminorm C σ U
CategoryTheory.Triangulated.stabSeminorm_smul.{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)
  (U : Λ →+ ℂ) (t : ℝ) :
  CategoryTheory.Triangulated.stabSeminorm
      C σ (t • U) =
    ENNReal.ofReal |t| *
      CategoryTheory.Triangulated.stabSeminorm
        C σ U

Something wrong, better idea? Suggest a change

13.3.11. stabSeminorm_smul_complex🔗

The Bridgeland seminorm is \mathbb{C}-homogeneous: \|t \cdot U\|_\sigma = \|t\| \cdot \|U\|_\sigma for t \in \mathbb{C}.

Proof: Same as stabSeminorm_smul using \|tU([E])\| = \|t\| \cdot \|U([E])\|.

🔗theorem
CategoryTheory.Triangulated.stabSeminorm_smul_complex.{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)
  (U : Λ →+ ℂ) (t : ℂ) :
  CategoryTheory.Triangulated.stabSeminorm C σ (t • U) =
    ENNReal.ofReal ‖t‖ * CategoryTheory.Triangulated.stabSeminorm C σ U
CategoryTheory.Triangulated.stabSeminorm_smul_complex.{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)
  (U : Λ →+ ℂ) (t : ℂ) :
  CategoryTheory.Triangulated.stabSeminorm
      C σ (t • U) =
    ENNReal.ofReal ‖t‖ *
      CategoryTheory.Triangulated.stabSeminorm
        C σ U

Something wrong, better idea? Suggest a change

13.3.12. stabSeminorm_add_le🔗

The Bridgeland seminorm satisfies the triangle inequality: \|U + V\|_\sigma \leq \|U\|_\sigma + \|V\|_\sigma.

Proof: For each semistable object, \|(U + V)([E])\| / \|Z([E])\| \leq \|U([E])\| / \|Z([E])\| + \|V([E])\| / \|Z([E])\| by the norm triangle inequality, then takes the supremum.

🔗theorem
CategoryTheory.Triangulated.stabSeminorm_add_le.{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)
  (U V : Λ →+ ℂ) :
  CategoryTheory.Triangulated.stabSeminorm C σ (U + V) ≤
    CategoryTheory.Triangulated.stabSeminorm C σ U +
      CategoryTheory.Triangulated.stabSeminorm C σ V
CategoryTheory.Triangulated.stabSeminorm_add_le.{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)
  (U V : Λ →+ ℂ) :
  CategoryTheory.Triangulated.stabSeminorm
      C σ (U + V) ≤
    CategoryTheory.Triangulated.stabSeminorm
        C σ U +
      CategoryTheory.Triangulated.stabSeminorm
        C σ V

Something wrong, better idea? Suggest a change

13.3.13. stabSeminorm_neg🔗

The Bridgeland seminorm satisfies \|-U\|_\sigma = \|U\|_\sigma.

Proof: Follows from \|-U([E])\| = \|U([E])\|.

🔗theorem
CategoryTheory.Triangulated.stabSeminorm_neg.{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)
  (U : Λ →+ ℂ) :
  CategoryTheory.Triangulated.stabSeminorm C σ (-U) =
    CategoryTheory.Triangulated.stabSeminorm C σ U
CategoryTheory.Triangulated.stabSeminorm_neg.{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)
  (U : Λ →+ ℂ) :
  CategoryTheory.Triangulated.stabSeminorm
      C σ (-U) =
    CategoryTheory.Triangulated.stabSeminorm
      C σ U

Something wrong, better idea? Suggest a change

13.3.14. stabSeminorm_dominated_of_basisNhd🔗

Local seminorm domination. If \tau \in B_\varepsilon(\sigma) with \varepsilon < 1/8, then there exists a finite constant K such that \|U\|_\sigma \leq K \cdot \|U\|_\tau for all U. This is the local form of Lemma 6.2.

Proof: Bounds \|\tau.Z - \sigma.Z\|_\tau using the explicit seminorm comparison, verifies M_Z / (c - M_Z) < c via the trigonometric inequality, then constructs the reverse comparison constant K = 1 / (c - N_Z).

🔗theorem
CategoryTheory.Triangulated.stabSeminorm_dominated_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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {ε : ℝ} (hε : 0 < ε) (hε8 : ε < 1 / 8)
  (hτ : τ ∈ CategoryTheory.Triangulated.basisNhd C σ ε) :
  ∃ K,
    K ≠ ⊤ ∧
      ∀ (U : Λ →+ ℂ),
        CategoryTheory.Triangulated.stabSeminorm C σ U ≤
          K * CategoryTheory.Triangulated.stabSeminorm C τ U
CategoryTheory.Triangulated.stabSeminorm_dominated_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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {ε : ℝ} (hε : 0 < ε) (hε8 : ε < 1 / 8)
  (hτ :
    τ ∈
      CategoryTheory.Triangulated.basisNhd
        C σ ε) :
  ∃ K,
    K ≠ ⊤ ∧
      ∀ (U : Λ →+ ℂ),
        CategoryTheory.Triangulated.stabSeminorm
            C σ U ≤
          K *
            CategoryTheory.Triangulated.stabSeminorm
              C τ U

Something wrong, better idea? Suggest a change

13.3.15. stabSeminorm_center_dominates_of_basisNhd🔗

Local forward domination. If \tau \in B_\varepsilon(\sigma), then \|U\|_\tau \leq K \cdot \|U\|_\sigma for some finite K.

Proof: Direct application of the explicit seminorm comparison stabSeminorm_le_of_near with the constant K = 1 / (\cos(\pi\varepsilon) - M_Z).

🔗theorem
CategoryTheory.Triangulated.stabSeminorm_center_dominates_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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {ε : ℝ} (hε : 0 < ε) (hε8 : ε < 1 / 8)
  (hτ : τ ∈ CategoryTheory.Triangulated.basisNhd C σ ε) :
  ∃ K,
    K ≠ ⊤ ∧
      ∀ (U : Λ →+ ℂ),
        CategoryTheory.Triangulated.stabSeminorm C τ U ≤
          K * CategoryTheory.Triangulated.stabSeminorm C σ U
CategoryTheory.Triangulated.stabSeminorm_center_dominates_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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {ε : ℝ} (hε : 0 < ε) (hε8 : ε < 1 / 8)
  (hτ :
    τ ∈
      CategoryTheory.Triangulated.basisNhd
        C σ ε) :
  ∃ K,
    K ≠ ⊤ ∧
      ∀ (U : Λ →+ ℂ),
        CategoryTheory.Triangulated.stabSeminorm
            C τ U ≤
          K *
            CategoryTheory.Triangulated.stabSeminorm
              C σ U

Something wrong, better idea? Suggest a change

13.3.16. basisNhd_self🔗

A basis neighborhood contains its center: \sigma \in B_\varepsilon(\sigma).

Proof: The charge difference is zero (seminorm zero), and the slicing distance is zero.

🔗theorem
CategoryTheory.Triangulated.basisNhd_self.{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) :
  σ ∈ CategoryTheory.Triangulated.basisNhd C σ ε
CategoryTheory.Triangulated.basisNhd_self.{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) :
  σ ∈
    CategoryTheory.Triangulated.basisNhd C
      σ ε

Something wrong, better idea? Suggest a change

13.3.17. basisNhd_mono🔗

Shrinking the radius shrinks the neighborhood: if \delta \leq \varepsilon < 1/8, then B_\delta(\sigma) \subseteq B_\varepsilon(\sigma).

Proof: Both the \sin(\pi\delta) \leq \sin(\pi\varepsilon) bound and \delta \leq \varepsilon are monotone.

🔗theorem
CategoryTheory.Triangulated.basisNhd_mono.{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δε : δ ≤ ε) (hε8 : ε < 1 / 8) :
  CategoryTheory.Triangulated.basisNhd C σ δ ⊆
    CategoryTheory.Triangulated.basisNhd C σ ε
CategoryTheory.Triangulated.basisNhd_mono.{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δε : δ ≤ ε)
  (hε8 : ε < 1 / 8) :
  CategoryTheory.Triangulated.basisNhd C σ
      δ ⊆
    CategoryTheory.Triangulated.basisNhd C
      σ ε

Something wrong, better idea? Suggest a change

13.3.18. exists_basisNhd_subset_basisNhd🔗

If \tau \in B_\varepsilon(\sigma), then some smaller basis neighborhood of \tau is contained in B_\varepsilon(\sigma). This is the local basis-refinement step.

Proof: Chooses \delta small enough that K \cdot \sin(\pi\delta) absorbs the gap in both the seminorm and slicing distance bounds, using the local domination constant and the triangle inequality.

🔗theorem
CategoryTheory.Triangulated.exists_basisNhd_subset_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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {ε : ℝ} (hε : 0 < ε) (hε8 : ε < 1 / 8)
  (hτ : τ ∈ CategoryTheory.Triangulated.basisNhd C σ ε) :
  ∃ δ,
    0 < δ ∧
      δ < 1 / 8 ∧
        CategoryTheory.Triangulated.basisNhd C τ δ ⊆
          CategoryTheory.Triangulated.basisNhd C σ ε
CategoryTheory.Triangulated.exists_basisNhd_subset_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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {ε : ℝ} (hε : 0 < ε) (hε8 : ε < 1 / 8)
  (hτ :
    τ ∈
      CategoryTheory.Triangulated.basisNhd
        C σ ε) :
  ∃ δ,
    0 < δ ∧
      δ < 1 / 8 ∧
        CategoryTheory.Triangulated.basisNhd
            C τ δ ⊆
          CategoryTheory.Triangulated.basisNhd
            C σ ε

Something wrong, better idea? Suggest a change

13.3.19. eq_of_same_Z_near🔗

[Lemma 6.4]

Lemma 6.4 consequence: two stability conditions with the same central charge and d(\mathcal{P}, \mathcal{Q}) < 1 are equal.

Proof: Applies bridgeland_lemma_6_4 to conclude \mathcal{P} = \mathcal{Q}, then uses extensionality with Z_\sigma = Z_\tau.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.eq_of_same_Z_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)
  (hZ : σ.Z = τ.Z)
  (hd :
    CategoryTheory.Triangulated.slicingDist C σ.slicing τ.slicing <
      ENNReal.ofReal 1) :
  σ = τ
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.eq_of_same_Z_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)
  (hZ : σ.Z = τ.Z)
  (hd :
    CategoryTheory.Triangulated.slicingDist
        C σ.slicing τ.slicing <
      ENNReal.ofReal 1) :
  σ = τ

Something wrong, better idea? Suggest a change

13.3.20. eq_of_same_Z_of_mem_basisNhd🔗

Two stability conditions in the same B_\varepsilon(\sigma) with the same central charge are equal.

Proof: Triangle inequality on slicing distances gives d(\mathcal{P}_1, \mathcal{P}_2) < 2\varepsilon < 1, then applies eq_of_same_Z_near.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.eq_of_same_Z_of_mem_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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {ε : ℝ} (hε : 0 < ε) (hε8 : ε < 1 / 8)
  {τ₁ τ₂ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v}
  (hτ₁ : τ₁ ∈ CategoryTheory.Triangulated.basisNhd C σ ε)
  (hτ₂ : τ₂ ∈ CategoryTheory.Triangulated.basisNhd C σ ε)
  (hZ : τ₁.Z = τ₂.Z) : τ₁ = τ₂
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.eq_of_same_Z_of_mem_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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {ε : ℝ} (hε : 0 < ε) (hε8 : ε < 1 / 8)
  {τ₁ τ₂ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v}
  (hτ₁ :
    τ₁ ∈
      CategoryTheory.Triangulated.basisNhd
        C σ ε)
  (hτ₂ :
    τ₂ ∈
      CategoryTheory.Triangulated.basisNhd
        C σ ε)
  (hZ : τ₁.Z = τ₂.Z) : τ₁ = τ₂

Something wrong, better idea? Suggest a change

13.3.21. basisNhd_subset_connectedComponent_small🔗

A small Bridgeland basis neighborhood (with radius below the local Theorem 7.1 witness) lies inside the connected component of its center. This is the direct straight-line interpolation argument from Bridgeland Section 7.

Proof: Constructs a continuous path \gamma \colon [0, 1] \to \operatorname{Stab} from \sigma to \tau by lifting the straight-line charge interpolation Z_t = (1-t) Z(\sigma) + t Z(\tau) via repeated application of Theorem 7.1. Continuity of \gamma follows from the local lifting: for each t, nearby times lift to nearby stability conditions via the same deformation theorem. The path connects \sigma and \tau, placing them in the same path component.

🔗theorem
CategoryTheory.Triangulated.basisNhd_subset_connectedComponent_small.{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ε₀10 : ε₀ < 1 / 10)
  (hWide :
    CategoryTheory.Triangulated.WideSectorFiniteLength C σ ε₀ hε₀ ⋯)
  (hε : 0 < ε) (hεε₀ : ε < ε₀) :
  CategoryTheory.Triangulated.basisNhd C σ ε ⊆
    {τ | ConnectedComponents.mk τ = ConnectedComponents.mk σ}
CategoryTheory.Triangulated.basisNhd_subset_connectedComponent_small.{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ε₀10 : ε₀ < 1 / 10)
  (hWide :
    CategoryTheory.Triangulated.WideSectorFiniteLength
      C σ ε₀ hε₀ ⋯)
  (hε : 0 < ε) (hεε₀ : ε < ε₀) :
  CategoryTheory.Triangulated.basisNhd C σ
      ε ⊆
    {τ |
      ConnectedComponents.mk τ =
        ConnectedComponents.mk σ}

Something wrong, better idea? Suggest a change

13.3.22. exists_local_lift_sameComponent_in_basisNhd🔗

Local continuation along the straight-line charge interpolation. Starting from a lifted point \rho_0 over time t, nearby times also admit lifts inside the same ambient basis neighborhood and in the same connected component as \rho_0.

Proof: Chooses \eta small enough that |s - t| < \eta implies the seminorm \|Z_s - Z(\rho_0)\|_{\rho_0} < \sin(\pi\delta) (using the scaling property of the seminorm), then applies Theorem 7.1 at \rho_0 and verifies the lifted point lies in both the ambient basis neighborhood (by monotonicity) and the correct connected component (by basisNhd_subset_connectedComponent_small).

🔗theorem
CategoryTheory.Triangulated.exists_local_lift_sameComponent_in_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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ ρ₀ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {ε t : ℝ} (hε : 0 < ε) (hε8 : ε < 1 / 8)
  (hτ : τ ∈ CategoryTheory.Triangulated.basisNhd C σ ε)
  (hρ₀mem : ρ₀ ∈ CategoryTheory.Triangulated.basisNhd C σ ε)
  (hρ₀Z :
    ρ₀.Z = CategoryTheory.Triangulated.linearInterpolationZ C σ τ t) :
  ∃ η,
    0 < η ∧
      ∀ ⦃s : ℝ⦄,
        |s - t| < η →
          ∃ ρ,
            ρ.Z =
                CategoryTheory.Triangulated.linearInterpolationZ C σ τ
                  s ∧
              ρ ∈ CategoryTheory.Triangulated.basisNhd C σ ε ∧
                ConnectedComponents.mk ρ = ConnectedComponents.mk ρ₀
CategoryTheory.Triangulated.exists_local_lift_sameComponent_in_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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ ρ₀ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {ε t : ℝ} (hε : 0 < ε) (hε8 : ε < 1 / 8)
  (hτ :
    τ ∈
      CategoryTheory.Triangulated.basisNhd
        C σ ε)
  (hρ₀mem :
    ρ₀ ∈
      CategoryTheory.Triangulated.basisNhd
        C σ ε)
  (hρ₀Z :
    ρ₀.Z =
      CategoryTheory.Triangulated.linearInterpolationZ
        C σ τ t) :
  ∃ η,
    0 < η ∧
      ∀ ⦃s : ℝ⦄,
        |s - t| < η →
          ∃ ρ,
            ρ.Z =
                CategoryTheory.Triangulated.linearInterpolationZ
                  C σ τ s ∧
              ρ ∈
                  CategoryTheory.Triangulated.basisNhd
                    C σ ε ∧
                ConnectedComponents.mk ρ =
                  ConnectedComponents.mk
                    ρ₀

Something wrong, better idea? Suggest a change