Bridgeland Stability Conditions

13.7. StabilityCondition: Topology🔗

13.7.1. im_divided_of_semistable🔗

For a \sigma-semistable nonzero object F of phase \psi, the imaginary part of Z(F) \cdot e^{-i\pi\phi} equals b \cdot \sin(\pi(\psi - \phi)) for some b > 0. This factors out the repeated divide-by-exponential-and-rewrite-to-sine computation used throughout the Lemma 6.4 proofs.

Proof: Obtains the ray decomposition Z([F]) = b \cdot e^{i\pi\psi} from compatibility, then applies im_ofReal_mul_exp_mul_exp_neg.

🔗theorem
CategoryTheory.Triangulated.im_divided_of_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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {F : C} {ψ φ : ℝ} (hne : ¬CategoryTheory.Limits.IsZero F)
  (hss : σ.slicing.P ψ F) :
  ∃ b,
    0 < b ∧
      (σ.charge F * Complex.exp (-(↑(Real.pi * φ) * Complex.I))).im =
        b * Real.sin (Real.pi * (ψ - φ))
CategoryTheory.Triangulated.im_divided_of_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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {F : C} {ψ φ : ℝ}
  (hne : ¬CategoryTheory.Limits.IsZero F)
  (hss : σ.slicing.P ψ F) :
  ∃ b,
    0 < b ∧
      (σ.charge F *
            Complex.exp
              (-(↑(Real.pi * φ) *
                  Complex.I))).im =
        b * Real.sin (Real.pi * (ψ - φ))

Something wrong, better idea? Suggest a change

13.7.2. false_of_all_hn_phases_below🔗

One-sided phase impossibility (below). If \sigma and \tau have the same central charge, E is nonzero and \tau-semistable of phase \phi, and all nonzero factors in a \sigma-HN filtration of E have phase strictly below \phi (and above \phi - 1), then we reach a contradiction. This is the core imaginary-part argument underlying Lemma 6.4.

Proof: Decomposes Z(E) = \sum Z(F_i) via K_0 additivity, divides by e^{i\pi\phi}, and shows the imaginary part is both zero (since Z(E) lies on the ray at angle \pi\phi) and strictly negative (each nonzero factor contributes b_i \sin(\pi(\theta_i - \phi)) < 0).

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.false_of_all_hn_phases_below.{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) {E : C} {φ : ℝ}
  (hE : ¬CategoryTheory.Limits.IsZero E) (hτ : τ.slicing.P φ E)
  (F : CategoryTheory.Triangulated.HNFiltration C σ.slicing.P E)
  (hlt :
    ∀ (i : Fin F.n),
      ¬CategoryTheory.Limits.IsZero (F.factor i) → F.φ i < φ)
  (hgt :
    ∀ (i : Fin F.n),
      ¬CategoryTheory.Limits.IsZero (F.factor i) → φ - 1 < F.φ i) :
  False
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.false_of_all_hn_phases_below.{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) {E : C} {φ : ℝ}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hτ : τ.slicing.P φ E)
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C σ.slicing.P E)
  (hlt :
    ∀ (i : Fin F.n),
      ¬CategoryTheory.Limits.IsZero
            (F.factor i) →
        F.φ i < φ)
  (hgt :
    ∀ (i : Fin F.n),
      ¬CategoryTheory.Limits.IsZero
            (F.factor i) →
        φ - 1 < F.φ i) :
  False

Something wrong, better idea? Suggest a change

13.7.3. false_of_all_hn_phases_above🔗

One-sided phase impossibility (above). Symmetric version: all nonzero HN factors have phase strictly above \phi (and below \phi + 1) leads to contradiction.

