feat(RingTheory/Polynomial/Hilbert): the definition of the Hilbert polynomial in terms of a natural number d and a polynomial p : ℤ[X]
#19303
Conversation
FMLJohn
added
t-algebraic-geometry
PR summary 6e90216589Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| 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 |
There was a problem hiding this comment.
I think it would be better to get this result in this PR as well, to make sure that this is actually the right definition.
There was a problem hiding this comment.
I think it would be better to get this result in this PR as well, to make sure that this is actually the right definition.
I have already proved the statement in the Visual Studio Code of my computer, so I can guarantee that the definition has no problem. But the proof is very long. I'm afraid that if I also include the proof in this PR, then it may not be so easy to be merged to Mathlib 4. I plan to include the proof of the statement in some other PR.
But that is only my own opinion. I'm not sure if my plan is good. What's your opinion?
There was a problem hiding this comment.
Please make a separate PR dependent on this one. That one may eventually be split but the reviewers can have a fuller picture
There was a problem hiding this comment.
FMLJohn
changed the title
d and a polynomial p : ℤ[X]d and a polynomial p : ℤ[X]
FMLJohn
changed the title
d and a polynomial p : ℤ[X]d and a polynomial p : ℤ[X]
| @@ -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"], | |||
There was a problem hiding this comment.
What are these changes about? Should you be shaking the file rather than announcing you're not shaking it?
| /-! | ||
| # 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. | ||
| -/ |
There was a problem hiding this comment.
Most of this module docstring is nothing to do with what is in the file. Also, the docstring does not follow the guidelines for module docstrings https://leanprover-community.github.io/contribute/doc.html at all. Here is a suggestion for a better module docstring.
/-!
# Hilbert polynomials
In this file, we formalise the following statement: 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)ᵈ`. This `h` is unique and is called the
Hilbert polynomial of `p` and `d` (`Polynomial.hilbert p d`).
## Main definitions
* `Polynomial.hilbert p d`. If `p : ℤ[X]` and `d : ℕ` then `Polynomial.hilbert p d : ℚ[X]`
is the polynomial whose value at `n` equals the coefficient of `Xⁿ` in the power
series expansion of `p/(1 - X)ᵈ`
## TODO
* Prove that `Polynomial.hilbert p d : ℚ[X]` is the polynomial whose value at `n` equals the
coefficient of `Xⁿ` in the power series expansion of `p/(1 - X)ᵈ`
* Hilbert polynomials of graded modules.
-/
Also, it is not clear to me why you restrict to p : ℤ[X] when clearly p : ℚ[X] would work just as well. In fact why not do p : k[X] for k any field?
| 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 |
There was a problem hiding this comment.
My guess is that you are making life very hard for yourself with this definition. You already have the result when p = 1 from your previous work. Call this polynomial h_d. Now the general polynomial for p=sum a_n X^n is just sum a_n * h_d(X-n) and that's it. There's no need to split into cases or to split on the number of times (X-1) goes into p. A cleaner definition will make for cleaner proofs.
There was a problem hiding this comment.
My guess is that you are making life very hard for yourself with this definition. You already have the result when
p = 1from your previous work. Call this polynomial h_d. Now the general polynomial for p=sum a_n X^n is just sum a_n * h_d(X-n) and that's it. There's no need to split into cases or to split on the number of times (X-1) goes into p. A cleaner definition will make for cleaner proofs.
The reason I have written the definition by dividing into different cases is that later we will have a theorem (that can be accessed in #19404):
theorem natDegree_hilbert (p : ℤ[X]) (d : ℕ) (hh : hilbert p d ≠ 0) :
(hilbert p d).natDegree = d - p.rootMultiplicity 1 - 1 := ...
which specifies the degree of any non-zero Hilbert polynomial. If I don't write the definition into cases, then I'm afraid that the proof of natDegree_hilbert would be more complicated.
Given any
p : ℤ[X]andd : ℕ, there exists someh : ℚ[X]such that for any large enoughn : ℕ,PowerSeries.coeff ℤ n (p * (PowerSeries.invOneSubPow ℤ d))is equal toh.eval (n : ℚ). Thishis unique and is called the Hilbert polynomial with respect topandd(Polynomial.hilbert p d).See also the docstring of the file Mathlib/RingTheory/Polynomial/Hilbert.lean, which explains why this is useful.