Bridgeland Stability Conditions

8.1. StabilityFunction: Basic🔗

8.1.1. StabilityFunction🔗

[Definition 2.1]

A stability function on an abelian category \mathcal{A} is a group homomorphism Z \colon K_0(\mathcal{A}) \to \mathbb{C} (here modelled as an object-level map Z \colon \operatorname{Ob}(\mathcal{A}) \to \mathbb{C}) satisfying: (i) Z(E) = 0 whenever E is a zero object, (ii) Z(B) = Z(A) + Z(C) for every short exact sequence 0 \to A \to B \to C \to 0, and (iii) for every nonzero object E, Z(E) lies in the semi-closed upper half plane H \cup \mathbb{R}_{<0} = \{z \in \mathbb{C} \mid \operatorname{Im}(z) > 0\} \cup \{z \in \mathbb{C} \mid \operatorname{Im}(z) = 0,\; \operatorname{Re}(z) < 0\}. This is Definition 2.1 of Bridgeland (2007).

Construction: The structure carries an object-level function Zobj : A \to \mathbb{C} together with proofs of vanishing on zero objects, additivity on short exact sequences (encoded via ShortComplex.ShortExact), and the upper-half-plane membership condition for nonzero objects.

🔗structure
CategoryTheory.StabilityFunction.{v, u} (A : Type u)
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] : Type u
CategoryTheory.StabilityFunction.{v, u}
  (A : Type u)
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] : Type u

Constructor

CategoryTheory.StabilityFunction.mk.{v, u}

Fields

Zobj : A → ℂ

The central charge on objects.

map_zero' : ∀ (X : A), CategoryTheory.Limits.IsZero X → self.Zobj X = 0

The zero object maps to zero.

additive : ∀ (S : CategoryTheory.ShortComplex A), S.ShortExact → self.Zobj S.X₂ = self.Zobj S.X₁ + self.Zobj S.X₃

Additivity on short exact sequences: Z(B) = Z(A) + Z(C) for 0 → A → B → C → 0.

upper : ∀ (E : A), ¬CategoryTheory.Limits.IsZero E → self.Zobj E ∈ CategoryTheory.upperHalfPlaneUnion

Every nonzero object maps into the semi-closed upper half plane.

Something wrong, better idea? Suggest a change

8.1.2. phase🔗

The phase of an object E with respect to a stability function Z is \phi(E) = \frac{1}{\pi} \arg Z(E). When E is nonzero, Z(E) lies in H \cup \mathbb{R}_{<0}, so \arg Z(E) \in (0, \pi] and hence \phi(E) \in (0, 1]. For a zero object, the phase is 0.

Construction: Defined as (1 / Real.pi) * arg (Z.Zobj E), using the standard branch of the complex argument.

🔗def
CategoryTheory.StabilityFunction.phase.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) (E : A) : ℝ
CategoryTheory.StabilityFunction.phase.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (E : A) : ℝ

Something wrong, better idea? Suggest a change

8.1.3. phase_pos🔗

For a nonzero object E, the phase \phi(E) is strictly positive.

Proof: Since Z(E) \in H \cup \mathbb{R}_{<0}, we have \arg Z(E) > 0, so \phi(E) = \frac{1}{\pi} \arg Z(E) > 0.

🔗theorem
CategoryTheory.StabilityFunction.phase_pos.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E) : 0 < Z.phase E
CategoryTheory.StabilityFunction.phase_pos.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  0 < Z.phase E

Something wrong, better idea? Suggest a change

8.1.4. phase_le_one🔗

The phase of any object satisfies \phi(E) \le 1.

Proof: Since \arg(z) \le \pi for all z \in \mathbb{C}, dividing by \pi gives \phi(E) \le 1.

🔗theorem
CategoryTheory.StabilityFunction.phase_le_one.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) (E : A) : Z.phase E ≤ 1
CategoryTheory.StabilityFunction.phase_le_one.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (E : A) : Z.phase E ≤ 1

Something wrong, better idea? Suggest a change

8.1.5. phase_mem_Ioc🔗

For a nonzero object E, \phi(E) \in (0, 1].

Proof: Combines phase_pos and phase_le_one.

