8.4. StabilityFunction: Uniqueness🔗

8.4.1. hn_unique🔗

Proposition 2.3 (Bridgeland). HN filtrations are essentially unique: when all objects have finite subobject lattices, any two HN filtrations of the same nonzero object have the same number of semistable factors.

Proof: Induction on |\operatorname{Sub}(E)|. If E is semistable, both filtrations have n = 1 (by hn_n_eq_one_of_semistable). Otherwise, both have n \ge 2, and the semistable descent lemma forces \operatorname{chain}(1) = M for the unique maximally destabilizing subobject M. Quotienting by M gives tail filtrations on E/M with strictly fewer subobjects, and the inductive hypothesis yields n_1 - 1 = n_2 - 1.

theorem

CategoryTheory.StabilityFunction.hn_unique.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub : ∀ (E : A), Finite (CategoryTheory.Subobject E))
  (F₁ F₂ : CategoryTheory.AbelianHNFiltration Z E) : F₁.n = F₂.n
CategoryTheory.StabilityFunction.hn_unique.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub :
    ∀ (E : A),
      Finite (CategoryTheory.Subobject E))
  (F₁ F₂ :
    CategoryTheory.AbelianHNFiltration Z
      E) :
  F₁.n = F₂.n

Something wrong, better idea? Suggest a change

8.4.2. hn_phiPlus_eq🔗

The highest phase \phi(0) of an HN filtration is independent of the filtration choice.

Proof: For semistable objects, n = 1 forces \phi(0) = \phi(E). For non-semistable objects, \phi(0) = \phi(\operatorname{chain}(1)) by chain_one_phase, and \operatorname{chain}(1) = M (the unique MDS) by chain_one_eq_MDS.

theorem

CategoryTheory.StabilityFunction.hn_phiPlus_eq.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub : ∀ (E : A), Finite (CategoryTheory.Subobject E))
  (F₁ F₂ : CategoryTheory.AbelianHNFiltration Z E) :
  F₁.φ ⟨0, ⋯⟩ = F₂.φ ⟨0, ⋯⟩
CategoryTheory.StabilityFunction.hn_phiPlus_eq.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub :
    ∀ (E : A),
      Finite (CategoryTheory.Subobject E))
  (F₁ F₂ :
    CategoryTheory.AbelianHNFiltration Z
      E) :
  F₁.φ ⟨0, ⋯⟩ = F₂.φ ⟨0, ⋯⟩

Something wrong, better idea? Suggest a change

8.4.3. hn_phiMinus_eq🔗

The lowest phase \phi(n-1) of an HN filtration is independent of the filtration choice.

Proof: Parallels hn_unique: induction on |\operatorname{Sub}(E)|. For semistable objects the result reduces to hn_phiPlus_eq. Otherwise, the tail filtrations on E/M have the same lowest phase by the inductive hypothesis, and tailHNFiltration_phiMinus transports this back to the original filtration.

theorem

CategoryTheory.StabilityFunction.hn_phiMinus_eq.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub : ∀ (E : A), Finite (CategoryTheory.Subobject E))
  (F₁ F₂ : CategoryTheory.AbelianHNFiltration Z E) :
  F₁.φ ⟨F₁.n - 1, ⋯⟩ = F₂.φ ⟨F₂.n - 1, ⋯⟩
CategoryTheory.StabilityFunction.hn_phiMinus_eq.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub :
    ∀ (E : A),
      Finite (CategoryTheory.Subobject E))
  (F₁ F₂ :
    CategoryTheory.AbelianHNFiltration Z
      E) :
  F₁.φ ⟨F₁.n - 1, ⋯⟩ = F₂.φ ⟨F₂.n - 1, ⋯⟩

Something wrong, better idea? Suggest a change

8.4.4. phiPlus🔗

The intrinsic highest phase \phi^+(E) of a nonzero object E: the phase of the maximally destabilizing subobject. Well-defined by hn_phiPlus_eq.

Construction: Defined as F.\phi(0) for an arbitrary HN filtration F obtained via Classical.choice.

def

CategoryTheory.StabilityFunction.phiPlus.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub : ∀ (E : A), Finite (CategoryTheory.Subobject E)) : ℝ
CategoryTheory.StabilityFunction.phiPlus.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub :
    ∀ (E : A),
      Finite
        (CategoryTheory.Subobject E)) :
  ℝ

