The weak Harder–Narasimhan property for the μ-slope on Coh X

Every nonzero coherent sheaf has a Harder–Narasimhan filtration for the weak μ-slope. This is the theorem the repository has carried as a hypothesis everywhere: HasHNProperty appears only as an assumption in the abstract theory, and this is its first instance on a geometric category.

The shape of the recursion, and why it is in two stages

Remove the maximal destabilizing subobject B from E and filter E / B; splice puts the two together. What is delicate is termination, and a single induction on multiplicity does not work: multiplicity is additive, so multiplicity (E / B) = multiplicity E - multiplicity B, and when B has multiplicity zero — the torsion case, where B has slope ⊤ — nothing decreases.

The fix is that this can happen at most once. multiplicity_pos_of_maximalDestabilizing says the quotient by the maximal destabilizing subobject is always pure, and for a pure sheaf every nonzero subobject, B included, has positive multiplicity, so multiplicity does strictly decrease at every later step. The recursion is therefore staged:

• exists_filtration_of_pure handles pure sheaves by induction on multiplicity;
• exists_filtration handles an arbitrary nonzero sheaf by splitting off the single torsion step first, after which the quotient is pure.

The chain condition in MuHNInput is what makes the maximal destabilizing subobject exist at each step. It is not what makes the recursion stop; multiplicity is.

The base case

B = ⊤ means the sheaf is its own maximal destabilizing subobject, hence semistable, and AbelianWeakHNFiltration.ofSemistable gives the one-step filtration. That is reused rather than rebuilt.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.isSemistable_of_maximalDestabilizing_eq_top {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) (htop : B = ⊤) : (P.weakSlopeData h).toWeakStabilityFunction.IsSemistable F

A subobject whose arrow is an isomorphism is the top subobject, so a sheaf equal to its own maximal destabilizing subobject is semistable.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.not_isZero_cokernel_of_ne_top {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {F : Coh X} {B : CategoryTheory.Subobject F} (hne : B ≠ ⊤) : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Limits.cokernel B.arrow)

If the subobject is not everything, the quotient by it is nonzero.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.multiplicity_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.multiplicity (CategoryTheory.Limits.cokernel B.arrow) = P.multiplicity F - P.multiplicity (CategoryTheory.Subobject.underlying.obj B)

Multiplicity of the quotient by a subobject, from additivity.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.isPure_cokernel {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) (hne : B ≠ ⊤) : P.IsPure (CategoryTheory.Limits.cokernel B.arrow)

The quotient by the maximal destabilizing subobject is pure.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.exists_filtration_of_pure {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) (n : ℕ) (F : Coh X) : P.IsPure F → (P.multiplicity F).toNat ≤ n → Nonempty (CategoryTheory.Triangulated.AbelianWeakHNFiltration (P.weakSlopeData h).toWeakStabilityFunction F)

Pure sheaves have Harder–Narasimhan filtrations, by induction on multiplicity.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.exists_filtration {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) : Nonempty (CategoryTheory.Triangulated.AbelianWeakHNFiltration (P.weakSlopeData h).toWeakStabilityFunction F)

Every nonzero coherent sheaf has a Harder–Narasimhan filtration.

A single torsion step is split off first: the quotient by the maximal destabilizing subobject is always pure, so the pure recursion takes over from there.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.hasHNProperty {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) : (P.weakSlopeData h).toWeakStabilityFunction.HasHNProperty

The weak Harder–Narasimhan property for the μ-slope on Coh X.

The abstract theory takes this as a hypothesis at every one of its use sites; this is its first proof on a geometric category.