🔗theorem
CategoryTheory.StabilityFunction.phase_mem_Ioc.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E) : Z.phase E ∈ Set.Ioc 0 1
CategoryTheory.StabilityFunction.phase_mem_Ioc.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  Z.phase E ∈ Set.Ioc 0 1

Something wrong, better idea? Suggest a change

8.1.6. IsSemistable🔗

[Definition 2.2]

An object E of an abelian category is semistable with respect to a stability function Z if E is nonzero and for every nonzero subobject B \hookrightarrow E, \phi(B) \le \phi(E) (Bridgeland, Definition 2.2).

Construction: A conjunction of \neg \operatorname{IsZero} E and the universal bound on phases of nonzero subobjects in the Subobject E lattice.

🔗def
CategoryTheory.StabilityFunction.IsSemistable.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) (E : A) : Prop
CategoryTheory.StabilityFunction.IsSemistable.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (E : A) : Prop

Something wrong, better idea? Suggest a change

8.1.7. IsStable🔗

An object E is stable if it is nonzero and every nonzero proper subobject B \hookrightarrow E with B \ne \top satisfies \phi(B) < \phi(E).

Construction: A conjunction of \neg \operatorname{IsZero} E and the strict phase bound on nonzero subobjects that are not \top.

🔗def
CategoryTheory.StabilityFunction.IsStable.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) (E : A) : Prop
CategoryTheory.StabilityFunction.IsStable.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (E : A) : Prop

Something wrong, better idea? Suggest a change

8.1.8. exists_destabilizing_of_not_semistable🔗

A nonzero object that is not semistable admits a destabilizing subobject: a nonzero subobject B \hookrightarrow E with \phi(B) > \phi(E).

Proof: Unfold the negation of the semistability predicate and extract the witness.

🔗theorem
CategoryTheory.StabilityFunction.exists_destabilizing_of_not_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)
  (hns : ¬Z.IsSemistable E) :
  ∃ B,
    ¬CategoryTheory.Limits.IsZero
          (CategoryTheory.Subobject.underlying.obj B) ∧
      Z.phase E < Z.phase (CategoryTheory.Subobject.underlying.obj B)
CategoryTheory.StabilityFunction.exists_destabilizing_of_not_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)
  (hns : ¬Z.IsSemistable E) :
  ∃ B,
    ¬CategoryTheory.Limits.IsZero
          (CategoryTheory.Subobject.underlying.obj
            B) ∧
      Z.phase E <
        Z.phase
          (CategoryTheory.Subobject.underlying.obj
            B)

Something wrong, better idea? Suggest a change

8.1.9. phase_le_max_of_shortExact🔗

Phase see-saw (upper bound). For a short exact sequence 0 \to A \to B \to C \to 0 with A, C nonzero, \phi(B) \le \max(\phi(A), \phi(C)).

Proof: From Z(B) = Z(A) + Z(C) and the convexity bound \arg(z_1 + z_2) \le \max(\arg z_1, \arg z_2) for vectors in the upper half plane.

