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 field F, a polynomial p : F[X] and a natural number d, if F is of characteristic 0, then Polynomial.hilbertPoly p d : F[X] is the polynomial whose value at n equals the coefficient of Xⁿ in the power series expansion of p/(1 - X)ᵈ.

TODO

• Hilbert polynomials of finitely generated graded modules over Noetherian rings.

noncomputable def Polynomial.preHilbertPoly (F : Type u_1) [Field F] (d k : ℕ) : Polynomial F

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)

theorem Polynomial.natDegree_preHilbertPoly (F : Type u_1) [Field F] [CharZero F] (d k : ℕ) : (Polynomial.preHilbertPoly F d k).natDegree = d

theorem Polynomial.coeff_preHilbertPoly_self (F : Type u_1) [Field F] [CharZero F] (d k : ℕ) : (Polynomial.preHilbertPoly F d k).coeff d = (↑d.factorial)⁻¹

theorem Polynomial.leadingCoeff_preHilbertPoly (F : Type u_1) [Field F] [CharZero F] (d k : ℕ) : (Polynomial.preHilbertPoly F d k).leadingCoeff = (↑d.factorial)⁻¹

theorem Polynomial.preHilbertPoly_eq_choose_sub_add (F : Type u_1) [Field F] [CharZero F] (d : ℕ) {k n : ℕ} (hkn : k ≤ n) : Polynomial.eval (↑n) (Polynomial.preHilbertPoly F d k) = ↑((n - k + d).choose d)

noncomputable def Polynomial.hilbertPoly {F : Type u_1} [Field F] (p : Polynomial F) (d : ℕ) : Polynomial F

Polynomial.hilbertPoly p 0 = 0; for any d : ℕ, Polynomial.hilbertPoly p (d + 1) is defined as ∑ i in 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

theorem Polynomial.hilbertPoly_zero_left {F : Type u_1} [Field F] (d : ℕ) : Polynomial.hilbertPoly 0 d = 0

theorem Polynomial.hilbertPoly_zero_right {F : Type u_1} [Field F] (p : Polynomial F) : p.hilbertPoly 0 = 0

theorem Polynomial.hilbertPoly_succ {F : Type u_1} [Field F] (p : Polynomial F) (d : ℕ) : p.hilbertPoly (d + 1) = ∑ i ∈ p.support, p.coeff i • Polynomial.preHilbertPoly F d i

theorem Polynomial.hilbertPoly_X_pow_succ {F : Type u_1} [Field F] (d k : ℕ) : (Polynomial.X ^ k).hilbertPoly (d + 1) = Polynomial.preHilbertPoly F d k

theorem Polynomial.hilbertPoly_add_left {F : Type u_1} [Field F] (p q : Polynomial F) (d : ℕ) : (p + q).hilbertPoly d = p.hilbertPoly d + q.hilbertPoly d

theorem Polynomial.hilbertPoly_smul {F : Type u_1} [Field F] (a : F) (p : Polynomial F) (d : ℕ) : (a • p).hilbertPoly d = a • p.hilbertPoly d

noncomputable def Polynomial.hilbertPoly_linearMap (F : Type u_1) [Field F] (d : ℕ) : Polynomial F →ₗ[F] Polynomial F

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' := ⋯ }

theorem Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval {F : Type u_1} [Field F] [CharZero F] {p : Polynomial F} (d : ℕ) {n : ℕ} (hn : p.natDegree < n) : (PowerSeries.coeff F n) (↑p * ↑(PowerSeries.invOneSubPow F d)) = Polynomial.eval (↑n) (p.hilbertPoly d)

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)ᵈ.

theorem Polynomial.existsUnique_hilbertPoly {F : Type u_1} [Field F] [CharZero F] (p : Polynomial F) (d : ℕ) : ∃! h : Polynomial F, ∃ (N : ℕ), ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(PowerSeries.invOneSubPow F d)) = Polynomial.eval (↑n) h

The polynomial satisfying the key property of Polynomial.hilbertPoly p d is unique.

@[deprecated Polynomial.existsUnique_hilbertPoly]

theorem Polynomial.exists_unique_hilbertPoly {F : Type u_1} [Field F] [CharZero F] (p : Polynomial F) (d : ℕ) : ∃! h : Polynomial F, ∃ (N : ℕ), ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(PowerSeries.invOneSubPow F d)) = Polynomial.eval (↑n) h

Alias of Polynomial.existsUnique_hilbertPoly.

---

The polynomial satisfying the key property of Polynomial.hilbertPoly p d is unique.

theorem Polynomial.eq_hilbertPoly_of_forall_coeff_eq_eval {F : Type u_1} [Field F] [CharZero F] {p h : Polynomial F} {d : ℕ} (N : ℕ) (hhN : ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(PowerSeries.invOneSubPow F d)) = Polynomial.eval (↑n) h) : h = p.hilbertPoly d

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.

theorem Polynomial.hilbertPoly_mul_one_sub_succ {F : Type u_1} [Field F] [CharZero F] (p : Polynomial F) (d : ℕ) : (p * (1 - Polynomial.X)).hilbertPoly (d + 1) = p.hilbertPoly d

theorem Polynomial.hilbertPoly_mul_one_sub_pow_add {F : Type u_1} [Field F] [CharZero F] (p : Polynomial F) (d e : ℕ) : (p * (1 - Polynomial.X) ^ e).hilbertPoly (d + e) = p.hilbertPoly d

theorem Polynomial.hilbertPoly_eq_zero_of_le_rootMultiplicity_one {F : Type u_1} [Field F] [CharZero F] {p : Polynomial F} {d : ℕ} (hdp : d ≤ Polynomial.rootMultiplicity 1 p) : p.hilbertPoly d = 0

theorem Polynomial.natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt {F : Type u_1} [Field F] [CharZero F] {p : Polynomial F} {d : ℕ} (hp : p ≠ 0) (hpd : Polynomial.rootMultiplicity 1 p < d) : (p.hilbertPoly d).natDegree = d - Polynomial.rootMultiplicity 1 p - 1

theorem Polynomial.natDegree_hilbertPoly_of_ne_zero {F : Type u_1} [Field F] [CharZero F] {p : Polynomial F} {d : ℕ} (hh : p.hilbertPoly d ≠ 0) : (p.hilbertPoly d).natDegree = d - Polynomial.rootMultiplicity 1 p - 1