From bbfba6a2f722ecd933ed6feb4494885eb28e9675 Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Wed, 14 Jun 2023 21:50:00 +0000 Subject: [PATCH 1/4] added graded submodule --- CommAlg/monalisa.lean | 25 +++++++++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/CommAlg/monalisa.lean b/CommAlg/monalisa.lean index 68579da..4d5f4d8 100644 --- a/CommAlg/monalisa.lean +++ b/CommAlg/monalisa.lean @@ -58,7 +58,7 @@ noncomputable def dimensionring { A: Type _} noncomputable def dimensionmodule ( A : Type _) (M : Type _) [CommRing A] [AddCommGroup M] [Module A M] := krullDim (PrimeSpectrum (A ⧸ ((⊤ : Submodule A M).annihilator)) ) --- (∃ (i : ℤ ), ∃ (x : 𝒜 i), p = (Submodule.span (⨁ i, 𝒜 i) {x}).annihilator ) + -- lemma graded_local (𝒜 : ℤ → Type _) [SetLike (⨁ i, 𝒜 i)] (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] -- [DirectSum.GCommRing 𝒜] @@ -98,4 +98,25 @@ lemma Associated_prime_of_graded_is_graded -- def standard_graded {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (n : ℕ) : -- Prop := --- ∃ J, Ideal.IsHomogeneous' 𝒜 J (J :Nonempty ((⨁ i, 𝒜 i) ≃+* (MvPolynomial (Fin n) (𝒜 0)) ⧸ J) + +def Component_of_graded_as_addsubgroup (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] +(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p) (i : ℤ) : AddSubgroup (𝒜 i) := sorry + + + +-- @ Quotient of a graded ring R by a graded ideal p is a graded R-Mod, preserving each component +instance Quotient_of_graded_is_graded +(𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] +(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p) + : DirectSum.Gmodule 𝒜 (fun i => (𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i)) := by + sorry + +instance graded_submodule +(𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) (𝓝 : ℤ → Type _) +[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝓝 i)] +[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝] +(opn : Submodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) (opnis : opn = (⨁ i, 𝓝 i)) + : (𝓝 i : Submodule (𝒜 0) (𝓜 i)) := by + sorry + + From 79a6844707076920aa6f83bac6023eba1f04a358 Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Wed, 14 Jun 2023 22:00:39 +0000 Subject: [PATCH 2/4] graded local lemmma added --- CommAlg/monalisa.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CommAlg/monalisa.lean b/CommAlg/monalisa.lean index 4d5f4d8..f3d174b 100644 --- a/CommAlg/monalisa.lean +++ b/CommAlg/monalisa.lean @@ -60,9 +60,9 @@ noncomputable def dimensionmodule ( A : Type _) (M : Type _) --- lemma graded_local (𝒜 : ℤ → Type _) [SetLike (⨁ i, 𝒜 i)] (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] --- [DirectSum.GCommRing 𝒜] --- [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) : ∃ ( I : Ideal ((⨁ i, 𝒜 i))),(HomogeneousMax 𝒜 I) := sorry +lemma graded_local (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) +[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] +[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) : ∃ ( I : Ideal ((⨁ i, 𝒜 i))),(HomogeneousMax 𝒜 I) := sorry def PolyType (f : ℤ → ℤ) (d : ℕ ) := ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), ∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly ∧ d = Polynomial.degree Poly From 37cc2c5a3c9a8e5de6900570f0ead7600b8d6e69 Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Thu, 15 Jun 2023 04:19:56 +0000 Subject: [PATCH 3/4] added graded morphism def --- CommAlg/monalisa.lean | 44 +++++++++++++++++++++++++++++++++++-------- 1 file changed, 36 insertions(+), 8 deletions(-) diff --git a/CommAlg/monalisa.lean b/CommAlg/monalisa.lean index f3d174b..7a8635e 100644 --- a/CommAlg/monalisa.lean +++ b/CommAlg/monalisa.lean @@ -4,6 +4,18 @@ import Mathlib.Algebra.Module.GradedModule import Mathlib.RingTheory.Ideal.AssociatedPrime import Mathlib.RingTheory.Artinian import Mathlib.Order.Height +import Mathlib.Algebra.Algebra.Subalgebra.Basic +import Mathlib.Algebra.Module.LinearMap + +instance {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] : + Algebra (𝒜 0) (⨁ i, 𝒜 i) := + Algebra.ofModule' + (by + intro r x + sorry) + (by + intro r x + sorry) noncomputable def length ( A : Type _) (M : Type _) [CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < ⊤} @@ -96,13 +108,28 @@ lemma Associated_prime_of_graded_is_graded sorry --- def standard_graded {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (n : ℕ) : --- Prop := +class StandardGraded {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] : Prop where + gen_in_first_piece : + Algebra.adjoin (𝒜 0) (DirectSum.of _ 1 : 𝒜 1 →+ ⨁ i, 𝒜 i).range = (⊤ : Subalgebra (𝒜 0) (⨁ i, 𝒜 i)) def Component_of_graded_as_addsubgroup (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p) (i : ℤ) : AddSubgroup (𝒜 i) := sorry +def graded_morphism (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) (𝓝 : ℤ → Type _) +[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝓝 i)] +[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝] (f : (⨁ i, 𝓜 i) → (⨁ i, 𝓝 i)) : ∀ i, ∀ (r : 𝓜 i), ∀ j, (j ≠ i → f (DirectSum.of _ i r) j = 0) ∧ (IsLinearMap (⨁ i, 𝒜 i) f) := by sorry + + +def graded_submodule +(𝒜 : ℤ → Type _) (𝓜 : ℤ → Type u) (𝓝 : ℤ → Type u) +[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝓝 i)] +[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝] +(opn : Submodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) (opnis : opn = (⨁ i, 𝓝 i)) (i : ℤ ) + : ∃(piece : Submodule (𝒜 0) (𝓜 i)), piece = 𝓝 i := by + sorry + + -- @ Quotient of a graded ring R by a graded ideal p is a graded R-Mod, preserving each component instance Quotient_of_graded_is_graded @@ -111,12 +138,13 @@ instance Quotient_of_graded_is_graded : DirectSum.Gmodule 𝒜 (fun i => (𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i)) := by sorry -instance graded_submodule -(𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) (𝓝 : ℤ → Type _) -[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝓝 i)] -[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝] -(opn : Submodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) (opnis : opn = (⨁ i, 𝓝 i)) - : (𝓝 i : Submodule (𝒜 0) (𝓜 i)) := by +theorem quotient_hilbert_polynomial (d : ℕ) (d1 : 1 ≤ d) (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] +[DirectSum.GCommRing 𝒜] +[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) (p : Ideal (⨁ i, 𝒜 i)) +(findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, ((𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i)) = d) (hilb : ℤ → ℤ) + (Hhilb: hilbert_function 𝒜 𝓜 hilb) (homprime: HomogeneousPrime 𝒜 p) +: PolyType hilb (d - 1) := by sorry + From 1f7a809e2c9ac2c91cdbdba17b72bba68564745d Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Thu, 15 Jun 2023 05:02:47 +0000 Subject: [PATCH 4/4] unified monalisa.lean and HilbertFunction.lean --- CommAlg/final_hil_pol.lean | 258 +++++++++++++++++++++++++++++++++++++ 1 file changed, 258 insertions(+) create mode 100644 CommAlg/final_hil_pol.lean diff --git a/CommAlg/final_hil_pol.lean b/CommAlg/final_hil_pol.lean new file mode 100644 index 0000000..591c6cc --- /dev/null +++ b/CommAlg/final_hil_pol.lean @@ -0,0 +1,258 @@ +import Mathlib.Order.KrullDimension +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Algebra.Module.GradedModule +import Mathlib.RingTheory.Ideal.AssociatedPrime +import Mathlib.RingTheory.Artinian +import Mathlib.Order.Height + + + +-- Setting for "library_search" +set_option maxHeartbeats 0 +macro "ls" : tactic => `(tactic|library_search) + +-- New tactic "obviously" +macro "obviously" : tactic => + `(tactic| ( + first + | dsimp; simp; done; dbg_trace "it was dsimp simp" + | simp; done; dbg_trace "it was simp" + | tauto; done; dbg_trace "it was tauto" + | simp; tauto; done; dbg_trace "it was simp tauto" + | rfl; done; dbg_trace "it was rfl" + | norm_num; done; dbg_trace "it was norm_num" + | /-change (@Eq ℝ _ _);-/ linarith; done; dbg_trace "it was linarith" + -- | gcongr; done + | ring; done; dbg_trace "it was ring" + | trivial; done; dbg_trace "it was trivial" + -- | nlinarith; done + | fail "No, this is not obvious.")) + + + +open GradedMonoid.GSmul +open DirectSum + + + +-- @Definitions (to be classified) +section + +-- Definition of polynomail of type d +def PolyType (f : ℤ → ℤ) (d : ℕ) := ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), ∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly ∧ d = Polynomial.degree Poly +noncomputable def length ( A : Type _) (M : Type _) + [CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < ⊤} + +-- Make instance of M_i being an R_0-module +instance tada1 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] + [DirectSum.Gmodule 𝒜 𝓜] (i : ℤ ) : SMul (𝒜 0) (𝓜 i) + where smul x y := @Eq.rec ℤ (0+i) (fun a _ => 𝓜 a) (GradedMonoid.GSmul.smul x y) i (zero_add i) + +lemma mylem (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] + [h : DirectSum.Gmodule 𝒜 𝓜] (i : ℤ) (a : 𝒜 0) (m : 𝓜 i) : + of _ _ (a • m) = of _ _ a • of _ _ m := by + refine' Eq.trans _ (Gmodule.of_smul_of 𝒜 𝓜 a m).symm + refine' of_eq_of_gradedMonoid_eq _ + exact Sigma.ext (zero_add _).symm <| eq_rec_heq _ _ + +instance tada2 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] + [h : DirectSum.Gmodule 𝒜 𝓜] (i : ℤ ) : SMulWithZero (𝒜 0) (𝓜 i) := by + letI := SMulWithZero.compHom (⨁ i, 𝓜 i) (of 𝒜 0).toZeroHom + exact Function.Injective.smulWithZero (of 𝓜 i).toZeroHom Dfinsupp.single_injective (mylem 𝒜 𝓜 i) + +instance tada3 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] + [h : DirectSum.Gmodule 𝒜 𝓜] (i : ℤ ): Module (𝒜 0) (𝓜 i) := by + letI := Module.compHom (⨁ j, 𝓜 j) (ofZeroRingHom 𝒜) + exact Dfinsupp.single_injective.module (𝒜 0) (of 𝓜 i) (mylem 𝒜 𝓜 i) + + +-- Definition of a Hilbert function of a graded module +section +noncomputable def hilbert_function (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] + [DirectSum.GCommRing 𝒜] + [DirectSum.Gmodule 𝒜 𝓜] (hilb : ℤ → ℤ) := ∀ i, hilb i = (ENat.toNat (length (𝒜 0) (𝓜 i))) + +noncomputable def dimensionring { A: Type _} + [CommRing A] := krullDim (PrimeSpectrum A) + +noncomputable def dimensionmodule ( A : Type _) (M : Type _) + [CommRing A] [AddCommGroup M] [Module A M] := krullDim (PrimeSpectrum (A ⧸ ((⊤ : Submodule A M).annihilator)) ) +end + + + +-- Definition of homogeneous ideal +def Ideal.IsHomogeneous' (𝒜 : ℤ → Type _) +[∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] +(I : Ideal (⨁ i, 𝒜 i)) := ∀ (i : ℤ ) +⦃r : (⨁ i, 𝒜 i)⦄, r ∈ I → DirectSum.of _ i ( r i : 𝒜 i) ∈ I + +-- Definition of homogeneous prime ideal +def HomogeneousPrime (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (I : Ideal (⨁ i, 𝒜 i)):= (Ideal.IsPrime I) ∧ (Ideal.IsHomogeneous' 𝒜 I) + +-- Definition of homogeneous maximal ideal +def HomogeneousMax (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (I : Ideal (⨁ i, 𝒜 i)):= (Ideal.IsMaximal I) ∧ (Ideal.IsHomogeneous' 𝒜 I) + +--theorem monotone_stabilizes_iff_noetherian : +-- (∀ f : ℕ →o Submodule R M, ∃ n, ∀ m, n ≤ m → f n = f m) ↔ IsNoetherian R M := by +-- rw [isNoetherian_iff_wellFounded, WellFounded.monotone_chain_condition] + + +instance {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] : + Algebra (𝒜 0) (⨁ i, 𝒜 i) := + Algebra.ofModule' + (by + intro r x + sorry) + (by + intro r x + sorry) + + + +class StandardGraded {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] : Prop where + gen_in_first_piece : + Algebra.adjoin (𝒜 0) (DirectSum.of _ 1 : 𝒜 1 →+ ⨁ i, 𝒜 i).range = (⊤ : Subalgebra (𝒜 0) (⨁ i, 𝒜 i)) + + +-- Each component of a graded ring is an additive subgroup +def Component_of_graded_as_addsubgroup (𝒜 : ℤ → Type _) +[∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] +(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p) (i : ℤ) : AddSubgroup (𝒜 i) := by + sorry + + +def graded_morphism (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) (𝓝 : ℤ → Type _) +[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝓝 i)] +[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝] (f : (⨁ i, 𝓜 i) → (⨁ i, 𝓝 i)) : ∀ i, ∀ (r : 𝓜 i), ∀ j, (j ≠ i → f (DirectSum.of _ i r) j = 0) ∧ (IsLinearMap (⨁ i, 𝒜 i) f) := by sorry + + +def graded_submodule +(𝒜 : ℤ → Type _) (𝓜 : ℤ → Type u) (𝓝 : ℤ → Type u) +[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝓝 i)] +[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝] +(opn : Submodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) (opnis : opn = (⨁ i, 𝓝 i)) (i : ℤ ) + : ∃(piece : Submodule (𝒜 0) (𝓜 i)), piece = 𝓝 i := by + sorry + + +end + + + + + + +-- @Quotient of a graded ring R by a graded ideal p is a graded R-Mod, preserving each component +instance Quotient_of_graded_is_graded +(𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] +(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p) + : DirectSum.Gmodule 𝒜 (fun i => (𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i)) := by + sorry + + +-- If A_0 is Artinian and local, then A is graded local +lemma Graded_local_if_zero_component_Artinian_and_local (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) +[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] +[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) : ∃ ( I : Ideal ((⨁ i, 𝒜 i))),(HomogeneousMax 𝒜 I) := by + sorry + + +-- @Existence of a chain of submodules of graded submoduels of a f.g graded R-mod M +lemma Exist_chain_of_graded_submodules (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) +[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] + [DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] + (fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) + : ∃ (c : List (Submodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))), c.Chain' (· < ·) ∧ ∀ M ∈ c, Ture := by + sorry + + +-- @[BH, 1.5.6 (b)(ii)] +-- An associated prime of a graded R-Mod M is graded +lemma Associated_prime_of_graded_is_graded +(𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) +[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] +[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] +(p : associatedPrimes (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) + : (Ideal.IsHomogeneous' 𝒜 p) ∧ ((∃ (i : ℤ ), ∃ (x : 𝒜 i), p = (Submodule.span (⨁ i, 𝒜 i) {DirectSum.of _ i x}).annihilator)) := by + sorry + + + + + + + + + +-- @[BH, 4.1.3] when d ≥ 1 +-- If M is a finite graed R-Mod of dimension d ≥ 1, then the Hilbert function H(M, n) is of polynomial type (d - 1) +theorem Hilbert_polynomial_d_ge_1 (d : ℕ) (d1 : 1 ≤ d) (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] +[DirectSum.GCommRing 𝒜] +[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) +(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) +(findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = d) +(hilb : ℤ → ℤ) (Hhilb: hilbert_function 𝒜 𝓜 hilb) +: PolyType hilb (d - 1) := by + sorry + + +-- (reduced version) [BH, 4.1.3] when d ≥ 1 +-- If M is a finite graed R-Mod of dimension d ≥ 1, and M = R⧸ 𝓅 for a graded prime ideal 𝓅, then the Hilbert function H(M, n) is of polynomial type (d - 1) +theorem Hilbert_polynomial_d_ge_1_reduced +(d : ℕ) (d1 : 1 ≤ d) +(𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] +[DirectSum.GCommRing 𝒜] +[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) +(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) +(findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = d) +(hilb : ℤ → ℤ) (Hhilb: hilbert_function 𝒜 𝓜 hilb) +(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p) +(hm : 𝓜 = (fun i => (𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i))) +: PolyType hilb (d - 1) := by + sorry + + +-- @[BH, 4.1.3] when d = 0 +-- If M is a finite graed R-Mod of dimension zero, then the Hilbert function H(M, n) = 0 for n >> 0 +theorem Hilbert_polynomial_d_0 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] +[DirectSum.GCommRing 𝒜] +[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) +(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) +(findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = 0) +(hilb : ℤ → ℤ) (Hhilb : hilbert_function 𝒜 𝓜 hilb) +: (∃ (N : ℤ), ∀ (n : ℤ), n ≥ N → hilb n = 0) := by + sorry + + +-- (reduced version) [BH, 4.1.3] when d = 0 +-- If M is a finite graed R-Mod of dimension zero, and M = R⧸ 𝓅 for a graded prime ideal 𝓅, then the Hilbert function H(M, n) = 0 for n >> 0 +theorem Hilbert_polynomial_d_0_reduced +(𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] +[DirectSum.GCommRing 𝒜] +[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) +(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) +(findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = 0) +(hilb : ℤ → ℤ) (Hhilb : hilbert_function 𝒜 𝓜 hilb) +(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p) +(hm : 𝓜 = (fun i => (𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i))) +: (∃ (N : ℤ), ∀ (n : ℤ), n ≥ N → hilb n = 0) := by + sorry + + + + + + + + + + + + + + + + + +