Weak slopes on an abelian category

PhaseGeometry.lean reads a strict stability function through arg, which is available because semiClosedUpperHalfPlane excludes 0. A weak stability function does not exclude it: a skyscraper on a surface has zero rank and zero degree, so its charge is exactly 0 and arg 0 = 0 carries no information. This file therefore reads a weak stability function through its slope in WithTop ℝ instead, with ⊤ on the whole real boundary.

That choice is not new here. Weak/Basic/Definitions.lean already stores weak slopes in WithTop ℝ, and Weak/HarderNarasimhan/Heart.lean already indexes weak HN filtrations by them, for exactly this reason. What is new is that both of those live on a t-structure, at heartDatum t, and speak through ambient distinguished triangles. This file states the same slope on the abelian side, at abelianDatum A, through subobjects and cokernels, which is the shape the abelian HN development of Uniqueness/ consumes.

Contents

• chargeSlope — the slope of a complex number: -Re/Im when 0 < Im, and ⊤ otherwise. The two see-saw lemmas for it, chargeSlope_le_add_le_of_le and chargeSlope_add_lt_of_lt, are proved on closedUpperHalfPlane and treat ⊤ explicitly. Both need the half-plane, not merely 0 ≤ Im: the boundary case Im = 0 uses Re ≤ 0.
• WeakStabilityFunctionOn.slope, IsSemistable at abelianDatum A.
• slope_le_of_epi — a nonzero quotient of a weak-semistable object has slope at least the source's. This is the weak counterpart of StabilityFunction.phase_le_of_epi, and its proof is shorter: the two see-saw cases split on le_total and neither needs an arg estimate.
• hom_eq_zero_of_semistable_slope_gt — the Hom-vanishing that the HN uniqueness development runs on.

The order convention, stated once

Slopes increase towards ⊤, and ⊤ is the slope of a rank-zero object. An HN filtration therefore stores a strictly decreasing μ : Fin n → WithTop ℝ whose first value may be ⊤, matching WeakAbelianHNFiltration. Nothing below subtracts or adds slopes; they are only ever compared, which is why WithTop ℝ suffices and why the strict development ports.

The slope of a charge value

noncomputable def CategoryTheory.Triangulated.chargeSlope (z : ℂ) : WithTop ℝ

The slope of a charge value: -Re z / Im z when 0 < Im z, and ⊤ otherwise. On closedUpperHalfPlane the second branch is exactly the real boundary, including 0, so a zero-charge object has slope ⊤ rather than an undefined argument.

Equations

• CategoryTheory.Triangulated.chargeSlope z = if 0 < z.im then ↑(-z.re / z.im) else ⊤

theorem CategoryTheory.Triangulated.chargeSlope_of_im_pos {z : ℂ} (h : 0 < z.im) : chargeSlope z = ↑(-z.re / z.im)

theorem CategoryTheory.Triangulated.chargeSlope_of_im_nonpos {z : ℂ} (h : ¬0 < z.im) : chargeSlope z = ⊤

theorem CategoryTheory.Triangulated.chargeSlope_ne_top_iff {z : ℂ} : chargeSlope z ≠ ⊤ ↔ 0 < z.im

theorem CategoryTheory.Triangulated.chargeSlope_lt_top_iff {z : ℂ} : chargeSlope z < ⊤ ↔ 0 < z.im

theorem CategoryTheory.Triangulated.im_pos_of_chargeSlope_lt {z w : ℂ} (h : chargeSlope z < chargeSlope w) : 0 < z.im

Positive imaginary part on the left of a strict slope comparison.

theorem CategoryTheory.Triangulated.im_nonneg_of_mem_closedUpperHalfPlane {z : ℂ} (hz : z ∈ closedUpperHalfPlane) : 0 ≤ z.im

Membership in the closed upper half-plane bounds the imaginary part.

theorem CategoryTheory.Triangulated.re_nonpos_of_mem_closedUpperHalfPlane_of_im_eq_zero {z : ℂ} (hz : z ∈ closedUpperHalfPlane) (him : z.im = 0) : z.re ≤ 0

