Bridgeland Stability Conditions

14.10. Deformation: IntervalAbelian🔗

14.10.1. im_Z_nonpos_of_heart_phases🔗

Im non-positivity for heart objects. If E is nonzero with \phi^+(E) \le \phi and \phi^-(E) > \phi - 1 (so all HN phases lie in (\phi - 1, \phi]), then \operatorname{Im}(Z(E) \cdot e^{-i\pi\phi}) \le 0.

Proof: Decompose Z(E) = \sum Z(F_j) via K_0. Each factor F_j has Z(F_j) = m_j e^{i\pi\phi_j} with \phi_j \in (\phi - 1, \phi], so \operatorname{Im}(Z(F_j) \cdot e^{-i\pi\phi}) = m_j \sin(\pi(\phi_j - \phi)) \le 0 since \sin \le 0 on (-\pi, 0].

🔗theorem
CategoryTheory.Triangulated.im_Z_nonpos_of_heart_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)
  {φ : ℝ} {E : C} (hE : ¬CategoryTheory.Limits.IsZero E)
  (hle :
    CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing E hE ≤ φ)
  (hgt :
    φ - 1 <
      CategoryTheory.Triangulated.Slicing.phiMinus C σ.slicing E hE) :
  (σ.charge E * Complex.exp (-(↑(Real.pi * φ) * Complex.I))).im ≤ 0
CategoryTheory.Triangulated.im_Z_nonpos_of_heart_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)
  {φ : ℝ} {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hle :
    CategoryTheory.Triangulated.Slicing.phiPlus
        C σ.slicing E hE ≤
      φ)
  (hgt :
    φ - 1 <
      CategoryTheory.Triangulated.Slicing.phiMinus
        C σ.slicing E hE) :
  (σ.charge E *
        Complex.exp
          (-(↑(Real.pi * φ) *
              Complex.I))).im ≤
    0

Something wrong, better idea? Suggest a change

14.10.2. P_phi_of_im_zero_heart🔗

From \operatorname{Im} = 0 to \mathcal{P}(\phi). If X is nonzero with all \sigma-phases in (\phi - 1, \phi] and \operatorname{Im}(Z(X) \cdot e^{-i\pi\phi}) = 0, then X \in \mathcal{P}(\phi).

Proof: Each HN factor contributes \le 0 to the imaginary sum, and the total is 0, so each contribution is 0. For nonzero factors, \sin(\pi(\psi - \phi)) = 0 with \psi \in (\phi - 1, \phi] forces \psi = \phi. Strict antitone of HN phases forces exactly one factor.

🔗theorem
CategoryTheory.Triangulated.P_phi_of_im_zero_heart.{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)
  {φ : ℝ} {X : C} (hXne : ¬CategoryTheory.Limits.IsZero X)
  (hX_le :
    CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing X hXne ≤ φ)
  (hX_gt :
    φ - 1 <
      CategoryTheory.Triangulated.Slicing.phiMinus C σ.slicing X hXne)
  (him_zero :
    (σ.charge X * Complex.exp (-(↑(Real.pi * φ) * Complex.I))).im = 0) :
  σ.slicing.P φ X
CategoryTheory.Triangulated.P_phi_of_im_zero_heart.{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)
  {φ : ℝ} {X : C}
  (hXne : ¬CategoryTheory.Limits.IsZero X)
  (hX_le :
    CategoryTheory.Triangulated.Slicing.phiPlus
        C σ.slicing X hXne ≤
      φ)
  (hX_gt :
    φ - 1 <
      CategoryTheory.Triangulated.Slicing.phiMinus
        C σ.slicing X hXne)
  (him_zero :
    (σ.charge X *
          Complex.exp
            (-(↑(Real.pi * φ) *
                Complex.I))).im =
      0) :
  σ.slicing.P φ X

Something wrong, better idea? Suggest a change

14.10.3. P_phi_of_heart_triangle🔗

If a distinguished triangle K \to E \to Q has E \in \mathcal{P}(\phi) and K, Q in the heart \mathcal{P}((\phi - 1, \phi]), then K, Q \in \mathcal{P}(\phi).

Proof: From Z(E) = Z(K) + Z(Q) and \operatorname{Im}(Z(E) \cdot e^{-i\pi\phi}) = 0 (since E \in \mathcal{P}(\phi)), combined with \operatorname{Im}(Z(K) \cdot e^{-i\pi\phi}) \le 0 and \operatorname{Im}(Z(Q) \cdot e^{-i\pi\phi}) \le 0, both imaginary parts must be zero. Apply P_phi_of_im_zero_heart.

