Where the rank-zero objects go, on a surface

SlopeCutoff.lean answers this question on a curve: degree_pos_of_rank_zero puts a nonzero rank-zero object on the strictly negative real axis, so it has phase one, so it lies in T β for every β < 1. On a surface that argument is unavailable — a skyscraper has c₁ = 0, hence degree 0, hence charge exactly 0, and arg 0 = 0 is not a phase. WeakSlope.lean says so explicitly and leaves the question open.

WeakSlopeTop.lean supplies the slope that can answer it, topSlope, valued in WithTop ℝ and ⊤ at rank zero. This file draws the consequence for the cut of WeakCutoff.lean, which is what that slope was for.

The comparison, which is the point

	curve (SlopeData)	surface (WeakSlopeData)
cutoff	β : ℝ, restricted to β < 1	μ₀ : WithTop ℝ, restricted to μ₀ ≠ ⊤
rank zero gives	φ⁻ = 1	μ⁻ = ⊤
needs	degree_pos_of_rank_zero	nothing beyond rank_nonneg

The Harder--Narasimhan filtration cannot get in the way for the same reason it could not on a curve: rank is additive and nonnegative, so rank zero passes to every subobject and quotient, hence to the last HN factor, hence μ⁻ = ⊤. rank_eq_zero_of_shortExact is that step and is omega on two inequalities.

Note what mem_hnTors_of_rank_zero does not ask for. It has no semistability hypothesis, and no hypothesis on the degree — so it holds for a skyscraper, whose charge is 0 and which therefore has no phase to be compared at all. That is strictly more than the curve statement can express, rather than a transcription of it.

What is here beyond WeakSlopeTop.lean

That file defines topSlope and pins its two values. This one adds the facts that need rank_nonneg as well — that ⊤ occurs at rank zero and nowhere else, and the order comparisons that follow — and then the cutoff consequence.

theorem CategoryTheory.Triangulated.WeakSlopeData.rank_eq_zero_of_shortExact {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) {S : ShortComplex A} (hS : S.ShortExact) (h : D.rank S.X₂ = 0) : D.rank S.X₁ = 0 ∧ D.rank S.X₃ = 0

Rank zero passes to both ends of a short exact sequence, because rank is additive and never negative. The SlopeData proof, which never reads the degree field and so did not need the curve hypothesis.

⊤ occurs at rank zero and nowhere else

WeakSlopeTop.lean proves each value in its own case. Combining them into an iff is where rank_nonneg enters: without it a negative rank would be a third case, and the charge would leave the closed upper half-plane.

theorem CategoryTheory.Triangulated.WeakSlopeData.topSlope_eq_top_iff_rank_eq_zero {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) {E : A} : D.topSlope E = ⊤ ↔ D.rank E = 0

The honest slope is ⊤ on exactly the rank-zero objects.

theorem CategoryTheory.Triangulated.WeakSlopeData.topSlope_ne_top_iff_rank_pos {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) {E : A} : D.topSlope E ≠ ⊤ ↔ 0 < D.rank E

The order, restated in WithTop ℝ

theorem CategoryTheory.Triangulated.WeakSlopeData.topSlope_le_topSlope_iff_slope_le {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) {E F : A} (hE : 0 < D.rank E) (hF : 0 < D.rank F) : D.topSlope E ≤ D.topSlope F ↔ D.slope E ≤ D.slope F

The honest slope order and the ℝ-valued slope order agree on objects of positive rank, where both are defined.

theorem CategoryTheory.Triangulated.WeakSlopeData.phase_le_iff_topSlope_le {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) {E F : A} (hE : 0 < D.rank E) (hF : 0 < D.rank F) : D.phase E ≤ D.phase F ↔ D.topSlope E ≤ D.topSlope F

The phase order is the honest slope order on objects of positive rank. WeakSlope.lean's phase_le_iff_slope_le, carried into WithTop ℝ.

theorem CategoryTheory.Triangulated.WeakSlopeData.topSlope_lt_topSlope_of_rank_pos_of_rank_zero {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) {E F : A} (hE : 0 < D.rank E) (hF : D.rank F = 0) : D.topSlope E < D.topSlope F

A rank-zero object has honest slope above every positive-rank object's. On a surface this is the whole ordering statement available about a skyscraper, and no phase comparison can reproduce it.

Rank zero is torsion at every finite cutoff

theorem CategoryTheory.Triangulated.WeakSlopeData.μMinus_eq_top_of_rank_zero {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) {E : A} (F : AbelianWeakHNFiltration D.toWeakStabilityFunction E) (h : D.rank E = 0) : F.μMinus = ⊤

Every Harder--Narasimhan factor of a rank-zero object has rank zero, so the lowest HN slope is ⊤. Rank is additive and nonnegative, so rank zero passes to each chain step and to its cokernel.

theorem CategoryTheory.Triangulated.WeakSlopeData.mem_hnTors_of_rank_zero {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) (hHN : D.toWeakStabilityFunction.HasHNProperty) {μ₀ : WithTop ℝ} (hμ : μ₀ ≠ ⊤) {E : A} (hE : ¬Limits.IsZero E) (h : D.rank E = 0) : E ∈ D.toWeakStabilityFunction.hnTors μ₀

Rank-zero objects are torsion at every finite cutoff.

The surface counterpart of SlopeData.mem_hnTors_of_rank_zero, and strictly stronger where the two overlap: that one needs degree_pos_of_rank_zero to reach phase one and so restricts to β < 1, while this one reads μ⁻ = ⊤ off rank_nonneg alone and so covers every cutoff short of ⊤ itself.

The curve case inherits

SlopeData.toWeakSlopeData forgets 0 < degree to 0 ≤ degree, so a curve lane gets the WithTop ℝ slope and everything above without a second development.

theorem CategoryTheory.Triangulated.SlopeData.toWeakSlopeData_topSlope_eq_top_iff {A : Type u} [Category.{v, u} A] [Abelian A] (D : SlopeData A) {E : A} : D.toWeakSlopeData.topSlope E = ⊤ ↔ D.rank E = 0

On a curve too, the honest slope is ⊤ exactly at rank zero.