From 79a6844707076920aa6f83bac6023eba1f04a358 Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Wed, 14 Jun 2023 22:00:39 +0000 Subject: [PATCH] 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