🔗theorem
CategoryTheory.StabilityFunction.phase_le_max_of_shortExact.{v, u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  (S : CategoryTheory.ShortComplex A) (hse : S.ShortExact)
  (hA : ¬CategoryTheory.Limits.IsZero S.X₁)
  (hC : ¬CategoryTheory.Limits.IsZero S.X₃) :
  Z.phase S.X₂ ≤ max (Z.phase S.X₁) (Z.phase S.X₃)
CategoryTheory.StabilityFunction.phase_le_max_of_shortExact.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (S : CategoryTheory.ShortComplex A)
  (hse : S.ShortExact)
  (hA :
    ¬CategoryTheory.Limits.IsZero S.X₁)
  (hC :
    ¬CategoryTheory.Limits.IsZero S.X₃) :
  Z.phase S.X₂ ≤
    max (Z.phase S.X₁) (Z.phase S.X₃)

Something wrong, better idea? Suggest a change

8.1.10. min_phase_le_of_shortExact🔗

Phase see-saw (lower bound). For a short exact sequence 0 \to A \to B \to C \to 0 with A, C nonzero, \min(\phi(A), \phi(C)) \le \phi(B).

Proof: Dual of the upper bound: \min(\arg z_1, \arg z_2) \le \arg(z_1 + z_2) applied to Z(B) = Z(A) + Z(C).

🔗theorem
CategoryTheory.StabilityFunction.min_phase_le_of_shortExact.{v, u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  (S : CategoryTheory.ShortComplex A) (hse : S.ShortExact)
  (hA : ¬CategoryTheory.Limits.IsZero S.X₁)
  (hC : ¬CategoryTheory.Limits.IsZero S.X₃) :
  min (Z.phase S.X₁) (Z.phase S.X₃) ≤ Z.phase S.X₂
CategoryTheory.StabilityFunction.min_phase_le_of_shortExact.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (S : CategoryTheory.ShortComplex A)
  (hse : S.ShortExact)
  (hA :
    ¬CategoryTheory.Limits.IsZero S.X₁)
  (hC :
    ¬CategoryTheory.Limits.IsZero S.X₃) :
  min (Z.phase S.X₁) (Z.phase S.X₃) ≤
    Z.phase S.X₂

Something wrong, better idea? Suggest a change

8.1.11. Zobj_eq_of_iso🔗

Z sends isomorphic objects to the same value: E \cong F \implies Z(E) = Z(F).

Proof: Use additivity on the short exact sequence 0 \to E \xrightarrow{\sim} F \to 0, noting the cokernel of an isomorphism is zero, so Z(F) = Z(E) + 0.

🔗theorem
CategoryTheory.StabilityFunction.Zobj_eq_of_iso.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {E F : A} (e : E ≅ F) :
  Z.Zobj E = Z.Zobj F
CategoryTheory.StabilityFunction.Zobj_eq_of_iso.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E F : A} (e : E ≅ F) :
  Z.Zobj E = Z.Zobj F

Something wrong, better idea? Suggest a change

8.1.12. phase_eq_of_iso🔗

Phase is invariant under isomorphisms: E \cong F \implies \phi(E) = \phi(F).

Proof: Immediate from Zobj_eq_of_iso.

🔗theorem
CategoryTheory.StabilityFunction.phase_eq_of_iso.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {E F : A} (e : E ≅ F) :
  Z.phase E = Z.phase F
CategoryTheory.StabilityFunction.phase_eq_of_iso.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E F : A} (e : E ≅ F) :
  Z.phase E = Z.phase F

Something wrong, better idea? Suggest a change

8.1.13. shortExact_of_mono🔗

For any monomorphism f \colon X \hookrightarrow Y in an abelian category, the short complex X \xrightarrow{f} Y \to \operatorname{coker} f is short exact.

Proof: Combine exactness at Y (from ShortComplex.exact_cokernel) with the mono and epi conditions.

🔗theorem
CategoryTheory.StabilityFunction.shortExact_of_mono.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  {X Y : A} (f : X ⟶ Y) [CategoryTheory.Mono f] :
  { X₁ := X, X₂ := Y, X₃ := CategoryTheory.Limits.cokernel f, f := f,
      g := CategoryTheory.Limits.cokernel.π f, zero := ⋯ }.ShortExact
CategoryTheory.StabilityFunction.shortExact_of_mono.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {X Y : A}
  (f : X ⟶ Y) [CategoryTheory.Mono f] :
  { X₁ := X, X₂ := Y,
      X₃ :=
        CategoryTheory.Limits.cokernel f,
      f := f,
      g :=
        CategoryTheory.Limits.cokernel.π
          f,
      zero := ⋯ }.ShortExact

Something wrong, better idea? Suggest a change

8.1.14. isSemistable_of_iso🔗

Semistability is invariant under isomorphisms: if X \cong Y and X is semistable, then Y is semistable.

Proof: Transport the phase bound on subobjects of X to subobjects of Y via the isomorphism, using phase_eq_of_iso to compare phases.

🔗theorem
CategoryTheory.StabilityFunction.isSemistable_of_iso.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {X Y : A} (e : X ≅ Y)
  (h : Z.IsSemistable X) : Z.IsSemistable Y
CategoryTheory.StabilityFunction.isSemistable_of_iso.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {X Y : A} (e : X ≅ Y)
  (h : Z.IsSemistable X) :
  Z.IsSemistable Y

Something wrong, better idea? Suggest a change

8.1.15. subobject_isZero_iff_eq_bot🔗

A subobject B of E is zero if and only if B = \bot in the subobject lattice.

Proof: Forward: if the underlying object is zero, the arrow is zero, hence mk is \bot. Backward: \bot is isomorphic to the zero object.

