8.3. StabilityFunction: MDQ🔗

8.3.1. IsMDQ🔗

A quotient q \colon E \twoheadrightarrow B is a maximally destabilizing quotient (MDQ) if q is epi, B is a nonzero semistable object of minimal phase among all semistable quotients of E, and whenever another semistable quotient B' has the same phase as B, the map q' factors through q.

Construction: The structure carries Epi q, non-zeroness and semistability of B, and a universal property: for every epi q' \colon E \twoheadrightarrow B' with B' nonzero semistable, \phi(B) \le \phi(B'), and equality implies factorisation q' = q \circ t.

structure

CategoryTheory.IsMDQ.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {E B : A} (q : E ⟶ B) : Prop
CategoryTheory.IsMDQ.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E B : A} (q : E ⟶ B) : Prop

Constructor

CategoryTheory.IsMDQ.mk.{v, u}

Fields

epi : CategoryTheory.Epi q

nonzero : ¬CategoryTheory.Limits.IsZero B

semistable : Z.IsSemistable B

minimal : ∀ {B' : A} (q' : E ⟶ B'),
  CategoryTheory.Epi q' →
    ¬CategoryTheory.Limits.IsZero B' →
      Z.IsSemistable B' →
        Z.phase B ≤ Z.phase B' ∧ (Z.phase B' = Z.phase B → ∃ t, q' = CategoryTheory.CategoryStruct.comp q t)

Something wrong, better idea? Suggest a change

8.3.2. exists_mdq_of_artinian_noetherian🔗

Existence of MDQ. Every nonzero Artinian--Noetherian object admits a maximally destabilizing quotient.

Proof: Well-founded induction on the subobject lattice (via WellFoundedGT). If E is semistable, the identity is an MDQ. Otherwise, find a destabilizing semistable subobject A', pass to \operatorname{coker}(A') (which is Artinian--Noetherian by isArtinianObject_of_epi and isNoetherianObject_of_epi), recurse to get an MDQ there, and pull it back to E via IsMDQ.comp_of_destabilizing_semistable_subobject.

theorem

CategoryTheory.exists_mdq_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) :
  ∃ B q, CategoryTheory.IsMDQ Z q
CategoryTheory.exists_mdq_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) :
  ∃ B q, CategoryTheory.IsMDQ Z q

Something wrong, better idea? Suggest a change

8.3.3. cokernelKernelSubobjectIsoTarget🔗

For an epimorphism q \colon E \twoheadrightarrow B, the quotient E / \ker(q) is canonically isomorphic to B.

Construction: Constructed by composing the cokernel-of-kernel-subobject isomorphism with the coimage--image isomorphism and the image-subobject isomorphism.

def

CategoryTheory.cokernelKernelSubobjectIsoTarget.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  {E B : A} (q : E ⟶ B) [CategoryTheory.Epi q] :
  CategoryTheory.Limits.cokernel
      (CategoryTheory.Limits.kernelSubobject q).arrow ≅
    B
CategoryTheory.cokernelKernelSubobjectIsoTarget.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] {E B : A}
  (q : E ⟶ B) [CategoryTheory.Epi q] :
  CategoryTheory.Limits.cokernel
      (CategoryTheory.Limits.kernelSubobject
          q).arrow ≅
    B

Something wrong, better idea? Suggest a change

8.3.4. lt_phase_of_kernel_mdq🔗

Kernel-step inequality (Bridgeland, Proposition 2.4e). If q \colon E \twoheadrightarrow B is an MDQ and q_K \colon \ker(q) \twoheadrightarrow B' is an MDQ of the kernel, then \phi(B) < \phi(B').

