The maximal destabilizing subobject for the μ-slope on Coh X

Harder–Narasimhan theory for the weak μ-slope rests on one lemma: every nonzero coherent sheaf has a subobject whose slope is maximal among nonzero subobjects, chosen maximal among those attaining that slope, and such a subobject is weak-semistable. This file proves it from two named inputs and nothing else.

What is supplied, and what is proved

MuHNInput carries exactly two facts:

• subobject-chain termination, IsNoetherianObject F for every coherent sheaf. This is now proved for every Noetherian scheme by Coh.isNoetherianObject; proper varieties obtain the required IsNoetherian X instance. MuHNInput.ofSlopeBoundedness installs this field from that theorem.
• slope boundedness, Grothendieck's lemma: the μ-slopes of nonzero subobjects of a fixed F are bounded above. This remains the geometric input unavailable here.

Neither the maximal destabilizing subobject nor HasHNProperty is a field. Everything below is derived.

Two corrections to the shape of the second input

The WithTop ℝ form of boundedness is vacuous. Stated as ∃ μ₀ : WithTop ℝ, ∀ B ≠ 0, slope B ≤ μ₀, the hypothesis is satisfied by μ₀ = ⊤ for every F, and carries no information. The field below therefore takes a real bound and quantifies only over subobjects of positive multiplicity — which is exactly Grothendieck's lemma, and leaves the multiplicity-zero case where it belongs, in slope_eq_top_iff_not_isPure.

No third input is needed. One might expect boundedness not to give an attained maximum, since slopes are quotients of integers and a bounded set of such is dense in general. It does here, because multiplicity is additive and nonnegative, so multiplicity B ≤ multiplicity F for every subobject: the denominators are bounded by a single integer. Every slope is then a multiple of 1 / (multiplicity F)!, and a set of such numbers bounded above has a greatest element. That is exists_slopeMax, and it is why MuHNInput has two fields rather than three.

structure AlgebraicGeometry.Stability.Gieseker.MuHNInput {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (h : MuPositivityData P) : Prop

The two inputs sheaf-level Harder–Narasimhan theory needs. The first is proved for Noetherian schemes; the second remains Grothendieck's boundedness lemma. See the module docstring for why boundedness must be stated with a real bound rather than in WithTop ℝ.

• noetherian (F : Coh X) : CategoryTheory.IsNoetherianObject F

  Ascending chains of subobjects terminate. Coh.isNoetherianObject supplies this on a Noetherian scheme.

• slope_bddAbove (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)) ≤ μ₀

  Grothendieck's boundedness lemma: the μ-slopes of the nonzero subobjects of positive multiplicity of a fixed sheaf are bounded above by a real number. Nothing in the tree supplies it. The bound is real, not WithTop ℝ, because ⊤ bounds everything.

theorem AlgebraicGeometry.Stability.Gieseker.MuHNInput.ofSlopeBoundedness {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] (slope_bddAbove : ∀ (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)) ≤ μ₀) : MuHNInput P h

On a Noetherian scheme, Grothendieck slope boundedness is the only remaining input for sheaf-level μ-Harder–Narasimhan theory.

Multiplicity is bounded along monomorphisms

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.multiplicity_le_of_mono {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} (h : MuPositivityData P) {G F : Coh X} (i : G ⟶ F) [CategoryTheory.Mono i] : P.multiplicity G ≤ P.multiplicity F

A subsheaf has multiplicity at most that of the ambient sheaf. Additivity of multiplicity on the short exact sequence defined by a monomorphism, together with nonnegativity of the multiplicity of the cokernel. This is what bounds the denominators of the slopes, and so what makes the maximal slope attained rather than merely bounded.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.multiplicity_subobject_le {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) : P.multiplicity (CategoryTheory.Subobject.underlying.obj B) ≤ P.multiplicity F

The subobject form of multiplicity_le_of_mono.

The maximal slope is attained

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.exists_slopeMax {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} (h : MuPositivityData P) (I : MuHNInput P h) {F : Coh X} (hF : ¬CategoryTheory.Limits.IsZero F) : ∃ (B : CategoryTheory.Subobject F), ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj B) ∧ ∀ (B' : CategoryTheory.Subobject F), ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj B') → (P.weakSlopeData h).topSlope (CategoryTheory.Subobject.underlying.obj B') ≤ (P.weakSlopeData h).topSlope (CategoryTheory.Subobject.underlying.obj B)

The maximal slope is attained.

Either some nonzero subobject has multiplicity zero, and its slope is ⊤, which dominates everything; or every nonzero subobject has multiplicity between 1 and multiplicity F, so every slope is an integer multiple of 1 / (multiplicity F)!, and boundedness above of a set of such numbers gives a greatest element.

The maximal destabilizing subobject

def AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.IsMaximalDestabilizing {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) : Prop

The maximal destabilizing subobject, as a property: nonzero, of maximal slope among nonzero subobjects, and maximal in the subobject order among those attaining that slope. The second clause is what makes the slope drop strictly on the quotient, which the recursion building the filtration needs.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.exists_maximalDestabilizing {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} (h : MuPositivityData P) (I : MuHNInput P h) {F : Coh X} (hF : ¬CategoryTheory.Limits.IsZero F) : ∃ (B : CategoryTheory.Subobject F), IsMaximalDestabilizing h F B

Every nonzero coherent sheaf has a maximal destabilizing subobject.

exists_slopeMax attains the slope; the chain condition then picks a subobject maximal among those attaining it.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.maximalDestabilizing_isSemistable {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} (hB : IsMaximalDestabilizing h F B) : (P.weakSlopeData h).toWeakStabilityFunction.IsSemistable (CategoryTheory.Subobject.underlying.obj B)

The maximal destabilizing subobject is weak-semistable. A nonzero subobject of it is a nonzero subobject of the ambient sheaf, so its slope cannot exceed the maximal one.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.topSlope_maximalDestabilizing_eq_top_iff {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} (hF : ¬CategoryTheory.Limits.IsZero F) {B : CategoryTheory.Subobject F} (hB : IsMaximalDestabilizing h F B) : (P.weakSlopeData h).topSlope (CategoryTheory.Subobject.underlying.obj B) = ⊤ ↔ ¬P.IsPure F

The maximal slope is ⊤ exactly when the sheaf is not pure.

This is the boundary case the WithTop valuation exists for, and it is what tells the filtration recursion that the first factor of a pure sheaf has finite slope.