The Gieseker order and Gieseker (semi)stability

A coherent sheaf is Gieseker-semistable when no nonzero subsheaf has a larger reduced Hilbert function for large n. This file defines that order, the two stability predicates, and proves the structural facts: the order is reflexive and transitive, it is decided by the normalized coefficient vector read lexicographically from the top, and it is total on sheaves of positive multiplicity.

Which classical definition this is

With IsPure as a conjunct, IsGiesekerSemistable is Huybrechts–Lehn's Gieseker semistability for a pure sheaf of dimension P.dim, with purity expressed through Hilbert multiplicity rather than through dimension of support. The geometric equivalence of the two forms of purity is not claimed: no dimension-of-support theory exists at this pin. The subsheaf quantifier is over monomorphisms G ⟶ F throughout; the translation to Subobject F is made where it is needed, in Comparison.lean, and is not mixed into the definitions here.

Why purity is a conjunct and not an afterthought

reducedHilbert P G divides by multiplicity P G and takes Lean's junk value 0 when that is zero. Without purity, every nonzero subsheaf of multiplicity zero would satisfy the order relation vacuously, the predicate would fail to exclude exactly the subsheaves it exists to exclude, and the comparison theorem of Comparison.lean would be false.

IsPure itself is not declared here. It mentions only the multiplicity, and the μ-slope lane needs it for a reason that has nothing to do with the Gieseker order, so MO1.08 (#1319) gave it the shared owner Purity.lean one level up. This file imports it like any other consumer.

Why this is not a StabilityFunctionOn

Gieseker stability is ordered by a polynomial, compared at infinity; the repository's StabilityFunctionOn is ordered by the argument of a complex charge in the upper half-plane. There is no charge whose argument reproduces this order, and encoding a polynomial in a complex number to force the two together would be a false unification of the kind docs/architecture/abstraction-tree.md forbids. The comparison between the two theories happens one level down, between slopes, and is proved in Comparison.lean — which is a comparison and not an identification: neither theory is defined in terms of the other, and only one direction of one implication is delivered.

The numerical core

eventually_nonneg_binomial_iff is subject-neutral: an integer binomial sum is eventually nonnegative exactly when its coefficient vector is lexicographically nonnegative from the top. It is stated here, for its only consumer, rather than added to Algebra/NumericalPolynomial/; if a second consumer appears it should move there. Its proof turns on integrality: a strictly increasing integer sequence increases without bound, which is what upgrades "the difference is eventually positive" to "the sum is eventually positive".

The numerical core: eventual sign of an integer binomial sum

theorem AlgebraicGeometry.Stability.Gieseker.sum_binomial_eq_of_vanishing {a : ℕ → ℤ} {J d : ℕ} (hJd : J ≤ d) (h : ∀ (i : ℕ), J < i → i ≤ d → a i = 0) (n : ℕ) : ∑ j ∈ Finset.range (d + 1), ↑(n.choose j) * a j = ∑ j ∈ Finset.range (J + 1), ↑(n.choose j) * a j

The binomial sum truncates at any index above which the coefficients vanish.

theorem AlgebraicGeometry.Stability.Gieseker.sum_binomial_succ_sub (a : ℕ → ℤ) (J n : ℕ) : ∑ j ∈ Finset.range (J + 1 + 1), ↑((n + 1).choose j) * a j - ∑ j ∈ Finset.range (J + 1 + 1), ↑(n.choose j) * a j = ∑ j ∈ Finset.range (J + 1), ↑(n.choose j) * a (j + 1)

One forward difference of a binomial sum shifts its coefficients down.

theorem AlgebraicGeometry.Stability.Gieseker.eventually_pos_of_succ_le {c : ℕ → ℤ} {N : ℕ} (h : ∀ (n : ℕ), N ≤ n → c n + 1 ≤ c (n + 1)) : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < c n

An integer sequence that eventually gains at least one per step is eventually positive. This is where integrality enters, and it is what makes the binomial induction below close.

theorem AlgebraicGeometry.Stability.Gieseker.eventually_pos_binomial_of_top_pos (J : ℕ) (a : ℕ → ℤ) (hJ : 0 < a J) : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < ∑ j ∈ Finset.range (J + 1), ↑(n.choose j) * a j

Integer binomial sums with a positive top coefficient are eventually positive.

The induction is on the top index. One forward difference lowers it by one, so the inductive hypothesis makes the sum eventually strictly increasing; eventually_pos_of_succ_le then turns that into eventual positivity, using that the values are integers.

theorem AlgebraicGeometry.Stability.Gieseker.exists_top_ne_zero {a : ℕ → ℤ} {d : ℕ} (h : ¬∀ j ≤ d, a j = 0) : ∃ J ≤ d, a J ≠ 0 ∧ ∀ (i : ℕ), J < i → i ≤ d → a i = 0

The top index at which a coefficient vector supported in range (d + 1) is nonzero.

theorem AlgebraicGeometry.Stability.Gieseker.eventually_nonneg_binomial_iff (a : ℕ → ℤ) (d : ℕ) : (∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ ∑ j ∈ Finset.range (d + 1), ↑(n.choose j) * a j) ↔ (∀ j ≤ d, a j = 0) ∨ ∃ J ≤ d, 0 < a J ∧ ∀ (i : ℕ), J < i → i ≤ d → a i = 0

The eventual sign of an integer binomial sum is decided lexicographically from the top.

The sum is eventually nonnegative exactly when either every coefficient vanishes, or the highest nonvanishing one is positive.

theorem AlgebraicGeometry.Stability.Gieseker.eventually_nonneg_binomial_total (a : ℕ → ℤ) (d : ℕ) : (∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ ∑ j ∈ Finset.range (d + 1), ↑(n.choose j) * a j) ∨ ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ ∑ j ∈ Finset.range (d + 1), ↑(n.choose j) * -a j

The lexicographic criterion is total: one of the two coefficient vectors dominates.

The Gieseker order

def AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.GiesekerLE {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F G : Coh X) : Prop

The Gieseker order: the reduced Hilbert function of F is eventually at most that of G. No Preorder instance is registered on Coh X; this is a relation, used as one.

Equations

• P.GiesekerLE F G = ∀ᶠ (n : ℕ) in Filter.atTop, P.reducedHilbert F ↑n ≤ P.reducedHilbert G ↑n

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.giesekerLE_refl {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F : Coh X) : P.GiesekerLE F F

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.giesekerLE_trans {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) {F G H : Coh X} (h₁ : P.GiesekerLE F G) (h₂ : P.GiesekerLE G H) : P.GiesekerLE F H

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.reducedHilbert_eq_of_iso {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) {F G : Coh X} (e : F ≅ G) : P.reducedHilbert F = P.reducedHilbert G

The reduced Hilbert function is an isomorphism invariant.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.giesekerLE_of_iso {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) {F G : Coh X} (e : F ≅ G) : P.GiesekerLE F G

Isomorphic sheaves are Gieseker-comparable.

def AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.GiesekerLT {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F G : Coh X) : Prop

Strict Gieseker order.

Equations

• P.GiesekerLT F G = (P.GiesekerLE F G ∧ ¬P.GiesekerLE G F)

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.giesekerLT_irrefl {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F : Coh X) : ¬P.GiesekerLT F F

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.giesekerLT_trans {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) {F G H : Coh X} (h₁ : P.GiesekerLT F G) (h₂ : P.GiesekerLT G H) : P.GiesekerLT F H

The lexicographic coefficient criterion

noncomputable def AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.normalizedCoefficient {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F : Coh X) (j : ℕ) : ℚ

The Hilbert coefficient vector normalized by the multiplicity. Its top entry is 1 for every sheaf of positive multiplicity, which is why the Gieseker comparison always drops to the entry below the top.

Equations

• P.normalizedCoefficient F j = ↑(P.hilbertCoefficient F j) / ↑(P.multiplicity F)

def AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.CoeffLexLE {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F G : Coh X) : Prop

The lexicographic order on normalized coefficient vectors, read from j = P.dim down.

Equations

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

noncomputable def AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.lexDiff {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F G : Coh X) (j : ℕ) : ℤ

The integer coefficient whose sign decides the Gieseker comparison at index j.

Equations

• P.lexDiff F G j = P.multiplicity F * P.hilbertCoefficient G j - P.multiplicity G * P.hilbertCoefficient F j

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.lexDiff_swap {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F G : Coh X) (j : ℕ) : P.lexDiff G F j = -P.lexDiff F G j

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.normalizedCoefficient_le_iff {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {F G : Coh X} (hF : 0 < P.multiplicity F) (hG : 0 < P.multiplicity G) (j : ℕ) : P.normalizedCoefficient F j ≤ P.normalizedCoefficient G j ↔ 0 ≤ P.lexDiff F G j

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.normalizedCoefficient_eq_iff {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {F G : Coh X} (hF : 0 < P.multiplicity F) (hG : 0 < P.multiplicity G) (j : ℕ) : P.normalizedCoefficient F j = P.normalizedCoefficient G j ↔ P.lexDiff F G j = 0

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.normalizedCoefficient_lt_iff {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {F G : Coh X} (hF : 0 < P.multiplicity F) (hG : 0 < P.multiplicity G) (j : ℕ) : P.normalizedCoefficient F j < P.normalizedCoefficient G j ↔ 0 < P.lexDiff F G j

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.reducedHilbert_le_iff_sum {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {F G : Coh X} (hF : 0 < P.multiplicity F) (hG : 0 < P.multiplicity G) (n : ℕ) : P.reducedHilbert F ↑n ≤ P.reducedHilbert G ↑n ↔ 0 ≤ ∑ j ∈ Finset.range (P.dim + 1), ↑(n.choose j) * P.lexDiff F G j

The Gieseker comparison at a single n, cross-multiplied into an integer binomial sum.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.giesekerLE_iff_coeffLexLE {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {F G : Coh X} (hF : 0 < P.multiplicity F) (hG : 0 < P.multiplicity G) : P.GiesekerLE F G ↔ P.CoeffLexLE F G

The lexicographic coefficient criterion. For sheaves of positive multiplicity, the Gieseker order is exactly the lexicographic order on normalized coefficient vectors read from the top. The proof compares the two Gregory–Newton sums delivered by Coefficients.lean.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.giesekerLE_total {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {F G : Coh X} (hF : 0 < P.multiplicity F) (hG : 0 < P.multiplicity G) : P.GiesekerLE F G ∨ P.GiesekerLE G F

Totality on sheaves of positive multiplicity, a corollary of the criterion.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.normalizedCoefficient_dim {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {F : Coh X} (hF : 0 < P.multiplicity F) : P.normalizedCoefficient F P.dim = 1

The normalized coefficient at the top index is 1 for every sheaf of positive multiplicity. This is why the Gieseker comparison always drops to the index below the top.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.normalizedCoefficient_pred_le_of_giesekerLE {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {F G : Coh X} (hF : 0 < P.multiplicity F) (hG : 0 < P.multiplicity G) (hle : P.GiesekerLE F G) : P.normalizedCoefficient F (P.dim - 1) ≤ P.normalizedCoefficient G (P.dim - 1)

The Gieseker comparison always drops to the index below the top.

At j = P.dim both normalized coefficients are 1, so the lexicographic comparison can never be decided there; whatever it decides, the entry at P.dim - 1 is comparable in the same direction. That entry is the slope, which is why this is the bridge to the weak slope theory.

Gieseker semistability and stability

def AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.IsGiesekerSemistable {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F : Coh X) : Prop

Gieseker semistability: a pure sheaf no nonzero subsheaf of which has eventually larger reduced Hilbert function. Purity is a conjunct, so every G reaching the quantifier has positive multiplicity and its reduced Hilbert function is never the junk value.

Equations

• P.IsGiesekerSemistable F = (P.IsPure F ∧ ∀ (G : AlgebraicGeometry.Coh X) (i : G ⟶ F), CategoryTheory.Mono i → ¬CategoryTheory.Limits.IsZero G → P.GiesekerLE G F)

def AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.IsGiesekerStable {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F : Coh X) : Prop

Gieseker stability: the strict form, on subsheaves that are not isomorphisms onto F.

Equations

• P.IsGiesekerStable F = (P.IsPure F ∧ ∀ (G : AlgebraicGeometry.Coh X) (i : G ⟶ F), CategoryTheory.Mono i → ¬CategoryTheory.Limits.IsZero G → ¬CategoryTheory.IsIso i → P.GiesekerLT G F)

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.IsGiesekerSemistable.isPure {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {F : Coh X} (h : P.IsGiesekerSemistable F) : P.IsPure F

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.IsGiesekerSemistable.multiplicity_pos {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {F : Coh X} (h : P.IsGiesekerSemistable F) : 0 < P.multiplicity F

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.IsGiesekerSemistable.not_isZero {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {F : Coh X} (h : P.IsGiesekerSemistable F) : ¬CategoryTheory.Limits.IsZero F

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.IsGiesekerStable.isGiesekerSemistable {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {F : Coh X} (h : P.IsGiesekerStable F) : P.IsGiesekerSemistable F

A stable sheaf is semistable: a subsheaf that is an isomorphism onto F is comparable by transport along that isomorphism, and every other one by the strict order.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.not_isGiesekerSemistable_of_isZero {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {F : Coh X} (hF : CategoryTheory.Limits.IsZero F) : ¬P.IsGiesekerSemistable F

The zero sheaf is not Gieseker-semistable, because it is not pure.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.not_isGiesekerStable_of_isZero {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {F : Coh X} (hF : CategoryTheory.Limits.IsZero F) : ¬P.IsGiesekerStable F

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.IsGiesekerSemistable.of_iso {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {F G : Coh X} (h : P.IsGiesekerSemistable F) (e : F ≅ G) : P.IsGiesekerSemistable G

Gieseker semistability is invariant under isomorphism.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.IsGiesekerStable.of_iso {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {F G : Coh X} (h : P.IsGiesekerStable F) (e : F ≅ G) : P.IsGiesekerStable G

Gieseker stability is invariant under isomorphism.