🔗theorem
CategoryTheory.Triangulated.P_phi_of_heart_triangle.{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)
  {φ : ℝ} {K E Q : C} {f₁ : K ⟶ E} {f₂ : E ⟶ Q}
  {f₃ : Q ⟶ (CategoryTheory.shiftFunctor C 1).obj K}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hPφ : σ.slicing.P φ E) (hE : ¬CategoryTheory.Limits.IsZero E)
  (hKne : ¬CategoryTheory.Limits.IsZero K)
  (hK_le :
    CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing K hKne ≤ φ)
  (hK_gt :
    φ - 1 <
      CategoryTheory.Triangulated.Slicing.phiMinus C σ.slicing K hKne)
  (hQne : ¬CategoryTheory.Limits.IsZero Q)
  (hQ_le :
    CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing Q hQne ≤ φ)
  (hQ_gt :
    φ - 1 <
      CategoryTheory.Triangulated.Slicing.phiMinus C σ.slicing Q hQne) :
  σ.slicing.P φ K ∧ σ.slicing.P φ Q
CategoryTheory.Triangulated.P_phi_of_heart_triangle.{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)
  {φ : ℝ} {K E Q : C} {f₁ : K ⟶ E}
  {f₂ : E ⟶ Q}
  {f₃ :
    Q ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        K}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hPφ : σ.slicing.P φ E)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hKne : ¬CategoryTheory.Limits.IsZero K)
  (hK_le :
    CategoryTheory.Triangulated.Slicing.phiPlus
        C σ.slicing K hKne ≤
      φ)
  (hK_gt :
    φ - 1 <
      CategoryTheory.Triangulated.Slicing.phiMinus
        C σ.slicing K hKne)
  (hQne : ¬CategoryTheory.Limits.IsZero Q)
  (hQ_le :
    CategoryTheory.Triangulated.Slicing.phiPlus
        C σ.slicing Q hQne ≤
      φ)
  (hQ_gt :
    φ - 1 <
      CategoryTheory.Triangulated.Slicing.phiMinus
        C σ.slicing Q hQne) :
  σ.slicing.P φ K ∧ σ.slicing.P φ Q

Something wrong, better idea? Suggest a change

14.10.4. im_Z_nonneg_of_phases_above🔗

If E is a nonzero object with all \sigma-phases in [\phi, \phi+1), then \mathrm{Im}(Z([E]) \cdot e^{-i\pi\phi}) \geq 0.

Proof: Decompose E via its HN filtration with phases \phi_i \in [\phi, \phi+1); write Z([F_i]) = m_i e^{i\pi\phi_i} with m_i > 0. Each summand contributes m_i \sin(\pi(\phi_i - \phi)) \geq 0 since \phi_i - \phi \in [0,1), so the sum is nonneg.

🔗theorem
CategoryTheory.Triangulated.im_Z_nonneg_of_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)
  {φ : ℝ} {E : C} (hE : ¬CategoryTheory.Limits.IsZero E)
  (hge :
    φ ≤ CategoryTheory.Triangulated.Slicing.phiMinus C σ.slicing E hE)
  (hlt :
    CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing E hE <
      φ + 1) :
  0 ≤ (σ.charge E * Complex.exp (-(↑(Real.pi * φ) * Complex.I))).im
CategoryTheory.Triangulated.im_Z_nonneg_of_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)
  {φ : ℝ} {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hge :
    φ ≤
      CategoryTheory.Triangulated.Slicing.phiMinus
        C σ.slicing E hE)
  (hlt :
    CategoryTheory.Triangulated.Slicing.phiPlus
        C σ.slicing E hE <
      φ + 1) :
  0 ≤
    (σ.charge E *
        Complex.exp
          (-(↑(Real.pi * φ) *
              Complex.I))).im

Something wrong, better idea? Suggest a change

14.10.5. P_phi_of_im_zero_above🔗

If X is a nonzero object with all \sigma-phases in [\phi, \phi+1) and \mathrm{Im}(Z([X]) \cdot e^{-i\pi\phi}) = 0, then X \in \mathcal{P}(\phi).

Proof: Decompose X via its HN filtration; each factor F_i has phase \phi_i \in [\phi, \phi+1), so Z([F_i]) = m_i e^{i\pi\phi_i} and the imaginary part contribution m_i \sin(\pi(\phi_i - \phi)) \geq 0. Since the sum of nonneg terms vanishes, each is zero, forcing \sin(\pi(\phi_i - \phi)) = 0, i.e., \phi_i = \phi.

🔗theorem
CategoryTheory.Triangulated.P_phi_of_im_zero_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)
  {φ : ℝ} {X : C} (hXne : ¬CategoryTheory.Limits.IsZero X)
  (hX_ge :
    φ ≤ CategoryTheory.Triangulated.Slicing.phiMinus C σ.slicing X hXne)
  (hX_lt :
    CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing X hXne <
      φ + 1)
  (him_zero :
    (σ.charge X * Complex.exp (-(↑(Real.pi * φ) * Complex.I))).im = 0) :
  σ.slicing.P φ X
