Degree and leading term of the affine Hilbert polynomial #
This file implements blueprint node A04′ of the algebra backend: for an ideal I of
P_d = MvPolynomial (Fin d) K whose affine Hilbert function is sandwiched, for all large t,
between ∑ i, (t - e i + k).choose k and Δ * (t + k).choose k (with k = quotDim I, Δ > 0
and shifts e : Fin Δ → ℕ), the affine Hilbert polynomial has natDegree = k and leading
coefficient Δ / k!, so degree I = Δ, 0 < degree I, and the upper bound reads
hilbert I t ≤ degree I * (t + k).choose k (the final form of blueprint node A08).
The two bounds are taken as hypotheses (_of_eventually_bounds for the ∀ᶠ form,
_of_bounds for the ∀ t form). They are produced, for [Infinite K] and prime I, by node
A08-core (exists_hilbert_bounds in Hilbert/DegreeUpper.lean): the lower bound comes from
a free submodule of rank Δ of the homogeneous coordinate ring over a Noether normalization, the
upper bound from the generic rank Δ. Everything here is field-free and needs no primality.
Main declarations:
Nikodym.LowerBound.lowerPoly k e: the comparison polynomial∑ i, choosePoly k ∘ (X - e i), withlowerPoly_eval_natCast,natDegree_lowerPoly_le,coeff_lowerPoly.Nikodym.LowerBound.natDegree_affineHilbertPoly_of_bounds,coeff_quotDim_affineHilbertPoly_of_bounds,degree_eq_of_bounds,leadingCoeff_affineHilbertPoly_of_bounds,degree_pos_of_bounds,hilbert_le_degree_mul_choose_of_bounds, and their_of_eventually_boundsversions.
The comparison polynomials #
Blueprint A04′: the lower comparison polynomial ∑ i, (choosePoly k).comp (X - C (e i)),
whose value at a natural number t ≥ max e is ∑ i, (t - e i + k).choose k.
Equations
- Nikodym.LowerBound.lowerPoly k e = ∑ i : Fin Δ, (Nikodym.LowerBound.choosePoly k).comp (Polynomial.X - Polynomial.C ↑(e i))
Instances For
Blueprint A04′: the coefficient of X ^ k in choosePoly k is 1 / k!.
Blueprint A04′: (C Δ * choosePoly k).eval t = Δ * (t + k).choose k for t : ℕ.
Blueprint A04′: C Δ * choosePoly k has degree at most k.
Blueprint A04′: the coefficient of X ^ k in C Δ * choosePoly k is Δ / k!.
The affine Hilbert polynomial under a two-sided bound #
Blueprint A04′: the eventual sandwich lowerPoly ≤ affineHilbertPoly I ≤ C Δ * choosePoly
along ℕ, from the two-sided bound on the Hilbert function and hilbert I t = p.eval t for
large t.
Blueprint A04′: under the eventual two-sided bound, natDegree (affineHilbertPoly I) ≤ k
and the coefficient of X ^ k is Δ / k!, where k = quotDim I.
Blueprint A04′: under the eventual two-sided bound, the coefficient of X ^ quotDim I in
the affine Hilbert polynomial is Δ / (quotDim I)!.
Blueprint A04′: under the eventual two-sided bound with 0 < Δ, the affine Hilbert
polynomial has natDegree = quotDim I.
Blueprint A04′: under the eventual two-sided bound with 0 < Δ, degree I = Δ.
Blueprint A04′: under the eventual two-sided bound with 0 < Δ, the leading coefficient of
the affine Hilbert polynomial is degree I / (quotDim I)!.
Blueprint A04′: under the eventual two-sided bound with 0 < Δ, 0 < degree I.
Blueprint A04′/A08: under the eventual lower bound and the upper bound at every t, with
0 < Δ, the Hilbert function satisfies hilbert I t ≤ degree I * (t + quotDim I).choose (quotDim I) for all t.
The ∀ t versions #
Blueprint A04′: natDegree (affineHilbertPoly I) = quotDim I from the two-sided bound
∑ i, (t - e i + k).choose k ≤ hilbert I t ≤ Δ * (t + k).choose k at every t, with 0 < Δ.
Blueprint A04′: the coefficient of X ^ quotDim I in the affine Hilbert polynomial is
Δ / (quotDim I)!, from the two-sided bound at every t.
Blueprint A04′: degree I = Δ from the two-sided bound at every t, with 0 < Δ.
Blueprint A04′: the leading coefficient of the affine Hilbert polynomial is
degree I / (quotDim I)!, from the two-sided bound at every t, with 0 < Δ.
Blueprint A04′: 0 < degree I from the two-sided bound at every t, with 0 < Δ.
Blueprint A08 (final form, modulo A08-core): hilbert I t ≤ degree I * (t + quotDim I).choose (quotDim I) for all t, from the two-sided bound at every t, with 0 < Δ.
Glue with A08-core #
Node A08-core (Hilbert/DegreeUpper.lean, exists_hilbert_bounds) supplies the two-sided bounds
for every prime over an infinite field; the resulting unconditional _of_infinite statements live
in Algebra/Assembly.lean.