Bridgeland Stability Conditions

8.2. StabilityFunction: HarderNarasimhan🔗

8.2.1. AbelianHNFiltration🔗

[Definition 2.3] HN filtration for abelian categories

A Harder--Narasimhan filtration of a nonzero object E in an abelian category with respect to a stability function Z is a finite chain of subobjects 0 = E_0 < E_1 < \cdots < E_n = E (with n \ge 1) such that the successive quotients E_i / E_{i-1} are semistable with strictly decreasing phases \phi_1 > \phi_2 > \cdots > \phi_n.

Construction: The structure carries the number of factors n, the strictly monotone chain chain : Fin (n+1) \to Subobject E with chain(0) = \bot and chain(n) = \top, the phase sequence \phi : Fin n \to \mathbb{R} which is StrictAnti, and proofs that each successive cokernel is semistable with the prescribed phase.

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

  • n ≥ 1 factors

  • the phases are strictly decreasing

  • each factor Eᵢ₊₁/Eᵢ is semistable with phase φ i

Constructor

CategoryTheory.AbelianHNFiltration.mk.{v, u}

Fields

n : ℕ

The number of semistable factors.

hn : 0 < self.n
chain : Fin (self.n + 1) → CategoryTheory.Subobject E

The chain of subobjects, strictly monotone.

chain_strictMono : StrictMono self.chain
chain_bot : self.chain ⟨0, ⋯⟩ = ⊥
chain_top : self.chain ⟨self.n, ⋯⟩ = ⊤
φ : Fin self.n → ℝ

The phases of the semistable quotients, in strictly decreasing order.

φ_anti : StrictAnti self.φ
factor_phase : ∀ (j : Fin self.n),
  Z.phase (CategoryTheory.Limits.cokernel ((self.chain j.castSucc).ofLE (self.chain j.succ) ⋯)) = self.φ j

The phase of each factor equals the given phase.

factor_semistable : ∀ (j : Fin self.n), Z.IsSemistable (CategoryTheory.Limits.cokernel ((self.chain j.castSucc).ofLE (self.chain j.succ) ⋯))

Each successive quotient is semistable.

Something wrong, better idea? Suggest a change

8.2.2. HasHNProperty🔗

[Definition 2.3] HN property predicate

A stability function Z has the Harder--Narasimhan property if every nonzero object admits an HN filtration (Bridgeland, Proposition 2.4).

Construction: Defined as the universal statement: for all nonzero E, the type AbelianHNFiltration Z E is nonempty.

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

Something wrong, better idea? Suggest a change

8.2.3. pullback_obj_injective_of_epi🔗

For an epimorphism p \colon X \twoheadrightarrow Y in an abelian category, the pullback functor p^* \colon \operatorname{Sub}(Y) \to \operatorname{Sub}(X) is injective on objects.

Proof: Two subobjects B_1, B_2 of Y with p^*(B_1) = p^*(B_2) have the same image subobject after precomposing with p. Since p is epi, precomposition does not change the image, so B_1 = B_2.

🔗theorem
CategoryTheory.pullback_obj_injective_of_epi.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  {X Y : A} (p : X ⟶ Y) [CategoryTheory.Epi p] :
  Function.Injective (CategoryTheory.Subobject.pullback p).obj
CategoryTheory.pullback_obj_injective_of_epi.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {X Y : A}
  (p : X ⟶ Y) [CategoryTheory.Epi p] :
  Function.Injective
    (CategoryTheory.Subobject.pullback
        p).obj

Something wrong, better idea? Suggest a change

8.2.4. isNoetherianObject_of_epi🔗

Quotients of Noetherian objects are Noetherian.

Proof: Given an ascending chain in \operatorname{Sub}(Y), pull it back along p to an ascending chain in \operatorname{Sub}(X). The pulled-back chain stabilizes by Noetherianity of X, and injectivity of p^* forces the original chain to stabilize.

🔗theorem
CategoryTheory.isNoetherianObject_of_epi.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  {X Y : A} (p : X ⟶ Y) [CategoryTheory.Epi p]
  [CategoryTheory.IsNoetherianObject X] :
  CategoryTheory.IsNoetherianObject Y
