Reducing Grothendieck slope boundedness to quotient degrees

For a fixed coherent sheaf F, Grothendieck's boundedness lemma says that the slopes of its positive-multiplicity subsheaves are bounded above. This file identifies the exact remaining geometric statement: the codimension-one Hilbert coefficients of the corresponding quotients are bounded below.

The reduction is an equivalence, not a weakening of MuHNInput. Additivity writes degree(F) = degree(B) + degree(F/B). In one direction, a lower bound for degree(F/B) bounds the numerator of the slope of B; in the other, the already-proved bound multiplicity(B) ≤ multiplicity(F) turns a slope bound into a numerator bound and hence a lower bound for degree(F/B).

The remaining geometric obligation

Nothing in the current PolarizedVarietyData API says that P.L is ample, and the tree has no uniform Castelnuovo--Mumford regularity theorem or equivalent graded-submodule estimate. Consequently this file does not claim Grothendieck boundedness. It isolates it as the sharp reusable obligation quotientDegree_bddBelow accepted by MuHNInput.ofQuotientDegreeLowerBound: for each ambient sheaf, uniformly lower-bound the codimension-one Hilbert coefficient of every quotient whose kernel has positive multiplicity.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.hilbertDegreeCoefficient_eq_add_cokernel {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {F : Coh X} (B : CategoryTheory.Subobject F) : P.hilbertDegreeCoefficient F = P.hilbertDegreeCoefficient (CategoryTheory.Subobject.underlying.obj B) + P.hilbertDegreeCoefficient (CategoryTheory.Limits.cokernel B.arrow)

The codimension-one Hilbert coefficient of a coherent sheaf is the sum of those of a subobject and its canonical quotient.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.slope_bddAbove_iff_quotientDegree_bddBelow {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} (h : MuPositivityData P) (F : Coh X) : (∃ (μ₀ : ℝ), ∀ (B : CategoryTheory.Subobject F), ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj B) → 0 < P.multiplicity (CategoryTheory.Subobject.underlying.obj B) → ↑(P.hilbertDegreeCoefficient (CategoryTheory.Subobject.underlying.obj B)) / ↑(P.multiplicity (CategoryTheory.Subobject.underlying.obj B)) ≤ μ₀) ↔ ∃ (d₀ : ℤ), ∀ (B : CategoryTheory.Subobject F), 0 < P.multiplicity (CategoryTheory.Subobject.underlying.obj B) → d₀ ≤ P.hilbertDegreeCoefficient (CategoryTheory.Limits.cokernel B.arrow)

Grothendieck slope boundedness is exactly lower boundedness of quotient degrees.

For a fixed F, the slopes of its nonzero positive-multiplicity subobjects are bounded above if and only if the codimension-one Hilbert coefficients of their canonical quotients are bounded below. Positive multiplicity already implies that the subobject is nonzero, so no separate nonzero hypothesis is needed on the quotient-degree side.

theorem AlgebraicGeometry.Stability.Gieseker.MuHNInput.ofQuotientDegreeLowerBound {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {h : MuPositivityData P} [IsNoetherian X] (quotientDegree_bddBelow : ∀ (F : Coh X), ∃ (d₀ : ℤ), ∀ (B : CategoryTheory.Subobject F), 0 < P.multiplicity (CategoryTheory.Subobject.underlying.obj B) → d₀ ≤ P.hilbertDegreeCoefficient (CategoryTheory.Limits.cokernel B.arrow)) : MuHNInput P h

On a Noetherian scheme, a uniform lower bound for quotient degree coefficients is exactly the remaining input needed to construct sheaf-level μ-Harder--Narasimhan filtrations. This constructor does not assert that bound: it packages a proof of the geometric obligation through PolarizedVarietyData.slope_bddAbove_iff_quotientDegree_bddBelow.