From fe64034b119c4dcba6772662d321de5b3bde3294 Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Thu, 15 Jun 2023 04:59:31 +0000 Subject: [PATCH] Added standard graded assumption --- CommAlg/final_hil_pol.lean | 3 ++- HilbertFunction.lean | 6 +++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/CommAlg/final_hil_pol.lean b/CommAlg/final_hil_pol.lean index 6981c5e..591c6cc 100644 --- a/CommAlg/final_hil_pol.lean +++ b/CommAlg/final_hil_pol.lean @@ -6,6 +6,7 @@ import Mathlib.RingTheory.Artinian import Mathlib.Order.Height + -- Setting for "library_search" set_option maxHeartbeats 0 macro "ls" : tactic => `(tactic|library_search) @@ -43,7 +44,7 @@ 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 𝒜] +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) diff --git a/HilbertFunction.lean b/HilbertFunction.lean index fccd2e4..7176de2 100644 --- a/HilbertFunction.lean +++ b/HilbertFunction.lean @@ -203,7 +203,7 @@ 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)) +[DirectSum.Gmodule 𝒜 𝓜] (st: StandardGraded 𝒜) (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) (fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) (findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = d) (hilb : ℤ → ℤ) (Hhilb: hilbert_function 𝒜 𝓜 hilb) @@ -217,7 +217,7 @@ theorem Hilbert_polynomial_d_ge_1_reduced -- 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)) +[DirectSum.Gmodule 𝒜 𝓜] (st: StandardGraded 𝒜) (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) (fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) (findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = 0) (hilb : ℤ → ℤ) (Hhilb : hilbert_function 𝒜 𝓜 hilb) @@ -230,7 +230,7 @@ theorem Hilbert_polynomial_d_0 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [ theorem Hilbert_polynomial_d_0_reduced (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] -[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) +[DirectSum.Gmodule 𝒜 𝓜] (st: StandardGraded 𝒜) (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) (fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) (findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = 0) (hilb : ℤ → ℤ) (Hhilb : hilbert_function 𝒜 𝓜 hilb)