CategoryTheory.isNoetherianObject_of_epi.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {X Y : A}
  (p : X ⟶ Y) [CategoryTheory.Epi p]
  [CategoryTheory.IsNoetherianObject X] :
  CategoryTheory.IsNoetherianObject Y

Something wrong, better idea? Suggest a change

8.2.5. isArtinianObject_of_epi🔗

Quotients of Artinian objects are Artinian.

Proof: Dual of isNoetherianObject_of_epi: pull back a descending chain in \operatorname{Sub}(Y) along the epi p to get a descending chain in \operatorname{Sub}(X)^{\mathrm{op}}, which stabilizes by the Artinian condition.

🔗theorem
CategoryTheory.isArtinianObject_of_epi.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  {X Y : A} (p : X ⟶ Y) [CategoryTheory.Epi p]
  [CategoryTheory.IsArtinianObject X] :
  CategoryTheory.IsArtinianObject Y
CategoryTheory.isArtinianObject_of_epi.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {X Y : A}
  (p : X ⟶ Y) [CategoryTheory.Epi p]
  [CategoryTheory.IsArtinianObject X] :
  CategoryTheory.IsArtinianObject Y

Something wrong, better idea? Suggest a change

8.2.6. card_subobject_cokernel_lt🔗

Cardinality decrease. For a nonzero subobject M of E with \operatorname{Sub}(E) finite, |\operatorname{Sub}(\operatorname{coker} M)| < |\operatorname{Sub}(E)|.

Proof: The pullback p^* \colon \operatorname{Sub}(\operatorname{coker} M) \hookrightarrow \operatorname{Sub}(E) is injective but M is not in its image (since every pullback subobject is \ge M \ne \bot), giving the strict inequality.

🔗theorem
CategoryTheory.card_subobject_cokernel_lt.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {E : A}
  {M : CategoryTheory.Subobject E} (hM_ne_bot : M ≠ ⊥)
  [hFin : Finite (CategoryTheory.Subobject E)] :
  Nat.card
      (CategoryTheory.Subobject
        (CategoryTheory.Limits.cokernel M.arrow)) <
    Nat.card (CategoryTheory.Subobject E)
CategoryTheory.card_subobject_cokernel_lt.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E : A}
  {M : CategoryTheory.Subobject E}
  (hM_ne_bot : M ≠ ⊥)
  [hFin :
    Finite (CategoryTheory.Subobject E)] :
  Nat.card
      (CategoryTheory.Subobject
        (CategoryTheory.Limits.cokernel
          M.arrow)) <
    Nat.card (CategoryTheory.Subobject E)

Something wrong, better idea? Suggest a change

8.2.7. pullback_cokernel_bot_eq🔗

The pullback of \bot along \operatorname{coker.\pi}(M) equals M as a subobject of E.

Proof: The pullback of \bot consists of elements mapping to 0 in the cokernel, which is exactly the kernel of \operatorname{coker.\pi}(M), i.e. M itself.

🔗theorem
CategoryTheory.pullback_cokernel_bot_eq.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {E : A}
  (M : CategoryTheory.Subobject E) :
  (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.cokernel.π M.arrow)).obj
      ⊥ =
    M
CategoryTheory.pullback_cokernel_bot_eq.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E : A}
  (M : CategoryTheory.Subobject E) :
  (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.cokernel.π
            M.arrow)).obj
      ⊥ =
    M

Something wrong, better idea? Suggest a change

8.2.8. exists_maxPhase_maximal_subobject🔗

Among all nonzero subobjects with maximal phase, there exists one that is also maximal in the subobject partial order. Every subobject strictly above it has strictly lower phase.

Proof: First find M_0 with maximal phase, then take the largest element (in the subobject order) among those with phase equal to \phi(M_0). Finiteness ensures this maximum exists.

🔗theorem
CategoryTheory.exists_maxPhase_maximal_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)) ∧
        ∀ (B : CategoryTheory.Subobject E),
          M < B →
            Z.phase (CategoryTheory.Subobject.underlying.obj B) <
              Z.phase (CategoryTheory.Subobject.underlying.obj M)