Proof: Identical structure to the below case: each divided term has strictly positive imaginary part via \sin(\pi(\theta_i - \phi)) > 0, contradicting the real LHS.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.false_of_all_hn_phases_above.{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) {E : C} {φ : ℝ}
  (hE : ¬CategoryTheory.Limits.IsZero E) (hτ : τ.slicing.P φ E)
  (F : CategoryTheory.Triangulated.HNFiltration C σ.slicing.P E)
  (hgt :
    ∀ (i : Fin F.n),
      ¬CategoryTheory.Limits.IsZero (F.factor i) → φ < F.φ i)
  (hlt :
    ∀ (i : Fin F.n),
      ¬CategoryTheory.Limits.IsZero (F.factor i) → F.φ i < φ + 1) :
  False
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.false_of_all_hn_phases_above.{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) {E : C} {φ : ℝ}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hτ : τ.slicing.P φ E)
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C σ.slicing.P E)
  (hgt :
    ∀ (i : Fin F.n),
      ¬CategoryTheory.Limits.IsZero
            (F.factor i) →
        φ < F.φ i)
  (hlt :
    ∀ (i : Fin F.n),
      ¬CategoryTheory.Limits.IsZero
            (F.factor i) →
        F.φ i < φ + 1) :
  False

Something wrong, better idea? Suggest a change

13.7.4. P_of_Q_of_P_semistable🔗

Lemma 6.4 for \mathcal{P}-semistable objects. If \sigma.Z = \tau.Z, d(\mathcal{P}, \mathcal{Q}) < 1, E is nonzero and \tau-semistable at \phi, and E is also \sigma-semistable at some phase c, then c = \phi and E \in \mathcal{P}(\phi).

Proof: Combines the metric phase bound |c - \phi| < 2 with phase_eq_of_same_Z to force c = \phi.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.P_of_Q_of_P_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] [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)
  {E : C} {φ c : ℝ} (hE : ¬CategoryTheory.Limits.IsZero E)
  (hτ : τ.slicing.P φ E) (hσ : σ.slicing.P c E) : σ.slicing.P φ E
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.P_of_Q_of_P_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]
  [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)
  {E : C} {φ c : ℝ}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hτ : τ.slicing.P φ E)
  (hσ : σ.slicing.P c E) : σ.slicing.P φ E

Something wrong, better idea? Suggest a change

13.7.5. phiMinus_le_le_phiPlus🔗

Phase straddling for Lemma 6.4. If \sigma.Z = \tau.Z, d(\mathcal{P}, \mathcal{Q}) < 1, and E is nonzero \tau-semistable at \phi, then \phi^-_\sigma(E) \leq \phi \leq \phi^+_\sigma(E). This pins \phi between the extreme \sigma-HN phases of E.

Proof: Each direction proceeds by contradiction: if \phi < \phi^-, all HN phases are above \phi, contradicting false_of_all_hn_phases_above; if \phi^+ < \phi, all are below, contradicting false_of_all_hn_phases_below.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.phiMinus_le_le_phiPlus.{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)
  {E : C} {φ : ℝ} (hE : ¬CategoryTheory.Limits.IsZero E)
  (hτ : τ.slicing.P φ E) :
  CategoryTheory.Triangulated.Slicing.phiMinus C σ.slicing E hE ≤ φ ∧
    φ ≤ CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing E hE
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.phiMinus_le_le_phiPlus.{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)
  {E : C} {φ : ℝ}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hτ : τ.slicing.P φ E) :
  CategoryTheory.Triangulated.Slicing.phiMinus
        C σ.slicing E hE ≤
      φ ∧
    φ ≤
      CategoryTheory.Triangulated.Slicing.phiPlus
        C σ.slicing E hE

Something wrong, better idea? Suggest a change

13.7.6. false_of_gt_and_le_phases🔗

Cross-slicing imaginary part contradiction. If \sigma.Z = \tau.Z, X is nonzero, all \sigma-HN phases of X lie in (\phi, \phi + 1), and all \tau-HN phases lie in (\phi - 1, \phi], then \mathsf{False}. From the \sigma-decomposition, \operatorname{Im}(Z(X)/e^{i\pi\phi}) > 0; from the \tau-decomposition, \operatorname{Im}(Z(X)/e^{i\pi\phi}) \leq 0.