Something wrong, better idea? Suggest a change

8.4.5. phiPlus_eq🔗

\phi^+(E) = F.\phi(0) for any HN filtration F of E.

Proof: Immediate from hn_phiPlus_eq.

theorem

CategoryTheory.StabilityFunction.phiPlus_eq.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub : ∀ (E : A), Finite (CategoryTheory.Subobject E))
  (F : CategoryTheory.AbelianHNFiltration Z E) :
  Z.phiPlus E hE hFinSub = F.φ ⟨0, ⋯⟩
CategoryTheory.StabilityFunction.phiPlus_eq.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub :
    ∀ (E : A),
      Finite (CategoryTheory.Subobject E))
  (F :
    CategoryTheory.AbelianHNFiltration Z
      E) :
  Z.phiPlus E hE hFinSub = F.φ ⟨0, ⋯⟩

Something wrong, better idea? Suggest a change

8.4.6. phiMinus🔗

The intrinsic lowest phase \phi^-(E) of a nonzero object E: the phase of the last HN factor. Well-defined by hn_phiMinus_eq.

Construction: Defined as F.\phi(n-1) for an arbitrary HN filtration F obtained via Classical.choice.

def

CategoryTheory.StabilityFunction.phiMinus.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub : ∀ (E : A), Finite (CategoryTheory.Subobject E)) : ℝ
CategoryTheory.StabilityFunction.phiMinus.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub :
    ∀ (E : A),
      Finite
        (CategoryTheory.Subobject E)) :
  ℝ

Something wrong, better idea? Suggest a change

8.4.7. phiMinus_eq🔗

\phi^-(E) = F.\phi(n-1) for any HN filtration F of E.

Proof: Immediate from hn_phiMinus_eq.

theorem

CategoryTheory.StabilityFunction.phiMinus_eq.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub : ∀ (E : A), Finite (CategoryTheory.Subobject E))
  (F : CategoryTheory.AbelianHNFiltration Z E) :
  Z.phiMinus E hE hFinSub = F.φ ⟨F.n - 1, ⋯⟩
CategoryTheory.StabilityFunction.phiMinus_eq.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub :
    ∀ (E : A),
      Finite (CategoryTheory.Subobject E))
  (F :
    CategoryTheory.AbelianHNFiltration Z
      E) :
  Z.phiMinus E hE hFinSub =
    F.φ ⟨F.n - 1, ⋯⟩

Something wrong, better idea? Suggest a change

8.4.8. phiMinus_le_phiPlus🔗

\phi^-(E) \le \phi^+(E) for nonzero objects.

Proof: Both values come from the same HN filtration's phase sequence, which is strictly anti-monotone. The last index n-1 \ge 0 gives \phi(n-1) \le \phi(0).

theorem

CategoryTheory.StabilityFunction.phiMinus_le_phiPlus.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub : ∀ (E : A), Finite (CategoryTheory.Subobject E)) :
  Z.phiMinus E hE hFinSub ≤ Z.phiPlus E hE hFinSub
CategoryTheory.StabilityFunction.phiMinus_le_phiPlus.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub :
    ∀ (E : A),
      Finite
        (CategoryTheory.Subobject E)) :
  Z.phiMinus E hE hFinSub ≤
    Z.phiPlus E hE hFinSub

Something wrong, better idea? Suggest a change

8.4.9. phiPlus_eq_phiMinus_of_semistable🔗

For semistable objects, \phi^+(E) = \phi^-(E) = \phi(E).

Proof: By hn_n_eq_one_of_semistable, the HN filtration has n = 1, so the only phase index is 0 = n - 1 and both \phi^+ and \phi^- equal \phi(E).

theorem

CategoryTheory.StabilityFunction.phiPlus_eq_phiMinus_of_semistable.{v,
    u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  (E : A) (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub : ∀ (E : A), Finite (CategoryTheory.Subobject E))
  (hss : Z.IsSemistable E) :
  Z.phiPlus E hE hFinSub = Z.phiMinus E hE hFinSub
CategoryTheory.StabilityFunction.phiPlus_eq_phiMinus_of_semistable.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hFinSub :
    ∀ (E : A),
      Finite (CategoryTheory.Subobject E))
  (hss : Z.IsSemistable E) :
  Z.phiPlus E hE hFinSub =
    Z.phiMinus E hE hFinSub

Something wrong, better idea? Suggest a change