Hilbert coefficients: multiplicity and degree #
The Hilbert function of a coherent sheaf has finite-difference degree at most P.dim, so it is
determined by its P.dim + 1 Newton coefficients. This file extracts them, proves that the top
two are additive on short exact sequences by exhibiting them as homomorphisms out of the
Grothendieck group, and proves the Gregory–Newton representation that recovers the Hilbert
function from them.
multiplicity is the top coefficient and plays the role of rank; hilbertDegreeCoefficient is
the next one down and plays the role of degree. Both are finite-difference coefficients: if
the Hilbert polynomial has leading term e · n ^ dim / dim !, then multiplicity F is e,
that is dim ! times the classical leading coefficient. Nothing here divides by a factorial,
and no statement below silently reads these as the classical coefficients.
The comparison at infinity #
reducedHilbert divides the Hilbert function by the multiplicity, and comparing two of these
functions for large n is what Gieseker stability is. The comparison is possible only because
hilbertFunction_eq_sum_choose writes the function as a finite binomial sum whose length is
P.dim + 1 and does not depend on n; without it, DegreeLE alone says nothing about
behaviour at infinity. That representation therefore lives here, with the coefficients, and not
in the file that defines the order.
The junk value #
reducedHilbert P F divides by multiplicity P F, and Lean's division returns 0 when that is
0. A sheaf of multiplicity zero — one whose support has dimension below P.dim — therefore has
reduced Hilbert function identically 0 rather than being undefined. Every statement about
reducedHilbert below carries a positivity hypothesis instead of relying on the quotient, and
the purity conjunct of Gieseker semistability, defined in Basic.lean, is what keeps such a
sheaf out of the semistability quantifier. The same junk value is what would make the
comparison theorem of MuStability.lean false without purity.
The Newton coefficients #
The Hilbert function of a zero sheaf vanishes identically, because it factors through the
Grothendieck group and the class of a zero object is 0.
The jth Hilbert coefficient: the j-fold forward difference of the Hilbert function,
evaluated at the origin.
Equations
Instances For
The Hilbert coefficient is the iterated ordinary forward difference at 0. This is the
existing one-variable bridge NumericalPolynomial.coefficient_oneVariable, not a new one.
Iterating the forward difference past the vanishing order kills every later coefficient.
A zero sheaf has vanishing Hilbert coefficients.
Hilbert coefficients are invariant under isomorphism.
Hilbert coefficients are additive on short exact sequences, coefficient by coefficient.
Multiplicity and degree #
The multiplicity: the top Hilbert coefficient, playing the role of rank. It is dim !
times the classical leading coefficient of the Hilbert polynomial; see the module docstring.
Equations
- P.multiplicity F = P.hilbertCoefficient F P.dim
Instances For
The degree coefficient: the Hilbert coefficient one below the top, playing the role of
degree. At P.dim = 0 truncated subtraction makes this the multiplicity again, which is the
correct degenerate reading: a zero-dimensional polarization has no degree direction.
Equations
- P.hilbertDegreeCoefficient F = P.hilbertCoefficient F (P.dim - 1)
Instances For
Multiplicity as a homomorphism out of the Grothendieck group. The type is exactly the
rankHom field of WeakSlopeData, so the instantiation in MuStability.lean needs no
adapter on this coordinate.
Equations
Instances For
The degree coefficient as a homomorphism out of the Grothendieck group.
Equations
Instances For
The reduced Hilbert function. At multiplicity P F = 0 this is Lean's junk value 0
rather than an undefined quotient; see the module docstring, and note that every statement
about it below assumes positive multiplicity.
Equations
- P.reducedHilbert F n = ↑(P.hilbertFunction F n) / ↑(P.multiplicity F)
Instances For
The Gregory–Newton representation #
Gregory–Newton. The Hilbert function is the binomial sum of its Hilbert coefficients,
over a range fixed by P.dim rather than by n. This is the representation that lets two
Hilbert functions be compared for large n.
The reduced Hilbert function as a binomial sum of normalized coefficients.