Proof: Decomposes Z(X) via both \sigma- and \tau-HN filtrations and shows the imaginary part of Z(X) \cdot e^{-i\pi\phi} is simultaneously strictly positive (from the \sigma-sum) and nonpositive (from the \tau-sum).

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.false_of_gt_and_le_phases.{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) {X : C} {φ : ℝ}
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (Fσ : CategoryTheory.Triangulated.HNFiltration C σ.slicing.P X)
  (hσgt : ∀ (i : Fin Fσ.n), φ < Fσ.φ i)
  (hσlt : ∀ (i : Fin Fσ.n), Fσ.φ i < φ + 1)
  (Fτ : CategoryTheory.Triangulated.HNFiltration C τ.slicing.P X)
  (hτle : ∀ (i : Fin Fτ.n), Fτ.φ i ≤ φ)
  (hτgt : ∀ (i : Fin Fτ.n), φ - 1 < Fτ.φ i) : False
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.false_of_gt_and_le_phases.{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) {X : C} {φ : ℝ}
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (Fσ :
    CategoryTheory.Triangulated.HNFiltration
      C σ.slicing.P X)
  (hσgt : ∀ (i : Fin Fσ.n), φ < Fσ.φ i)
  (hσlt :
    ∀ (i : Fin Fσ.n), Fσ.φ i < φ + 1)
  (Fτ :
    CategoryTheory.Triangulated.HNFiltration
      C τ.slicing.P X)
  (hτle : ∀ (i : Fin Fτ.n), Fτ.φ i ≤ φ)
  (hτgt :
    ∀ (i : Fin Fτ.n), φ - 1 < Fτ.φ i) :
  False

Something wrong, better idea? Suggest a change

13.7.7. false_of_hn_phases_le_with_lt🔗

One-sided phase impossibility (below with equality). If all \sigma-HN phases are \leq \phi with at least one nonzero factor strictly below \phi, and E is \tau-semistable at \phi with the same central charge, then \mathsf{False}.

Proof: The terms with phase = \phi contribute zero imaginary part; the term with phase < \phi contributes strictly negative imaginary part. The sum is strictly negative, contradicting the real LHS.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.false_of_hn_phases_le_with_lt.{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) {E : C} {φ : ℝ}
  (hE : ¬CategoryTheory.Limits.IsZero E) (hτ : τ.slicing.P φ E)
  (F : CategoryTheory.Triangulated.HNFiltration C σ.slicing.P E)
  (hle : ∀ (i : Fin F.n), F.φ i ≤ φ)
  (hgt : ∀ (i : Fin F.n), φ - 1 < F.φ i)
  (hstrict :
    ∃ i, ¬CategoryTheory.Limits.IsZero (F.factor i) ∧ F.φ i < φ) :
  False
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.false_of_hn_phases_le_with_lt.{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) {E : C} {φ : ℝ}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hτ : τ.slicing.P φ E)
  (F :
    CategoryTheory.Triangulated.HNFiltration
      C σ.slicing.P E)
  (hle : ∀ (i : Fin F.n), F.φ i ≤ φ)
  (hgt : ∀ (i : Fin F.n), φ - 1 < F.φ i)
  (hstrict :
    ∃ i,
      ¬CategoryTheory.Limits.IsZero
            (F.factor i) ∧
        F.φ i < φ) :
  False

Something wrong, better idea? Suggest a change

13.7.8. gt_phases_of_gtProp🔗

For a nonzero object with \mathcal{P}(>\phi) property, the intrinsic minimum HN phase satisfies \phi^-(X) > \phi.

Proof: Uses the characterization of \mathcal{P}(>\phi) in terms of a filtration whose minimum phase exceeds \phi, then compares with the canonical HN filtration.

🔗theorem
CategoryTheory.Triangulated.gt_phases_of_gtProp.{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) {X : C} {φ : ℝ}
  (hXne : ¬CategoryTheory.Limits.IsZero X)
  (hXgt : CategoryTheory.Triangulated.Slicing.gtProp C s φ X) :
  φ < CategoryTheory.Triangulated.Slicing.phiMinus C s X hXne