🔗theorem
CategoryTheory.StabilityFunction.subobject_isZero_iff_eq_bot.{v, u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E : A} (B : CategoryTheory.Subobject E) :
  CategoryTheory.Limits.IsZero
      (CategoryTheory.Subobject.underlying.obj B) ↔
    B = ⊥
CategoryTheory.StabilityFunction.subobject_isZero_iff_eq_bot.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E : A}
  (B : CategoryTheory.Subobject E) :
  CategoryTheory.Limits.IsZero
      (CategoryTheory.Subobject.underlying.obj
        B) ↔
    B = ⊥

Something wrong, better idea? Suggest a change

8.1.16. subobject_ne_bot_of_not_isZero🔗

A nonzero subobject is not \bot.

Proof: Contrapositive of the forward direction of subobject_isZero_iff_eq_bot.

🔗theorem
CategoryTheory.StabilityFunction.subobject_ne_bot_of_not_isZero.{v, u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E : A} {B : CategoryTheory.Subobject E}
  (h :
    ¬CategoryTheory.Limits.IsZero
        (CategoryTheory.Subobject.underlying.obj B)) :
  B ≠ ⊥
CategoryTheory.StabilityFunction.subobject_ne_bot_of_not_isZero.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E : A}
  {B : CategoryTheory.Subobject E}
  (h :
    ¬CategoryTheory.Limits.IsZero
        (CategoryTheory.Subobject.underlying.obj
          B)) :
  B ≠ ⊥

Something wrong, better idea? Suggest a change

8.1.17. subobject_not_isZero_of_ne_bot🔗

A subobject that is not \bot is nonzero.

Proof: Contrapositive of the backward direction of subobject_isZero_iff_eq_bot.

🔗theorem
CategoryTheory.StabilityFunction.subobject_not_isZero_of_ne_bot.{v, u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E : A} {B : CategoryTheory.Subobject E}
  (h : B ≠ ⊥) :
  ¬CategoryTheory.Limits.IsZero
      (CategoryTheory.Subobject.underlying.obj B)
CategoryTheory.StabilityFunction.subobject_not_isZero_of_ne_bot.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E : A}
  {B : CategoryTheory.Subobject E}
  (h : B ≠ ⊥) :
  ¬CategoryTheory.Limits.IsZero
      (CategoryTheory.Subobject.underlying.obj
        B)

Something wrong, better idea? Suggest a change

8.1.18. subobject_top_ne_bot_of_not_isZero🔗

For a nonzero object E, \top \ne \bot in the subobject lattice of E.

Proof: If \top = \bot then \top is zero, so E \cong (\top : \operatorname{Sub} E) is zero, contradicting the hypothesis.

🔗theorem
CategoryTheory.StabilityFunction.subobject_top_ne_bot_of_not_isZero.{v,
    u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E : A}
  (hE : ¬CategoryTheory.Limits.IsZero E) : ⊤ ≠ ⊥
CategoryTheory.StabilityFunction.subobject_top_ne_bot_of_not_isZero.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E : A}
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  ⊤ ≠ ⊥

Something wrong, better idea? Suggest a change

8.1.19. ofLE_bot🔗

The morphism ofLE \bot S h is the zero morphism, since \bot is a zero object.

Proof: The source is isomorphic to the zero object via botCoeIsoZero.

🔗theorem
CategoryTheory.StabilityFunction.Subobject.ofLE_bot.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {E : A}
  (S : CategoryTheory.Subobject E) (h : ⊥ ≤ S) : ⊥.ofLE S h = 0
CategoryTheory.StabilityFunction.Subobject.ofLE_bot.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E : A}
  (S : CategoryTheory.Subobject E)
  (h : ⊥ ≤ S) : ⊥.ofLE S h = 0

Something wrong, better idea? Suggest a change

8.1.20. cokernelBotIso🔗

The cokernel of ofLE \bot S h is isomorphic to (S : A).

Construction: Since ofLE \bot S h = 0, the cokernel of zero is the target, giving \operatorname{coker}(0 \to S) \cong S.

🔗def
CategoryTheory.StabilityFunction.Subobject.cokernelBotIso.{v, u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E : A} (S : CategoryTheory.Subobject E)
  (h : ⊥ ≤ S) :
  CategoryTheory.Limits.cokernel (⊥.ofLE S h) ≅
    CategoryTheory.Subobject.underlying.obj S
