The maximally destabilizing subobject and the extremal phase functions

This file owns the public interface built on the uniqueness argument: the canonical maximally destabilizing subobject of a nonzero object, its destabilizing quotient and the short exact sequence they form, and the extremal phase functions phiPlus and phiMinus with the characterisation of semistability as their equality.

This is the module a consumer of the uniqueness milestone should import.

noncomputable def CategoryTheory.Triangulated.StabilityFunction.maxDestabilizingSubobject {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) (E : A) (hE : ¬Limits.IsZero E) : Subobject E

The canonical maximally destabilizing subobject of a nonzero object.

Equations

• Z.maxDestabilizingSubobject hHN E hE = (Classical.choice ⋯).chain ⟨1, ⋯⟩

theorem CategoryTheory.Triangulated.StabilityFunction.maxDestabilizingSubobject_eq_filtration {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) {E : A} (hE : ¬Limits.IsZero E) (F : AbelianHNFiltration Z E) : Z.maxDestabilizingSubobject hHN E hE = F.chain ⟨1, ⋯⟩

The canonical maximally destabilizing subobject agrees with the first nonzero term of every owner HN filtration.

theorem CategoryTheory.Triangulated.StabilityFunction.maxDestabilizingSubobject_ne_bot {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) (E : A) (hE : ¬Limits.IsZero E) : Z.maxDestabilizingSubobject hHN E hE ≠ ⊥

The canonical maximally destabilizing subobject is nonzero.

theorem CategoryTheory.Triangulated.StabilityFunction.maxDestabilizingSubobject_isSemistable {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) (E : A) (hE : ¬Limits.IsZero E) : Z.IsSemistable (Subobject.underlying.obj (Z.maxDestabilizingSubobject hHN E hE))

The canonical maximally destabilizing subobject is semistable.

theorem CategoryTheory.Triangulated.StabilityFunction.maxDestabilizingSubobject_eq_top_iff_isSemistable {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) (E : A) (hE : ¬Limits.IsZero E) : Z.maxDestabilizingSubobject hHN E hE = ⊤ ↔ Z.IsSemistable E

A nonzero object is semistable exactly when its canonical maximally destabilizing subobject is the whole object.

noncomputable def CategoryTheory.Triangulated.StabilityFunction.destabilizingQuotient {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) (E : A) (hE : ¬Limits.IsZero E) : A

The quotient left after removing the canonical maximally destabilizing subobject.

Equations

• Z.destabilizingQuotient hHN E hE = CategoryTheory.Limits.cokernel (Z.maxDestabilizingSubobject hHN E hE).arrow

theorem CategoryTheory.Triangulated.StabilityFunction.isZero_destabilizingQuotient_iff_isSemistable {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) (E : A) (hE : ¬Limits.IsZero E) : Limits.IsZero (Z.destabilizingQuotient hHN E hE) ↔ Z.IsSemistable E

The destabilizing quotient is zero exactly for semistable objects.

theorem CategoryTheory.Triangulated.StabilityFunction.destabilizingQuotient_not_isZero_of_not_isSemistable {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) (E : A) (hE : ¬Limits.IsZero E) (hnot : ¬Z.IsSemistable E) : ¬Limits.IsZero (Z.destabilizingQuotient hHN E hE)

A non-semistable object has a nonzero destabilizing quotient.

noncomputable def CategoryTheory.Triangulated.StabilityFunction.destabilizingShortComplex {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) (E : A) (hE : ¬Limits.IsZero E) : ShortComplex A

The canonical short complex presenting an object as an extension of its maximally destabilizing subobject by the destabilizing quotient.

Equations

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

theorem CategoryTheory.Triangulated.StabilityFunction.destabilizingShortComplex_shortExact {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) (E : A) (hE : ¬Limits.IsZero E) : (Z.destabilizingShortComplex hHN E hE).ShortExact

The canonical destabilizing short complex is short exact.

theorem CategoryTheory.Triangulated.StabilityFunction.charge_eq_maxDestabilizingSubobject_add_destabilizingQuotient {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) (E : A) (hE : ¬Limits.IsZero E) : Z.charge E = Z.charge (Subobject.underlying.obj (Z.maxDestabilizingSubobject hHN E hE)) + Z.charge (Z.destabilizingQuotient hHN E hE)

The central charge splits across the canonical destabilizing short exact sequence.

noncomputable def CategoryTheory.Triangulated.StabilityFunction.phiPlus {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) (E : A) (hE : ¬Limits.IsZero E) : ℝ

The intrinsic highest HN phase of a nonzero object.

Equations

• Z.phiPlus hHN E hE = (Classical.choice ⋯).phiPlus

noncomputable def CategoryTheory.Triangulated.StabilityFunction.phiMinus {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) (E : A) (hE : ¬Limits.IsZero E) : ℝ

The intrinsic lowest HN phase of a nonzero object.

Equations

• Z.phiMinus hHN E hE = (Classical.choice ⋯).phiMinus

theorem CategoryTheory.Triangulated.StabilityFunction.phiPlus_eq_filtration {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) {E : A} (hE : ¬Limits.IsZero E) (F : AbelianHNFiltration Z E) : Z.phiPlus hHN E hE = F.phiPlus

The intrinsic highest phase agrees with every owner HN filtration.

theorem CategoryTheory.Triangulated.StabilityFunction.phase_maxDestabilizingSubobject {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) (E : A) (hE : ¬Limits.IsZero E) : Z.phase (Subobject.underlying.obj (Z.maxDestabilizingSubobject hHN E hE)) = Z.phiPlus hHN E hE

The canonical maximally destabilizing subobject has the intrinsic highest HN phase.

theorem CategoryTheory.Triangulated.StabilityFunction.le_maxDestabilizingSubobject_of_semistable_phase_eq_phiPlus {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) {E : A} (hE : ¬Limits.IsZero E) {B : Subobject E} (hB : Z.IsSemistable (Subobject.underlying.obj B)) (hphase : Z.phase (Subobject.underlying.obj B) = Z.phiPlus hHN E hE) : B ≤ Z.maxDestabilizingSubobject hHN E hE

Every semistable subobject at the intrinsic highest HN phase lies in the canonical maximally destabilizing subobject.

theorem CategoryTheory.Triangulated.StabilityFunction.phiMinus_eq_filtration {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) {E : A} (hE : ¬Limits.IsZero E) (F : AbelianHNFiltration Z E) : Z.phiMinus hHN E hE = F.phiMinus

The intrinsic lowest phase agrees with every owner HN filtration.

theorem CategoryTheory.Triangulated.StabilityFunction.phiMinus_le_phiPlus {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) (E : A) (hE : ¬Limits.IsZero E) : Z.phiMinus hHN E hE ≤ Z.phiPlus hHN E hE

The intrinsic lowest HN phase is at most the intrinsic highest phase.

theorem CategoryTheory.Triangulated.StabilityFunction.isSemistable_iff_phiPlus_eq_phiMinus {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (hHN : Z.HasHNProperty) (E : A) (hE : ¬Limits.IsZero E) : Z.IsSemistable E ↔ Z.phiPlus hHN E hE = Z.phiMinus hHN E hE

A nonzero object is semistable exactly when its intrinsic HN phase interval degenerates to a point.