μ-slope stability on Coh X, the first geometric slope datum #
WeakSlopeData asks for a rank, a degree, and two positivity facts. The Hilbert multiplicity and
degree coefficient of Coefficients.lean are already homomorphisms out of K₀Ab (Coh X), so
coherent sheaves on a polarized variety become an inhabitant of the repository's abstract slope
theory by supplying only the two positivity facts. Everything downstream — the charge
Z(E) = -degree E + i · rank E, the weak slope in WithTop ℝ, the phase, the order bridge
phase_le_iff_slope_le, weak semistability, and the whole WeakStabilityFunctionOn interface —
then arrives rather than being rebuilt.
What is supplied #
MuPositivityData carries exactly the two facts WeakSlopeData needs and this pin cannot prove,
because both are consequences of ampleness of the polarization, which does not exist here:
multiplicity is nonnegative, and a nonzero sheaf of multiplicity zero has nonnegative degree
coefficient. These are geometric input, not proof holes.
Abelian/Stability/Weak/Slope.lean's own docstring says the corresponding two
fields are geometric input there too, and that both hold on a polarised surface; the strict form
of the second is false on a surface, which is why the curve case below is a separate datum.
Rank stays integral, degree does not #
WeakSlopeData.degreeHom is real-valued, so the integral degree coefficient is composed with
Int.castAddHom ℝ here. The rank stays integral, and that is not incidental: integrality of the
rank is what the boundary arguments of the Mukai lane use. The multiplicity homomorphism is
therefore handed over unchanged.
What this file is not #
It is not the Gieseker theory, and it does not import it. μ-stability orders sheaves by one
ratio of Hilbert coefficients; Gieseker stability orders them by the whole reduced Hilbert
polynomial at infinity. The two are compared — in one direction, for pure sheaves — by
Stability/Comparison.lean, which imports both siblings and is imported by neither.
Until MO1.08 (#1319) this file was Gieseker/MuStability.lean, a child of the Gieseker
directory, and the μ-Harder–Narasimhan existence theorem sat below Gieseker/HarderNarasimhan/.
Nothing in either mentions the Gieseker order. Their new home is Slope/, a sibling of
Gieseker/ over the shared HilbertPolynomial.lean, Coefficients.lean and Purity.lean. The
directory name is the only thing that changed: Slope/HarderNarasimhan/Existence.lean proves
HN existence for the μ-slope, and must not be read as proving it for Gieseker stability.
Placement #
Slope/ reaches CategoryTheory/Abelian/Stability/ and stops there. It needs no t-structure, no
heart and no triangulated category, which is what the abelian owner of the slope theory buys:
the geometric instantiation of a slope datum is independent of the derived category the
Bridgeland theory is stated in. Slope/HarderNarasimhan/HeartTransport.lean is the one module
that crosses into the derived category, and it is deliberately a leaf.
The two positivity facts a polarization supplies. Both are consequences of ampleness and neither is provable at this pin; see the module docstring.
Multiplicity is nonnegative — geometric input.
- degree_nonneg_of_multiplicity_zero (F : Coh X) : ¬CategoryTheory.Limits.IsZero F → P.multiplicity F = 0 → 0 ≤ P.hilbertDegreeCoefficient F
A nonzero sheaf of multiplicity zero has nonnegative degree coefficient — geometric input, and what puts such a sheaf on the closed rather than the strictly negative real axis.
Instances For
The curve form of the same input, with the strict inequality. It is false on a surface,
where a skyscraper has multiplicity and degree coefficient both zero; see
Abelian/Stability/Weak/Slope.lean.
Multiplicity is nonnegative — geometric input.
- degree_pos_of_multiplicity_zero (F : Coh X) : ¬CategoryTheory.Limits.IsZero F → P.multiplicity F = 0 → 0 < P.hilbertDegreeCoefficient F
A nonzero sheaf of multiplicity zero has positive degree coefficient — the curve condition.
Instances For
Forgetting the strict inequality, exactly as SlopeData.toWeakSlopeData does.
The slope datum #
Coherent sheaves on a polarized variety, as a weak slope datum. Rank is the Hilbert
multiplicity, degree is the Hilbert degree coefficient cast to ℝ, and the two positivity fields
are the supplied geometric input. No new carrier: this is an instance of the abstract
structure.
Equations
- P.weakSlopeData h = { rankHom := P.multiplicityHom, degreeHom := (Int.castAddHom ℝ).comp P.degreeHom, rank_nonneg := ⋯, degree_nonneg_of_rank_zero := ⋯ }
Instances For
The weak slope of the datum, as a ratio of Hilbert coefficients.
The honest slope at positive multiplicity: the ratio, coerced into WithTop ℝ.
The honest slope at multiplicity zero is ⊤. This is not a corner case: it is what makes
the comparison theorem below false without purity.
The curve case #
The curve form of the slope datum, from the strict positivity input.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The two presentations agree. Forgetting the curve condition gives back the surface datum, field for field, so rank, degree, charge and slope are literally the same.