The Hilbert function of a coherent sheaf against a polarization

For a coherent sheaf F on a variety X over a field k and a line-bundle class L, the Hilbert function is n ↦ χ(F ⊗ L^n). This file names it, proves it invariant under isomorphism and additive on short exact sequences, factors it through the Grothendieck group as hilbertHom : K₀Ab (Coh X) →+ (ℤ → ℤ), and records that Snapper's theorem bounds its finite-difference degree by the supplied dimension.

Both the numerical content and the supplied-input carrier already exist under other names: Snapper.oneVariableEulerFunction is the function, and IntersectionTheory.Number.TwistContext is the carrier of Snapper's inputs. This file is the geometric packaging and the additivity that nobody had stated. It creates no new carrier.

What is supplied, and why

PolarizedVarietyData k X is the …Data idiom for genuinely external input. Its five fields are a line-bundle class L, finite coherent cohomology D, a linear connecting system C, a natural number dim, and, for every coherent sheaf, a TwistContext. Every supplied-not-proved field reachable from it is listed here:

• L : Pic X is not asserted to be ample. Ampleness does not exist at this pin; git grep -in 'ample' finds only numerical-example docstrings. Nothing below uses it, and the objects that would (positivity of the leading coefficient, hyperplane sections) belong to later issues in this lane.
• D : FiniteCohomology k X supplies coherent cohomology as finite-dimensional k-modules with a vanishing bound, the two inputs that make χ a finite sum.
• C : D.LinearConnectingSystem chooses, for every short exact sequence of coherent sheaves, k-linear connecting maps compatible with the Ext connecting maps. Euler additivity is proved from it; it is the temporary input that a Grothendieck-group factorization needs.
• twists F : TwistContext D F dim bundles, for every finite family of Picard classes, the coherence of every integer twist (CoherentTwistFamily), the hyperplane-section induction that the classical proof of Snapper's theorem uses (GeometricInduction), and a Picard-level Euler function eulerPic together with its identification realization with the geometric one. Coherence of a twist by an invertible sheaf and the geometric induction are both open at this pin; dim is the number of cuts after which the induction terminates, and is not derived from X.

Compare RiemannRoch.ReconstructionSystem, which also quantifies a TwistContext over every coherent sheaf but additionally demands a PairingContext, a graded ring, a rank, and takes additivity of eulerPic as a field. None of that is needed here, and additivity of the Hilbert function is a theorem below rather than an assumption.

Why the definition goes through oneVariableEulerFunction

hilbertFunction is defined as Snapper.oneVariableEulerFunction on the rank-one twist family, and hilbertFunction_eq_eulerPic identifies it with eulerPic (L ^ n) as a lemma. Defining it through eulerPic directly would be shorter but would leave additivity unprovable: TwistContext carries no additivity of eulerPic, which is precisely the field ReconstructionSystem adds. Through eulerFunction the additivity is a genuine theorem, from Coh.shortExact_map_ι, Modules.shortExact_map_tensorLeft_of_invertible and eulerCharacteristic_additive_modules, and both descriptions are then available.

Placement

AlgebraicGeometry/Stability/ is stability of sheaves: slope, Gieseker, and their Harder–Narasimhan theory on Coh X. It is distinct from AlgebraicGeometry/StabilityCondition/, which belongs to the derived-category families lane, and it imports nothing from the abstract stability-condition tree.

Not here: coefficient extraction (multiplicity and degree), any semistability notion, Harder–Narasimhan filtrations, and any construction of GeometricInduction from ampleness.

structure AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] : Type (u + 2)

A polarized variety, as supplied data. A line-bundle class, finite coherent cohomology with linear connecting maps, a dimension, and Snapper's inputs for every coherent sheaf. See the module docstring for what each field supplies and why none is proved here; in particular L is not asserted to be ample.

• L : Scheme.Modules.Pic X

  The polarizing line-bundle class. Not asserted to be ample.

• D : Cohomology.FiniteCohomology k X

  Finite coherent cohomology: finite-dimensional Hⁱ with a vanishing bound.

• C : self.D.LinearConnectingSystem

  Linear connecting maps for every short exact sequence of coherent sheaves.

• dim : ℕ

  The number of hyperplane cuts after which the geometric induction terminates.

• twists (F : Coh X) : IntersectionTheory.Number.TwistContext self.D F self.dim

  Snapper's supplied inputs for every coherent sheaf: coherence of every twist, the geometric induction, and the Picard-level Euler function with its realization.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.twistFamily {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F : Coh X) : IntersectionTheory.Snapper.CoherentTwistFamily F fun (x : Fin 1) => P.L