The real part is nonpositive on the boundary of the closed upper half-plane.

theorem CategoryTheory.Triangulated.chargeSlope_le_add_le_of_le {z w : ℂ} (hz : z ∈ closedUpperHalfPlane) (hw : w ∈ closedUpperHalfPlane) (h : chargeSlope z ≤ chargeSlope w) : chargeSlope z ≤ chargeSlope (z + w) ∧ chargeSlope (z + w) ≤ chargeSlope w

The non-strict see-saw. If the two ends of a short exact sequence have ordered slopes, the middle slope lies between them. Three cases: both interior, one on the boundary, both on the boundary. The ⊤ branch is where the weak theory differs from the strict one, and it is handled rather than excluded.

theorem CategoryTheory.Triangulated.chargeSlope_add_lt_of_lt {z w : ℂ} (hz : z ∈ closedUpperHalfPlane) (h : chargeSlope w < chargeSlope z) : chargeSlope (z + w) < chargeSlope z

The strict see-saw. If the quotient end is strictly below the sub end, the middle is strictly below the sub end too. Both ⊤ cases are decided by im_pos_of_chargeSlope_lt.

@[reducible, inline]

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

The central charge on objects.

Equations

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

@[simp]

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

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.charge_mem {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) (E : A) (hE : ¬Limits.IsZero E) : W.charge E ∈ closedUpperHalfPlane

Nonzero objects have charge in the closed upper half-plane.

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

Zero objects have zero charge.

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

Isomorphic objects have the same charge.

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

The charge is additive on short exact sequences.

noncomputable def CategoryTheory.Triangulated.WeakStabilityFunctionOn.slope {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) (E : A) : WithTop ℝ

The weak slope of an object, in WithTop ℝ, with ⊤ exactly on the real boundary of the closed upper half-plane — in particular at charge 0.

Equations

• W.slope E = CategoryTheory.Triangulated.chargeSlope (W.charge E)

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.slope_eq_chargeSlope {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) (E : A) : W.slope E = chargeSlope (W.charge E)

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.slope_of_im_pos {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) {E : A} (h : 0 < (W.charge E).im) : W.slope E = ↑(-(W.charge E).re / (W.charge E).im)

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.slope_of_im_nonpos {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) {E : A} (h : ¬0 < (W.charge E).im) : W.slope E = ⊤

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.slope_eq_top_of_charge_eq_zero {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) {E : A} (h : W.charge E = 0) : W.slope E = ⊤

A zero-charge object has slope ⊤. This is the skyscraper, and it is the case a phase-indexed weak cutoff cannot express.

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.slope_eq_of_iso {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) {E F : A} (e : E ≅ F) : W.slope E = W.slope F

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

Weak semistability: no nonzero subobject has slope above the object's own. The comparison is in WithTop ℝ, so a rank-zero subobject of slope ⊤ forces the ambient slope to be ⊤ as well.

Equations

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

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

Weak stability: every nonzero proper subobject has strictly smaller slope.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.IsStable.isSemistable {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) {E : A} (h : W.IsStable E) : W.IsSemistable E

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

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

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.slope_le_of_epi {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) {E Q : A} (p : E ⟶ Q) [Epi p] (hE : W.IsSemistable E) (hQ : ¬Limits.IsZero Q) : W.slope E ≤ W.slope Q

A nonzero quotient of a weak-semistable object has slope at least the source's.

The weak counterpart of StabilityFunction.phase_le_of_epi, and shorter: the kernel's slope is bounded by semistability, and the two see-saws decide the remaining comparison by le_total without any arg estimate.

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.hom_eq_zero_of_semistable_slope_gt {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) {E F : A} (hE : W.IsSemistable E) (hF : W.IsSemistable F) (hslope : W.slope F < W.slope E) (f : E ⟶ F) : f = 0

Hom-vanishing between weak-semistable objects of decreasing slope. The image is a quotient of the source and a subobject of the target, so its slope is trapped; a strict slope drop leaves no room for it.