Stability functions on abelian categories

This file introduces the repository-owned stability-function interface. Its central charge is additive on short exact sequences and sends every nonzero object to the semi-closed upper half-plane. Phase, stability, and semistability are then defined intrinsically from that charge.

The module is Mathlib-only and is the canonical stability-function interface for this repository.

structure CategoryTheory.Triangulated.StabilityFunctionOn {O : Type u_1} {G : Type u_2} [AddCommGroup G] (D : ClassDatum O G) : Type u_2

A stability function relative to a class datum. One structure; the abelian and ambient theories are two instantiations of it.

• Z : G →+ ℂ

  The central charge, as a hom out of the class group.

• nonzero_mem : IsStabilityCharge D self.Z

  Relevant objects have charge in the strict half-plane.

structure CategoryTheory.Triangulated.WeakStabilityFunctionOn {O : Type u_1} {G : Type u_2} [AddCommGroup G] (D : ClassDatum O G) : Type u_2

A weak stability function relative to a class datum.

• Z : G →+ ℂ

  The central charge, as a hom out of the class group.

• nonzero_mem : IsWeakStabilityCharge D self.Z

  Relevant objects have charge in the closed half-plane.

def CategoryTheory.Triangulated.StabilityFunctionOn.toWeak {O : Type u_1} {G : Type u_2} [AddCommGroup G] {D : ClassDatum O G} (Z : StabilityFunctionOn D) : WeakStabilityFunctionOn D

Every stability function is a weak one, at any class datum.

Equations

• Z.toWeak = { Z := Z.Z, nonzero_mem := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.StabilityFunctionOn.toWeak_Z {O : Type u_1} {G : Type u_2} [AddCommGroup G] {D : ClassDatum O G} (Z : StabilityFunctionOn D) : Z.toWeak.Z = Z.Z

def CategoryTheory.Triangulated.abelianDatum (A : Type u) [Category.{v, u} A] [Abelian A] : ClassDatum A (K₀Ab A)

The class datum of an abelian category: nonzero objects, classes in K₀Ab.

Equations

• CategoryTheory.Triangulated.abelianDatum A = { Relevant := fun (E : A) => ¬CategoryTheory.Limits.IsZero E, cl := CategoryTheory.K₀Ab.of }

@[reducible, inline]

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

An additive central charge on an abelian category whose nonzero values lie in the semi-closed upper half-plane.

This is StabilityFunctionOn at abelianDatum, not a structure of its own. charge remains available as an abbreviation and map_zero / map_iso / additive remain available as theorems, so consumers are unaffected.

Equations

• CategoryTheory.Triangulated.StabilityFunction A = CategoryTheory.Triangulated.StabilityFunctionOn (CategoryTheory.Triangulated.abelianDatum A)

@[simp]

theorem CategoryTheory.Triangulated.abelianDatum_cl {A : Type u} [Category.{v, u} A] [Abelian A] (E : A) : (abelianDatum A).cl E = K₀Ab.of E

@[simp]

theorem CategoryTheory.Triangulated.abelianDatum_relevant {A : Type u} [Category.{v, u} A] [Abelian A] (E : A) : (abelianDatum A).Relevant E ↔ ¬Limits.IsZero E

@[reducible, inline]

abbrev CategoryTheory.Triangulated.StabilityFunction.charge {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (E : A) : ℂ

The central charge on objects.

Equations

• Z.charge E = Z.Z (CategoryTheory.K₀Ab.of E)

@[simp]

theorem CategoryTheory.Triangulated.StabilityFunction.charge_apply {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (E : A) : Z.charge E = Z.Z (K₀Ab.of E)

theorem CategoryTheory.Triangulated.StabilityFunction.map_zero {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (E : A) (hE : Limits.IsZero E) : Z.charge E = 0

Zero objects have zero charge — a theorem now, not a field.

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

Isomorphic objects have the same charge — a theorem now, not a field.

theorem CategoryTheory.Triangulated.StabilityFunction.additive {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (S : ShortComplex A) (hS : S.ShortExact) : Z.charge S.X₂ = Z.charge S.X₁ + Z.charge S.X₃

The charge is additive on short exact sequences — a theorem now, not a field.

theorem CategoryTheory.Triangulated.StabilityFunction.ext {A : Type u} [Category.{v, u} A] [Abelian A] {Z W : StabilityFunction A} (hcharge : Z.charge = W.charge) : Z = W

Two stability functions with the same charge on objects are equal. This now needs K₀Ab.hom_ext rather than structure eta: equal charges on generators is what forces the two homs to agree.

theorem CategoryTheory.Triangulated.StabilityFunction.ext_iff {A : Type u} [Category.{v, u} A] [Abelian A] {Z W : StabilityFunction A} : Z = W ↔ Z.charge = W.charge

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

The phase of an object, normalized to lie in (0, 1] when the object is nonzero. The phase of a zero object is 0.

Equations

• Z.phase E = (Z.charge E).arg / Real.pi

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

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

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

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

A nonzero object is semistable when no nonzero subobject has larger phase.

Equations

• One or more equations did not get rendered due to their size.

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

A nonzero object is stable when every nonzero proper subobject has strictly smaller phase.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.StabilityFunction.exists_destabilizing_of_not_semistable {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (E : A) (hE : ¬Limits.IsZero E) (h : ¬Z.IsSemistable E) : ∃ (B : Subobject E), ¬Limits.IsZero (Subobject.underlying.obj B) ∧ Z.phase E < Z.phase (Subobject.underlying.obj B)

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

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

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

theorem CategoryTheory.Triangulated.StabilityFunction.isSemistable_iff_of_iso {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) {E F : A} (e : E ≅ F) : Z.IsSemistable E ↔ Z.IsSemistable F