Proof: Let K = \ker(q), K' = \ker(q_K), T = K' pushed into E, and Q = E/T. The map Q \twoheadrightarrow B factors through q but K \to Q is nonzero (since T \ne K), so \phi(Q) \ne \phi(B) by the MDQ factorisation property. The MDQ bound gives \phi(B) \le \phi(Q), and the Z-value decomposition Z(Q) = Z(B') + Z(B) with the arg convexity bound shows \phi(Q) \le \max(\phi(B'), \phi(B)) = \phi(B) would hold if \phi(B') \le \phi(B), contradicting \phi(B) < \phi(Q).

theorem

CategoryTheory.IsMDQ.lt_phase_of_kernel_mdq.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {E B B' : A}
  [CategoryTheory.IsArtinianObject E]
  [CategoryTheory.IsNoetherianObject E] {q : E ⟶ B}
  (hq : CategoryTheory.IsMDQ Z q)
  {qK :
    CategoryTheory.Subobject.underlying.obj
        (CategoryTheory.Limits.kernelSubobject q) ⟶
      B'}
  (hqK : CategoryTheory.IsMDQ Z qK) : Z.phase B < Z.phase B'
CategoryTheory.IsMDQ.lt_phase_of_kernel_mdq.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E B B' : A}
  [CategoryTheory.IsArtinianObject E]
  [CategoryTheory.IsNoetherianObject E]
  {q : E ⟶ B}
  (hq : CategoryTheory.IsMDQ Z q)
  {qK :
    CategoryTheory.Subobject.underlying.obj
        (CategoryTheory.Limits.kernelSubobject
          q) ⟶
      B'}
  (hqK : CategoryTheory.IsMDQ Z qK) :
  Z.phase B < Z.phase B'

Something wrong, better idea? Suggest a change

8.3.5. phase_cokernel_mapMono_eq🔗

For a monomorphism f \colon X \hookrightarrow Y and subobjects S \le T of X, the phase of \operatorname{coker}(f_*(S) \hookrightarrow f_*(T)) equals \phi(\operatorname{coker}(S \hookrightarrow T)).

Proof: The two cokernels are isomorphic via the natural map induced by f.

theorem

CategoryTheory.phase_cokernel_mapMono_eq.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {X Y : A} (f : X ⟶ Y)
  [CategoryTheory.Mono f] {S T : CategoryTheory.Subobject X}
  (h : S ≤ T) :
  Z.phase
      (CategoryTheory.Limits.cokernel
        (((CategoryTheory.Subobject.map f).obj S).ofLE
          ((CategoryTheory.Subobject.map f).obj T) ⋯)) =
    Z.phase (CategoryTheory.Limits.cokernel (S.ofLE T h))
CategoryTheory.phase_cokernel_mapMono_eq.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {X Y : A} (f : X ⟶ Y)
  [CategoryTheory.Mono f]
  {S T : CategoryTheory.Subobject X}
  (h : S ≤ T) :
  Z.phase
      (CategoryTheory.Limits.cokernel
        (((CategoryTheory.Subobject.map
                  f).obj
              S).ofLE
          ((CategoryTheory.Subobject.map
                f).obj
            T)
          ⋯)) =
    Z.phase
      (CategoryTheory.Limits.cokernel
        (S.ofLE T h))

Something wrong, better idea? Suggest a change

8.3.6. isSemistable_cokernel_mapMono_iff🔗

Semistability of \operatorname{coker}(f_*(S) \hookrightarrow f_*(T)) is equivalent to semistability of \operatorname{coker}(S \hookrightarrow T), for a mono f.

Proof: Transport via isSemistable_of_iso in both directions using Subobject.cokernelMapMonoIso.

theorem

CategoryTheory.isSemistable_cokernel_mapMono_iff.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {X Y : A} (f : X ⟶ Y)
  [CategoryTheory.Mono f] {S T : CategoryTheory.Subobject X}
  (h : S ≤ T) :
  Z.IsSemistable
      (CategoryTheory.Limits.cokernel
        (((CategoryTheory.Subobject.map f).obj S).ofLE
          ((CategoryTheory.Subobject.map f).obj T) ⋯)) ↔
    Z.IsSemistable (CategoryTheory.Limits.cokernel (S.ofLE T h))
CategoryTheory.isSemistable_cokernel_mapMono_iff.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {X Y : A} (f : X ⟶ Y)
  [CategoryTheory.Mono f]
  {S T : CategoryTheory.Subobject X}
  (h : S ≤ T) :
  Z.IsSemistable
      (CategoryTheory.Limits.cokernel
        (((CategoryTheory.Subobject.map
                  f).obj
              S).ofLE
          ((CategoryTheory.Subobject.map
                f).obj
            T)
          ⋯)) ↔
    Z.IsSemistable
      (CategoryTheory.Limits.cokernel
        (S.ofLE T h))

Something wrong, better idea? Suggest a change

8.3.7. append_hn_filtration_of_mono🔗

Given a monomorphism i \colon X \hookrightarrow Y, an HN filtration F of X, a semistable quotient B \cong \operatorname{coker}(i) with \phi(B) < \phi_{n-1}(F), one can append B to produce an HN filtration of Y.

Proof: Push the chain of F forward via \operatorname{Subobject.map}(i) and append \top. The last factor is B, and the phase bound ensures strict anti-monotonicity is preserved.

theorem

CategoryTheory.append_hn_filtration_of_mono.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {X Y B : A} (i : X ⟶ Y)
  [CategoryTheory.Mono i] (F : CategoryTheory.AbelianHNFiltration Z X)
  (eB : CategoryTheory.Limits.cokernel i ≅ B) (hB : Z.IsSemistable B)
  (hlast : Z.phase B < F.φ ⟨F.n - 1, ⋯⟩) :
  ∃ G, G.φ ⟨G.n - 1, ⋯⟩ = Z.phase B
CategoryTheory.append_hn_filtration_of_mono.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {X Y B : A} (i : X ⟶ Y)
  [CategoryTheory.Mono i]
  (F :
    CategoryTheory.AbelianHNFiltration Z
      X)
  (eB :
    CategoryTheory.Limits.cokernel i ≅ B)
  (hB : Z.IsSemistable B)
  (hlast : Z.phase B < F.φ ⟨F.n - 1, ⋯⟩) :
  ∃ G, G.φ ⟨G.n - 1, ⋯⟩ = Z.phase B

Something wrong, better idea? Suggest a change

8.3.8. exists_hn_with_last_phase_of_semistable🔗

A semistable object has an HN filtration whose last (and only) phase equals \phi(E).

Proof: Construct the trivial single-factor filtration \bot < \top with phase \phi(E).

theorem

CategoryTheory.exists_hn_with_last_phase_of_semistable.{v, u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  {E : A} (hss : Z.IsSemistable E) : ∃ F, F.φ ⟨F.n - 1, ⋯⟩ = Z.phase E
CategoryTheory.exists_hn_with_last_phase_of_semistable.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A} (hss : Z.IsSemistable E) :
  ∃ F, F.φ ⟨F.n - 1, ⋯⟩ = Z.phase E

Something wrong, better idea? Suggest a change

8.3.9. exists_hn_of_semistable🔗

A semistable object admits an HN filtration.

Proof: Immediate from exists_hn_with_last_phase_of_semistable.

theorem

CategoryTheory.exists_hn_of_semistable.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A) {E : A}
  (hss : Z.IsSemistable E) :
  Nonempty (CategoryTheory.AbelianHNFiltration Z E)
CategoryTheory.exists_hn_of_semistable.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  {E : A} (hss : Z.IsSemistable E) :
  Nonempty
    (CategoryTheory.AbelianHNFiltration Z
      E)

Something wrong, better idea? Suggest a change

8.3.10. ofIso🔗

An HN filtration can be transported along an isomorphism E \cong E'.

Construction: Push the chain forward via Subobject.map(e.hom) and transfer phases and semistability via phase_cokernel_mapMono_eq and isSemistable_cokernel_mapMono_iff.

def

CategoryTheory.AbelianHNFiltration.ofIso.{v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  {Z : CategoryTheory.StabilityFunction A} {E E' : A}
  (F : CategoryTheory.AbelianHNFiltration Z E) (e : E ≅ E') :
  CategoryTheory.AbelianHNFiltration Z E'
CategoryTheory.AbelianHNFiltration.ofIso.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  {Z : CategoryTheory.StabilityFunction A}
  {E E' : A}
  (F :
    CategoryTheory.AbelianHNFiltration Z
      E)
  (e : E ≅ E') :
  CategoryTheory.AbelianHNFiltration Z E'

Something wrong, better idea? Suggest a change

8.3.11. hasHN_of_artinian_noetherian🔗

Proposition 2.4 (Bridgeland, Artinian--Noetherian form). If every object of \mathcal{A} is both Artinian and Noetherian, then any stability function on \mathcal{A} has the HN property.

Proof: Reduce to the subobject case via the canonical isomorphism \operatorname{Subobject.mk}(\mathrm{id}_E) \cong E. The recursive construction uses maximally destabilizing quotients (MDQ): for a non-semistable object, find a destabilizing semistable subobject, pass to the quotient, recurse to get an MDQ there, and pull back. The kernel-step inequality (IsMDQ.lt_phase_of_kernel_mdq) ensures the phases decrease, and append_hn_filtration_of_mono concatenates the pieces.

theorem

CategoryTheory.StabilityFunction.hasHN_of_artinian_noetherian.{v, u}
  {A : Type u} [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A] (Z : CategoryTheory.StabilityFunction A)
  (hArt : ∀ (E : A), CategoryTheory.IsArtinianObject E)
  (hNoeth : ∀ (E : A), CategoryTheory.IsNoetherianObject E) :
  Z.HasHNProperty
CategoryTheory.StabilityFunction.hasHN_of_artinian_noetherian.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  [CategoryTheory.Abelian A]
  (Z : CategoryTheory.StabilityFunction A)
  (hArt :
    ∀ (E : A),
      CategoryTheory.IsArtinianObject E)
  (hNoeth :
    ∀ (E : A),
      CategoryTheory.IsNoetherianObject
        E) :
  Z.HasHNProperty

Something wrong, better idea? Suggest a change