CategoryTheory.exists_maxPhase_maximal_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)) ∧
        ∀
          (B :
            CategoryTheory.Subobject E),
          M < B →
            Z.phase
                (CategoryTheory.Subobject.underlying.obj
                  B) <
              Z.phase
                (CategoryTheory.Subobject.underlying.obj
                  M)

Something wrong, better idea? Suggest a change

8.2.9. cokernel_nonzero_of_ne_top🔗

If M \ne \top as a subobject of E, then \operatorname{coker}(M.\mathrm{arrow}) is nonzero.

Proof: If the cokernel were zero, M.\mathrm{arrow} would be epi, hence an isomorphism (being also mono), forcing M = \top.

🔗theorem
CategoryTheory.cokernel_nonzero_of_ne_top.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {E : A}
  {M : CategoryTheory.Subobject E} (hM : M ≠ ⊤) :
  ¬CategoryTheory.Limits.IsZero (CategoryTheory.Limits.cokernel M.arrow)
CategoryTheory.cokernel_nonzero_of_ne_top.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E : A}
  {M : CategoryTheory.Subobject E}
  (hM : M ≠ ⊤) :
  ¬CategoryTheory.Limits.IsZero
      (CategoryTheory.Limits.cokernel
        M.arrow)

Something wrong, better idea? Suggest a change

8.2.10. le_pullback_cokernel🔗

