From a249cba40330594cd38fe9bd46af60c5162a253a Mon Sep 17 00:00:00 2001 From: FMLJohn <417963616@qq.com> Date: Wed, 20 Nov 2024 20:19:35 +0000 Subject: [PATCH 01/16] defined hilbert polynomials --- Mathlib.lean | 1 + Mathlib/Data/Nat/Factorial/BigOperators.lean | 4 + Mathlib/RingTheory/Polynomial/Hilbert.lean | 92 +++++++++++++++++++ Mathlib/RingTheory/PowerSeries/WellKnown.lean | 5 +- 4 files changed, 99 insertions(+), 3 deletions(-) create mode 100644 Mathlib/RingTheory/Polynomial/Hilbert.lean diff --git a/Mathlib.lean b/Mathlib.lean index 7566572fa39e6..9c246dd493249 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Data/Nat/Factorial/BigOperators.lean b/Mathlib/Data/Nat/Factorial/BigOperators.lean index 56a55af7e4af1..606f5b7c49b2d 100644 --- a/Mathlib/Data/Nat/Factorial/BigOperators.lean +++ b/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] diff --git a/Mathlib/RingTheory/Polynomial/Hilbert.lean b/Mathlib/RingTheory/Polynomial/Hilbert.lean new file mode 100644 index 0000000000000..c24a2d7e3e304 --- /dev/null +++ b/Mathlib/RingTheory/Polynomial/Hilbert.lean @@ -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.Eval.SMul +import Mathlib.Algebra.Polynomial.RingDivision +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 diff --git a/Mathlib/RingTheory/PowerSeries/WellKnown.lean b/Mathlib/RingTheory/PowerSeries/WellKnown.lean index 292659bb8862f..0cff04b7bee73 100644 --- a/Mathlib/RingTheory/PowerSeries/WellKnown.lean +++ b/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 := From 6a38e3854277c458ed58b7406742efcc6cee605b Mon Sep 17 00:00:00 2001 From: FMLJohn <417963616@qq.com> Date: Wed, 20 Nov 2024 20:31:52 +0000 Subject: [PATCH 02/16] removed unused imports --- Mathlib/RingTheory/Polynomial/Hilbert.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Polynomial/Hilbert.lean b/Mathlib/RingTheory/Polynomial/Hilbert.lean index c24a2d7e3e304..46ea97301b2be 100644 --- a/Mathlib/RingTheory/Polynomial/Hilbert.lean +++ b/Mathlib/RingTheory/Polynomial/Hilbert.lean @@ -3,8 +3,9 @@ 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.Algebra.Polynomial.RingDivision import Mathlib.Data.Nat.Factorial.BigOperators import Mathlib.RingTheory.PowerSeries.WellKnown From 950a37865cfc8935fb95b7025961de41de6a29e9 Mon Sep 17 00:00:00 2001 From: FMLJohn <417963616@qq.com> Date: Thu, 21 Nov 2024 11:30:25 +0000 Subject: [PATCH 03/16] lake exe shake --update --- scripts/noshake.json | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/scripts/noshake.json b/scripts/noshake.json index 23b0f103e1de8..b6b91bdfc8240 100644 --- a/scripts/noshake.json +++ b/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"], From 2339e8e91a83b64e0e511d5e9b0b2da52aed6328 Mon Sep 17 00:00:00 2001 From: FMLJohn <417963616@qq.com> Date: Sat, 23 Nov 2024 12:26:14 +0000 Subject: [PATCH 04/16] proved the key property of Hilbert polynomials --- Mathlib/RingTheory/Polynomial/Hilbert.lean | 127 ++++++++++++++++++++- 1 file changed, 121 insertions(+), 6 deletions(-) diff --git a/Mathlib/RingTheory/Polynomial/Hilbert.lean b/Mathlib/RingTheory/Polynomial/Hilbert.lean index 46ea97301b2be..f69b14f171c13 100644 --- a/Mathlib/RingTheory/Polynomial/Hilbert.lean +++ b/Mathlib/RingTheory/Polynomial/Hilbert.lean @@ -42,8 +42,7 @@ namespace Polynomial section greatestFactorOneSubNotDvd -variable {R : Type*} [CommRing R] [Nontrivial R] [NoZeroDivisors R] -variable (p : R[X]) (hp : p ≠ 0) (d : ℕ) +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 @@ -57,6 +56,51 @@ noncomputable def greatestFactorOneSubNotDvd : R[X] := ((- 1 : R[X]) ^ p.rootMultiplicity 1) * (exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp 1).choose +local notation "gFOSND" => greatestFactorOneSubNotDvd + +theorem pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq : + ((1 - X : R[X]) ^ p.rootMultiplicity 1) * greatestFactorOneSubNotDvd p hp = p := by + rw [greatestFactorOneSubNotDvd, ← mul_assoc, ← mul_pow] + simp only [mul_neg, mul_one, neg_sub, map_one] + exact id (exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp 1).choose_spec.1.symm + +theorem greatestFactorOneSubNotDvd_ne_zero : + greatestFactorOneSubNotDvd p hp ≠ 0 := fun h0 => by + let hpow := pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq p hp + rw [h0, mul_zero] at hpow; exact hp <| id hpow.symm + +theorem natDegree_greatestFactorOneSubNotDvd_le [Nontrivial R] [NoZeroDivisors R] : + (greatestFactorOneSubNotDvd p hp).natDegree ≤ p.natDegree := by + have : p.natDegree = ((1 - X : R[X]) ^ p.rootMultiplicity 1 * gFOSND p hp).natDegree := by + rw [pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq] + rw [this, natDegree_mul] + · exact (gFOSND p hp).natDegree.le_add_left (natDegree ((1 - X) ^ p.rootMultiplicity 1)) + · exact pow_ne_zero _ <| fun h0 => by + let this : (1 - X : R[X]).coeff 0 = 0 := by rw [h0]; simp only [coeff_zero]; + simp only [coeff_sub, coeff_one_zero, coeff_X_zero, sub_zero, one_ne_zero] at this + exact greatestFactorOneSubNotDvd_ne_zero p hp + +theorem natDegree_pow_rootMultiplicity_sub_mul_greatestFactorOneSubNotDvd_le + [Nontrivial R] [NoZeroDivisors R] (hp1 : d ≤ p.rootMultiplicity 1) : + ((1 - X) ^ ((p.rootMultiplicity 1) - d) * greatestFactorOneSubNotDvd p hp).natDegree + ≤ p.natDegree := by + let this := pow_ne_zero (p.rootMultiplicity 1 - d) <| fun (h0 : (1 - X : R[X]) = 0) => by + let this : (1 - X : R[X]).coeff 0 = 0 := by rw [h0, coeff_zero]; + simp only [coeff_sub, coeff_one_zero, coeff_X_zero, sub_zero, one_ne_zero] at this + rw [show p.natDegree = ((((1 - X : R[X]) ^ (p.rootMultiplicity 1 - d + d))) * + (gFOSND p hp)).natDegree by rw [← Nat.eq_add_of_sub_eq hp1 rfl, + pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq], pow_add, mul_assoc, + mul_comm ((1 - X) ^ d), ← mul_assoc, natDegree_mul, natDegree_mul, natDegree_mul] + · simp only [natDegree_pow, le_add_iff_nonneg_right, zero_le] + · exact this + · exact greatestFactorOneSubNotDvd_ne_zero p hp + · rw [mul_ne_zero_iff]; exact ⟨this, greatestFactorOneSubNotDvd_ne_zero p hp⟩ + · exact pow_ne_zero _ <| fun h0 => by + let this : (1 - X : R[X]).coeff 0 = 0 := by rw [h0, coeff_zero]; + simp only [coeff_sub, coeff_one_zero, coeff_X_zero, sub_zero, one_ne_zero] at this + · exact this + · exact greatestFactorOneSubNotDvd_ne_zero p hp + end greatestFactorOneSubNotDvd /-- @@ -67,6 +111,8 @@ A polynomial which makes it easier to define the Hilbert polynomial. See also th noncomputable def preHilbert (d k : ℕ) : ℚ[X] := (d.factorial : ℚ)⁻¹ • (∏ i : Finset.range d, (X - (C (k : ℚ)) + (C (i : ℚ)) + 1)) +local notation "gFOSND" => greatestFactorOneSubNotDvd + 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] @@ -79,10 +125,10 @@ theorem preHilbert_eq_choose_sub_add (d k n : ℕ) (hkn : k ≤ n): 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. +Given `p : ℤ[X]` and `d : ℕ`, the Hilbert polynomial of `p` and `d`. +See also `Polynomial.coeff_mul_invOneSubPow_eq_hilbert_eval`, which says +that `PowerSeries.coeff ℤ n (p * (@invOneSubPow ℤ _ d))` is equal to +`(Polynomial.hilbert p d).eval (n : ℚ)` for any large enough `n : ℕ`. -/ noncomputable def hilbert (p : ℤ[X]) (d : ℕ) : ℚ[X] := if h : p = 0 then 0 @@ -90,4 +136,73 @@ noncomputable def hilbert (p : ℤ[X]) (d : ℕ) : ℚ[X] := else ∑ i in Finset.range ((greatestFactorOneSubNotDvd p h).natDegree + 1), ((greatestFactorOneSubNotDvd p h).coeff i) * preHilbert (d - (p.rootMultiplicity 1) - 1) i +/-- +Given `p : ℤ[X]` and `d : ℕ`. The key property of the Hilbert polynomial with respect to +`p` and `d`, which says that for any term of `p * (@invOneSubPow ℤ _ d)` whose degree is +large enough, its coefficient can be obtained by evaluating the Hilbert polynomial. +-/ +theorem coeff_mul_invOneSubPow_eq_hilbert_eval (p : ℤ[X]) (d n : ℕ) (hn : p.natDegree < n) : + PowerSeries.coeff ℤ n (p * (@invOneSubPow ℤ _ d)) = (hilbert p d).eval (n : ℚ) := by + rw [hilbert]; by_cases h : p = 0 + · simp only [h, coe_zero, zero_mul, map_zero, Int.cast_zero, reduceDIte, eval_zero] + · simp only [h, reduceDIte, zsmul_eq_mul] + have coe_one_sub : (1 - X : ℤ[X]).toPowerSeries = 1 - (PowerSeries.X : ℤ⟦X⟧) := by + simp only [coe_sub, coe_one, coe_X] + by_cases h1 : d ≤ p.rootMultiplicity 1 + · simp only [h1, ↓reduceIte, eval_zero, Int.cast_eq_zero] + rw [← pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq p h, mul_comm, coe_mul, + ← mul_assoc, coe_pow, coe_one_sub, ← @Nat.sub_add_cancel (p.rootMultiplicity 1) + d h1, mul_comm (invOneSubPow ℤ d).val, pow_add, mul_assoc ((1 - PowerSeries.X) ^ + (p.rootMultiplicity 1 - d))] + rw [← PowerSeries.invOneSubPow_inv_eq_one_sub_pow ℤ d, Units.inv_eq_val_inv, Units.inv_mul, + mul_one, ← coe_one_sub, ← coe_pow, ← coe_mul, coeff_coe] + exact coeff_eq_zero_of_natDegree_lt (lt_of_le_of_lt + (natDegree_pow_rootMultiplicity_sub_mul_greatestFactorOneSubNotDvd_le p h d h1) hn) + · simp only [h1, ↓reduceIte] + rw [coe_inj.2 (pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq p h).symm, coe_mul, + mul_comm ((1 - X : ℤ[X]) ^ p.rootMultiplicity 1).toPowerSeries, mul_assoc, + invOneSubPow_eq_inv_one_sub_pow, show d = p.rootMultiplicity 1 + + (d - p.rootMultiplicity 1) by rw [Nat.add_sub_of_le <| Nat.le_of_not_ge h1], pow_add, + Units.val_mul, ← mul_assoc ((1 - X : ℤ[X]) ^ rootMultiplicity 1 p).toPowerSeries, coe_pow, + coe_one_sub, ← invOneSubPow_eq_inv_one_sub_pow, ← invOneSubPow_inv_eq_one_sub_pow ℤ + (rootMultiplicity 1 p), Units.inv_eq_val_inv, Units.inv_mul, one_mul] + simp only [inv_pow, add_tsub_cancel_left, ← inv_pow, + ← PowerSeries.invOneSubPow_eq_inv_one_sub_pow] + have hhh : 0 < d - rootMultiplicity 1 p := by + simp at h1 + exact zero_lt_sub_of_lt h1 + rw [PowerSeries.invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos _ _ hhh] + rw [show (gFOSND p h).toPowerSeries = (Finset.sum (Finset.range ((gFOSND p h).natDegree + 1)) + (fun (i : ℕ) => ((gFOSND p h).coeff i) • (X ^ i)) : ℤ[X]).toPowerSeries by + simp only [zsmul_eq_mul, coe_inj]; exact as_sum_range_C_mul_X_pow (gFOSND p h)] + simp only [zsmul_eq_mul]; rw [eval_finset_sum]; simp only [eval_mul] + rw [(Finset.sum_eq_sum_iff_of_le (fun i hi => by + simp only [Subtype.forall, Finset.mem_range] at *; rw [preHilbert_eq_choose_sub_add + (d - p.rootMultiplicity 1 - 1) i n <| Nat.le_trans (Nat.le_of_lt_succ hi) (le_trans + (natDegree_greatestFactorOneSubNotDvd_le p h) (le_of_lt hn))])).2 <| fun i hi => by + simp only [Subtype.forall, Finset.mem_range, mul_eq_mul_left_iff, Int.cast_eq_zero] at *; + exact Or.intro_left _ <| preHilbert_eq_choose_sub_add (d - p.rootMultiplicity 1 - 1) i n <| + Nat.le_trans (Nat.le_of_lt_succ hi) (le_trans (natDegree_greatestFactorOneSubNotDvd_le p h) + (le_of_lt hn)), PowerSeries.coeff_mul] + simp only [coeff_coe, finset_sum_coeff, coeff_intCast_mul, Int.cast_id, coeff_X_pow, mul_ite, + mul_one, mul_zero, Finset.sum_ite_eq, Finset.mem_range, coeff_mk, ite_mul, zero_mul, + Int.cast_sum, Int.cast_ite, Int.cast_mul, Int.cast_ofNat, Int.cast_zero] + rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, + show n.succ = (gFOSND p h).natDegree + 1 + (n.succ - ((gFOSND p h).natDegree + 1)) by + simp only [Nat.succ_sub_succ_eq_sub]; rw [add_assoc, add_comm, add_assoc, + Nat.sub_add_cancel (le_trans (natDegree_greatestFactorOneSubNotDvd_le p h) (le_of_lt hn))]; + exact n.succ_eq_one_add, Finset.sum_range_add] + simp only [Nat.succ_sub_succ_eq_sub, add_lt_iff_neg_left, not_lt_zero', ↓reduceIte, + Finset.sum_const_zero, add_zero] + rw [Finset.sum_eq_sum_iff_of_le] + · intro i hi + simp only [Finset.mem_range] at hi + simp only [hi, mul_eq_mul_left_iff] + rw [add_comm] + simp only [↓reduceIte, Int.cast_natCast, eval_intCast] + · intro i hi + simp only [Finset.mem_range] at hi + simp only [hi, ↓reduceIte, Int.cast_natCast, eval_intCast] + rw [add_comm] + end Polynomial From 6694b584899bc62f963357b7f22ce3c9f245ab4b Mon Sep 17 00:00:00 2001 From: FMLJohn <417963616@qq.com> Date: Sat, 23 Nov 2024 19:14:14 +0000 Subject: [PATCH 05/16] simplified a bunch of codes --- Mathlib/RingTheory/Polynomial/Hilbert.lean | 92 +++++++++------------- 1 file changed, 36 insertions(+), 56 deletions(-) diff --git a/Mathlib/RingTheory/Polynomial/Hilbert.lean b/Mathlib/RingTheory/Polynomial/Hilbert.lean index f69b14f171c13..2ad1b84700826 100644 --- a/Mathlib/RingTheory/Polynomial/Hilbert.lean +++ b/Mathlib/RingTheory/Polynomial/Hilbert.lean @@ -84,21 +84,19 @@ theorem natDegree_pow_rootMultiplicity_sub_mul_greatestFactorOneSubNotDvd_le [Nontrivial R] [NoZeroDivisors R] (hp1 : d ≤ p.rootMultiplicity 1) : ((1 - X) ^ ((p.rootMultiplicity 1) - d) * greatestFactorOneSubNotDvd p hp).natDegree ≤ p.natDegree := by - let this := pow_ne_zero (p.rootMultiplicity 1 - d) <| fun (h0 : (1 - X : R[X]) = 0) => by - let this : (1 - X : R[X]).coeff 0 = 0 := by rw [h0, coeff_zero]; - simp only [coeff_sub, coeff_one_zero, coeff_X_zero, sub_zero, one_ne_zero] at this + have : (1 - X : R[X]) ≠ 0 := fun h0 => by + let h : (1 - X : R[X]).coeff 0 = 0 := by rw [h0, coeff_zero]; + simp only [coeff_sub, coeff_one_zero, coeff_X_zero, sub_zero, one_ne_zero] at h rw [show p.natDegree = ((((1 - X : R[X]) ^ (p.rootMultiplicity 1 - d + d))) * (gFOSND p hp)).natDegree by rw [← Nat.eq_add_of_sub_eq hp1 rfl, pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq], pow_add, mul_assoc, mul_comm ((1 - X) ^ d), ← mul_assoc, natDegree_mul, natDegree_mul, natDegree_mul] · simp only [natDegree_pow, le_add_iff_nonneg_right, zero_le] - · exact this + · exact pow_ne_zero _ this · exact greatestFactorOneSubNotDvd_ne_zero p hp - · rw [mul_ne_zero_iff]; exact ⟨this, greatestFactorOneSubNotDvd_ne_zero p hp⟩ - · exact pow_ne_zero _ <| fun h0 => by - let this : (1 - X : R[X]).coeff 0 = 0 := by rw [h0, coeff_zero]; - simp only [coeff_sub, coeff_one_zero, coeff_X_zero, sub_zero, one_ne_zero] at this - · exact this + · rw [mul_ne_zero_iff]; exact ⟨pow_ne_zero _ this, greatestFactorOneSubNotDvd_ne_zero p hp⟩ + · exact pow_ne_zero _ this + · exact pow_ne_zero _ this · exact greatestFactorOneSubNotDvd_ne_zero p hp end greatestFactorOneSubNotDvd @@ -149,60 +147,42 @@ theorem coeff_mul_invOneSubPow_eq_hilbert_eval (p : ℤ[X]) (d n : ℕ) (hn : p. have coe_one_sub : (1 - X : ℤ[X]).toPowerSeries = 1 - (PowerSeries.X : ℤ⟦X⟧) := by simp only [coe_sub, coe_one, coe_X] by_cases h1 : d ≤ p.rootMultiplicity 1 - · simp only [h1, ↓reduceIte, eval_zero, Int.cast_eq_zero] + · simp only [h1, reduceIte, eval_zero, Int.cast_eq_zero] rw [← pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq p h, mul_comm, coe_mul, - ← mul_assoc, coe_pow, coe_one_sub, ← @Nat.sub_add_cancel (p.rootMultiplicity 1) - d h1, mul_comm (invOneSubPow ℤ d).val, pow_add, mul_assoc ((1 - PowerSeries.X) ^ - (p.rootMultiplicity 1 - d))] - rw [← PowerSeries.invOneSubPow_inv_eq_one_sub_pow ℤ d, Units.inv_eq_val_inv, Units.inv_mul, - mul_one, ← coe_one_sub, ← coe_pow, ← coe_mul, coeff_coe] + ← mul_assoc, coe_pow, coe_one_sub, ← Nat.sub_add_cancel h1, mul_comm (invOneSubPow ℤ d).val, + pow_add, mul_assoc (_ ^ _), ← invOneSubPow_inv_eq_one_sub_pow ℤ d, Units.inv_eq_val_inv, + Units.inv_mul, mul_one, ← coe_one_sub, ← coe_pow, ← coe_mul, coeff_coe] exact coeff_eq_zero_of_natDegree_lt (lt_of_le_of_lt (natDegree_pow_rootMultiplicity_sub_mul_greatestFactorOneSubNotDvd_le p h d h1) hn) - · simp only [h1, ↓reduceIte] + · simp only [h1, reduceIte] rw [coe_inj.2 (pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq p h).symm, coe_mul, - mul_comm ((1 - X : ℤ[X]) ^ p.rootMultiplicity 1).toPowerSeries, mul_assoc, - invOneSubPow_eq_inv_one_sub_pow, show d = p.rootMultiplicity 1 + - (d - p.rootMultiplicity 1) by rw [Nat.add_sub_of_le <| Nat.le_of_not_ge h1], pow_add, - Units.val_mul, ← mul_assoc ((1 - X : ℤ[X]) ^ rootMultiplicity 1 p).toPowerSeries, coe_pow, - coe_one_sub, ← invOneSubPow_eq_inv_one_sub_pow, ← invOneSubPow_inv_eq_one_sub_pow ℤ - (rootMultiplicity 1 p), Units.inv_eq_val_inv, Units.inv_mul, one_mul] - simp only [inv_pow, add_tsub_cancel_left, ← inv_pow, - ← PowerSeries.invOneSubPow_eq_inv_one_sub_pow] - have hhh : 0 < d - rootMultiplicity 1 p := by - simp at h1 - exact zero_lt_sub_of_lt h1 - rw [PowerSeries.invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos _ _ hhh] - rw [show (gFOSND p h).toPowerSeries = (Finset.sum (Finset.range ((gFOSND p h).natDegree + 1)) - (fun (i : ℕ) => ((gFOSND p h).coeff i) • (X ^ i)) : ℤ[X]).toPowerSeries by - simp only [zsmul_eq_mul, coe_inj]; exact as_sum_range_C_mul_X_pow (gFOSND p h)] - simp only [zsmul_eq_mul]; rw [eval_finset_sum]; simp only [eval_mul] - rw [(Finset.sum_eq_sum_iff_of_le (fun i hi => by - simp only [Subtype.forall, Finset.mem_range] at *; rw [preHilbert_eq_choose_sub_add - (d - p.rootMultiplicity 1 - 1) i n <| Nat.le_trans (Nat.le_of_lt_succ hi) (le_trans - (natDegree_greatestFactorOneSubNotDvd_le p h) (le_of_lt hn))])).2 <| fun i hi => by - simp only [Subtype.forall, Finset.mem_range, mul_eq_mul_left_iff, Int.cast_eq_zero] at *; - exact Or.intro_left _ <| preHilbert_eq_choose_sub_add (d - p.rootMultiplicity 1 - 1) i n <| - Nat.le_trans (Nat.le_of_lt_succ hi) (le_trans (natDegree_greatestFactorOneSubNotDvd_le p h) - (le_of_lt hn)), PowerSeries.coeff_mul] + mul_comm ((_ : ℤ[X]) ^ _).toPowerSeries, mul_assoc, invOneSubPow_eq_inv_one_sub_pow, + ← Nat.add_sub_of_le (Nat.le_of_not_ge h1), pow_add, Units.val_mul, ← mul_assoc + ((_ : ℤ[X]) ^ _).toPowerSeries, coe_pow, coe_one_sub, ← invOneSubPow_eq_inv_one_sub_pow, + ← invOneSubPow_inv_eq_one_sub_pow, Units.inv_eq_val_inv, add_tsub_cancel_left, + ← invOneSubPow_eq_inv_one_sub_pow, invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos _ _ <| + zero_lt_sub_of_lt <| gt_of_not_le h1, Units.inv_mul, one_mul, coe_inj.2 <| + as_sum_range_C_mul_X_pow _, eval_finset_sum] + simp only [eq_intCast, eval_mul] + rw [PowerSeries.coeff_mul, ← Finset.sum_coe_sort _ (fun _ => eval .. * _)] + simp_rw [show ∀ (x : Finset.range _), eval _ (preHilbert (d - rootMultiplicity 1 p - 1) _) = + _ by intro x; rw [preHilbert_eq_choose_sub_add]; exact Nat.le_trans (Nat.le_of_lt_succ + (lt_add_one_of_le (Finset.mem_range_succ_iff.1 x.2))) (le_trans + (natDegree_greatestFactorOneSubNotDvd_le p h) (le_of_lt hn))] + rw [Finset.sum_coe_sort _ (fun x => eval _ (@Int.cast ℚ[X] ..) * + (n - x + (d - rootMultiplicity 1 p - 1)).choose (d - rootMultiplicity 1 p - 1))] simp only [coeff_coe, finset_sum_coeff, coeff_intCast_mul, Int.cast_id, coeff_X_pow, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq, Finset.mem_range, coeff_mk, ite_mul, zero_mul, Int.cast_sum, Int.cast_ite, Int.cast_mul, Int.cast_ofNat, Int.cast_zero] - rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, - show n.succ = (gFOSND p h).natDegree + 1 + (n.succ - ((gFOSND p h).natDegree + 1)) by - simp only [Nat.succ_sub_succ_eq_sub]; rw [add_assoc, add_comm, add_assoc, - Nat.sub_add_cancel (le_trans (natDegree_greatestFactorOneSubNotDvd_le p h) (le_of_lt hn))]; - exact n.succ_eq_one_add, Finset.sum_range_add] - simp only [Nat.succ_sub_succ_eq_sub, add_lt_iff_neg_left, not_lt_zero', ↓reduceIte, + rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, Eq.symm <| add_sub_of_le <| + succ_le_succ <| le_trans (natDegree_greatestFactorOneSubNotDvd_le p h) (le_of_lt hn), + Finset.sum_range_add] + simp only [succ_sub_succ_eq_sub, add_lt_iff_neg_left, not_lt_zero', reduceIte, Finset.sum_const_zero, add_zero] - rw [Finset.sum_eq_sum_iff_of_le] - · intro i hi - simp only [Finset.mem_range] at hi - simp only [hi, mul_eq_mul_left_iff] - rw [add_comm] - simp only [↓reduceIte, Int.cast_natCast, eval_intCast] - · intro i hi - simp only [Finset.mem_range] at hi - simp only [hi, ↓reduceIte, Int.cast_natCast, eval_intCast] - rw [add_comm] + exact (Finset.sum_eq_sum_iff_of_le (fun i hi => by + simp only [Finset.mem_range] at hi; simp only [hi, reduceIte]; + rw [Int.cast_natCast, eval_intCast, add_comm])).2 (fun i hi => by + rw [Finset.mem_range] at hi; simp only [hi, reduceIte]; rw [add_comm]; + simp only [Int.cast_natCast, eval_intCast]) end Polynomial From 0c99f07f60452ab5b7ab2163f9022fde748c020b Mon Sep 17 00:00:00 2001 From: FMLJohn <417963616@qq.com> Date: Tue, 26 Nov 2024 15:51:16 +0000 Subject: [PATCH 06/16] added `natDegree_hilbert` --- Mathlib/RingTheory/Polynomial/Hilbert.lean | 89 +++++++++++++++++++--- 1 file changed, 78 insertions(+), 11 deletions(-) diff --git a/Mathlib/RingTheory/Polynomial/Hilbert.lean b/Mathlib/RingTheory/Polynomial/Hilbert.lean index 2ad1b84700826..f1406ee6dbb08 100644 --- a/Mathlib/RingTheory/Polynomial/Hilbert.lean +++ b/Mathlib/RingTheory/Polynomial/Hilbert.lean @@ -6,7 +6,10 @@ Authors: Fangming Li, Jujian Zhang import Mathlib.Algebra.Polynomial.AlgebraMap import Mathlib.Algebra.Polynomial.Div import Mathlib.Algebra.Polynomial.Eval.SMul +import Mathlib.Algebra.Polynomial.Roots import Mathlib.Data.Nat.Factorial.BigOperators +import Mathlib.Order.Interval.Set.Infinite +import Mathlib.RingTheory.Polynomial.Pochhammer import Mathlib.RingTheory.PowerSeries.WellKnown /-! @@ -107,25 +110,21 @@ A polynomial which makes it easier to define the Hilbert polynomial. See also th `(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)) + (d.factorial : ℚ)⁻¹ • ((ascPochhammer ℚ d).comp (X - (C (k : ℚ)) + 1)) local notation "gFOSND" => greatestFactorOneSubNotDvd 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] + rw [preHilbert, eval_smul, eval_comp, map_natCast, eval_add, eval_sub, eval_X, eval_natCast, + eval_one, smul_eq_mul, ← cast_sub hkn, ← cast_add_one, ← ascPochhammer_eval_cast, + ascPochhammer_nat_eq_ascFactorial, ascFactorial_eq_factorial_mul_choose, cast_mul, + ← mul_assoc, ← div_eq_inv_mul, div_self (cast_ne_zero.2 (factorial_ne_zero d)), one_mul] /-- Given `p : ℤ[X]` and `d : ℕ`, the Hilbert polynomial of `p` and `d`. See also `Polynomial.coeff_mul_invOneSubPow_eq_hilbert_eval`, which says -that `PowerSeries.coeff ℤ n (p * (@invOneSubPow ℤ _ d))` is equal to +that `PowerSeries.coeff ℤ n (p * (invOneSubPow ℤ d))` is equal to `(Polynomial.hilbert p d).eval (n : ℚ)` for any large enough `n : ℕ`. -/ noncomputable def hilbert (p : ℤ[X]) (d : ℕ) : ℚ[X] := @@ -136,7 +135,7 @@ noncomputable def hilbert (p : ℤ[X]) (d : ℕ) : ℚ[X] := /-- Given `p : ℤ[X]` and `d : ℕ`. The key property of the Hilbert polynomial with respect to -`p` and `d`, which says that for any term of `p * (@invOneSubPow ℤ _ d)` whose degree is +`p` and `d`, which says that for any term of `p * (invOneSubPow ℤ d)` whose degree is large enough, its coefficient can be obtained by evaluating the Hilbert polynomial. -/ theorem coeff_mul_invOneSubPow_eq_hilbert_eval (p : ℤ[X]) (d n : ℕ) (hn : p.natDegree < n) : @@ -185,4 +184,72 @@ theorem coeff_mul_invOneSubPow_eq_hilbert_eval (p : ℤ[X]) (d n : ℕ) (hn : p. rw [Finset.mem_range] at hi; simp only [hi, reduceIte]; rw [add_comm]; simp only [Int.cast_natCast, eval_intCast]) +/-- +The Hilbert polynomial is unique. In other words, for any `h : ℚ[X]`, if `h` +satisfies the key property of the Hilbert polynomial (i.e. for any large enough +`n : ℕ`, `PowerSeries.coeff ℤ n (p * (invOneSubPow ℤ d)) = h.eval (n : ℚ)`), +then `h` is the Hilbert polynomial. +-/ +theorem exists_unique_hilbert (p : Polynomial ℤ) (d : ℕ) : + ∃! (h : ℚ[X]), (∃ (N : ℕ), (∀ (n : ℕ) (_ : N < n), + PowerSeries.coeff ℤ n (p * (invOneSubPow ℤ d)) = h.eval (n : ℚ))) := + ⟨hilbert p d, ⟨p.natDegree, fun n hn => coeff_mul_invOneSubPow_eq_hilbert_eval p d n hn⟩, + fun q ⟨N, hqN⟩ => eq_of_infinite_eval_eq q (hilbert p d) <| fun hfin => Set.Infinite.image + (Set.injOn_of_injective Nat.cast_injective) (Set.Ioi_infinite (max N p.natDegree)) <| + Set.Finite.subset hfin <| show @Nat.cast ℚ _ '' (Set.Ioi (max N p.natDegree)) ⊆ + (@setOf ℚ fun x => q.eval x = (hilbert p d).eval x) by + intro x hx; simp only [Set.mem_image, Set.mem_Ioi, max_lt_iff, Set.mem_setOf_eq] at hx ⊢; + rcases hx with ⟨n, ⟨h1, h2⟩, h3⟩; rw [← h3, ← coeff_mul_invOneSubPow_eq_hilbert_eval p d n h2]; + exact (Rat.ext (congrArg Rat.num (hqN n h1)) (congrArg Rat.den (hqN n h1))).symm⟩ + +theorem leadingCoeff_ascPochhammer (R : Type*) [Semiring R] [Nontrivial R] (n : ℕ) : + leadingCoeff (ascPochhammer R n) = 1 := by + induction n with + | zero => simp only [ascPochhammer_zero, monic_one, Monic.leadingCoeff] + | succ n hn => + rw [ascPochhammer_succ_right, leadingCoeff_mul'] + · rw [hn, one_mul, ← C_eq_natCast, leadingCoeff_X_add_C] + · rw [hn, one_mul, ← C_eq_natCast, leadingCoeff_X_add_C]; exact one_ne_zero + +/-- +This theorem tells us the specific degree of any non-zero Hilbert polynomial. +-/ +theorem natDegree_hilbert (p : ℤ[X]) (d : ℕ) (hh : hilbert p d ≠ 0) : + (hilbert p d).natDegree = d - p.rootMultiplicity 1 - 1 := by + by_cases h : p = 0 + · exfalso; rw [hilbert] at hh; simp only [h, reduceDIte, ne_eq, not_true_eq_false] at hh + · by_cases h1 : d ≤ p.rootMultiplicity 1 + · rw [hilbert] at hh + simp only [h1, reduceIte, dite_eq_ite, ite_self, ne_eq, not_true_eq_false] at hh + · rw [hilbert]; apply natDegree_eq_of_le_of_coeff_ne_zero _ _ + · simp only [h, reduceDIte, h1, reduceIte] + apply natDegree_sum_le_of_forall_le _ _ _ + · intro i _; apply le_trans natDegree_mul_le _ + · simp only [natDegree_intCast, zero_add] + apply le_trans (natDegree_smul_le _ _) _ + · rw [natDegree_comp, ascPochhammer_natDegree, add_comm_sub, show 1 - _ = C (1 - i : ℚ) + by simp only [map_sub, map_one], natDegree_add_C, natDegree_X, mul_one] + · simp only [h, reduceDIte, h1, reduceIte, finset_sum_coeff, coeff_intCast_mul, preHilbert, + coeff_smul, map_natCast, smul_eq_mul] + have (x : ℕ) : ((ascPochhammer ℚ (d - rootMultiplicity 1 p - 1)).comp + (X - (x : ℚ[X]) + 1)).coeff (d - rootMultiplicity 1 p - 1) = 1 := by + rw [sub_add, show x - 1 = C (x - 1 : ℚ) by simp only [map_natCast, map_sub, map_one]] + have : ((ascPochhammer ℚ (d - rootMultiplicity 1 p - 1)).comp + (X - C ((x : ℚ) - 1))).coeff (d - rootMultiplicity 1 p - 1) = ((ascPochhammer ℚ + (d - rootMultiplicity 1 p - 1)).comp (X - C ((x : ℚ) - 1))).coeff ((ascPochhammer ℚ + (d - rootMultiplicity 1 p - 1)).comp (X - C ((x : ℚ) - 1))).natDegree := by + rw [natDegree_comp, ascPochhammer_natDegree, natDegree_X_sub_C, mul_one] + rw [this, coeff_natDegree, leadingCoeff_comp <| ne_of_eq_of_ne (natDegree_X_sub_C _) + one_ne_zero, leadingCoeff_ascPochhammer, one_mul, leadingCoeff_X_sub_C, one_pow] + simp_rw [this] + rw [mul_one, ← Finset.sum_mul, show ∑ x in _, @Int.cast ℚ _ _ = (gFOSND p h).eval 1 by + rw [eval_eq_sum_range]; simp only [one_pow, mul_one, Int.cast_sum], ne_eq, + _root_.mul_eq_zero, inv_eq_zero, cast_eq_zero, not_or, greatestFactorOneSubNotDvd] + constructor + · simp only [eval_mul, eval_pow, eval_neg, eval_one, _root_.mul_eq_zero, pow_eq_zero_iff', + neg_eq_zero, one_ne_zero, false_and, Int.cast_eq_zero, false_or] + exact (not_iff_not.2 dvd_iff_isRoot).1 + (exists_eq_pow_rootMultiplicity_mul_and_not_dvd p h 1).choose_spec.2 + · exact Nat.factorial_ne_zero _ + end Polynomial From 3833f08147842e903f1968c1b814fb3dea905b93 Mon Sep 17 00:00:00 2001 From: FMLJohn <417963616@qq.com> Date: Tue, 26 Nov 2024 15:56:52 +0000 Subject: [PATCH 07/16] removed some imports --- Mathlib/RingTheory/Polynomial/Hilbert.lean | 40 +++++++++------------- 1 file changed, 16 insertions(+), 24 deletions(-) diff --git a/Mathlib/RingTheory/Polynomial/Hilbert.lean b/Mathlib/RingTheory/Polynomial/Hilbert.lean index f1406ee6dbb08..d35254ac2809f 100644 --- a/Mathlib/RingTheory/Polynomial/Hilbert.lean +++ b/Mathlib/RingTheory/Polynomial/Hilbert.lean @@ -3,11 +3,8 @@ 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.Algebra.Polynomial.Roots -import Mathlib.Data.Nat.Factorial.BigOperators import Mathlib.Order.Interval.Set.Infinite import Mathlib.RingTheory.Polynomial.Pochhammer import Mathlib.RingTheory.PowerSeries.WellKnown @@ -15,28 +12,23 @@ 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 +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)ᵈ` (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. +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. -/ open BigOperators Nat PowerSeries From e82c08561e7595eff88ea3bf893529b6f58c4558 Mon Sep 17 00:00:00 2001 From: FMLJohn <417963616@qq.com> Date: Thu, 28 Nov 2024 16:29:26 +0000 Subject: [PATCH 08/16] generalised to fields F with char(F) = 0 --- Mathlib/RingTheory/Polynomial/Hilbert.lean | 165 ++++++++++----------- 1 file changed, 76 insertions(+), 89 deletions(-) diff --git a/Mathlib/RingTheory/Polynomial/Hilbert.lean b/Mathlib/RingTheory/Polynomial/Hilbert.lean index d35254ac2809f..cd845770714a0 100644 --- a/Mathlib/RingTheory/Polynomial/Hilbert.lean +++ b/Mathlib/RingTheory/Polynomial/Hilbert.lean @@ -12,20 +12,20 @@ import Mathlib.RingTheory.PowerSeries.WellKnown /-! # 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`). +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 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)ᵈ` +* `Polynomial.hilbert p d`. If `F` is a field with characteristic `0`, `p : F[X]` and `d : ℕ`, then + `Polynomial.hilbert 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 -* Prove that `Polynomial.hilbert p d : ℚ[X]` is the polynomial whose value at `n` equals the +* Prove that `Polynomial.hilbert 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)ᵈ` * Hilbert polynomials of graded modules. @@ -96,117 +96,105 @@ theorem natDegree_pow_rootMultiplicity_sub_mul_greatestFactorOneSubNotDvd_le end greatestFactorOneSubNotDvd +variable {F : Type*} [Field F] [CharZero F] + /-- 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`. +`(Polynomial.preHilbert d k).eval (n : F) = (n - k + d).choose d`. -/ -noncomputable def preHilbert (d k : ℕ) : ℚ[X] := - (d.factorial : ℚ)⁻¹ • ((ascPochhammer ℚ d).comp (X - (C (k : ℚ)) + 1)) +noncomputable def preHilbert (d k : ℕ) : F[X] := + (d.factorial : F)⁻¹ • ((ascPochhammer F d).comp (X - (C (k : F)) + 1)) local notation "gFOSND" => greatestFactorOneSubNotDvd theorem preHilbert_eq_choose_sub_add (d k n : ℕ) (hkn : k ≤ n): - (preHilbert d k).eval (n : ℚ) = (n - k + d).choose d := by + (preHilbert d k).eval (n : F) = (n - k + d).choose d := by rw [preHilbert, eval_smul, eval_comp, map_natCast, eval_add, eval_sub, eval_X, eval_natCast, eval_one, smul_eq_mul, ← cast_sub hkn, ← cast_add_one, ← ascPochhammer_eval_cast, ascPochhammer_nat_eq_ascFactorial, ascFactorial_eq_factorial_mul_choose, cast_mul, - ← mul_assoc, ← div_eq_inv_mul, div_self (cast_ne_zero.2 (factorial_ne_zero d)), one_mul] + ← mul_assoc] + simp only [isUnit_iff_ne_zero, ne_eq, Ne.symm <| @NeZero.ne' _ _ _ <| @NeZero.charZero _ _ + ⟨factorial_ne_zero d⟩ .., not_false_eq_true, IsUnit.inv_mul_cancel, one_mul] /-- -Given `p : ℤ[X]` and `d : ℕ`, the Hilbert polynomial of `p` and `d`. +Given `p : F[X]` and `d : ℕ`, the Hilbert polynomial of `p` and `d`. See also `Polynomial.coeff_mul_invOneSubPow_eq_hilbert_eval`, which says -that `PowerSeries.coeff ℤ n (p * (invOneSubPow ℤ d))` is equal to -`(Polynomial.hilbert p d).eval (n : ℚ)` for any large enough `n : ℕ`. +that `PowerSeries.coeff F n (p * (invOneSubPow F d))` is equal to +`(Polynomial.hilbert p d).eval (n : F)` for any large enough `n : ℕ`. -/ -noncomputable def hilbert (p : ℤ[X]) (d : ℕ) : ℚ[X] := +noncomputable def hilbert (p : F[X]) (d : ℕ) : F[X] := + let _ := Classical.propDecidable (p = 0) 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 + ((greatestFactorOneSubNotDvd p h).coeff i) • preHilbert (d - (p.rootMultiplicity 1) - 1) i /-- -Given `p : ℤ[X]` and `d : ℕ`. The key property of the Hilbert polynomial with respect to -`p` and `d`, which says that for any term of `p * (invOneSubPow ℤ d)` whose degree is +Given `p : F[X]` and `d : ℕ`. The key property of the Hilbert polynomial with respect to +`p` and `d`, which says that for any term of `p * (invOneSubPow F d)` whose degree is large enough, its coefficient can be obtained by evaluating the Hilbert polynomial. -/ -theorem coeff_mul_invOneSubPow_eq_hilbert_eval (p : ℤ[X]) (d n : ℕ) (hn : p.natDegree < n) : - PowerSeries.coeff ℤ n (p * (@invOneSubPow ℤ _ d)) = (hilbert p d).eval (n : ℚ) := by +theorem coeff_mul_invOneSubPow_eq_hilbert_eval (p : F[X]) (d n : ℕ) (hn : p.natDegree < n) : + PowerSeries.coeff F n (p * (invOneSubPow F d)) = (hilbert p d).eval (n : F) := by rw [hilbert]; by_cases h : p = 0 - · simp only [h, coe_zero, zero_mul, map_zero, Int.cast_zero, reduceDIte, eval_zero] - · simp only [h, reduceDIte, zsmul_eq_mul] - have coe_one_sub : (1 - X : ℤ[X]).toPowerSeries = 1 - (PowerSeries.X : ℤ⟦X⟧) := by - simp only [coe_sub, coe_one, coe_X] + · simp only [h, coe_zero, zero_mul, map_zero, reduceDIte, eval_zero] + · simp only [h, reduceDIte] + have coe : ((1 - X : F[X]) : F⟦X⟧) = 1 - PowerSeries.X := by simp only [coe_sub, coe_one, coe_X] by_cases h1 : d ≤ p.rootMultiplicity 1 - · simp only [h1, reduceIte, eval_zero, Int.cast_eq_zero] + · simp only [h1, reduceIte, eval_zero] rw [← pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq p h, mul_comm, coe_mul, - ← mul_assoc, coe_pow, coe_one_sub, ← Nat.sub_add_cancel h1, mul_comm (invOneSubPow ℤ d).val, - pow_add, mul_assoc (_ ^ _), ← invOneSubPow_inv_eq_one_sub_pow ℤ d, Units.inv_eq_val_inv, - Units.inv_mul, mul_one, ← coe_one_sub, ← coe_pow, ← coe_mul, coeff_coe] + ← mul_assoc, coe_pow, coe, ← Nat.sub_add_cancel h1, mul_comm (invOneSubPow ..).val, + pow_add, mul_assoc (_ ^ _), ← invOneSubPow_inv_eq_one_sub_pow F d, Units.inv_eq_val_inv, + Units.inv_mul, mul_one, ← coe, ← coe_pow, ← coe_mul, coeff_coe] exact coeff_eq_zero_of_natDegree_lt (lt_of_le_of_lt (natDegree_pow_rootMultiplicity_sub_mul_greatestFactorOneSubNotDvd_le p h d h1) hn) · simp only [h1, reduceIte] rw [coe_inj.2 (pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq p h).symm, coe_mul, - mul_comm ((_ : ℤ[X]) ^ _).toPowerSeries, mul_assoc, invOneSubPow_eq_inv_one_sub_pow, - ← Nat.add_sub_of_le (Nat.le_of_not_ge h1), pow_add, Units.val_mul, ← mul_assoc - ((_ : ℤ[X]) ^ _).toPowerSeries, coe_pow, coe_one_sub, ← invOneSubPow_eq_inv_one_sub_pow, + mul_comm ((_ : F[X]) ^ _).toPowerSeries, mul_assoc, invOneSubPow_eq_inv_one_sub_pow, + ← add_sub_of_le (le_of_not_ge h1), pow_add, Units.val_mul, ← mul_assoc + ((_ : F[X]) ^ _).toPowerSeries, coe_pow, coe, ← invOneSubPow_eq_inv_one_sub_pow, ← invOneSubPow_inv_eq_one_sub_pow, Units.inv_eq_val_inv, add_tsub_cancel_left, ← invOneSubPow_eq_inv_one_sub_pow, invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos _ _ <| zero_lt_sub_of_lt <| gt_of_not_le h1, Units.inv_mul, one_mul, coe_inj.2 <| as_sum_range_C_mul_X_pow _, eval_finset_sum] - simp only [eq_intCast, eval_mul] - rw [PowerSeries.coeff_mul, ← Finset.sum_coe_sort _ (fun _ => eval .. * _)] - simp_rw [show ∀ (x : Finset.range _), eval _ (preHilbert (d - rootMultiplicity 1 p - 1) _) = - _ by intro x; rw [preHilbert_eq_choose_sub_add]; exact Nat.le_trans (Nat.le_of_lt_succ + simp only [eval_smul, smul_eq_mul] + rw [PowerSeries.coeff_mul, ← Finset.sum_coe_sort _ (fun _ => _ * eval _ _)] + simp_rw [show (_ : Finset.range _) → eval (n : F) (preHilbert (d - rootMultiplicity 1 p - 1) + _) = _ by intro x; rw [preHilbert_eq_choose_sub_add]; exact Nat.le_trans (Nat.le_of_lt_succ (lt_add_one_of_le (Finset.mem_range_succ_iff.1 x.2))) (le_trans (natDegree_greatestFactorOneSubNotDvd_le p h) (le_of_lt hn))] - rw [Finset.sum_coe_sort _ (fun x => eval _ (@Int.cast ℚ[X] ..) * - (n - x + (d - rootMultiplicity 1 p - 1)).choose (d - rootMultiplicity 1 p - 1))] - simp only [coeff_coe, finset_sum_coeff, coeff_intCast_mul, Int.cast_id, coeff_X_pow, mul_ite, - mul_one, mul_zero, Finset.sum_ite_eq, Finset.mem_range, coeff_mk, ite_mul, zero_mul, - Int.cast_sum, Int.cast_ite, Int.cast_mul, Int.cast_ofNat, Int.cast_zero] + rw [Finset.sum_coe_sort _ (fun x => ((gFOSND p h).coeff ↑x) * (n - x + _).choose _)] + simp only [coeff_coe, finset_sum_coeff, coeff_C_mul, coeff_X_pow, mul_ite, mul_zero, + Finset.sum_ite_eq, Finset.mem_range, ite_mul, zero_mul] rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, Eq.symm <| add_sub_of_le <| succ_le_succ <| le_trans (natDegree_greatestFactorOneSubNotDvd_le p h) (le_of_lt hn), Finset.sum_range_add] - simp only [succ_sub_succ_eq_sub, add_lt_iff_neg_left, not_lt_zero', reduceIte, - Finset.sum_const_zero, add_zero] - exact (Finset.sum_eq_sum_iff_of_le (fun i hi => by - simp only [Finset.mem_range] at hi; simp only [hi, reduceIte]; - rw [Int.cast_natCast, eval_intCast, add_comm])).2 (fun i hi => by - rw [Finset.mem_range] at hi; simp only [hi, reduceIte]; rw [add_comm]; - simp only [Int.cast_natCast, eval_intCast]) + simp only [add_lt_iff_neg_left, not_lt_zero', reduceIte, Finset.sum_const_zero, add_zero] + exact Finset.sum_congr rfl <| fun i hi => by + rw [Finset.mem_range] at hi; simp only [hi, reduceIte, mul_one, coeff_mk, add_comm (n - i)] /-- -The Hilbert polynomial is unique. In other words, for any `h : ℚ[X]`, if `h` +The Hilbert polynomial is unique. In other words, for any `h : F[X]`, if `h` satisfies the key property of the Hilbert polynomial (i.e. for any large enough -`n : ℕ`, `PowerSeries.coeff ℤ n (p * (invOneSubPow ℤ d)) = h.eval (n : ℚ)`), +`n : ℕ`, `PowerSeries.coeff F n (p * (invOneSubPow F d)) = h.eval (n : ℚ)`), then `h` is the Hilbert polynomial. -/ -theorem exists_unique_hilbert (p : Polynomial ℤ) (d : ℕ) : - ∃! (h : ℚ[X]), (∃ (N : ℕ), (∀ (n : ℕ) (_ : N < n), - PowerSeries.coeff ℤ n (p * (invOneSubPow ℤ d)) = h.eval (n : ℚ))) := +theorem exists_unique_hilbert (p : Polynomial F) (d : ℕ) : + ∃! (h : F[X]), (∃ (N : ℕ), (∀ (n : ℕ) (_ : N < n), + PowerSeries.coeff F n (p * (invOneSubPow F d)) = h.eval (n : F))) := ⟨hilbert p d, ⟨p.natDegree, fun n hn => coeff_mul_invOneSubPow_eq_hilbert_eval p d n hn⟩, - fun q ⟨N, hqN⟩ => eq_of_infinite_eval_eq q (hilbert p d) <| fun hfin => Set.Infinite.image - (Set.injOn_of_injective Nat.cast_injective) (Set.Ioi_infinite (max N p.natDegree)) <| - Set.Finite.subset hfin <| show @Nat.cast ℚ _ '' (Set.Ioi (max N p.natDegree)) ⊆ - (@setOf ℚ fun x => q.eval x = (hilbert p d).eval x) by - intro x hx; simp only [Set.mem_image, Set.mem_Ioi, max_lt_iff, Set.mem_setOf_eq] at hx ⊢; - rcases hx with ⟨n, ⟨h1, h2⟩, h3⟩; rw [← h3, ← coeff_mul_invOneSubPow_eq_hilbert_eval p d n h2]; - exact (Rat.ext (congrArg Rat.num (hqN n h1)) (congrArg Rat.den (hqN n h1))).symm⟩ - -theorem leadingCoeff_ascPochhammer (R : Type*) [Semiring R] [Nontrivial R] (n : ℕ) : - leadingCoeff (ascPochhammer R n) = 1 := by - induction n with - | zero => simp only [ascPochhammer_zero, monic_one, Monic.leadingCoeff] - | succ n hn => - rw [ascPochhammer_succ_right, leadingCoeff_mul'] - · rw [hn, one_mul, ← C_eq_natCast, leadingCoeff_X_add_C] - · rw [hn, one_mul, ← C_eq_natCast, leadingCoeff_X_add_C]; exact one_ne_zero + fun q ⟨N, hqN⟩ => eq_of_infinite_eval_eq q (hilbert p d) <| fun hfin => + Set.Infinite.image (Set.injOn_of_injective Nat.cast_injective) + (Set.Ioi_infinite (max N p.natDegree)) <| Set.Finite.subset hfin <| fun x hx => by + simp only [Set.mem_image, Set.mem_Ioi, sup_lt_iff, Set.mem_setOf_eq] at hx ⊢; + rcases hx with ⟨n, ⟨h1, h2⟩, h3⟩; + rw [← h3, ← coeff_mul_invOneSubPow_eq_hilbert_eval p d n h2, hqN n h1]⟩ /-- This theorem tells us the specific degree of any non-zero Hilbert polynomial. -/ -theorem natDegree_hilbert (p : ℤ[X]) (d : ℕ) (hh : hilbert p d ≠ 0) : +theorem natDegree_hilbert (p : F[X]) (d : ℕ) (hh : hilbert p d ≠ 0) : (hilbert p d).natDegree = d - p.rootMultiplicity 1 - 1 := by by_cases h : p = 0 · exfalso; rw [hilbert] at hh; simp only [h, reduceDIte, ne_eq, not_true_eq_false] at hh @@ -214,32 +202,31 @@ theorem natDegree_hilbert (p : ℤ[X]) (d : ℕ) (hh : hilbert p d ≠ 0) : · rw [hilbert] at hh simp only [h1, reduceIte, dite_eq_ite, ite_self, ne_eq, not_true_eq_false] at hh · rw [hilbert]; apply natDegree_eq_of_le_of_coeff_ne_zero _ _ - · simp only [h, reduceDIte, h1, reduceIte] - apply natDegree_sum_le_of_forall_le _ _ _ - · intro i _; apply le_trans natDegree_mul_le _ - · simp only [natDegree_intCast, zero_add] - apply le_trans (natDegree_smul_le _ _) _ - · rw [natDegree_comp, ascPochhammer_natDegree, add_comm_sub, show 1 - _ = C (1 - i : ℚ) + · simp only [h, h1, reduceIte]; apply natDegree_sum_le_of_forall_le _ _ _ + · intro i _; apply le_trans (natDegree_smul_le _ _) + · apply le_trans (natDegree_smul_le _ _) _ + · rw [natDegree_comp, ascPochhammer_natDegree, add_comm_sub, show 1 - _ = C (1 - i : F) by simp only [map_sub, map_one], natDegree_add_C, natDegree_X, mul_one] - · simp only [h, reduceDIte, h1, reduceIte, finset_sum_coeff, coeff_intCast_mul, preHilbert, - coeff_smul, map_natCast, smul_eq_mul] - have (x : ℕ) : ((ascPochhammer ℚ (d - rootMultiplicity 1 p - 1)).comp - (X - (x : ℚ[X]) + 1)).coeff (d - rootMultiplicity 1 p - 1) = 1 := by - rw [sub_add, show x - 1 = C (x - 1 : ℚ) by simp only [map_natCast, map_sub, map_one]] - have : ((ascPochhammer ℚ (d - rootMultiplicity 1 p - 1)).comp - (X - C ((x : ℚ) - 1))).coeff (d - rootMultiplicity 1 p - 1) = ((ascPochhammer ℚ - (d - rootMultiplicity 1 p - 1)).comp (X - C ((x : ℚ) - 1))).coeff ((ascPochhammer ℚ - (d - rootMultiplicity 1 p - 1)).comp (X - C ((x : ℚ) - 1))).natDegree := by + · simp only [h, reduceDIte, h1, reduceIte, finset_sum_coeff, preHilbert, coeff_smul, + map_natCast, smul_eq_mul] + have (x : ℕ) : ((ascPochhammer F (d - rootMultiplicity 1 p - 1)).comp + (X - (x : F[X]) + 1)).coeff (d - rootMultiplicity 1 p - 1) = 1 := by + rw [sub_add, show x - 1 = C (x - 1 : F) by simp only [map_natCast, map_sub, map_one]] + have : ((ascPochhammer F (d - rootMultiplicity 1 p - 1)).comp + (X - C ((x : F) - 1))).coeff (d - rootMultiplicity 1 p - 1) = ((ascPochhammer F + (d - rootMultiplicity 1 p - 1)).comp (X - C ((x : F) - 1))).coeff ((ascPochhammer F + (d - rootMultiplicity 1 p - 1)).comp (X - C ((x : F) - 1))).natDegree := by rw [natDegree_comp, ascPochhammer_natDegree, natDegree_X_sub_C, mul_one] rw [this, coeff_natDegree, leadingCoeff_comp <| ne_of_eq_of_ne (natDegree_X_sub_C _) - one_ne_zero, leadingCoeff_ascPochhammer, one_mul, leadingCoeff_X_sub_C, one_pow] + one_ne_zero, Monic.def.1 (monic_ascPochhammer ..), one_mul, leadingCoeff_X_sub_C, + one_pow] simp_rw [this] - rw [mul_one, ← Finset.sum_mul, show ∑ x in _, @Int.cast ℚ _ _ = (gFOSND p h).eval 1 by + rw [mul_one, ← Finset.sum_mul, show ∑ x in _, _ = (gFOSND p h).eval 1 by rw [eval_eq_sum_range]; simp only [one_pow, mul_one, Int.cast_sum], ne_eq, _root_.mul_eq_zero, inv_eq_zero, cast_eq_zero, not_or, greatestFactorOneSubNotDvd] constructor · simp only [eval_mul, eval_pow, eval_neg, eval_one, _root_.mul_eq_zero, pow_eq_zero_iff', - neg_eq_zero, one_ne_zero, false_and, Int.cast_eq_zero, false_or] + neg_eq_zero, one_ne_zero, false_and, false_or] exact (not_iff_not.2 dvd_iff_isRoot).1 (exists_eq_pow_rootMultiplicity_mul_and_not_dvd p h 1).choose_spec.2 · exact Nat.factorial_ne_zero _ From 70ccfab1b20be370242d01fa00111e76452a3db4 Mon Sep 17 00:00:00 2001 From: FMLJohn <417963616@qq.com> Date: Thu, 28 Nov 2024 16:45:40 +0000 Subject: [PATCH 09/16] changed `F` into explicit --- Mathlib/RingTheory/Polynomial/Hilbert.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/Polynomial/Hilbert.lean b/Mathlib/RingTheory/Polynomial/Hilbert.lean index cd845770714a0..7cc98df3de94b 100644 --- a/Mathlib/RingTheory/Polynomial/Hilbert.lean +++ b/Mathlib/RingTheory/Polynomial/Hilbert.lean @@ -96,7 +96,7 @@ theorem natDegree_pow_rootMultiplicity_sub_mul_greatestFactorOneSubNotDvd_le end greatestFactorOneSubNotDvd -variable {F : Type*} [Field F] [CharZero F] +variable (F : Type*) [Field F] [CharZero F] /-- A polynomial which makes it easier to define the Hilbert polynomial. See also the theorem @@ -109,7 +109,7 @@ noncomputable def preHilbert (d k : ℕ) : F[X] := local notation "gFOSND" => greatestFactorOneSubNotDvd theorem preHilbert_eq_choose_sub_add (d k n : ℕ) (hkn : k ≤ n): - (preHilbert d k).eval (n : F) = (n - k + d).choose d := by + (preHilbert F d k).eval (n : F) = (n - k + d).choose d := by rw [preHilbert, eval_smul, eval_comp, map_natCast, eval_add, eval_sub, eval_X, eval_natCast, eval_one, smul_eq_mul, ← cast_sub hkn, ← cast_add_one, ← ascPochhammer_eval_cast, ascPochhammer_nat_eq_ascFactorial, ascFactorial_eq_factorial_mul_choose, cast_mul, @@ -117,6 +117,8 @@ theorem preHilbert_eq_choose_sub_add (d k n : ℕ) (hkn : k ≤ n): simp only [isUnit_iff_ne_zero, ne_eq, Ne.symm <| @NeZero.ne' _ _ _ <| @NeZero.charZero _ _ ⟨factorial_ne_zero d⟩ .., not_false_eq_true, IsUnit.inv_mul_cancel, one_mul] +variable {F} + /-- Given `p : F[X]` and `d : ℕ`, the Hilbert polynomial of `p` and `d`. See also `Polynomial.coeff_mul_invOneSubPow_eq_hilbert_eval`, which says @@ -128,7 +130,7 @@ noncomputable def hilbert (p : F[X]) (d : ℕ) : F[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 + ((greatestFactorOneSubNotDvd p h).coeff i) • preHilbert F (d - (p.rootMultiplicity 1) - 1) i /-- Given `p : F[X]` and `d : ℕ`. The key property of the Hilbert polynomial with respect to @@ -160,7 +162,7 @@ theorem coeff_mul_invOneSubPow_eq_hilbert_eval (p : F[X]) (d n : ℕ) (hn : p.na as_sum_range_C_mul_X_pow _, eval_finset_sum] simp only [eval_smul, smul_eq_mul] rw [PowerSeries.coeff_mul, ← Finset.sum_coe_sort _ (fun _ => _ * eval _ _)] - simp_rw [show (_ : Finset.range _) → eval (n : F) (preHilbert (d - rootMultiplicity 1 p - 1) + simp_rw [show (_ : Finset.range _) → eval (n : F) (preHilbert F (d - rootMultiplicity 1 p - 1) _) = _ by intro x; rw [preHilbert_eq_choose_sub_add]; exact Nat.le_trans (Nat.le_of_lt_succ (lt_add_one_of_le (Finset.mem_range_succ_iff.1 x.2))) (le_trans (natDegree_greatestFactorOneSubNotDvd_le p h) (le_of_lt hn))] From 02d010163b2d32b3872a09cdd155df25c65c6a21 Mon Sep 17 00:00:00 2001 From: FMLJohn <417963616@qq.com> Date: Sat, 30 Nov 2024 17:21:04 +0000 Subject: [PATCH 10/16] changed the definition of `hilbert` --- Mathlib/RingTheory/Polynomial/Hilbert.lean | 204 ++++++++---------- Mathlib/RingTheory/Polynomial/Pochhammer.lean | 10 + 2 files changed, 94 insertions(+), 120 deletions(-) diff --git a/Mathlib/RingTheory/Polynomial/Hilbert.lean b/Mathlib/RingTheory/Polynomial/Hilbert.lean index 7cc98df3de94b..39cce0ed2bcab 100644 --- a/Mathlib/RingTheory/Polynomial/Hilbert.lean +++ b/Mathlib/RingTheory/Polynomial/Hilbert.lean @@ -8,6 +8,7 @@ import Mathlib.Algebra.Polynomial.Roots import Mathlib.Order.Interval.Set.Infinite import Mathlib.RingTheory.Polynomial.Pochhammer import Mathlib.RingTheory.PowerSeries.WellKnown +import Mathlib.Tactic.FieldSimp /-! # Hilbert polynomials @@ -15,23 +16,20 @@ import Mathlib.RingTheory.PowerSeries.WellKnown 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 called the Hilbert polynomial of `p` and `d` (`Polynomial.hilbert p d`). +This `h` is unique and is denoted as `Polynomial.hilbert p d`. ## Main definitions -* `Polynomial.hilbert p d`. If `F` is a field with characteristic `0`, `p : F[X]` and `d : ℕ`, then - `Polynomial.hilbert 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)ᵈ` +* `Polynomial.hilbert p d`. Given a field `F`, a polynomial `p : F[X]` and a natural number `d`, if + `F` is of characteristic `0`, then `Polynomial.hilbert 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 -* Prove that `Polynomial.hilbert 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)ᵈ` - -* Hilbert polynomials of graded modules. +* Hilbert polynomials of finitely generated graded modules over Noetherian rings. -/ -open BigOperators Nat PowerSeries +open Nat PowerSeries namespace Polynomial @@ -96,93 +94,99 @@ theorem natDegree_pow_rootMultiplicity_sub_mul_greatestFactorOneSubNotDvd_le end greatestFactorOneSubNotDvd -variable (F : Type*) [Field F] [CharZero F] +variable (F : Type*) [Field F] /-- -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 : F) = (n - k + d).choose d`. +For any field `F` and natrual numbers `d` and `k`, `Polynomial.preHilbert 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.preHilbert ℚ d 0` is exactly the Hilbert polynomial of +the polynomial ring `ℚ[X_0,...,X_d]` viewed as a graded module over itself. See also the theorem +`Polynomial.preHilbert_eq_choose_sub_add`, which states that if `CharZero F`, then for any +`d k n : ℕ` with `k ≤ n`, `(Polynomial.preHilbert F d k).eval (n : F) = (n - k + d).choose d`. -/ noncomputable def preHilbert (d k : ℕ) : F[X] := (d.factorial : F)⁻¹ • ((ascPochhammer F d).comp (X - (C (k : F)) + 1)) -local notation "gFOSND" => greatestFactorOneSubNotDvd - -theorem preHilbert_eq_choose_sub_add (d k n : ℕ) (hkn : k ≤ n): +theorem preHilbert_eq_choose_sub_add [CharZero F] (d k n : ℕ) (hkn : k ≤ n): (preHilbert F d k).eval (n : F) = (n - k + d).choose d := by - rw [preHilbert, eval_smul, eval_comp, map_natCast, eval_add, eval_sub, eval_X, eval_natCast, - eval_one, smul_eq_mul, ← cast_sub hkn, ← cast_add_one, ← ascPochhammer_eval_cast, - ascPochhammer_nat_eq_ascFactorial, ascFactorial_eq_factorial_mul_choose, cast_mul, - ← mul_assoc] - simp only [isUnit_iff_ne_zero, ne_eq, Ne.symm <| @NeZero.ne' _ _ _ <| @NeZero.charZero _ _ - ⟨factorial_ne_zero d⟩ .., not_false_eq_true, IsUnit.inv_mul_cancel, one_mul] + have : ((d ! : ℕ) : F) ≠ 0 := by norm_cast; positivity + calc + _ = (↑d !)⁻¹ * eval (↑(n - k + 1)) (ascPochhammer F d) := by simp [cast_sub hkn, preHilbert] + _ = (n - k + d).choose d := by + rw [ascPochhammer_nat_eq_natCast_ascFactorial]; + field_simp [ascFactorial_eq_factorial_mul_choose] variable {F} /-- -Given `p : F[X]` and `d : ℕ`, the Hilbert polynomial of `p` and `d`. -See also `Polynomial.coeff_mul_invOneSubPow_eq_hilbert_eval`, which says -that `PowerSeries.coeff F n (p * (invOneSubPow F d))` is equal to -`(Polynomial.hilbert p d).eval (n : F)` for any large enough `n : ℕ`. +`Polynomial.hilbert p 0 = 0`; for any `d : ℕ`, `Polynomial.hilbert p (d + 1)` is +defined as `∑ i in p.support, (p.coeff i) • Polynomial.preHilbert 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.hilbert p d` is the Hilbert +polynomial of `M`. See also `Polynomial.coeff_mul_invOneSubPow_eq_hilbert_eval`, +which says that `PowerSeries.coeff F n (p * (PowerSeries.invOneSubPow F d))` is +equal to `(Polynomial.hilbert p d).eval (n : F)` for any large enough `n : ℕ`. -/ -noncomputable def hilbert (p : F[X]) (d : ℕ) : F[X] := - let _ := Classical.propDecidable (p = 0) - 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 F (d - (p.rootMultiplicity 1) - 1) i +noncomputable def hilbert (p : F[X]) : (d : ℕ) → F[X] + | 0 => 0 + | d + 1 => ∑ i in p.support, (p.coeff i) • preHilbert F d i -/-- -Given `p : F[X]` and `d : ℕ`. The key property of the Hilbert polynomial with respect to -`p` and `d`, which says that for any term of `p * (invOneSubPow F d)` whose degree is -large enough, its coefficient can be obtained by evaluating the Hilbert polynomial. --/ -theorem coeff_mul_invOneSubPow_eq_hilbert_eval (p : F[X]) (d n : ℕ) (hn : p.natDegree < n) : - PowerSeries.coeff F n (p * (invOneSubPow F d)) = (hilbert p d).eval (n : F) := by - rw [hilbert]; by_cases h : p = 0 - · simp only [h, coe_zero, zero_mul, map_zero, reduceDIte, eval_zero] - · simp only [h, reduceDIte] - have coe : ((1 - X : F[X]) : F⟦X⟧) = 1 - PowerSeries.X := by simp only [coe_sub, coe_one, coe_X] - by_cases h1 : d ≤ p.rootMultiplicity 1 - · simp only [h1, reduceIte, eval_zero] - rw [← pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq p h, mul_comm, coe_mul, - ← mul_assoc, coe_pow, coe, ← Nat.sub_add_cancel h1, mul_comm (invOneSubPow ..).val, - pow_add, mul_assoc (_ ^ _), ← invOneSubPow_inv_eq_one_sub_pow F d, Units.inv_eq_val_inv, - Units.inv_mul, mul_one, ← coe, ← coe_pow, ← coe_mul, coeff_coe] - exact coeff_eq_zero_of_natDegree_lt (lt_of_le_of_lt - (natDegree_pow_rootMultiplicity_sub_mul_greatestFactorOneSubNotDvd_le p h d h1) hn) - · simp only [h1, reduceIte] - rw [coe_inj.2 (pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq p h).symm, coe_mul, - mul_comm ((_ : F[X]) ^ _).toPowerSeries, mul_assoc, invOneSubPow_eq_inv_one_sub_pow, - ← add_sub_of_le (le_of_not_ge h1), pow_add, Units.val_mul, ← mul_assoc - ((_ : F[X]) ^ _).toPowerSeries, coe_pow, coe, ← invOneSubPow_eq_inv_one_sub_pow, - ← invOneSubPow_inv_eq_one_sub_pow, Units.inv_eq_val_inv, add_tsub_cancel_left, - ← invOneSubPow_eq_inv_one_sub_pow, invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos _ _ <| - zero_lt_sub_of_lt <| gt_of_not_le h1, Units.inv_mul, one_mul, coe_inj.2 <| - as_sum_range_C_mul_X_pow _, eval_finset_sum] - simp only [eval_smul, smul_eq_mul] - rw [PowerSeries.coeff_mul, ← Finset.sum_coe_sort _ (fun _ => _ * eval _ _)] - simp_rw [show (_ : Finset.range _) → eval (n : F) (preHilbert F (d - rootMultiplicity 1 p - 1) - _) = _ by intro x; rw [preHilbert_eq_choose_sub_add]; exact Nat.le_trans (Nat.le_of_lt_succ - (lt_add_one_of_le (Finset.mem_range_succ_iff.1 x.2))) (le_trans - (natDegree_greatestFactorOneSubNotDvd_le p h) (le_of_lt hn))] - rw [Finset.sum_coe_sort _ (fun x => ((gFOSND p h).coeff ↑x) * (n - x + _).choose _)] - simp only [coeff_coe, finset_sum_coeff, coeff_C_mul, coeff_X_pow, mul_ite, mul_zero, - Finset.sum_ite_eq, Finset.mem_range, ite_mul, zero_mul] - rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, Eq.symm <| add_sub_of_le <| - succ_le_succ <| le_trans (natDegree_greatestFactorOneSubNotDvd_le p h) (le_of_lt hn), - Finset.sum_range_add] - simp only [add_lt_iff_neg_left, not_lt_zero', reduceIte, Finset.sum_const_zero, add_zero] - exact Finset.sum_congr rfl <| fun i hi => by - rw [Finset.mem_range] at hi; simp only [hi, reduceIte, mul_one, coeff_mk, add_comm (n - i)] +variable (F) in +lemma hilbert_zero (d : ℕ) : hilbert (0 : F[X]) d = 0 := by + delta hilbert; induction d with + | zero => simp only + | succ d _ => simp only [coeff_zero, zero_smul, Finset.sum_const_zero] /-- -The Hilbert polynomial is unique. In other words, for any `h : F[X]`, if `h` -satisfies the key property of the Hilbert polynomial (i.e. for any large enough -`n : ℕ`, `PowerSeries.coeff F n (p * (invOneSubPow F d)) = h.eval (n : ℚ)`), -then `h` is the Hilbert polynomial. +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.hilbert p d).eval (n : F)` is equal to the +coefficient of `Xⁿ` in the power series expansion of `p/(1 - X)ᵈ`. -/ -theorem exists_unique_hilbert (p : Polynomial F) (d : ℕ) : +theorem coeff_mul_invOneSubPow_eq_hilbert_eval + [CharZero F] (p : F[X]) (d n : ℕ) (hn : p.natDegree < n) : + PowerSeries.coeff F n (p * (invOneSubPow F d)) = (hilbert p d).eval (n : F) := by + delta hilbert; induction d with + | zero => simp only [invOneSubPow_zero, Units.val_one, mul_one, coeff_coe, eval_zero] + exact coeff_eq_zero_of_natDegree_lt hn + | succ d hd => + simp only [eval_finset_sum, eval_smul, smul_eq_mul]; rw [← Finset.sum_coe_sort] + simp_rw [show (i : p.support) → eval ↑n (preHilbert F d ↑i) = (n + d - ↑i).choose d by + intro i; rw [preHilbert_eq_choose_sub_add _ _ _ _ <| le_trans (le_natDegree_of_ne_zero + <| mem_support_iff.1 i.2) (le_of_lt hn)]; rw [Nat.sub_add_comm]; + exact le_trans (le_natDegree_of_ne_zero <| mem_support_iff.1 i.2) (le_of_lt hn)] + rw [Finset.sum_coe_sort _ (fun x => (p.coeff ↑x) * (_ + d - ↑x).choose _), + PowerSeries.coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, + invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos _ _ (zero_lt_succ d)] + simp only [coeff_coe, coeff_mk] + exact Eq.symm <| Finset.sum_subset_zero_on_sdiff (fun s hs => Finset.mem_range_succ_iff.mpr + <| le_trans (le_natDegree_of_ne_zero <| mem_support_iff.1 hs) (le_of_lt hn)) (fun x hx => by + simp only [Finset.mem_sdiff, mem_support_iff, not_not] at hx; rw [hx.2, zero_mul]) + (fun x hx => by rw [add_comm, Nat.add_sub_assoc <| le_trans (le_natDegree_of_ne_zero <| + mem_support_iff.1 hx) (le_of_lt hn), succ_eq_add_one, add_tsub_cancel_right]) + +lemma hilbert_succ [CharZero F] (p : F[X]) (d : ℕ) : + hilbert (p * (1 - X)) (d + 1) = hilbert p d := by + have (n : Set.Ioi (p * (1 - X)).natDegree) : + (hilbert (p * (1 - X)) (d + 1)).eval (n : F) = (hilbert p d).eval (n : F) := by + by_cases hp : p = 0 + · simp only [hp, zero_mul, hilbert_zero] + · rw [← coeff_mul_invOneSubPow_eq_hilbert_eval, ← coeff_mul_invOneSubPow_eq_hilbert_eval] + · apply PowerSeries.ext_iff.1 <| by + simp only [coe_mul, mul_assoc, mul_eq_mul_left_iff, coe_eq_zero_iff, hp] + rw [invOneSubPow_eq_inv_one_sub_pow, pow_add, ← invOneSubPow_eq_inv_one_sub_pow, + ← invOneSubPow_eq_inv_one_sub_pow, mul_comm, Units.val_mul, mul_assoc] + simp only [coe_sub, coe_one, coe_X, ne_eq, Units.ne_zero, not_false_eq_true, mul_eq_left₀, + or_false] + exact Units.mul_eq_one_iff_inv_eq.mpr (pow_one (1 - PowerSeries.X)) + · exact lt_of_add_right_lt <| le_of_eq_of_le (congr_arg succ <| natDegree_mul hp <| + ne_zero_of_natDegree_gt <| lt_of_lt_of_eq one_pos (show ((1 : F[X]) - X).natDegree = 1 by + rw [← natDegree_neg, neg_sub]; exact natDegree_X_sub_C 1).symm).symm <| Set.mem_Ici.1 n.2 + · exact Set.mem_Ici.1 n.2 + exact eq_of_infinite_eval_eq _ _ <| fun hfin => Set.Infinite.image (Set.injOn_of_injective + cast_injective) (Set.Ioi_infinite _) (Set.Finite.subset hfin <| show Nat.cast '' _ ⊆ _ by + intro x hx; rcases hx with ⟨n, hn1, hn2⟩; rw [← hn2]; exact this ⟨n, hn1⟩) + +theorem exists_unique_hilbert [CharZero F] (p : F[X]) (d : ℕ) : ∃! (h : F[X]), (∃ (N : ℕ), (∀ (n : ℕ) (_ : N < n), PowerSeries.coeff F n (p * (invOneSubPow F d)) = h.eval (n : F))) := ⟨hilbert p d, ⟨p.natDegree, fun n hn => coeff_mul_invOneSubPow_eq_hilbert_eval p d n hn⟩, @@ -193,44 +197,4 @@ theorem exists_unique_hilbert (p : Polynomial F) (d : ℕ) : rcases hx with ⟨n, ⟨h1, h2⟩, h3⟩; rw [← h3, ← coeff_mul_invOneSubPow_eq_hilbert_eval p d n h2, hqN n h1]⟩ -/-- -This theorem tells us the specific degree of any non-zero Hilbert polynomial. --/ -theorem natDegree_hilbert (p : F[X]) (d : ℕ) (hh : hilbert p d ≠ 0) : - (hilbert p d).natDegree = d - p.rootMultiplicity 1 - 1 := by - by_cases h : p = 0 - · exfalso; rw [hilbert] at hh; simp only [h, reduceDIte, ne_eq, not_true_eq_false] at hh - · by_cases h1 : d ≤ p.rootMultiplicity 1 - · rw [hilbert] at hh - simp only [h1, reduceIte, dite_eq_ite, ite_self, ne_eq, not_true_eq_false] at hh - · rw [hilbert]; apply natDegree_eq_of_le_of_coeff_ne_zero _ _ - · simp only [h, h1, reduceIte]; apply natDegree_sum_le_of_forall_le _ _ _ - · intro i _; apply le_trans (natDegree_smul_le _ _) - · apply le_trans (natDegree_smul_le _ _) _ - · rw [natDegree_comp, ascPochhammer_natDegree, add_comm_sub, show 1 - _ = C (1 - i : F) - by simp only [map_sub, map_one], natDegree_add_C, natDegree_X, mul_one] - · simp only [h, reduceDIte, h1, reduceIte, finset_sum_coeff, preHilbert, coeff_smul, - map_natCast, smul_eq_mul] - have (x : ℕ) : ((ascPochhammer F (d - rootMultiplicity 1 p - 1)).comp - (X - (x : F[X]) + 1)).coeff (d - rootMultiplicity 1 p - 1) = 1 := by - rw [sub_add, show x - 1 = C (x - 1 : F) by simp only [map_natCast, map_sub, map_one]] - have : ((ascPochhammer F (d - rootMultiplicity 1 p - 1)).comp - (X - C ((x : F) - 1))).coeff (d - rootMultiplicity 1 p - 1) = ((ascPochhammer F - (d - rootMultiplicity 1 p - 1)).comp (X - C ((x : F) - 1))).coeff ((ascPochhammer F - (d - rootMultiplicity 1 p - 1)).comp (X - C ((x : F) - 1))).natDegree := by - rw [natDegree_comp, ascPochhammer_natDegree, natDegree_X_sub_C, mul_one] - rw [this, coeff_natDegree, leadingCoeff_comp <| ne_of_eq_of_ne (natDegree_X_sub_C _) - one_ne_zero, Monic.def.1 (monic_ascPochhammer ..), one_mul, leadingCoeff_X_sub_C, - one_pow] - simp_rw [this] - rw [mul_one, ← Finset.sum_mul, show ∑ x in _, _ = (gFOSND p h).eval 1 by - rw [eval_eq_sum_range]; simp only [one_pow, mul_one, Int.cast_sum], ne_eq, - _root_.mul_eq_zero, inv_eq_zero, cast_eq_zero, not_or, greatestFactorOneSubNotDvd] - constructor - · simp only [eval_mul, eval_pow, eval_neg, eval_one, _root_.mul_eq_zero, pow_eq_zero_iff', - neg_eq_zero, one_ne_zero, false_and, false_or] - exact (not_iff_not.2 dvd_iff_isRoot).1 - (exists_eq_pow_rootMultiplicity_mul_and_not_dvd p h 1).choose_spec.2 - · exact Nat.factorial_ne_zero _ - end Polynomial diff --git a/Mathlib/RingTheory/Polynomial/Pochhammer.lean b/Mathlib/RingTheory/Polynomial/Pochhammer.lean index d6872afb27cbc..29176297e9018 100644 --- a/Mathlib/RingTheory/Polynomial/Pochhammer.lean +++ b/Mathlib/RingTheory/Polynomial/Pochhammer.lean @@ -153,10 +153,20 @@ theorem ascPochhammer_nat_eq_ascFactorial (n : ℕ) : rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X, eval_natCast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm] +theorem ascPochhammer_nat_eq_natCast_ascFactorial (S : Type*) [Semiring S] (n k : ℕ) : + (ascPochhammer S k).eval (n : S) = n.ascFactorial k := by + norm_cast + rw [ascPochhammer_nat_eq_ascFactorial] + theorem ascPochhammer_nat_eq_descFactorial (a b : ℕ) : (ascPochhammer ℕ b).eval a = (a + b - 1).descFactorial b := by rw [ascPochhammer_nat_eq_ascFactorial, Nat.add_descFactorial_eq_ascFactorial'] +theorem ascPochhammer_nat_eq_natCast_descFactorial (S : Type*) [Semiring S] (a b : ℕ) : + (ascPochhammer S b).eval (a : S) = (a + b - 1).descFactorial b := by + norm_cast + rw [ascPochhammer_nat_eq_descFactorial] + @[simp] theorem ascPochhammer_natDegree (n : ℕ) [NoZeroDivisors S] [Nontrivial S] : (ascPochhammer S n).natDegree = n := by From 9f257904d54f8bc05be34600973b1acb4b1911bc Mon Sep 17 00:00:00 2001 From: FMLJohn <417963616@qq.com> Date: Tue, 3 Dec 2024 17:25:02 +0000 Subject: [PATCH 11/16] merge --- Mathlib/RingTheory/Polynomial/Hilbert.lean | 200 --------------------- 1 file changed, 200 deletions(-) delete mode 100644 Mathlib/RingTheory/Polynomial/Hilbert.lean diff --git a/Mathlib/RingTheory/Polynomial/Hilbert.lean b/Mathlib/RingTheory/Polynomial/Hilbert.lean deleted file mode 100644 index 39cce0ed2bcab..0000000000000 --- a/Mathlib/RingTheory/Polynomial/Hilbert.lean +++ /dev/null @@ -1,200 +0,0 @@ -/- -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.Eval.SMul -import Mathlib.Algebra.Polynomial.Roots -import Mathlib.Order.Interval.Set.Infinite -import Mathlib.RingTheory.Polynomial.Pochhammer -import Mathlib.RingTheory.PowerSeries.WellKnown -import Mathlib.Tactic.FieldSimp - -/-! -# 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.hilbert p d`. - -## Main definitions - -* `Polynomial.hilbert p d`. Given a field `F`, a polynomial `p : F[X]` and a natural number `d`, if - `F` is of characteristic `0`, then `Polynomial.hilbert 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. --/ - -open 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 - -local notation "gFOSND" => greatestFactorOneSubNotDvd - -theorem pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq : - ((1 - X : R[X]) ^ p.rootMultiplicity 1) * greatestFactorOneSubNotDvd p hp = p := by - rw [greatestFactorOneSubNotDvd, ← mul_assoc, ← mul_pow] - simp only [mul_neg, mul_one, neg_sub, map_one] - exact id (exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp 1).choose_spec.1.symm - -theorem greatestFactorOneSubNotDvd_ne_zero : - greatestFactorOneSubNotDvd p hp ≠ 0 := fun h0 => by - let hpow := pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq p hp - rw [h0, mul_zero] at hpow; exact hp <| id hpow.symm - -theorem natDegree_greatestFactorOneSubNotDvd_le [Nontrivial R] [NoZeroDivisors R] : - (greatestFactorOneSubNotDvd p hp).natDegree ≤ p.natDegree := by - have : p.natDegree = ((1 - X : R[X]) ^ p.rootMultiplicity 1 * gFOSND p hp).natDegree := by - rw [pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq] - rw [this, natDegree_mul] - · exact (gFOSND p hp).natDegree.le_add_left (natDegree ((1 - X) ^ p.rootMultiplicity 1)) - · exact pow_ne_zero _ <| fun h0 => by - let this : (1 - X : R[X]).coeff 0 = 0 := by rw [h0]; simp only [coeff_zero]; - simp only [coeff_sub, coeff_one_zero, coeff_X_zero, sub_zero, one_ne_zero] at this - exact greatestFactorOneSubNotDvd_ne_zero p hp - -theorem natDegree_pow_rootMultiplicity_sub_mul_greatestFactorOneSubNotDvd_le - [Nontrivial R] [NoZeroDivisors R] (hp1 : d ≤ p.rootMultiplicity 1) : - ((1 - X) ^ ((p.rootMultiplicity 1) - d) * greatestFactorOneSubNotDvd p hp).natDegree - ≤ p.natDegree := by - have : (1 - X : R[X]) ≠ 0 := fun h0 => by - let h : (1 - X : R[X]).coeff 0 = 0 := by rw [h0, coeff_zero]; - simp only [coeff_sub, coeff_one_zero, coeff_X_zero, sub_zero, one_ne_zero] at h - rw [show p.natDegree = ((((1 - X : R[X]) ^ (p.rootMultiplicity 1 - d + d))) * - (gFOSND p hp)).natDegree by rw [← Nat.eq_add_of_sub_eq hp1 rfl, - pow_rootMultiplicity_mul_greatestFactorOneSubNotDvd_eq], pow_add, mul_assoc, - mul_comm ((1 - X) ^ d), ← mul_assoc, natDegree_mul, natDegree_mul, natDegree_mul] - · simp only [natDegree_pow, le_add_iff_nonneg_right, zero_le] - · exact pow_ne_zero _ this - · exact greatestFactorOneSubNotDvd_ne_zero p hp - · rw [mul_ne_zero_iff]; exact ⟨pow_ne_zero _ this, greatestFactorOneSubNotDvd_ne_zero p hp⟩ - · exact pow_ne_zero _ this - · exact pow_ne_zero _ this - · exact greatestFactorOneSubNotDvd_ne_zero p hp - -end greatestFactorOneSubNotDvd - -variable (F : Type*) [Field F] - -/-- -For any field `F` and natrual numbers `d` and `k`, `Polynomial.preHilbert 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.preHilbert ℚ d 0` is exactly the Hilbert polynomial of -the polynomial ring `ℚ[X_0,...,X_d]` viewed as a graded module over itself. See also the theorem -`Polynomial.preHilbert_eq_choose_sub_add`, which states that if `CharZero F`, then for any -`d k n : ℕ` with `k ≤ n`, `(Polynomial.preHilbert F d k).eval (n : F) = (n - k + d).choose d`. --/ -noncomputable def preHilbert (d k : ℕ) : F[X] := - (d.factorial : F)⁻¹ • ((ascPochhammer F d).comp (X - (C (k : F)) + 1)) - -theorem preHilbert_eq_choose_sub_add [CharZero F] (d k n : ℕ) (hkn : k ≤ n): - (preHilbert F d k).eval (n : F) = (n - k + d).choose d := by - have : ((d ! : ℕ) : F) ≠ 0 := by norm_cast; positivity - calc - _ = (↑d !)⁻¹ * eval (↑(n - k + 1)) (ascPochhammer F d) := by simp [cast_sub hkn, preHilbert] - _ = (n - k + d).choose d := by - rw [ascPochhammer_nat_eq_natCast_ascFactorial]; - field_simp [ascFactorial_eq_factorial_mul_choose] - -variable {F} - -/-- -`Polynomial.hilbert p 0 = 0`; for any `d : ℕ`, `Polynomial.hilbert p (d + 1)` is -defined as `∑ i in p.support, (p.coeff i) • Polynomial.preHilbert 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.hilbert p d` is the Hilbert -polynomial of `M`. See also `Polynomial.coeff_mul_invOneSubPow_eq_hilbert_eval`, -which says that `PowerSeries.coeff F n (p * (PowerSeries.invOneSubPow F d))` is -equal to `(Polynomial.hilbert p d).eval (n : F)` for any large enough `n : ℕ`. --/ -noncomputable def hilbert (p : F[X]) : (d : ℕ) → F[X] - | 0 => 0 - | d + 1 => ∑ i in p.support, (p.coeff i) • preHilbert F d i - -variable (F) in -lemma hilbert_zero (d : ℕ) : hilbert (0 : F[X]) d = 0 := by - delta hilbert; induction d with - | zero => simp only - | succ d _ => simp only [coeff_zero, zero_smul, Finset.sum_const_zero] - -/-- -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.hilbert p d).eval (n : F)` is equal to the -coefficient of `Xⁿ` in the power series expansion of `p/(1 - X)ᵈ`. --/ -theorem coeff_mul_invOneSubPow_eq_hilbert_eval - [CharZero F] (p : F[X]) (d n : ℕ) (hn : p.natDegree < n) : - PowerSeries.coeff F n (p * (invOneSubPow F d)) = (hilbert p d).eval (n : F) := by - delta hilbert; induction d with - | zero => simp only [invOneSubPow_zero, Units.val_one, mul_one, coeff_coe, eval_zero] - exact coeff_eq_zero_of_natDegree_lt hn - | succ d hd => - simp only [eval_finset_sum, eval_smul, smul_eq_mul]; rw [← Finset.sum_coe_sort] - simp_rw [show (i : p.support) → eval ↑n (preHilbert F d ↑i) = (n + d - ↑i).choose d by - intro i; rw [preHilbert_eq_choose_sub_add _ _ _ _ <| le_trans (le_natDegree_of_ne_zero - <| mem_support_iff.1 i.2) (le_of_lt hn)]; rw [Nat.sub_add_comm]; - exact le_trans (le_natDegree_of_ne_zero <| mem_support_iff.1 i.2) (le_of_lt hn)] - rw [Finset.sum_coe_sort _ (fun x => (p.coeff ↑x) * (_ + d - ↑x).choose _), - PowerSeries.coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, - invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos _ _ (zero_lt_succ d)] - simp only [coeff_coe, coeff_mk] - exact Eq.symm <| Finset.sum_subset_zero_on_sdiff (fun s hs => Finset.mem_range_succ_iff.mpr - <| le_trans (le_natDegree_of_ne_zero <| mem_support_iff.1 hs) (le_of_lt hn)) (fun x hx => by - simp only [Finset.mem_sdiff, mem_support_iff, not_not] at hx; rw [hx.2, zero_mul]) - (fun x hx => by rw [add_comm, Nat.add_sub_assoc <| le_trans (le_natDegree_of_ne_zero <| - mem_support_iff.1 hx) (le_of_lt hn), succ_eq_add_one, add_tsub_cancel_right]) - -lemma hilbert_succ [CharZero F] (p : F[X]) (d : ℕ) : - hilbert (p * (1 - X)) (d + 1) = hilbert p d := by - have (n : Set.Ioi (p * (1 - X)).natDegree) : - (hilbert (p * (1 - X)) (d + 1)).eval (n : F) = (hilbert p d).eval (n : F) := by - by_cases hp : p = 0 - · simp only [hp, zero_mul, hilbert_zero] - · rw [← coeff_mul_invOneSubPow_eq_hilbert_eval, ← coeff_mul_invOneSubPow_eq_hilbert_eval] - · apply PowerSeries.ext_iff.1 <| by - simp only [coe_mul, mul_assoc, mul_eq_mul_left_iff, coe_eq_zero_iff, hp] - rw [invOneSubPow_eq_inv_one_sub_pow, pow_add, ← invOneSubPow_eq_inv_one_sub_pow, - ← invOneSubPow_eq_inv_one_sub_pow, mul_comm, Units.val_mul, mul_assoc] - simp only [coe_sub, coe_one, coe_X, ne_eq, Units.ne_zero, not_false_eq_true, mul_eq_left₀, - or_false] - exact Units.mul_eq_one_iff_inv_eq.mpr (pow_one (1 - PowerSeries.X)) - · exact lt_of_add_right_lt <| le_of_eq_of_le (congr_arg succ <| natDegree_mul hp <| - ne_zero_of_natDegree_gt <| lt_of_lt_of_eq one_pos (show ((1 : F[X]) - X).natDegree = 1 by - rw [← natDegree_neg, neg_sub]; exact natDegree_X_sub_C 1).symm).symm <| Set.mem_Ici.1 n.2 - · exact Set.mem_Ici.1 n.2 - exact eq_of_infinite_eval_eq _ _ <| fun hfin => Set.Infinite.image (Set.injOn_of_injective - cast_injective) (Set.Ioi_infinite _) (Set.Finite.subset hfin <| show Nat.cast '' _ ⊆ _ by - intro x hx; rcases hx with ⟨n, hn1, hn2⟩; rw [← hn2]; exact this ⟨n, hn1⟩) - -theorem exists_unique_hilbert [CharZero F] (p : F[X]) (d : ℕ) : - ∃! (h : F[X]), (∃ (N : ℕ), (∀ (n : ℕ) (_ : N < n), - PowerSeries.coeff F n (p * (invOneSubPow F d)) = h.eval (n : F))) := - ⟨hilbert p d, ⟨p.natDegree, fun n hn => coeff_mul_invOneSubPow_eq_hilbert_eval p d n hn⟩, - fun q ⟨N, hqN⟩ => eq_of_infinite_eval_eq q (hilbert p d) <| fun hfin => - Set.Infinite.image (Set.injOn_of_injective Nat.cast_injective) - (Set.Ioi_infinite (max N p.natDegree)) <| Set.Finite.subset hfin <| fun x hx => by - simp only [Set.mem_image, Set.mem_Ioi, sup_lt_iff, Set.mem_setOf_eq] at hx ⊢; - rcases hx with ⟨n, ⟨h1, h2⟩, h3⟩; - rw [← h3, ← coeff_mul_invOneSubPow_eq_hilbert_eval p d n h2, hqN n h1]⟩ - -end Polynomial From f8a3097c9d392b09bdc469f6167a0ec6a8352bf6 Mon Sep 17 00:00:00 2001 From: FMLJohn <417963616@qq.com> Date: Tue, 3 Dec 2024 17:27:19 +0000 Subject: [PATCH 12/16] changed noshake --- scripts/noshake.json | 2 -- 1 file changed, 2 deletions(-) diff --git a/scripts/noshake.json b/scripts/noshake.json index 88b1d09224b2c..acb992ed41e28 100644 --- a/scripts/noshake.json +++ b/scripts/noshake.json @@ -318,8 +318,6 @@ "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": From 24b0b96bf5abca35d2f05fabe7ce11f2b9ee4f07 Mon Sep 17 00:00:00 2001 From: FMLJohn <417963616@qq.com> Date: Tue, 3 Dec 2024 19:01:14 +0000 Subject: [PATCH 13/16] the Hilbert polynomial is unique --- .../RingTheory/Polynomial/HilbertPoly.lean | 31 +++++++++++++++++-- 1 file changed, 28 insertions(+), 3 deletions(-) diff --git a/Mathlib/RingTheory/Polynomial/HilbertPoly.lean b/Mathlib/RingTheory/Polynomial/HilbertPoly.lean index 302a9660f7465..1a46a08f1cff4 100644 --- a/Mathlib/RingTheory/Polynomial/HilbertPoly.lean +++ b/Mathlib/RingTheory/Polynomial/HilbertPoly.lean @@ -5,6 +5,8 @@ Authors: Fangming Li, Jujian Zhang -/ import Mathlib.Algebra.Polynomial.AlgebraMap import Mathlib.Algebra.Polynomial.Eval.SMul +import Mathlib.Algebra.Polynomial.Roots +import Mathlib.Order.Interval.Set.Infinite import Mathlib.RingTheory.Polynomial.Pochhammer import Mathlib.RingTheory.PowerSeries.WellKnown import Mathlib.Tactic.FieldSimp @@ -17,9 +19,9 @@ given any `p : F[X]` and `d : ℕ`, there exists some `h : F[X]` such that for a `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` is the polynomial `(n + 1)···(n + d)/d!`. Note that +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 `(n + 1)···(n + d)/d!`. Note that if `d! = 0` in `F`, then the polynomial `(n + 1)···(n + 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`. @@ -127,4 +129,27 @@ theorem coeff_mul_invOneSubPow_eq_hilbertPoly_eval rw [hx.2, zero_mul] · rw [add_comm, Nat.add_sub_assoc (h_le ⟨x, hx⟩), succ_eq_add_one, add_tsub_cancel_right] +/-- +The polynomial satisfying the key property of `Polynomial.hilbertPoly p d` is unique. In other +words, 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 exists_unique_hilbertPoly [CharZero F] (p : F[X]) (d : ℕ) : + ∃! (h : F[X]), (∃ (N : ℕ), (∀ (n : ℕ) (_ : N < n), + PowerSeries.coeff F n (p * (invOneSubPow F d)) = h.eval (n : F))) := by + use hilbertPoly p d; constructor + · use p.natDegree + exact fun n hn => coeff_mul_invOneSubPow_eq_hilbertPoly_eval d hn + · rintro h ⟨N, hhN⟩ + refine eq_of_infinite_eval_eq h (hilbertPoly p d) ?_ + intro hfin + have : Nat.cast '' Set.Ioi (N ⊔ p.natDegree) ⊆ {x | h.eval x = (p.hilbertPoly d).eval x} := by + intro x hx + simp only [Set.mem_image, Set.mem_Ioi, sup_lt_iff, Set.mem_setOf_eq] at hx ⊢ + rcases hx with ⟨n, ⟨h1, h2⟩, h3⟩ + rw [← h3, ← coeff_mul_invOneSubPow_eq_hilbertPoly_eval d h2, hhN n h1] + exact Set.Infinite.image (Set.injOn_of_injective Nat.cast_injective) + (Set.Ioi_infinite (N ⊔ p.natDegree)) (Set.Finite.subset hfin this) + end Polynomial From 2445eb65968a2735ee534ba620fb41abb915d76e Mon Sep 17 00:00:00 2001 From: FMLJohn <417963616@qq.com> Date: Wed, 4 Dec 2024 16:06:01 +0000 Subject: [PATCH 14/16] added two main lemmas --- .../RingTheory/Polynomial/HilbertPoly.lean | 47 ++++++++++++++++--- Mathlib/RingTheory/PowerSeries/WellKnown.lean | 14 ++++++ 2 files changed, 55 insertions(+), 6 deletions(-) diff --git a/Mathlib/RingTheory/Polynomial/HilbertPoly.lean b/Mathlib/RingTheory/Polynomial/HilbertPoly.lean index 1a46a08f1cff4..b5695eba6e62c 100644 --- a/Mathlib/RingTheory/Polynomial/HilbertPoly.lean +++ b/Mathlib/RingTheory/Polynomial/HilbertPoly.lean @@ -98,13 +98,15 @@ lemma hilbertPoly_X_pow_succ (d k : ℕ) : hilbertPoly ((X : F[X]) ^ k) (d + 1) = preHilbertPoly F d k := by delta hilbertPoly; simp +variable [CharZero F] + /-- 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 coeff_mul_invOneSubPow_eq_hilbertPoly_eval - [CharZero F] {p : F[X]} (d : ℕ) {n : ℕ} (hn : p.natDegree < n) : + {p : F[X]} (d : ℕ) {n : ℕ} (hn : p.natDegree < n) : PowerSeries.coeff F n (p * (invOneSubPow F d)) = (hilbertPoly p d).eval (n : F) := by delta hilbertPoly; induction d with | zero => simp only [invOneSubPow_zero, Units.val_one, mul_one, coeff_coe, eval_zero] @@ -135,7 +137,7 @@ words, if `h : F[X]` and there exists some `N : ℕ` such that for any number `n `N` we have `PowerSeries.coeff F n (p * (invOneSubPow F d)) = h.eval (n : F)`, then `h` is exactly `Polynomial.hilbertPoly p d`. -/ -theorem exists_unique_hilbertPoly [CharZero F] (p : F[X]) (d : ℕ) : +theorem exists_unique_hilbertPoly (p : F[X]) (d : ℕ) : ∃! (h : F[X]), (∃ (N : ℕ), (∀ (n : ℕ) (_ : N < n), PowerSeries.coeff F n (p * (invOneSubPow F d)) = h.eval (n : F))) := by use hilbertPoly p d; constructor @@ -144,12 +146,45 @@ theorem exists_unique_hilbertPoly [CharZero F] (p : F[X]) (d : ℕ) : · rintro h ⟨N, hhN⟩ refine eq_of_infinite_eval_eq h (hilbertPoly p d) ?_ intro hfin - have : Nat.cast '' Set.Ioi (N ⊔ p.natDegree) ⊆ {x | h.eval x = (p.hilbertPoly d).eval x} := by + have hsub : Nat.cast '' Set.Ioi (N ⊔ p.natDegree) ⊆ + { x | h.eval x = (p.hilbertPoly d).eval x } := by intro x hx simp only [Set.mem_image, Set.mem_Ioi, sup_lt_iff, Set.mem_setOf_eq] at hx ⊢ - rcases hx with ⟨n, ⟨h1, h2⟩, h3⟩ - rw [← h3, ← coeff_mul_invOneSubPow_eq_hilbertPoly_eval d h2, hhN n h1] + rcases hx with ⟨n, ⟨hn1, hn2⟩, hn3⟩ + rw [← hn3, ← coeff_mul_invOneSubPow_eq_hilbertPoly_eval d hn2, hhN n hn1] exact Set.Infinite.image (Set.injOn_of_injective Nat.cast_injective) - (Set.Ioi_infinite (N ⊔ p.natDegree)) (Set.Finite.subset hfin this) + (Set.Ioi_infinite (N ⊔ p.natDegree)) (Set.Finite.subset hfin hsub) + +lemma hilbertPoly_mul_one_sub_succ (p : F[X]) (d : ℕ) : + hilbertPoly (p * (1 - X)) (d + 1) = hilbertPoly p d := by + have heq (n : Set.Ioi (p * (1 - X)).natDegree) : + (hilbertPoly (p * (1 - X)) (d + 1)).eval (n : F) = (hilbertPoly p d).eval (n : F) := by + by_cases hp : p = 0 + · simp only [hp, zero_mul, hilbertPoly_zero_nat] + · have hlt : (p * (1 - X)).natDegree < (n : ℕ) := Set.mem_Ioi.1 n.2 + rw [← coeff_mul_invOneSubPow_eq_hilbertPoly_eval _ hlt, + ← coeff_mul_invOneSubPow_eq_hilbertPoly_eval] + · apply PowerSeries.ext_iff.1 <| by simp only [coe_mul, mul_assoc, coe_sub, coe_one, coe_X, + ← one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val F d 1, pow_one] + · have hne : (1 : F[X]) - X ≠ 0 := fun h0 => by simpa only [coeff_sub, coeff_one_zero, + coeff_X_zero, sub_zero, coeff_zero, one_ne_zero] using ext_iff.1 h0 0 + simp_rw [natDegree_mul hp hne] at hlt + exact lt_of_add_right_lt hlt + refine eq_of_infinite_eval_eq _ _ ?_ + · intro hfin + have hsub : Nat.cast '' Set.Ioi (p * (1 - X)).natDegree ⊆ + { x | ((p * (1 - X)).hilbertPoly (d + 1)).eval x = (p.hilbertPoly d).eval x } := by + intro x hx + rcases hx with ⟨n, hn1, hn2⟩ + rw [← hn2] + exact heq ⟨n, hn1⟩ + exact Set.Infinite.image (Set.injOn_of_injective cast_injective) (Set.Ioi_infinite _) + (Set.Finite.subset hfin hsub) + +lemma hilbertPoly_mul_one_sub_pow_add (p : F[X]) (d e : ℕ) : + hilbertPoly (p * (1 - X) ^ e) (d + e) = hilbertPoly p d := by + induction e with + | zero => simp + | succ e he => rw [pow_add, pow_one, ← mul_assoc, ← add_assoc, hilbertPoly_mul_one_sub_succ, he] end Polynomial diff --git a/Mathlib/RingTheory/PowerSeries/WellKnown.lean b/Mathlib/RingTheory/PowerSeries/WellKnown.lean index ca5bd0b442330..8701ade4b7f16 100644 --- a/Mathlib/RingTheory/PowerSeries/WellKnown.lean +++ b/Mathlib/RingTheory/PowerSeries/WellKnown.lean @@ -159,6 +159,20 @@ 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 := (invOneSubPow S (d + 1)).val_inv +theorem invOneSubPow_add (e : ℕ) : + invOneSubPow S (d + e) = invOneSubPow S d * invOneSubPow S e := by + simp_rw [invOneSubPow_eq_inv_one_sub_pow, pow_add] + +theorem one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val (e : ℕ) : + (1 - X) ^ e * (invOneSubPow S (d + e)).val = (invOneSubPow S d).val := by + rw [invOneSubPow_add, Units.val_mul, mul_comm, mul_assoc, ← invOneSubPow_inv_eq_one_sub_pow] + simp + +theorem one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow (e : ℕ) : + (1 - X) ^ (d + e) * (invOneSubPow S e).val = (1 - X) ^ d := by + rw [pow_add, mul_assoc, ← invOneSubPow_inv_eq_one_sub_pow S e] + simp + end invOneSubPow section Field From b9ce0bf6827baba4d762dc625a910bae926a11e1 Mon Sep 17 00:00:00 2001 From: FMLJohn <417963616@qq.com> Date: Wed, 4 Dec 2024 16:51:46 +0000 Subject: [PATCH 15/16] applied Johan's suggestion --- .../RingTheory/Polynomial/HilbertPoly.lean | 20 ++++++------------- 1 file changed, 6 insertions(+), 14 deletions(-) diff --git a/Mathlib/RingTheory/Polynomial/HilbertPoly.lean b/Mathlib/RingTheory/Polynomial/HilbertPoly.lean index b5695eba6e62c..20705443d63b6 100644 --- a/Mathlib/RingTheory/Polynomial/HilbertPoly.lean +++ b/Mathlib/RingTheory/Polynomial/HilbertPoly.lean @@ -145,15 +145,11 @@ theorem exists_unique_hilbertPoly (p : F[X]) (d : ℕ) : exact fun n hn => coeff_mul_invOneSubPow_eq_hilbertPoly_eval d hn · rintro h ⟨N, hhN⟩ refine eq_of_infinite_eval_eq h (hilbertPoly p d) ?_ - intro hfin - have hsub : Nat.cast '' Set.Ioi (N ⊔ p.natDegree) ⊆ - { x | h.eval x = (p.hilbertPoly d).eval x } := by + · apply ((Set.Ioi_infinite (N ⊔ p.natDegree)).image cast_injective.injOn).mono intro x hx simp only [Set.mem_image, Set.mem_Ioi, sup_lt_iff, Set.mem_setOf_eq] at hx ⊢ rcases hx with ⟨n, ⟨hn1, hn2⟩, hn3⟩ rw [← hn3, ← coeff_mul_invOneSubPow_eq_hilbertPoly_eval d hn2, hhN n hn1] - exact Set.Infinite.image (Set.injOn_of_injective Nat.cast_injective) - (Set.Ioi_infinite (N ⊔ p.natDegree)) (Set.Finite.subset hfin hsub) lemma hilbertPoly_mul_one_sub_succ (p : F[X]) (d : ℕ) : hilbertPoly (p * (1 - X)) (d + 1) = hilbertPoly p d := by @@ -171,15 +167,11 @@ lemma hilbertPoly_mul_one_sub_succ (p : F[X]) (d : ℕ) : simp_rw [natDegree_mul hp hne] at hlt exact lt_of_add_right_lt hlt refine eq_of_infinite_eval_eq _ _ ?_ - · intro hfin - have hsub : Nat.cast '' Set.Ioi (p * (1 - X)).natDegree ⊆ - { x | ((p * (1 - X)).hilbertPoly (d + 1)).eval x = (p.hilbertPoly d).eval x } := by - intro x hx - rcases hx with ⟨n, hn1, hn2⟩ - rw [← hn2] - exact heq ⟨n, hn1⟩ - exact Set.Infinite.image (Set.injOn_of_injective cast_injective) (Set.Ioi_infinite _) - (Set.Finite.subset hfin hsub) + · apply ((Set.Ioi_infinite (p * (1 - X)).natDegree).image cast_injective.injOn).mono + intro x hx + rcases hx with ⟨n, hn1, hn2⟩ + rw [← hn2] + exact heq ⟨n, hn1⟩ lemma hilbertPoly_mul_one_sub_pow_add (p : F[X]) (d e : ℕ) : hilbertPoly (p * (1 - X) ^ e) (d + e) = hilbertPoly p d := by From a99bae1b50e13317e37b19eb206856824ec43c98 Mon Sep 17 00:00:00 2001 From: FMLJohn <417963616@qq.com> Date: Wed, 4 Dec 2024 20:05:16 +0000 Subject: [PATCH 16/16] applied further suggestions from Johan --- .../RingTheory/Polynomial/HilbertPoly.lean | 46 ++++++++----------- Mathlib/RingTheory/PowerSeries/WellKnown.lean | 6 +-- 2 files changed, 22 insertions(+), 30 deletions(-) diff --git a/Mathlib/RingTheory/Polynomial/HilbertPoly.lean b/Mathlib/RingTheory/Polynomial/HilbertPoly.lean index 20705443d63b6..7aa04415b3b93 100644 --- a/Mathlib/RingTheory/Polynomial/HilbertPoly.lean +++ b/Mathlib/RingTheory/Polynomial/HilbertPoly.lean @@ -142,36 +142,30 @@ theorem exists_unique_hilbertPoly (p : F[X]) (d : ℕ) : PowerSeries.coeff F n (p * (invOneSubPow F d)) = h.eval (n : F))) := by use hilbertPoly p d; constructor · use p.natDegree - exact fun n hn => coeff_mul_invOneSubPow_eq_hilbertPoly_eval d hn + exact fun n => coeff_mul_invOneSubPow_eq_hilbertPoly_eval d · rintro h ⟨N, hhN⟩ - refine eq_of_infinite_eval_eq h (hilbertPoly p d) ?_ - · apply ((Set.Ioi_infinite (N ⊔ p.natDegree)).image cast_injective.injOn).mono - intro x hx - simp only [Set.mem_image, Set.mem_Ioi, sup_lt_iff, Set.mem_setOf_eq] at hx ⊢ - rcases hx with ⟨n, ⟨hn1, hn2⟩, hn3⟩ - rw [← hn3, ← coeff_mul_invOneSubPow_eq_hilbertPoly_eval d hn2, hhN n hn1] + apply eq_of_infinite_eval_eq h (hilbertPoly p d) + apply ((Set.Ioi_infinite (max N p.natDegree)).image cast_injective.injOn).mono + rintro x ⟨n, hn, rfl⟩ + simp only [Set.mem_Ioi, sup_lt_iff, Set.mem_setOf_eq] at hn ⊢ + rw [← coeff_mul_invOneSubPow_eq_hilbertPoly_eval d hn.2, hhN n hn.1] lemma hilbertPoly_mul_one_sub_succ (p : F[X]) (d : ℕ) : hilbertPoly (p * (1 - X)) (d + 1) = hilbertPoly p d := by - have heq (n : Set.Ioi (p * (1 - X)).natDegree) : - (hilbertPoly (p * (1 - X)) (d + 1)).eval (n : F) = (hilbertPoly p d).eval (n : F) := by - by_cases hp : p = 0 - · simp only [hp, zero_mul, hilbertPoly_zero_nat] - · have hlt : (p * (1 - X)).natDegree < (n : ℕ) := Set.mem_Ioi.1 n.2 - rw [← coeff_mul_invOneSubPow_eq_hilbertPoly_eval _ hlt, - ← coeff_mul_invOneSubPow_eq_hilbertPoly_eval] - · apply PowerSeries.ext_iff.1 <| by simp only [coe_mul, mul_assoc, coe_sub, coe_one, coe_X, - ← one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val F d 1, pow_one] - · have hne : (1 : F[X]) - X ≠ 0 := fun h0 => by simpa only [coeff_sub, coeff_one_zero, - coeff_X_zero, sub_zero, coeff_zero, one_ne_zero] using ext_iff.1 h0 0 - simp_rw [natDegree_mul hp hne] at hlt - exact lt_of_add_right_lt hlt - refine eq_of_infinite_eval_eq _ _ ?_ - · apply ((Set.Ioi_infinite (p * (1 - X)).natDegree).image cast_injective.injOn).mono - intro x hx - rcases hx with ⟨n, hn1, hn2⟩ - rw [← hn2] - exact heq ⟨n, hn1⟩ + apply eq_of_infinite_eval_eq + apply ((Set.Ioi_infinite (p * (1 - X)).natDegree).image cast_injective.injOn).mono + rintro x ⟨n, hn, rfl⟩ + simp only [Set.mem_setOf_eq] + by_cases hp : p = 0 + · simp only [hp, zero_mul, hilbertPoly_zero_nat] + · simp only [Set.mem_Ioi] at hn + have hpn : p.natDegree < n := by + suffices (1 : F[X]) - X ≠ 0 from lt_of_add_right_lt (natDegree_mul hp this ▸ hn) + rw [sub_ne_zero, ne_eq, ext_iff, not_forall] + use 0 + simp + simp only [hn, ← coeff_mul_invOneSubPow_eq_hilbertPoly_eval, coe_mul, coe_sub, coe_one, coe_X, + mul_assoc, hpn, ← one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val F d 1, pow_one] lemma hilbertPoly_mul_one_sub_pow_add (p : F[X]) (d e : ℕ) : hilbertPoly (p * (1 - X) ^ e) (d + e) = hilbertPoly p d := by diff --git a/Mathlib/RingTheory/PowerSeries/WellKnown.lean b/Mathlib/RingTheory/PowerSeries/WellKnown.lean index 8701ade4b7f16..783e6348c6aa9 100644 --- a/Mathlib/RingTheory/PowerSeries/WellKnown.lean +++ b/Mathlib/RingTheory/PowerSeries/WellKnown.lean @@ -165,13 +165,11 @@ theorem invOneSubPow_add (e : ℕ) : theorem one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val (e : ℕ) : (1 - X) ^ e * (invOneSubPow S (d + e)).val = (invOneSubPow S d).val := by - rw [invOneSubPow_add, Units.val_mul, mul_comm, mul_assoc, ← invOneSubPow_inv_eq_one_sub_pow] - simp + simp [invOneSubPow_add, Units.val_mul, mul_comm, mul_assoc, ← invOneSubPow_inv_eq_one_sub_pow] theorem one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow (e : ℕ) : (1 - X) ^ (d + e) * (invOneSubPow S e).val = (1 - X) ^ d := by - rw [pow_add, mul_assoc, ← invOneSubPow_inv_eq_one_sub_pow S e] - simp + simp [pow_add, mul_assoc, ← invOneSubPow_inv_eq_one_sub_pow S e] end invOneSubPow