The rank-one coherent twist family n ↦ F ⊗ L^n, projected from twists.

Equations

• ⋯ = ⋯

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

The Hilbert function n ↦ χ(F ⊗ L^n), as Snapper's one-variable Euler function of the rank-one twist family.

Equations

• P.hilbertFunction F = AlgebraicGeometry.IntersectionTheory.Snapper.oneVariableEulerFunction P.D P.L ⋯

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.hilbertFunction_apply {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F : Coh X) (n : ℤ) : P.hilbertFunction F n = P.D.eulerCharacteristic (⋯.obj (NumericalPolynomial.oneVariablePoint n))

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.picardMonomial_fin_one {X : Scheme} (L : Scheme.Modules.Pic X) (n : ℤ) : IntersectionTheory.Number.picardMonomial (fun (x : Fin 1) => L) (NumericalPolynomial.oneVariablePoint n) = IntersectionTheory.Snapper.picardPower L n

The rank-one Picard monomial is the Picard power.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.hilbertFunction_eq_eulerPic {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F : Coh X) (n : ℤ) : P.hilbertFunction F n = (P.twists F).eulerPic (IntersectionTheory.Snapper.picardPower P.L n)

The Hilbert function is the Picard-level Euler function at L ^ n. This is the identification TwistContext.realization provides; it is a lemma, not the definition, for the reason given in the module docstring.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.hilbertFunction_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.hilbertFunction F = P.hilbertFunction G

The Hilbert function is invariant under isomorphism of coherent sheaves.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.twistModules_fin_one {X : Scheme} (L : Scheme.Modules.Pic X) (n : ℤ) (M : X.Modules) : IntersectionTheory.Snapper.twistModules (fun (x : Fin 1) => L) (NumericalPolynomial.oneVariablePoint n) M = (IntersectionTheory.Snapper.linePower L n).tensorObj M

At rank one the simultaneous twist is a single tensor product by the integer power.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.isCoherent_tensor_linePower {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F : Coh X) (n : ℤ) : Scheme.Modules.IsCoherent X ((IntersectionTheory.Snapper.linePower P.L n).tensorObj F.obj)

Coherence of F ⊗ L^n, read off the supplied twist family.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.hilbertFunction_eq_eulerCharacteristic_tensor {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F : Coh X) (n : ℤ) : P.hilbertFunction F n = P.D.eulerCharacteristic { obj := (IntersectionTheory.Snapper.linePower P.L n).tensorObj F.obj, property := ⋯ }

The Hilbert function evaluated at n is the Euler characteristic of the single tensor product F ⊗ L^n, as a coherent sheaf.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.hilbertFunction_additive {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (S : CategoryTheory.ShortComplex (Coh X)) (hS : S.ShortExact) (n : ℤ) : P.hilbertFunction S.X₂ n = P.hilbertFunction S.X₁ n + P.hilbertFunction S.X₃ n

Additivity of the Hilbert function, as a theorem. The short exact sequence is pushed to module sheaves by Coh.shortExact_map_ι, tensored by the invertible sheaf L^n with Modules.shortExact_map_tensorLeft_of_invertible, and returned to coherent sheaves by eulerCharacteristic_additive_modules with connecting maps from C.

noncomputable def AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.hilbertHom {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) : CategoryTheory.K₀Ab (Coh X) →+ ℤ → ℤ

The Hilbert function as a homomorphism K₀(Coh X) → (ℤ → ℤ), by the universal property of the Grothendieck group, exactly as FiniteCohomology.grothendieckEulerHom factors χ.

Equations

• P.hilbertHom = CategoryTheory.K₀Ab.liftOf P.hilbertFunction ⋯

@[simp]

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.hilbertHom_of {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F : Coh X) : P.hilbertHom (CategoryTheory.K₀Ab.of F) = P.hilbertFunction F

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.hilbertFunction_degreeLE {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F : Coh X) : NumericalPolynomial.DegreeLE P.dim (NumericalPolynomial.oneVariable (P.hilbertFunction F))

Snapper's bound: the Hilbert function has finite-difference degree at most dim, from the supplied geometric induction.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.fwdDiff_hilbertFunction {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : PolarizedVarietyData k X) (F : Coh X) : (fwdDiff 1)^[P.dim + 1] (P.hilbertFunction F) = 0

The ordinary form of Snapper's bound: the (dim + 1)st forward difference of the Hilbert function vanishes.