For any subobject B of \operatorname{coker}(M'), the pullback satisfies M' \le p^*(B) where p = \operatorname{coker.\pi}(M').

Proof: By pullback_cokernel_bot_eq, p^*(\bot) = M', and \bot \le B implies p^*(\bot) \le p^*(B) by monotonicity.

🔗theorem
CategoryTheory.le_pullback_cokernel.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {E : A}
  (M' : CategoryTheory.Subobject E)
  (B :
    CategoryTheory.Subobject
      (CategoryTheory.Limits.cokernel M'.arrow)) :
  M' ≤
    (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.cokernel.π M'.arrow)).obj
      B
CategoryTheory.le_pullback_cokernel.{v, u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E : A}
  (M' : CategoryTheory.Subobject E)
  (B :
    CategoryTheory.Subobject
      (CategoryTheory.Limits.cokernel
        M'.arrow)) :
  M' ≤
    (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.cokernel.π
            M'.arrow)).obj
      B

Something wrong, better idea? Suggest a change

8.2.11. Zobj_pullback_eq_add🔗

Z-additivity for the pullback short exact sequence: Z(p^*(B)) = Z(M') + Z(B) where p = \operatorname{coker.\pi}(M').

Proof: Apply Z-additivity to the short exact sequence M' \hookrightarrow p^*(B) \twoheadrightarrow B.

🔗theorem
CategoryTheory.Zobj_pullback_eq_add.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {E : A}
  (M' : CategoryTheory.Subobject E)
  (B :
    CategoryTheory.Subobject
      (CategoryTheory.Limits.cokernel M'.arrow)) :
  Z.Zobj
      (CategoryTheory.Subobject.underlying.obj
        ((CategoryTheory.Subobject.pullback
              (CategoryTheory.Limits.cokernel.π M'.arrow)).obj
          B)) =
    Z.Zobj (CategoryTheory.Subobject.underlying.obj M') +
      Z.Zobj (CategoryTheory.Subobject.underlying.obj B)
CategoryTheory.Zobj_pullback_eq_add.{v, u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A}
  (M' : CategoryTheory.Subobject E)
  (B :
    CategoryTheory.Subobject
      (CategoryTheory.Limits.cokernel
        M'.arrow)) :
  Z.Zobj
      (CategoryTheory.Subobject.underlying.obj
        ((CategoryTheory.Subobject.pullback
              (CategoryTheory.Limits.cokernel.π
                M'.arrow)).obj
          B)) =
    Z.Zobj
        (CategoryTheory.Subobject.underlying.obj
          M') +
      Z.Zobj
        (CategoryTheory.Subobject.underlying.obj
          B)

Something wrong, better idea? Suggest a change

8.2.12. phase_cokernel_pullback_eq🔗

The cokernel of consecutive pulled-back subobjects has the same phase as the original cokernel factor: \phi(\operatorname{coker}(p^*(A') \hookrightarrow p^*(B'))) = \phi(\operatorname{coker}(A' \hookrightarrow B')).

Proof: Follows from the Z-value equality Zobj_cokernel_pullback_eq and the definition of phase in terms of \arg.

🔗theorem
CategoryTheory.phase_cokernel_pullback_eq.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {E : A}
  (M' : CategoryTheory.Subobject E)
  {A' B' :
    CategoryTheory.Subobject (CategoryTheory.Limits.cokernel M'.arrow)}
  (h : A' ≤ B') :
  Z.phase
      (CategoryTheory.Limits.cokernel
        (((CategoryTheory.Subobject.pullback
                  (CategoryTheory.Limits.cokernel.π M'.arrow)).obj
              A').ofLE
          ((CategoryTheory.Subobject.pullback
                (CategoryTheory.Limits.cokernel.π M'.arrow)).obj
            B')
          ⋯)) =
    Z.phase (CategoryTheory.Limits.cokernel (A'.ofLE B' h))
CategoryTheory.phase_cokernel_pullback_eq.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A}
  (M' : CategoryTheory.Subobject E)
  {A' B' :
    CategoryTheory.Subobject
      (CategoryTheory.Limits.cokernel
        M'.arrow)}
  (h : A' ≤ B') :
  Z.phase
      (CategoryTheory.Limits.cokernel
        (((CategoryTheory.Subobject.pullback
                  (CategoryTheory.Limits.cokernel.π
                    M'.arrow)).obj
              A').ofLE
          ((CategoryTheory.Subobject.pullback
                (CategoryTheory.Limits.cokernel.π
                  M'.arrow)).obj
            B')
          ⋯)) =
    Z.phase
      (CategoryTheory.Limits.cokernel
        (A'.ofLE B' h))

Something wrong, better idea? Suggest a change

8.2.13. cokernelPullbackIso🔗

The cokernel of consecutive pulled-back subobjects is isomorphic to the original cokernel factor.

Construction: Constructed by showing the natural map between the cokernels is both mono (via a Z-value kernel argument) and epi (since the pullback morphism is epi), hence an isomorphism.

🔗def
CategoryTheory.cokernelPullbackIso.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {E : A}
  (M' : CategoryTheory.Subobject E)
  {A' B' :
    CategoryTheory.Subobject (CategoryTheory.Limits.cokernel M'.arrow)}
  (h : A' < B') :
  CategoryTheory.Limits.cokernel
      (((CategoryTheory.Subobject.pullback
                (CategoryTheory.Limits.cokernel.π M'.arrow)).obj
            A').ofLE
        ((CategoryTheory.Subobject.pullback
              (CategoryTheory.Limits.cokernel.π M'.arrow)).obj
          B')
        ⋯) ≅
    CategoryTheory.Limits.cokernel (A'.ofLE B' ⋯)
CategoryTheory.cokernelPullbackIso.{v, u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A}
  (M' : CategoryTheory.Subobject E)
  {A' B' :
    CategoryTheory.Subobject
      (CategoryTheory.Limits.cokernel
        M'.arrow)}
  (h : A' < B') :
  CategoryTheory.Limits.cokernel
      (((CategoryTheory.Subobject.pullback
                (CategoryTheory.Limits.cokernel.π
                  M'.arrow)).obj
            A').ofLE
        ((CategoryTheory.Subobject.pullback
              (CategoryTheory.Limits.cokernel.π
                M'.arrow)).obj
          B')
        ⋯) ≅
    CategoryTheory.Limits.cokernel
      (A'.ofLE B' ⋯)

Something wrong, better idea? Suggest a change

8.2.14. phase_cokernel_ofLE_congr🔗

Phase equality when the ofLE subobject arguments are propositionally equal: if A_1 = A_2 and B_1 = B_2 then \phi(\operatorname{coker}(A_1 \hookrightarrow B_1)) = \phi(\operatorname{coker}(A_2 \hookrightarrow B_2)).

Proof: By substitution.

🔗theorem
CategoryTheory.phase_cokernel_ofLE_congr.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {E : A}
  {A₁ A₂ B₁ B₂ : CategoryTheory.Subobject E} (hA : A₁ = A₂)
  (hB : B₁ = B₂) {h₁ : A₁ ≤ B₁} {h₂ : A₂ ≤ B₂} :
  Z.phase (CategoryTheory.Limits.cokernel (A₁.ofLE B₁ h₁)) =
    Z.phase (CategoryTheory.Limits.cokernel (A₂.ofLE B₂ h₂))
CategoryTheory.phase_cokernel_ofLE_congr.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A}
  {A₁ A₂ B₁ B₂ :
    CategoryTheory.Subobject E}
  (hA : A₁ = A₂) (hB : B₁ = B₂)
  {h₁ : A₁ ≤ B₁} {h₂ : A₂ ≤ B₂} :
  Z.phase
      (CategoryTheory.Limits.cokernel
        (A₁.ofLE B₁ h₁)) =
    Z.phase
      (CategoryTheory.Limits.cokernel
        (A₂.ofLE B₂ h₂))

Something wrong, better idea? Suggest a change

8.2.15. isSemistable_cokernel_ofLE_congr🔗

Semistability transfer when ofLE subobject arguments are propositionally equal.

Proof: By substitution.

🔗theorem
CategoryTheory.isSemistable_cokernel_ofLE_congr.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {E : A}
  {A₁ A₂ B₁ B₂ : CategoryTheory.Subobject E} (hA : A₁ = A₂)
  (hB : B₁ = B₂) {h₁ : A₁ ≤ B₁} {h₂ : A₂ ≤ B₂}
  (hs :
    Z.IsSemistable (CategoryTheory.Limits.cokernel (A₂.ofLE B₂ h₂))) :
  Z.IsSemistable (CategoryTheory.Limits.cokernel (A₁.ofLE B₁ h₁))
CategoryTheory.isSemistable_cokernel_ofLE_congr.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A}
  {A₁ A₂ B₁ B₂ :
    CategoryTheory.Subobject E}
  (hA : A₁ = A₂) (hB : B₁ = B₂)
  {h₁ : A₁ ≤ B₁} {h₂ : A₂ ≤ B₂}
  (hs :
    Z.IsSemistable
      (CategoryTheory.Limits.cokernel
        (A₂.ofLE B₂ h₂))) :
  Z.IsSemistable
    (CategoryTheory.Limits.cokernel
      (A₁.ofLE B₁ h₁))

Something wrong, better idea? Suggest a change

8.2.16. hasHN_of_finiteLength🔗

Proposition 2.4 (Bridgeland). If every object of \mathcal{A} has a finite subobject lattice, then any stability function on \mathcal{A} has the Harder--Narasimhan property.

Proof: Induction on |\operatorname{Sub}(E)|. If E is semistable, it is its own single-factor HN filtration. Otherwise, find the maximally destabilizing subobject M (max-phase, semistable by maxPhase_isSemistable), recurse on E/M (which has strictly fewer subobjects by card_subobject_cokernel_lt), and concatenate the result with M as the first factor.

🔗theorem
CategoryTheory.StabilityFunction.hasHN_of_finiteLength.{v, u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  (hFinSub : ∀ (E : A), Finite (CategoryTheory.Subobject E)) :
  Z.HasHNProperty
CategoryTheory.StabilityFunction.hasHN_of_finiteLength.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (hFinSub :
    ∀ (E : A),
      Finite
        (CategoryTheory.Subobject E)) :
  Z.HasHNProperty

Something wrong, better idea? Suggest a change

8.2.17. cokernelPullbackTopIso🔗

The quotient E / p^*(B) (where p = \operatorname{coker.\pi}(M) and B \ne \top) is canonically isomorphic to \operatorname{coker}(B).

Construction: Constructed by composing three cokernel isomorphisms: normalizing the arrow via ofLE, applying cokernelPullbackIso, and unnormalizing.

🔗def
CategoryTheory.cokernelPullbackTopIso.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {E : A}
  (M : CategoryTheory.Subobject E)
  {B :
    CategoryTheory.Subobject (CategoryTheory.Limits.cokernel M.arrow)}
  (hB : B ≠ ⊤) :
  CategoryTheory.Limits.cokernel
      ((CategoryTheory.Subobject.pullback
              (CategoryTheory.Limits.cokernel.π M.arrow)).obj
          B).arrow ≅
    CategoryTheory.Limits.cokernel B.arrow
CategoryTheory.cokernelPullbackTopIso.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A} (M : CategoryTheory.Subobject E)
  {B :
    CategoryTheory.Subobject
      (CategoryTheory.Limits.cokernel
        M.arrow)}
  (hB : B ≠ ⊤) :
  CategoryTheory.Limits.cokernel
      ((CategoryTheory.Subobject.pullback
              (CategoryTheory.Limits.cokernel.π
                M.arrow)).obj
          B).arrow ≅
    CategoryTheory.Limits.cokernel B.arrow

Something wrong, better idea? Suggest a change

8.2.18. phase_cokernel_le_of_destabilizing_semistable_subobject🔗

If A' is a semistable subobject of E with \phi(E) < \phi(A') and A' \ne \top, then \phi(\operatorname{coker} A') \le \phi(E).

Proof: From the short exact sequence A' \hookrightarrow E \twoheadrightarrow E/A' and the phase see-saw lower bound: \min(\phi(A'), \phi(E/A')) \le \phi(E). Since \phi(A') > \phi(E), the minimum must be \phi(E/A').

🔗theorem
CategoryTheory.phase_cokernel_le_of_destabilizing_semistable_subobject.{v,
    u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  {E : A} {A' : CategoryTheory.Subobject E}
  (hA'_ss : Z.IsSemistable (CategoryTheory.Subobject.underlying.obj A'))
  (hA'_phase :
    Z.phase E < Z.phase (CategoryTheory.Subobject.underlying.obj A'))
  (hA'_top : A' ≠ ⊤) :
  Z.phase (CategoryTheory.Limits.cokernel A'.arrow) ≤ Z.phase E
CategoryTheory.phase_cokernel_le_of_destabilizing_semistable_subobject.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A}
  {A' : CategoryTheory.Subobject E}
  (hA'_ss :
    Z.IsSemistable
      (CategoryTheory.Subobject.underlying.obj
        A'))
  (hA'_phase :
    Z.phase E <
      Z.phase
        (CategoryTheory.Subobject.underlying.obj
          A'))
  (hA'_top : A' ≠ ⊤) :
  Z.phase
      (CategoryTheory.Limits.cokernel
        A'.arrow) ≤
    Z.phase E

Something wrong, better idea? Suggest a change

8.2.19. phase_cokernel_lt_of_destabilizing_semistable_subobject🔗

In the same situation, the quotient has strictly smaller phase: \phi(\operatorname{coker} A') < \phi(E).

Proof: Uses the strict version of the arg-addition inequality: when the two summands have distinct arguments, the inequality \min(\arg z_1, \arg z_2) < \arg(z_1+z_2) is strict. The arguments are distinct because equality would force \phi(A') \le \phi(E), contradicting the destabilizing hypothesis.

🔗theorem
CategoryTheory.phase_cokernel_lt_of_destabilizing_semistable_subobject.{v,
    u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  {E : A} {A' : CategoryTheory.Subobject E}
  (hA'_ss : Z.IsSemistable (CategoryTheory.Subobject.underlying.obj A'))
  (hA'_phase :
    Z.phase E < Z.phase (CategoryTheory.Subobject.underlying.obj A'))
  (hA'_top : A' ≠ ⊤) :
  Z.phase (CategoryTheory.Limits.cokernel A'.arrow) < Z.phase E
CategoryTheory.phase_cokernel_lt_of_destabilizing_semistable_subobject.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A}
  {A' : CategoryTheory.Subobject E}
  (hA'_ss :
    Z.IsSemistable
      (CategoryTheory.Subobject.underlying.obj
        A'))
  (hA'_phase :
    Z.phase E <
      Z.phase
        (CategoryTheory.Subobject.underlying.obj
          A'))
  (hA'_top : A' ≠ ⊤) :
  Z.phase
      (CategoryTheory.Limits.cokernel
        A'.arrow) <
    Z.phase E

Something wrong, better idea? Suggest a change

8.2.20. exists_semistable_quotient_le_phase_of_artinian_noetherian🔗

Every nonzero Artinian--Noetherian object admits a nonzero semistable quotient whose phase is at most the phase of the object.

Proof: Recursive construction: if E is semistable, take the identity. Otherwise find a destabilizing semistable subobject A', pass to E/A' (which has \phi(E/A') < \phi(E)), and recurse. Termination uses WellFoundedGT on the subobject lattice.

🔗theorem
CategoryTheory.exists_semistable_quotient_le_phase_of_artinian_noetherian.{v,
    u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  {E : A} [CategoryTheory.IsArtinianObject E]
  [CategoryTheory.IsNoetherianObject E]
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  ∃ Q p,
    CategoryTheory.Epi p ∧
      ¬CategoryTheory.Limits.IsZero Q ∧
        Z.IsSemistable Q ∧ Z.phase Q ≤ Z.phase E
CategoryTheory.exists_semistable_quotient_le_phase_of_artinian_noetherian.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A}
  [CategoryTheory.IsArtinianObject E]
  [CategoryTheory.IsNoetherianObject E]
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  ∃ Q p,
    CategoryTheory.Epi p ∧
      ¬CategoryTheory.Limits.IsZero Q ∧
        Z.IsSemistable Q ∧
          Z.phase Q ≤ Z.phase E

Something wrong, better idea? Suggest a change

8.2.21. phase_le_of_epi🔗

For a semistable object E, every nonzero epi quotient E \twoheadrightarrow Q satisfies \phi(E) \le \phi(Q).

Proof: The kernel K of p has \phi(K) \le \phi(E) by semistability. If \phi(Q) < \phi(E), the phase see-saw upper bound gives \phi(E) \le \max(\phi(K), \phi(Q)) < \phi(E), a contradiction.

🔗theorem
CategoryTheory.phase_le_of_epi.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {E Q : A} (p : E ⟶ Q)
  [CategoryTheory.Epi p] (hss : Z.IsSemistable E)
  (hQ : ¬CategoryTheory.Limits.IsZero Q) : Z.phase E ≤ Z.phase Q
CategoryTheory.phase_le_of_epi.{v, u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E Q : A} (p : E ⟶ Q)
  [CategoryTheory.Epi p]
  (hss : Z.IsSemistable E)
  (hQ : ¬CategoryTheory.Limits.IsZero Q) :
  Z.phase E ≤ Z.phase Q

Something wrong, better idea? Suggest a change

8.2.22. hom_zero_of_semistable_phase_gt🔗

Hom-vanishing. If E is semistable with \phi(E) > \phi(F) and F is semistable, then every morphism f \colon E \to F is zero.

Proof: If f \ne 0, the image \operatorname{im}(f) is nonzero. By phase_le_of_epi, \phi(E) \le \phi(\operatorname{im} f), and by semistability of F, \phi(\operatorname{im} f) \le \phi(F). This gives \phi(E) \le \phi(F), contradicting \phi(E) > \phi(F).

🔗theorem
CategoryTheory.hom_zero_of_semistable_phase_gt.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {E F : A}
  (hE : Z.IsSemistable E) (hF : Z.IsSemistable F)
  (hph : Z.phase F < Z.phase E) (f : E ⟶ F) : f = 0
CategoryTheory.hom_zero_of_semistable_phase_gt.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E F : A} (hE : Z.IsSemistable E)
  (hF : Z.IsSemistable F)
  (hph : Z.phase F < Z.phase E)
  (f : E ⟶ F) : f = 0

Something wrong, better idea? Suggest a change