CategoryTheory.StabilityFunction.Subobject.cokernelBotIso.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E : A}
  (S : CategoryTheory.Subobject E)
  (h : ⊥ ≤ S) :
  CategoryTheory.Limits.cokernel
      (⊥.ofLE S h) ≅
    CategoryTheory.Subobject.underlying.obj
      S

Something wrong, better idea? Suggest a change

8.1.21. liftSub🔗

Given a subobject B of E and a subobject C of (B : A), the lifted subobject liftSub B C is the subobject of E obtained by composing the inclusion arrows C \hookrightarrow B \hookrightarrow E.

Construction: Defined as Subobject.mk (C.arrow \gg B.arrow).

🔗def
CategoryTheory.StabilityFunction.liftSub.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] {E : A}
  (B : CategoryTheory.Subobject E)
  (C :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj B)) :
  CategoryTheory.Subobject E
CategoryTheory.StabilityFunction.liftSub.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  {E : A} (B : CategoryTheory.Subobject E)
  (C :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj
        B)) :
  CategoryTheory.Subobject E

Something wrong, better idea? Suggest a change

8.1.22. liftSub_le🔗

The lifted subobject satisfies \operatorname{liftSub}(B, C) \le B.

Proof: The inclusion C \to B \to E factors through B.

🔗theorem
CategoryTheory.StabilityFunction.liftSub_le.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] {E : A}
  (B : CategoryTheory.Subobject E)
  (C :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj B)) :
  CategoryTheory.StabilityFunction.liftSub B C ≤ B
CategoryTheory.StabilityFunction.liftSub_le.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  {E : A} (B : CategoryTheory.Subobject E)
  (C :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj
        B)) :
  CategoryTheory.StabilityFunction.liftSub
      B C ≤
    B

Something wrong, better idea? Suggest a change

8.1.23. phase_liftSub🔗

The phase of the lifted subobject equals the phase of C: \phi(\operatorname{liftSub}(B, C)) = \phi(C).

Proof: The underlying objects are isomorphic via the canonical isomorphism from Subobject.underlyingIso.

🔗theorem
CategoryTheory.StabilityFunction.phase_liftSub.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {E : A}
  (B : CategoryTheory.Subobject E)
  (C :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj B)) :
  Z.phase
      (CategoryTheory.Subobject.underlying.obj
        (CategoryTheory.StabilityFunction.liftSub B C)) =
    Z.phase (CategoryTheory.Subobject.underlying.obj C)
CategoryTheory.StabilityFunction.phase_liftSub.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A} (B : CategoryTheory.Subobject E)
  (C :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj
        B)) :
  Z.phase
      (CategoryTheory.Subobject.underlying.obj
        (CategoryTheory.StabilityFunction.liftSub
          B C)) =
    Z.phase
      (CategoryTheory.Subobject.underlying.obj
        C)

Something wrong, better idea? Suggest a change

8.1.24. liftSub_bot🔗

Lifting \bot gives \bot: \operatorname{liftSub}(B, \bot) = \bot.

Proof: The composition involves the zero arrow from \bot.

🔗theorem
CategoryTheory.StabilityFunction.liftSub_bot.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {E : A}
  (B : CategoryTheory.Subobject E) :
  CategoryTheory.StabilityFunction.liftSub B ⊥ = ⊥
CategoryTheory.StabilityFunction.liftSub_bot.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E : A}
  (B : CategoryTheory.Subobject E) :
  CategoryTheory.StabilityFunction.liftSub
      B ⊥ =
    ⊥

Something wrong, better idea? Suggest a change

8.1.25. liftSub_ne_bot🔗

Lifting a nonzero subobject gives a nonzero subobject.

Proof: If the lift were \bot, the underlying object would be zero, contradicting non-zeroness of C via the canonical isomorphism.

🔗theorem
CategoryTheory.StabilityFunction.liftSub_ne_bot.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {E : A}
  (B : CategoryTheory.Subobject E)
  (C :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj B))
  (hC : C ≠ ⊥) : CategoryTheory.StabilityFunction.liftSub B C ≠ ⊥