CategoryTheory.Triangulated.P_phi_of_im_zero_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)
  {φ : ℝ} {X : C}
  (hXne : ¬CategoryTheory.Limits.IsZero X)
  (hX_ge :
    φ ≤
      CategoryTheory.Triangulated.Slicing.phiMinus
        C σ.slicing X hXne)
  (hX_lt :
    CategoryTheory.Triangulated.Slicing.phiPlus
        C σ.slicing X hXne <
      φ + 1)
  (him_zero :
    (σ.charge X *
          Complex.exp
            (-(↑(Real.pi * φ) *
                Complex.I))).im =
      0) :
  σ.slicing.P φ X

Something wrong, better idea? Suggest a change

14.10.6. P_phi_biprod🔗

\mathcal{P}(\phi) is closed under binary biproducts.

Proof: The biproduct triangle is distinguished; both factors in \mathcal{P}(\phi) means the biproduct has all phases equal to \phi.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.P_phi_biprod.{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)
  {φ : ℝ} {X Y : C} (hX : σ.slicing.P φ X) (hY : σ.slicing.P φ Y) :
  σ.slicing.P φ (X ⊞ Y)
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.P_phi_biprod.{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)
  {φ : ℝ} {X Y : C} (hX : σ.slicing.P φ X)
  (hY : σ.slicing.P φ Y) :
  σ.slicing.P φ (X ⊞ Y)

Something wrong, better idea? Suggest a change

14.10.7. P_phi_closedUnderBinaryProducts🔗

\mathcal{P}(\phi) is closed under binary products.

Proof: Follows from closure under biproducts.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.P_phi_closedUnderBinaryProducts.{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)
  (φ : ℝ) : (σ.slicing.P φ).IsClosedUnderBinaryProducts
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.P_phi_closedUnderBinaryProducts.{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)
  (φ : ℝ) :
  (σ.slicing.P
      φ).IsClosedUnderBinaryProducts

Something wrong, better idea? Suggest a change

14.10.8. P_phi_closedUnderFiniteProducts🔗

\mathcal{P}(\phi) is closed under finite products.

Proof: Induction from binary products and the zero object.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.P_phi_closedUnderFiniteProducts.{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)
  (φ : ℝ) : (σ.slicing.P φ).IsClosedUnderFiniteProducts
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.P_phi_closedUnderFiniteProducts.{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)
  (φ : ℝ) :
  (σ.slicing.P
      φ).IsClosedUnderFiniteProducts

Something wrong, better idea? Suggest a change

14.10.9. P_phi_hasFiniteProducts🔗

For any stability condition \sigma and phase \phi \in \mathbb{R}, the full subcategory \mathcal{P}(\phi) has finite products.

