Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[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. #19303

Closed
wants to merge 18 commits into from
Closed
1 change: 1 addition & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 4 additions & 0 deletions Mathlib/Data/Nat/Factorial/BigOperators.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
92 changes: 92 additions & 0 deletions Mathlib/RingTheory/Polynomial/Hilbert.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,92 @@
/-
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.
-/
FMLJohn marked this conversation as resolved.
Show resolved Hide resolved

open BigOperators Nat PowerSeries

namespace Polynomial

section greatestFactorOneSubNotDvd

variable {R : Type*} [CommRing R] (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))
FMLJohn marked this conversation as resolved.
Show resolved Hide resolved

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
FMLJohn marked this conversation as resolved.
Show resolved Hide resolved
`(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
FMLJohn marked this conversation as resolved.
Show resolved Hide resolved

end Polynomial
5 changes: 2 additions & 3 deletions Mathlib/RingTheory/PowerSeries/WellKnown.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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]
erdOne marked this conversation as resolved.
Show resolved Hide resolved

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 :=
Expand Down
7 changes: 4 additions & 3 deletions scripts/noshake.json
Original file line number Diff line number Diff line change
Expand Up @@ -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"],
kbuzzard marked this conversation as resolved.
Show resolved Hide resolved
"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":
Expand Down Expand Up @@ -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"],
Expand All @@ -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"],
Expand Down