Where the rank-zero objects go

Slope.lean puts a nonzero object of rank zero on the negative real axis, by degree_pos_of_rank_zero. This file draws the consequence for the cut of Cutoff.lean: such an object has phase one, the largest a phase can be, and so lies in the torsion class T β for every cutoff β < 1.

That is not a convention chosen here. It is forced by the charge -degree + i · rank, and it is what makes the geometric statement come out right: on a surface the rank-zero coherent sheaves are the torsion sheaves, and Bridgeland's T β contains all of them at every β.

Why the Harder–Narasimhan filtration cannot get in the way

Membership in T β asks for β < φ⁻, not for semistability, so the argument has to reach the last HN factor of a rank-zero object. It is again rank zero: rank is additive and nonnegative, so a subobject and its quotient both inherit rank zero from the whole, and the last HN factor is such a quotient. Hence its phase is one, hence φ⁻ = 1.

theorem CategoryTheory.Triangulated.SlopeData.rank_eq_zero_of_shortExact {A : Type u} [Category.{v, u} A] [Abelian A] (D : SlopeData 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.

theorem CategoryTheory.Triangulated.SlopeData.phase_eq_one_of_rank_zero {A : Type u} [Category.{v, u} A] [Abelian A] (D : SlopeData A) {E : A} (hE : ¬Limits.IsZero E) (h : D.rank E = 0) : D.toStabilityFunction.phase E = 1

A nonzero object of rank zero has phase one. Its charge is -degree, a negative real, and arg of a negative real is π.

theorem CategoryTheory.Triangulated.SlopeData.mem_hnTors_of_rank_zero {A : Type u} [Category.{v, u} A] [Abelian A] (D : SlopeData A) (hHN : D.toStabilityFunction.HasHNProperty) {β : ℝ} (hβ : β < 1) {E : A} (hE : ¬Limits.IsZero E) (h : D.rank E = 0) : E ∈ D.toStabilityFunction.hnTors β

Rank-zero objects are torsion at every cutoff below one. The last Harder–Narasimhan factor of a rank-zero object again has rank zero, so φ⁻ is one.