Hilbert polynomials #
In this file, we formalise the following statement: if F is a field with characteristic 0, then
given any p : F[X] and d : ℕ, there exists some h : F[X] such that for any large enough
n : ℕ, h(n) is equal to the coefficient of Xⁿ in the power series expansion of p/(1 - X)ᵈ.
This h is unique and is denoted as Polynomial.hilbertPoly p d.
For example, given d : ℕ, the power series expansion of 1/(1 - X)ᵈ⁺¹ in F[X]
is Σₙ ((d + n).choose d)Xⁿ, which equals Σₙ ((n + 1)···(n + d)/d!)Xⁿ and hence
Polynomial.hilbertPoly (1 : F[X]) (d + 1) is the polynomial (X + 1)···(X + d)/d!. Note that
if d! = 0 in F, then the polynomial (X + 1)···(X + d)/d! no longer works, so we do not want
the characteristic of F to be divisible by d!. As Polynomial.hilbertPoly may take any
p : F[X] and d : ℕ as its inputs, it is necessary for us to assume that CharZero F.
Main definitions #
Polynomial.hilbertPoly p d. Given a fieldF, a polynomialp : F[X]and a natural numberd, ifFis of characteristic0, thenPolynomial.hilbertPoly p d : F[X]is the polynomial whose value atnequals the coefficient ofXⁿin the power series expansion ofp/(1 - X)ᵈ.
TODO #
- Hilbert polynomials of finitely generated graded modules over Noetherian rings.
For any field F and natural numbers d and k, Polynomial.preHilbertPoly F d k
is defined as (d.factorial : F)⁻¹ • ((ascPochhammer F d).comp (X - (C (k : F)) + 1)).
This is the most basic form of Hilbert polynomials. Polynomial.preHilbertPoly ℚ d 0
is exactly the Hilbert polynomial of the polynomial ring ℚ[X_0,...,X_d] viewed as
a graded module over itself. In fact, Polynomial.preHilbertPoly F d k is the
same as Polynomial.hilbertPoly ((X : F[X]) ^ k) (d + 1) for any field F and
d k : ℕ (see the lemma Polynomial.hilbertPoly_X_pow_succ). See also the lemma
Polynomial.preHilbertPoly_eq_choose_sub_add, which states that if CharZero F,
then for any d k n : ℕ with k ≤ n, (Polynomial.preHilbertPoly F d k).eval (n : F)
equals (n - k + d).choose d.
Equations
- Polynomial.preHilbertPoly F d k = (↑d.factorial)⁻¹ • (ascPochhammer F d).comp (Polynomial.X - Polynomial.C ↑k + 1)
Instances For
Polynomial.hilbertPoly p 0 = 0; for any d : ℕ, Polynomial.hilbertPoly p (d + 1)
is defined as ∑ i ∈ p.support, (p.coeff i) • Polynomial.preHilbertPoly F d i. If
M is a graded module whose Poincaré series can be written as p(X)/(1 - X)ᵈ for some
p : ℚ[X] with integer coefficients, then Polynomial.hilbertPoly p d is the Hilbert
polynomial of M. See also Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval,
which says that PowerSeries.coeff F n (p * PowerSeries.invOneSubPow F d) equals
(Polynomial.hilbertPoly p d).eval (n : F) for any large enough n : ℕ.
Equations
- p.hilbertPoly 0 = 0
- p.hilbertPoly d.succ = ∑ i ∈ p.support, p.coeff i • Polynomial.preHilbertPoly F d i
Instances For
The function that sends any p : F[X] to Polynomial.hilbertPoly p d is an F-linear map from
F[X] to F[X].
Equations
- Polynomial.hilbertPoly_linearMap F d = { toFun := fun (p : Polynomial F) => p.hilbertPoly d, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The key property of Hilbert polynomials. If F is a field with characteristic 0, p : F[X] and
d : ℕ, then for any large enough n : ℕ, (Polynomial.hilbertPoly p d).eval (n : F) equals the
coefficient of Xⁿ in the power series expansion of p/(1 - X)ᵈ.
The polynomial satisfying the key property of Polynomial.hilbertPoly p d is unique.
Alias of Polynomial.existsUnique_hilbertPoly.
The polynomial satisfying the key property of Polynomial.hilbertPoly p d is unique.
If h : F[X] and there exists some N : ℕ such that for any number n : ℕ bigger than N
we have PowerSeries.coeff F n (p * invOneSubPow F d) = h.eval (n : F), then h is exactly
Polynomial.hilbertPoly p d.