Construction: Constructs the HasFiniteProducts instance on \mathcal{P}(\phi) from the existing binary products and terminal object instances, via hasFiniteProducts_of_has_binary_and_terminal.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.P_phi_hasFiniteProducts.{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.Limits.HasFiniteProducts
    (σ.slicing.P φ).FullSubcategory
CategoryTheory.Triangulated.StabilityCondition.P_phi_hasFiniteProducts.{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.Limits.HasFiniteProducts
    (σ.slicing.P φ).FullSubcategory

Something wrong, better idea? Suggest a change

14.10.10. P_phi_hom_vanishing🔗

Negative-degree Hom vanishing in \mathcal{P}(\varphi). For X, Y \in \mathcal{P}(\varphi) and n < 0, every morphism \iota(X) \to \iota(Y)\llbracket n \rrbracket is zero.

Proof: The shift axiom gives Y\llbracket n \rrbracket \in \mathcal{P}(\varphi + n). Since n < 0, we have \varphi > \varphi + n, so the slicing's Hom-vanishing axiom applies directly.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.P_phi_hom_vanishing.{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)
  (φ : ℝ) ⦃X Y : (σ.slicing.P φ).FullSubcategory⦄ ⦃n : ℤ⦄
  (f :
    (σ.slicing.P φ).ι.obj X ⟶
      (CategoryTheory.shiftFunctor C n).obj ((σ.slicing.P φ).ι.obj Y)) :
  n < 0 → f = 0
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.P_phi_hom_vanishing.{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)
  (φ : ℝ)
  ⦃X Y : (σ.slicing.P φ).FullSubcategory⦄
  ⦃n : ℤ⦄
  (f :
    (σ.slicing.P φ).ι.obj X ⟶
      (CategoryTheory.shiftFunctor C
            n).obj
        ((σ.slicing.P φ).ι.obj Y)) :
  n < 0 → f = 0

Something wrong, better idea? Suggest a change

14.10.11. P_phi_of_truncation_of_P_phi_cone🔗

Given a distinguished triangle A \to B \to X_3 \to A[1] with A, B \in \mathcal{P}(\phi), both t-structure truncations of X_3 (with respect to the heart \mathcal{P}((\phi-1,\phi])) lie in \mathcal{P}(\phi).

Proof: From A, B \in \mathcal{P}(\phi) one gets \mathrm{Im}(Z([X_3]) \cdot e^{-i\pi\phi}) = 0 by K_0-additivity. The truncation triangle decomposes this into the heart piece Q (with \mathrm{Im} \leq 0) and the co-heart piece L shifted (with \mathrm{Im} \geq 0); since they sum to zero, both imaginary parts vanish, and P_phi_of_im_zero_heart resp. P_phi_of_im_zero_above promote each to \mathcal{P}(\phi).

🔗theorem
CategoryTheory.Triangulated.P_phi_of_truncation_of_P_phi_cone.{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)
  (φ : ℝ) {A B X₃ : C} (hA : σ.slicing.P φ A) (hB : σ.slicing.P φ B)
  {f₁ : A ⟶ B} {f₂ : B ⟶ X₃}
  {f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj A}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  have t :=
    CategoryTheory.Triangulated.Slicing.toTStructure C
      (CategoryTheory.Triangulated.Slicing.phaseShift C σ.slicing
        (φ - 1));
  σ.slicing.P φ ((t.truncGE 0).obj X₃) ∧
    σ.slicing.P φ
      ((CategoryTheory.shiftFunctor C (-1)).obj ((t.truncLT 0).obj X₃))
CategoryTheory.Triangulated.P_phi_of_truncation_of_P_phi_cone.{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)
  (φ : ℝ) {A B X₃ : C}
  (hA : σ.slicing.P φ A)
  (hB : σ.slicing.P φ B) {f₁ : A ⟶ B}
  {f₂ : B ⟶ X₃}
  {f₃ :
    X₃ ⟶
      (CategoryTheory.shiftFunctor C
            1).obj
        A}
  (hT :
    CategoryTheory.Pretriangulated.Triangle.mk
        f₁ f₂ f₃ ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles) :
  have t :=
    CategoryTheory.Triangulated.Slicing.toTStructure
      C
      (CategoryTheory.Triangulated.Slicing.phaseShift
        C σ.slicing (φ - 1));
  σ.slicing.P φ ((t.truncGE 0).obj X₃) ∧
    σ.slicing.P φ
      ((CategoryTheory.shiftFunctor C
            (-1)).obj
        ((t.truncLT 0).obj X₃))

Something wrong, better idea? Suggest a change

14.10.12. P_phi_admissible🔗

\mathcal{P}(\phi) is admissible in the heart \mathcal{P}((\phi - 1, \phi]): it is closed under subobjects, quotients, and extensions in the heart.

Proof: For subobjects/quotients: a short exact sequence 0 \to K \to E \to Q \to 0 in the heart with E \in \mathcal{P}(\phi) gives Z(E) = Z(K) + Z(Q). The imaginary-part argument forces both K, Q \in \mathcal{P}(\phi). Extension closure is similar.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.P_phi_admissible.{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)
  (φ : ℝ) :
  have _t :=
    CategoryTheory.Triangulated.Slicing.toTStructure C
      (CategoryTheory.Triangulated.Slicing.phaseShift C σ.slicing
        (φ - 1));
  CategoryTheory.Triangulated.AbelianSubcategory.admissibleMorphism
      (σ.slicing.P φ).ι =
    ⊤
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.P_phi_admissible.{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)
  (φ : ℝ) :
  have _t :=
    CategoryTheory.Triangulated.Slicing.toTStructure
      C
      (CategoryTheory.Triangulated.Slicing.phaseShift
        C σ.slicing (φ - 1));
  CategoryTheory.Triangulated.AbelianSubcategory.admissibleMorphism
      (σ.slicing.P φ).ι =
    ⊤

Something wrong, better idea? Suggest a change

14.10.13. P_phi_abelian🔗

[Lemma 5.2]

Bridgeland's Lemma 5.2. Each \mathcal{P}(\phi) is an abelian category.

Construction: Defined as the abelian subcategory structure obtained from \mathcal{P}(\phi) being admissible in the abelian heart \mathcal{P}((\phi - 1, \phi]).

🔗def
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.P_phi_abelian.{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.Abelian (σ.slicing.P φ).FullSubcategory
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.P_phi_abelian.{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.Abelian
    (σ.slicing.P φ).FullSubcategory

Something wrong, better idea? Suggest a change