CategoryTheory.StabilityFunction.liftSub_ne_bot.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E : A}
  (B : CategoryTheory.Subobject E)
  (C :
    CategoryTheory.Subobject
      (CategoryTheory.Subobject.underlying.obj
        B))
  (hC : C ≠ ⊥) :
  CategoryTheory.StabilityFunction.liftSub
      B C ≠
    ⊥

Something wrong, better idea? Suggest a change

8.1.26. simple_isSemistable🔗

A simple object is semistable: its only nonzero subobject is \top \cong E itself, so the phase condition \phi(B) \le \phi(E) holds trivially.

Proof: By simplicity the subobject lattice is simple order, so every nonzero subobject equals \top, and the phase bound becomes an equality.

🔗theorem
CategoryTheory.StabilityFunction.simple_isSemistable.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {E : A}
  (hS : CategoryTheory.Simple E) : Z.IsSemistable E
CategoryTheory.StabilityFunction.simple_isSemistable.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A} (hS : CategoryTheory.Simple E) :
  Z.IsSemistable E

Something wrong, better idea? Suggest a change

8.1.27. exists_semistable_subobject_ge_phase_of_artinian🔗

In an Artinian object, every nonzero subobject contains a semistable subobject of at least the same phase. This is the first chain-condition step in Bridgeland's Proposition 2.4.

Proof: Well-founded induction on the subobject lattice (using the Artinian condition). If a subobject B is not semistable, extract a destabilizing subobject D, lift it to E, and recurse. Termination is guaranteed by the strictly descending chain.