CategoryTheory.Triangulated.gt_phases_of_gtProp.{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)
  {X : C} {φ : ℝ}
  (hXne : ¬CategoryTheory.Limits.IsZero X)
  (hXgt :
    CategoryTheory.Triangulated.Slicing.gtProp
      C s φ X) :
  φ <
    CategoryTheory.Triangulated.Slicing.phiMinus
      C s X hXne

Something wrong, better idea? Suggest a change

13.7.9. phiPlus_le_of_leProp🔗

For a nonzero object with \mathcal{P}(\leq \phi) property, the intrinsic maximum HN phase satisfies \phi^+(Y) \leq \phi.

Proof: Dual to gt_phases_of_gtProp, using the \phi^+ characterization.

🔗theorem
CategoryTheory.Triangulated.phiPlus_le_of_leProp.{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) {Y : C} {φ : ℝ}
  (hYne : ¬CategoryTheory.Limits.IsZero Y)
  (hYle : CategoryTheory.Triangulated.Slicing.leProp C s φ Y) :
  CategoryTheory.Triangulated.Slicing.phiPlus C s Y hYne ≤ φ
CategoryTheory.Triangulated.phiPlus_le_of_leProp.{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)
  {Y : C} {φ : ℝ}
  (hYne : ¬CategoryTheory.Limits.IsZero Y)
  (hYle :
    CategoryTheory.Triangulated.Slicing.leProp
      C s φ Y) :
  CategoryTheory.Triangulated.Slicing.phiPlus
      C s Y hYne ≤
    φ

Something wrong, better idea? Suggest a change

13.7.10. bridgeland_lemma_6_4🔗

Bridgeland's Lemma 6.4. If two stability conditions \sigma and \tau have the same central charge and d(\mathcal{P}, \mathcal{Q}) < 1, then their slicings agree on all phases: \mathcal{P}(\phi) = \mathcal{Q}(\phi) for all \phi \in \mathbb{R}. In particular, the central charge map \sigma \mapsto Z(\sigma) is locally injective on \operatorname{Stab}(\mathcal{D}).

Proof: The biconditional is proved by applying the one-direction argument (bridgeland_6_4_one_dir) twice. The one-direction proof for E \in \mathcal{Q}(\phi) \Rightarrow E \in \mathcal{P}(\phi) proceeds in four steps: (1) split E at the cutoff \phi using \sigma's t-structure; (2) show \tau.\phi^+(X) \leq \phi by hom-vanishing; (3) conclude X = 0 via the cross-slicing imaginary part argument; (4) transfer semistability from Y \cong E using the imaginary part argument to force all phases equal to \phi.

🔗theorem
CategoryTheory.Triangulated.bridgeland_lemma_6_4.{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)
  (φ : ℝ) (E : C) : σ.slicing.P φ E ↔ τ.slicing.P φ E
CategoryTheory.Triangulated.bridgeland_lemma_6_4.{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)
  (φ : ℝ) (E : C) :
  σ.slicing.P φ E ↔ τ.slicing.P φ E

  1. Split E via σ's t-structure at φ: X → E → Y → X⟦1⟧ with X ∈ P(>φ) and Y ∈ P(≤φ), all σ-phases in (φ-1, φ+1).

  2. Show τ.phiPlus(X) ≤ φ by contradiction: if τ's top factor U of X had phase > φ, then Hom(U, E) = 0 (τ-hom-vanishing) forces U → X to factor through Y⟦-1⟧, but Hom(U, Y⟦-1⟧) = 0 too, giving U → X = 0, contradicting U ≠ 0.

  3. Now X has σ-phases > φ and τ-phases ≤ φ: the cross-slicing imaginary part argument (false_of_gt_and_le_phases) gives X = 0.

  4. So E ≅ Y has all σ-phases ≤ φ. The imaginary part argument then forces all phases = φ, making E σ-semistable at φ.

Something wrong, better idea? Suggest a change