From cf7f08df3eed4c8138e985e069a1d998083cf3c6 Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Wed, 14 Jun 2023 20:31:39 +0000 Subject: [PATCH] added associated prime graded --- CommAlg/monalisa.lean | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/CommAlg/monalisa.lean b/CommAlg/monalisa.lean index 357578b..43cb907 100644 --- a/CommAlg/monalisa.lean +++ b/CommAlg/monalisa.lean @@ -4,6 +4,8 @@ import Mathlib.Algebra.Module.GradedModule import Mathlib.RingTheory.Ideal.AssociatedPrime import Mathlib.RingTheory.Artinian import Mathlib.Order.Height +import Mathlib.Order.ConditionallyCompleteLattice.Basic +import Mathlib.RingTheory.FiniteType noncomputable def length ( A : Type _) (M : Type _) [CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < ⊤} @@ -87,19 +89,15 @@ theorem hilbert_polynomial_0 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [ : true := by sorry -lemma ass_graded (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) -[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] -[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] -(p : associatedPrimes (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) : (HomogeneousMax 𝒜 p) := by -sorry - 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 x i}).annihilator)) := by + : (Ideal.IsHomogeneous' 𝒜 p) ∧ ((∃ (i : ℤ ), ∃ (x : 𝒜 i), p = (Submodule.span (⨁ i, 𝒜 i) {DirectSum.of _ i x}).annihilator)) := by sorry -def standard_graded (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (I : Ideal (⨁ i, 𝒜 i)) := (⨁ i, 𝒜 i) +-- def standard_graded {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (n : ℕ) : +-- Prop := +-- ∃ J, Ideal.IsHomogeneous' 𝒜 J (J :Nonempty ((⨁ i, 𝒜 i) ≃+* (MvPolynomial (Fin n) (𝒜 0)) ⧸ J)