Slope stability is a stability function #
Rank and degree data on an abelian category — what a polarised curve gives to
Coh X, with degree the usual degree — determine the charge
Z (E) = -degree E + i * rank E
and that charge is a stability function: it is additive on short exact sequences because rank and degree are, and a nonzero object lands in the semi-closed upper half-plane because rank is nonnegative and a nonzero object of rank zero has positive degree.
So μ-slope stability is not a parallel theory: it is the repository's own
StabilityFunction, and the phase, semistability, and Harder–Narasimhan
machinery already built on that interface applies to it unchanged.
The order bridge #
phase_le_iff_slope_le: on objects of positive rank the phase order is the
slope order. The computation is one line through phaseCross,
phaseCross (Z E) (Z F) = rank E * degree F - degree E * rank F,
which is nonnegative exactly when degree E / rank E ≤ degree F / rank F. That
is what lets a torsion pair cut by a slope be read as one cut by a phase, which
is the form the tilting machinery consumes.
What is data and what is proved #
rank_nonneg and degree_pos_of_rank_zero are fields: they are the
geometric input, not provable here, since A is an arbitrary abelian category.
They are the CURVE case, not the surface case, and an earlier version of this
docstring said surface. On a curve a nonzero torsion sheaf has degree equal to
its length, which is positive. On a surface it is false: a dimension-zero
sheaf — a skyscraper — has c₁ = 0, hence degree = c₁ · ω = 0, so
degree_pos_of_rank_zero fails on exactly those objects.
The consequence is not cosmetic. μ-slope on a surface is a weak stability
function, not a stability function: a skyscraper has zero rank and zero degree, so
its charge is 0, which semiClosedUpperHalfPlane excludes. That is why the weak
theory exists, and it is why a surface lane must not instantiate SlopeData.
The slope itself is degree / rank, which is junk at rank zero where the
classical slope is +∞; every statement about it carries a positive-rank
hypothesis, and the torsion sheaves are handled by the charge rather than by the
slope.
The surface case is the weakening, not a parallel theory #
WeakSlopeData (in WeakSlope.lean) replaces degree_pos_of_rank_zero by
degree_nonneg_of_rank_zero, and toWeakSlopeData below is the forgetful map
0 < d → 0 ≤ d. Everything in this file that carries a positive-rank hypothesis
— phaseCross_charge, charge_ne_zero_of_rank_pos, arg_pos_of_rank_pos and
the order bridge phase_le_iff_slope_le — is proved once on WeakSlopeData and
inherited here, so the surface lane gets the order bridge without a second copy
of its proof.
Rank and degree data on an abelian category: what a polarised curve gives
to its category of coherent sheaves. See the module docstring — on a surface
degree_pos_of_rank_zero is false for skyscrapers.
The rank, as a hom out of the Grothendieck group.
The degree, as a hom out of the Grothendieck group. Real-valued, as in
WeakSlopeData, so that a real polarisation can supply it.Rank is nonnegative — geometric input.
- degree_pos_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 positive degree — geometric input, and what puts torsion sheaves on the negative real axis. True on a curve; false on a surface, where a skyscraper has
c₁ = 0and so degree0. See the module docstring.
Instances For
The rank of an object.
Equations
- D.rank E = D.rankHom (CategoryTheory.K₀Ab.of E)
Instances For
The degree of an object.
Equations
- D.degree E = D.degreeHom (CategoryTheory.K₀Ab.of E)
Instances For
The six formal properties, now theorems #
rank_zero, rank_iso, rank_additive and their degree counterparts were fields.
They are exactly K₀Ab.of_isZero, of_iso and of_shortExact composed with a hom,
so they are proved here and the names and argument shapes are unchanged.
The curve case is an instance of the surface case #
degree_pos_of_rank_zero implies degree_nonneg_of_rank_zero, so every
SlopeData is a WeakSlopeData. Rank, degree, charge and slope are unchanged
by the map: it forgets a hypothesis and nothing else.
Forget 0 < degree to 0 ≤ degree. This is what makes WeakSlopeData
a genuine weakening of SlopeData rather than a second parallel structure.
Equations
Instances For
Slope stability is a stability function.
map_zero and map_iso are gone: they were consequences of additivity all
along, and K₀Ab proves them once. Only the additivity of charge on short
exact sequences is supplied here, and it is the same two-line computation the
additive field used to carry.
Equations
- D.toStabilityFunction = { Z := CategoryTheory.K₀Ab.liftOf D.charge ⋯, nonzero_mem := ⋯ }
Instances For
The slope degree / rank. It is junk at rank zero, where the classical
slope is +∞; every statement below asks for positive rank.
Instances For
The phase of toStabilityFunction is the weak phase of toWeakSlopeData:
both are arg of the same charge, normalised. This is the bridge along which the
positive-rank results below are inherited.
The phase order is the slope order on objects of positive rank.
phaseCross turns the comparison of arguments into the sign of
rank E * degree F - degree E * rank F, which is the comparison of slopes once
both ranks are positive.
The proof is WeakSlopeData.phase_le_iff_slope_le, transported along
toWeakSlopeData: nothing in it uses degree_pos_of_rank_zero, because a
positive-rank charge is in the open upper half-plane.