Gieseker stability against μ-slope stability

The two stability notions on Coh X are ordered by different data: Gieseker stability by the whole reduced Hilbert polynomial compared at infinity, μ-stability by a single ratio of Hilbert coefficients. This file owns everything that mentions both, and is imported by neither.

What is delivered, and what is not

One implication in one direction: a Gieseker-semistable sheaf is weakly μ-semistable. The converse — μ-semistable implies Gieseker-semistable — is not delivered here in any form, and neither is any statement relating the two strict notions.

The two theories are therefore compared and not identified. IsGiesekerSemistable is defined from the Gieseker order alone, WeakStabilityFunctionOn.IsSemistable from the weak slope alone, and neither definition mentions the other. Gieseker/Basic.lean records separately why no central charge can reproduce the Gieseker order, so the comparison is between slopes and happens here rather than at the level of the stability functions.

Why purity is what makes the implication true

WeakStabilityFunctionOn.IsSemistable quantifies over every nonzero B : Subobject F and compares in WithTop ℝ, where a multiplicity-zero subobject has slope ⊤ and would destabilise F — while satisfying the Gieseker order vacuously, because its reduced Hilbert function is the junk value 0. The purity conjunct of IsGiesekerSemistable is exactly what rules that out: every nonzero subobject then has positive multiplicity, both slopes are finite, and the lexicographic criterion read at P.dim - 1 is the slope comparison. Without purity the statement is false, so the hypothesis travels with the theorem and is not weakened by the relocation.

This is also where the subsheaf quantifier changes shape. Gieseker stability quantifies over monomorphisms G ⟶ F; the abstract slope theory quantifies over Subobject F. The translation is made here, in the one file that needs both, and is kept out of either definition.

Placement

MO1.08 (#1319) made Slope/ and Gieseker/ siblings over the shared Hilbert-polynomial data, and this file is the comparison owner that split names. The declarations below were previously the tail of Gieseker/MuStability.lean and of Gieseker/HarderNarasimhan/Consequences.lean, where they were the only reason either module reached the other theory.

The slope, read as a normalized Hilbert coefficient

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.weakSlopeData_slope_eq_normalizedCoefficient {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) : (P.weakSlopeData h).slope F = ↑(P.normalizedCoefficient F (P.dim - 1))

The slope is the normalized Hilbert coefficient one below the top, read in ℝ. This holds without any positivity hypothesis, because both sides take the same junk value at multiplicity zero.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.weakSlopeData_topSlope_eq_normalizedCoefficient {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 : 0 < P.multiplicity F) : (P.weakSlopeData h).topSlope F = ↑↑(P.normalizedCoefficient F (P.dim - 1))

The same identification in WithTop ℝ, where positive multiplicity is what keeps the slope finite.

The comparison of the two orders

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.topSlope_le_of_giesekerLE {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} (h : MuPositivityData P) {F G : Coh X} (hF : 0 < P.multiplicity F) (hG : 0 < P.multiplicity G) (hle : P.GiesekerLE F G) : (P.weakSlopeData h).topSlope F ≤ (P.weakSlopeData h).topSlope G

The Gieseker order between sheaves of positive multiplicity implies the slope inequality, by the lexicographic criterion read at P.dim - 1.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.giesekerSemistable_implies_muSemistable {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 : P.IsGiesekerSemistable F) : (P.weakSlopeData h).toWeakStabilityFunction.IsSemistable F

Gieseker semistability implies weak μ-semistability.

The proof uses purity twice and visibly: it is what gives every nonzero subobject positive multiplicity, so that its slope is finite rather than ⊤, and it is what puts that subobject into the Gieseker quantifier with a reduced Hilbert function that is not the junk value. For a non-pure sheaf the statement is false: a nonzero multiplicity-zero subobject has slope ⊤, which exceeds every finite slope, while satisfying the Gieseker order vacuously.

Only this direction is delivered. The reverse implication is not in scope.

The Harder–Narasimhan filtration of a Gieseker-semistable sheaf

noncomputable def AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.hnTrivialOfGiesekerSemistable {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 : P.IsGiesekerSemistable F) : CategoryTheory.Triangulated.AbelianWeakHNFiltration (P.weakSlopeData h).toWeakStabilityFunction F

The one-step Harder–Narasimhan filtration of a Gieseker-semistable sheaf.

Gieseker semistability implies μ-semistability, and a semistable object is its own filtration. This closes the loop back to the Gieseker order: the coarser numerical invariant sees no destabilizing subsheaf either. It needs no MuHNInput, because the filtration is exhibited rather than obtained from the existence theorem.

Equations

• AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.hnTrivialOfGiesekerSemistable h hF = CategoryTheory.Triangulated.AbelianWeakHNFiltration.ofSemistable ⋯

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

A Gieseker-semistable sheaf has a one-step Harder–Narasimhan filtration. The propositional form of hnTrivialOfGiesekerSemistable, which is the name #905 asks for; the data itself carries a camelCase name because mathlib's naming convention forbids underscores in a def.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.giesekerSemistable_hn_trivial_n {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 : P.IsGiesekerSemistable F) : (hnTrivialOfGiesekerSemistable h hF).n = 1

The trivial filtration has exactly one factor.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.giesekerSemistable_hn_trivial_muPlus {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 : P.IsGiesekerSemistable F) : (hnTrivialOfGiesekerSemistable h hF).μPlus = (P.weakSlopeData h).topSlope F

Both extrema of the trivial filtration are the slope of the sheaf itself.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.giesekerSemistable_hn_trivial_muMinus {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 : P.IsGiesekerSemistable F) : (hnTrivialOfGiesekerSemistable h hF).μMinus = (P.weakSlopeData h).topSlope F

Both extrema of the trivial filtration are the slope of the sheaf itself.