🔗theorem
CategoryTheory.StabilityFunction.exists_semistable_subobject_ge_phase_of_artinian.{v,
    u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {Z : CategoryTheory.StabilityFunction A}
  {E : A} [CategoryTheory.IsArtinianObject E]
  {B : CategoryTheory.Subobject E} (hB : B ≠ ⊥) :
  ∃ C ≤ B,
    C ≠ ⊥ ∧
      Z.IsSemistable (CategoryTheory.Subobject.underlying.obj C) ∧
        Z.phase (CategoryTheory.Subobject.underlying.obj B) ≤
          Z.phase (CategoryTheory.Subobject.underlying.obj C)
CategoryTheory.StabilityFunction.exists_semistable_subobject_ge_phase_of_artinian.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  {Z : CategoryTheory.StabilityFunction A}
  {E : A}
  [CategoryTheory.IsArtinianObject E]
  {B : CategoryTheory.Subobject E}
  (hB : B ≠ ⊥) :
  ∃ C ≤ B,
    C ≠ ⊥ ∧
      Z.IsSemistable
          (CategoryTheory.Subobject.underlying.obj
            C) ∧
        Z.phase
            (CategoryTheory.Subobject.underlying.obj
              B) ≤
          Z.phase
            (CategoryTheory.Subobject.underlying.obj
              C)

Something wrong, better idea? Suggest a change

8.1.28. exists_semistable_subobject_gt_phase_of_not_semistable🔗

In a non-semistable Artinian object, there exists a semistable subobject with strictly larger phase than E.

Proof: Combine exists_destabilizing_of_not_semistable to get a destabilizing subobject, then apply exists_semistable_subobject_ge_phase_of_artinian to refine it to a semistable one.

🔗theorem
CategoryTheory.StabilityFunction.exists_semistable_subobject_gt_phase_of_not_semistable.{v,
    u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {Z : CategoryTheory.StabilityFunction A}
  {E : A} [CategoryTheory.IsArtinianObject E]
  (hE : ¬CategoryTheory.Limits.IsZero E) (hns : ¬Z.IsSemistable E) :
  ∃ B,
    B ≠ ⊥ ∧
      Z.IsSemistable (CategoryTheory.Subobject.underlying.obj B) ∧
        Z.phase E < Z.phase (CategoryTheory.Subobject.underlying.obj B)
CategoryTheory.StabilityFunction.exists_semistable_subobject_gt_phase_of_not_semistable.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  {Z : CategoryTheory.StabilityFunction A}
  {E : A}
  [CategoryTheory.IsArtinianObject E]
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hns : ¬Z.IsSemistable E) :
  ∃ B,
    B ≠ ⊥ ∧
      Z.IsSemistable
          (CategoryTheory.Subobject.underlying.obj
            B) ∧
        Z.phase E <
          Z.phase
            (CategoryTheory.Subobject.underlying.obj
              B)

Something wrong, better idea? Suggest a change

8.1.29. exists_maxPhase_subobject🔗

Among all nonzero subobjects of a nonzero object with a finite subobject lattice, there exists one with maximal phase.

Proof: The set of nonzero subobjects is nonempty (contains \top) and finite, so the phase function attains its maximum.

🔗theorem
CategoryTheory.StabilityFunction.exists_maxPhase_subobject.{v, u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  (E : A) (hE : ¬CategoryTheory.Limits.IsZero E)
  [hFin : Finite (CategoryTheory.Subobject E)] :
  ∃ M,
    M ≠ ⊥ ∧
      ∀ (B : CategoryTheory.Subobject E),
        B ≠ ⊥ →
          Z.phase (CategoryTheory.Subobject.underlying.obj B) ≤
            Z.phase (CategoryTheory.Subobject.underlying.obj M)
CategoryTheory.StabilityFunction.exists_maxPhase_subobject.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (E : A)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  [hFin :
    Finite (CategoryTheory.Subobject E)] :
  ∃ M,
    M ≠ ⊥ ∧
      ∀ (B : CategoryTheory.Subobject E),
        B ≠ ⊥ →
          Z.phase
              (CategoryTheory.Subobject.underlying.obj
                B) ≤
            Z.phase
              (CategoryTheory.Subobject.underlying.obj
                M)

Something wrong, better idea? Suggest a change

8.1.30. maxPhase_isSemistable🔗

A subobject M with maximal phase among all nonzero subobjects of E is semistable as an object.

Proof: Any destabilizing subobject of (M : A) lifts to a nonzero subobject of E with higher phase via liftSub, contradicting the maximality of M.

🔗theorem
CategoryTheory.StabilityFunction.maxPhase_isSemistable.{v, u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  {E : A} {M : CategoryTheory.Subobject E} (hM : M ≠ ⊥)
  (hmax :
    ∀ (B : CategoryTheory.Subobject E),
      B ≠ ⊥ →
        Z.phase (CategoryTheory.Subobject.underlying.obj B) ≤
          Z.phase (CategoryTheory.Subobject.underlying.obj M)) :
  Z.IsSemistable (CategoryTheory.Subobject.underlying.obj M)
CategoryTheory.StabilityFunction.maxPhase_isSemistable.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A} {M : CategoryTheory.Subobject E}
  (hM : M ≠ ⊥)
  (hmax :
    ∀ (B : CategoryTheory.Subobject E),
      B ≠ ⊥ →
        Z.phase
            (CategoryTheory.Subobject.underlying.obj
              B) ≤
          Z.phase
            (CategoryTheory.Subobject.underlying.obj
              M)) :
  Z.IsSemistable
    (CategoryTheory.Subobject.underlying.obj
      M)

Something wrong, better idea? Suggest a change

8.1.31. maxPhase_ne_top_of_not_semistable🔗

When E is not semistable, the max-phase subobject M satisfies M \ne \top. Since \phi(\top) = \phi(E) and \phi(M) > \phi(E), we have M \ne \top.

Proof: If M = \top, then M being semistable would make E semistable via the isomorphism \top \cong E, contradicting the hypothesis.

🔗theorem
CategoryTheory.StabilityFunction.maxPhase_ne_top_of_not_semistable.{v,
    u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  {E : A} (hns : ¬Z.IsSemistable E) (M : CategoryTheory.Subobject E) :
  M ≠ ⊥ →
    (∀ (B : CategoryTheory.Subobject E),
        B ≠ ⊥ →
          Z.phase (CategoryTheory.Subobject.underlying.obj B) ≤
            Z.phase (CategoryTheory.Subobject.underlying.obj M)) →
      M ≠ ⊤
CategoryTheory.StabilityFunction.maxPhase_ne_top_of_not_semistable.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A} (hns : ¬Z.IsSemistable E)
  (M : CategoryTheory.Subobject E) :
  M ≠ ⊥ →
    (∀ (B : CategoryTheory.Subobject E),
        B ≠ ⊥ →
          Z.phase
              (CategoryTheory.Subobject.underlying.obj
                B) ≤
            Z.phase
              (CategoryTheory.Subobject.underlying.obj
                M)) →
      M ≠ ⊤

Something wrong, better idea? Suggest a change