μ-slope on a surface: the weak slope data

SlopeData is the curve case, and its own docstring says so: its field degree_pos_of_rank_zero is false on a surface, where a skyscraper has c₁ = 0 and hence degree 0. This file supplies the structure a surface lane may instantiate.

The single difference

SlopeData      degree_pos_of_rank_zero    : … → 0 < degree E
WeakSlopeData  degree_nonneg_of_rank_zero : … → 0 ≤ degree E

That 0 ≤ in place of 0 < is the whole of the weakening, and it is exactly the skyscraper: rank zero and degree zero, so charge 0, which semiClosedUpperHalfPlane excludes and closedUpperHalfPlane admits. The charge is therefore a WeakStabilityFunctionOn (abelianDatum A) and not a StabilityFunctionOn (abelianDatum A).

SlopeData.toWeakSlopeData (in Slope.lean) forgets 0 < d to 0 ≤ d, so this is a genuine weakening with the curve case as an instance, not a second parallel structure.

The order bridge survives

phase_le_iff_slope_le carries a positive-rank hypothesis on both objects, and at positive rank the charge lies in the open upper half-plane, where the argument behaves exactly as it does in the strict theory. Nothing in that proof touches the degree hypothesis: it goes through phaseCross and the sign of rank E * degree F - degree E * rank F. So the order bridge is stated once here, and SlopeData inherits it through toWeakSlopeData.

What breaks, and why that is the content rather than a defect

SlopeCutoff.lean's chain does not survive. phase_eq_one_of_rank_zero and mem_hnTors_of_rank_zero both derive from degree_pos_of_rank_zero: a rank-zero object of positive degree lands on the negative real axis, so has phase one, so lies in T β for every β < 1. With only 0 ≤ degree a degree-zero rank-zero object — the skyscraper — has charge exactly 0, and arg 0 = 0, so it has no phase and cannot be placed by any phase comparison.

That is not a gap to route around with an extra hypothesis. It is the mathematical content of the weakening, and it is why the weak Harder–Narasimhan theory (WeakAbelianHNFiltration, Weak/HarderNarasimhan/Heart.lean) exists. On a K3 surface the skyscrapers are precisely the objects the surface case is about, so a hypothesis excluding them would exclude the subject.

What is supplied and what is proved

rank_nonneg and degree_nonneg_of_rank_zero are fields: they are the geometric input, unprovable here because A is an arbitrary abelian category. Everything else in this file is proved. Unlike SlopeData's degree_pos_of_rank_zero, both fields do hold on a polarised surface, so the structure has geometric inhabitants.

This file delivers the charge and the slope order on a surface. It does not deliver a cutoff to read them against: hnTorsProperty, hnFreeProperty and hnTorsionPair are all defined on the strict StabilityFunction, and there are no weak counterparts yet.

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

Rank and degree data on an abelian category, in the form a polarised surface supplies: rank is nonnegative, and a nonzero object of rank zero has degree at least zero. See the module docstring — the single difference from SlopeData is 0 ≤ where it has 0 <, and that is exactly the skyscraper.

• rankHom : K₀Ab A →+ ℤ

  The rank, as a hom out of the Grothendieck group.

• degreeHom : K₀Ab A →+ ℝ

  The degree, as a hom out of the Grothendieck group. It is real-valued so that a real polarisation ω can supply ω·c₁; the rank stays integral because integrality of the rank, not of the degree, is what the positivity arguments downstream use.

• rank_nonneg (E : A) : 0 ≤ self.rankHom (K₀Ab.of E)

  Rank is nonnegative — geometric input.

• degree_nonneg_of_rank_zero (E : A) : ¬Limits.IsZero E → self.rankHom (K₀Ab.of E) = 0 → 0 ≤ self.degreeHom (K₀Ab.of E)

  A nonzero object of rank zero has nonnegative degree — geometric input, and what puts torsion sheaves on the closed nonpositive real axis rather than the strictly negative one. True on a surface, where a skyscraper has c₁ = 0 and so degree 0.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakSlopeData.rank {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) (E : A) : ℤ

The rank of an object.

Equations

• D.rank E = D.rankHom (CategoryTheory.K₀Ab.of E)

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakSlopeData.degree {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) (E : A) : ℝ

The degree of an object.

Equations

• D.degree E = D.degreeHom (CategoryTheory.K₀Ab.of E)

The six formal properties

These are K₀Ab.of_isZero, of_iso and of_shortExact composed with a hom, so they are free of both geometric fields. The names and argument shapes match SlopeData's.

