[Merged by Bors] - feat(RingTheory/Polynomial/HilbertPoly): the definition and key property of Polynomial.hilbertPoly p d for p : F[X] and d : ℕ, where F is a field.

Mathlib.lean

@@ -4387,6 +4387,7 @@ import Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
 import Mathlib.RingTheory.Polynomial.GaussLemma
 import Mathlib.RingTheory.Polynomial.Hermite.Basic
 import Mathlib.RingTheory.Polynomial.Hermite.Gaussian
+import Mathlib.RingTheory.Polynomial.Hilbert
 import Mathlib.RingTheory.Polynomial.IntegralNormalization
 import Mathlib.RingTheory.Polynomial.IrreducibleRing
 import Mathlib.RingTheory.Polynomial.Nilpotent

Mathlib/Data/Nat/Factorial/BigOperators.lean

@@ -33,6 +33,10 @@ theorem prod_factorial_dvd_factorial_sum : (∏ i ∈ s, (f i)!) ∣ (∑ i ∈
   · rw [prod_cons, Finset.sum_cons]
     exact (mul_dvd_mul_left _ ih).trans (Nat.factorial_mul_factorial_dvd_factorial_add _ _)
 
+theorem ascFactorial_eq_prod_range (n : ℕ) : ∀ k, n.ascFactorial k = ∏ i ∈ range k, (n + i)
+  | 0 => rfl
+  | k + 1 => by rw [ascFactorial, prod_range_succ, mul_comm, ascFactorial_eq_prod_range n k]
+
 theorem descFactorial_eq_prod_range (n : ℕ) : ∀ k, n.descFactorial k = ∏ i ∈ range k, (n - i)
   | 0 => rfl
   | k + 1 => by rw [descFactorial, prod_range_succ, mul_comm, descFactorial_eq_prod_range n k]

Mathlib/RingTheory/Polynomial/Hilbert.lean

@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2024 Fangming Li. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fangming Li, Jujian Zhang
+-/
+import Mathlib.Algebra.Polynomial.AlgebraMap
+import Mathlib.Algebra.Polynomial.Div
+import Mathlib.Algebra.Polynomial.Eval.SMul
+import Mathlib.Data.Nat.Factorial.BigOperators
+import Mathlib.RingTheory.PowerSeries.WellKnown
+
+/-!
+# Hilbert polynomials
+
+In this file, we aim to formalise a useful fact: given any `p : ℤ[X]` and `d : ℕ`, there exists
+some `h : ℚ[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)ᵈ` (or `p * (PowerSeries.invOneSubPow ℤ d)`). This `h` is
+unique and is called the Hilbert polynomial with respect to `p` and `d` (`Polynomial.hilbert p d`).
+
+The above fact is used to construct the Hilbert polynomial of a graded module that satisfies certain
+conditions. Specifically:
+* Assume `A = ⊕ₙAₙ` is a Noetherian ring graded by `ℕ` such that `A` is generated by `a₁,...,aₛ` as
+  an `A₀`-algebra, where for each `i = 1,...,s`, `aᵢ` is a homogeneous element in `A` of degree
+  `dᵢ > 0`. Let `M = ⊕ₙMₙ` be a finitely generated `A`-module graded by `ℕ`. Then it is true that
+  each `Mₙ` is a finitely generated module over `A₀`.
+* Let `λ : C → ℤ` be an additive function, where `C` is the collection of all finitely generated
+  `A₀`-modules; in other words, given any short exact sequence `0 ⟶ N ⟶ O ⟶ P ⟶ 0` of finitely
+  generated modules over `A₀`, we have `λ(O) = λ(N) + λ(P)`. Then the Poincaré series of `M` in
+  terms of `λ` is the formal power series `P(M, λ, X) = Σₙλ(Mₙ)Xⁿ`. The Hilbert-Serre Theorem states
+  that `P(M, λ, X)` can be written as `p(X)/∏ᵢ₌₁,...,ₛ(1 - X ^ dᵢ)`, where `p(X)` is a polynomial
+  with coefficients in `ℤ`.
+* For the case when `d₁,...,dₛ = 1`, the Poincaré series of `M` with respect to `λ` can be expressed
+  as `p(X)/(1 - X)ˢ`. Hence the fact stated in the beginning guarantees an `h : ℚ[X]` such that for
+  any large enough `n : ℕ`, the coefficient of `Xⁿ` in `P(M, λ, X)` equals `h.eval (n : ℚ)`. This
+  `h` is called the Hilbert polynomial of `M` in terms of `λ`, which is what we eventually want to
+  formalise.
+-/
+
+open BigOperators Nat PowerSeries
+
+namespace Polynomial
+
+section greatestFactorOneSubNotDvd
+
+variable {R : Type*} [CommRing R] [Nontrivial R] [NoZeroDivisors R]
+variable (p : R[X]) (hp : p ≠ 0) (d : ℕ)
+
+/--
+Given a polynomial `p`, the factor `f` of `p` such that the product of `f` and
+`(1 - X : R[X]) ^ p.rootMultiplicity 1` equals `p`. We define this here because if `p` is divisible
+by `1 - X`, then the expression `p/(1 - X)ᵈ` can be reduced. We want to construct the Hilbert
+polynomial based on the most reduced form of the fraction `p/(1 - X)ᵈ`. Later we will see that this
+method of construction makes it much easier to calculate the specific degree of the Hilbert
+polynomial.
+-/
+noncomputable def greatestFactorOneSubNotDvd : R[X] :=
+  ((- 1 : R[X]) ^ p.rootMultiplicity 1) *
+  (exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp 1).choose
+
+end greatestFactorOneSubNotDvd
+
+/--
+A polynomial which makes it easier to define the Hilbert polynomial. See also the theorem
+`Polynomial.preHilbert_eq_choose_sub_add`, which states that for any `d k n : ℕ` with `k ≤ n`,
+`(Polynomial.preHilbert d k).eval (n : ℚ) = (n - k + d).choose d`.
+-/
+noncomputable def preHilbert (d k : ℕ) : ℚ[X] :=
+  (d.factorial : ℚ)⁻¹ • (∏ i : Finset.range d, (X - (C (k : ℚ)) + (C (i : ℚ)) + 1))
+
+theorem preHilbert_eq_choose_sub_add (d k n : ℕ) (hkn : k ≤ n):
+    (preHilbert d k).eval (n : ℚ) = (n - k + d).choose d := by
+  delta preHilbert; simp only [Finset.univ_eq_attach, map_natCast, eval_smul, smul_eq_mul]
+  rw [eval_prod, Finset.prod_attach _ (fun _ => eval _ (_ - _ + _ + _)), add_choose,
+    cast_div (factorial_mul_factorial_dvd_factorial_add ..) (cast_ne_zero.2 <| mul_ne_zero
+    (n - k).factorial_ne_zero d.factorial_ne_zero), cast_mul, div_mul_eq_div_div, div_eq_inv_mul,
+    mul_eq_mul_left_iff, ← cast_div (factorial_dvd_factorial <| Nat.le_add_right (n - k) d)
+    (cast_ne_zero.2 <| factorial_ne_zero (n - k)), ← ascFactorial_eq_div]
+  simp_rw [eval_add, eval_sub, eval_X, eval_natCast, eval_one, ascFactorial_eq_prod_range,
+    cast_prod, cast_add, cast_one, Nat.cast_sub hkn, add_assoc, add_comm, true_or]
+
+/--
+Given `p : ℤ[X]` and `d : ℕ`, the Hilbert polynomial of `p` and `d`. Later we will
+show that `PowerSeries.coeff ℤ n (p * (PowerSeries.invOneSubPow ℤ d))` is equal to
+`(Polynomial.hilbert p d).eval (n : ℚ)` for any large enough `n : ℕ`, which is the
+key property of the Hilbert polynomial.
+-/
+noncomputable def hilbert (p : ℤ[X]) (d : ℕ) : ℚ[X] :=
+  if h : p = 0 then 0
+  else if d ≤ p.rootMultiplicity 1 then 0
+  else ∑ i in Finset.range ((greatestFactorOneSubNotDvd p h).natDegree + 1),
+  ((greatestFactorOneSubNotDvd p h).coeff i) * preHilbert (d - (p.rootMultiplicity 1) - 1) i
+
+end Polynomial

Mathlib/RingTheory/PowerSeries/WellKnown.lean

@@ -152,10 +152,9 @@ theorem invOneSubPow_inv_eq_one_sub_pow :
   | zero => exact Eq.symm <| pow_zero _
   | succ d => rfl
 
-theorem invOneSubPow_inv_eq_one_of_eq_zero (h : d = 0) :
-    (invOneSubPow S d).inv = 1 := by
+theorem invOneSubPow_inv_zero_eq_one : (invOneSubPow S 0).inv = 1 := by
   delta invOneSubPow
-  simp only [h, Units.inv_eq_val_inv, inv_one, Units.val_one]
+  simp only [Units.inv_eq_val_inv, inv_one, Units.val_one]
 
 theorem mk_add_choose_mul_one_sub_pow_eq_one :
     (mk fun n ↦ Nat.choose (d + n) d : S⟦X⟧) * ((1 - X) ^ (d + 1)) = 1 :=

scripts/noshake.json

@@ -317,14 +317,15 @@
   "Mathlib.RingTheory.PowerSeries.Basic":
   ["Mathlib.Algebra.CharP.Defs", "Mathlib.Tactic.MoveAdd"],
   "Mathlib.RingTheory.PolynomialAlgebra": ["Mathlib.Data.Matrix.DMatrix"],
+  "Mathlib.RingTheory.Polynomial.Hilbert":
+  ["Mathlib.RingTheory.PowerSeries.WellKnown"],
   "Mathlib.RingTheory.MvPolynomial.Homogeneous":
   ["Mathlib.Algebra.DirectSum.Internal"],
   "Mathlib.RingTheory.KrullDimension.Basic":
   ["Mathlib.Algebra.MvPolynomial.CommRing", "Mathlib.Algebra.Polynomial.Basic"],
   "Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs":
   ["Mathlib.Tactic.Algebraize"],
-  "Mathlib.RingTheory.Finiteness.Defs":
-  ["Mathlib.Tactic.Algebraize"],
+  "Mathlib.RingTheory.Finiteness.Defs": ["Mathlib.Tactic.Algebraize"],
   "Mathlib.RingTheory.Binomial": ["Mathlib.Algebra.Order.Floor"],
   "Mathlib.RingTheory.Adjoin.Basic": ["Mathlib.LinearAlgebra.Finsupp.SumProd"],
   "Mathlib.RepresentationTheory.FdRep":
@@ -365,7 +366,6 @@
   "Mathlib.Deprecated.NatLemmas": ["Batteries.Data.Nat.Lemmas", "Batteries.WF"],
   "Mathlib.Deprecated.MinMax": ["Mathlib.Order.MinMax"],
   "Mathlib.Deprecated.ByteArray": ["Batteries.Data.ByteSubarray"],
-  "Mathlib.Data.ENat.Lattice": ["Mathlib.Algebra.Group.Action.Defs"],
   "Mathlib.Data.Vector.Basic": ["Mathlib.Control.Applicative"],
   "Mathlib.Data.Set.Image":
   ["Batteries.Tactic.Congr", "Mathlib.Data.Set.SymmDiff"],
@@ -387,6 +387,7 @@
   "Mathlib.Data.Int.Defs": ["Batteries.Data.Int.Order"],
   "Mathlib.Data.FunLike.Basic": ["Mathlib.Logic.Function.Basic"],
   "Mathlib.Data.Finset.Insert": ["Mathlib.Data.Finset.Attr"],
+  "Mathlib.Data.ENat.Lattice": ["Mathlib.Algebra.Group.Action.Defs"],
   "Mathlib.Data.ByteArray": ["Batteries.Data.ByteSubarray"],
   "Mathlib.Data.Bool.Basic": ["Batteries.Tactic.Init"],
   "Mathlib.Control.Traversable.Instances": ["Mathlib.Control.Applicative"],