theorem CategoryTheory.Triangulated.WeakSlopeData.rank_zero {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) (E : A) (hE : Limits.IsZero E) : D.rank E = 0

theorem CategoryTheory.Triangulated.WeakSlopeData.degree_zero {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) (E : A) (hE : Limits.IsZero E) : D.degree E = 0

theorem CategoryTheory.Triangulated.WeakSlopeData.rank_iso {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) {E F : A} (e : E ≅ F) : D.rank E = D.rank F

theorem CategoryTheory.Triangulated.WeakSlopeData.degree_iso {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) {E F : A} (e : E ≅ F) : D.degree E = D.degree F

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

theorem CategoryTheory.Triangulated.WeakSlopeData.degree_additive {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) (S : ShortComplex A) (hS : S.ShortExact) : D.degree S.X₂ = D.degree S.X₁ + D.degree S.X₃

def CategoryTheory.Triangulated.WeakSlopeData.charge {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) (E : A) : ℂ

The charge -degree + i * rank.

Equations

• D.charge E = { re := -D.degree E, im := ↑(D.rank E) }

@[simp]

theorem CategoryTheory.Triangulated.WeakSlopeData.charge_re {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) (E : A) : (D.charge E).re = -D.degree E

@[simp]

theorem CategoryTheory.Triangulated.WeakSlopeData.charge_im {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) (E : A) : (D.charge E).im = ↑(D.rank E)

theorem CategoryTheory.Triangulated.WeakSlopeData.charge_mem_closedUpperHalfPlane {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) {E : A} (hE : ¬Limits.IsZero E) : D.charge E ∈ closedUpperHalfPlane

A nonzero object has charge in the closed upper half-plane. Two cases, both immediate: positive rank gives 0 < im, the first disjunct; rank zero gives im = 0 together with re = -degree ≤ 0, the second. A skyscraper realises the boundary case charge = 0, which is why the half-plane here must be the closed one.

noncomputable def CategoryTheory.Triangulated.WeakSlopeData.toWeakStabilityFunction {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) : WeakStabilityFunctionOn (abelianDatum A)

μ-slope on a surface is a weak stability function.

There is no WeakStabilityFunction A abbreviation to land in: the name WeakStabilityFunction is already taken, by the t-structure-indexed structure in Weak/Basic/Definitions.lean. The datum is written out instead.

Equations

• D.toWeakStabilityFunction = { Z := CategoryTheory.K₀Ab.liftOf D.charge ⋯, nonzero_mem := ⋯ }

@[simp]

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

noncomputable def CategoryTheory.Triangulated.WeakSlopeData.slope {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) (E : A) : ℝ

The slope degree / rank. It is junk at rank zero, where the classical slope is +∞; every statement below asks for positive rank.

Equations

• D.slope E = D.degree E / ↑(D.rank E)

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

The phase, normalised to (0, 1] on objects of nonzero charge. Unlike the strict theory's StabilityFunction.phase, this is not positive on every nonzero object: a skyscraper has charge 0 and so phase 0.

Equations

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

theorem CategoryTheory.Triangulated.WeakSlopeData.phase_eq_arg_div_pi {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) (E : A) : D.phase E = (D.toWeakStabilityFunction.Z (K₀Ab.of E)).arg / Real.pi

theorem CategoryTheory.Triangulated.WeakSlopeData.phaseCross_charge {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) (E F : A) : phaseCross (D.charge E) (D.charge F) = ↑(D.rank E) * D.degree F - D.degree E * ↑(D.rank F)

theorem CategoryTheory.Triangulated.WeakSlopeData.charge_ne_zero_of_rank_pos {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) {E : A} (hE : 0 < D.rank E) : D.charge E ≠ 0

theorem CategoryTheory.Triangulated.WeakSlopeData.arg_pos_of_rank_pos {A : Type u} [Category.{v, u} A] [Abelian A] (D : WeakSlopeData A) {E : A} (hE : 0 < D.rank E) : 0 < (D.charge E).arg

theorem CategoryTheory.Triangulated.WeakSlopeData.phase_le_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.phase E ≤ D.phase F ↔ D.slope E ≤ D.slope F

The phase order is the slope order on objects of positive rank, on a surface exactly as on a curve.

At positive rank the charge lies in the open upper half-plane, so the degree field plays no part: the proof runs through phaseCross, whose value rank E * degree F - degree E * rank F is nonnegative exactly when degree E / rank E ≤ degree F / rank F. This is the statement SlopeData inherits through SlopeData.toWeakSlopeData.