From fc37344614e375ae7c9d3f2a40a02327836867c7 Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Sat, 10 Jun 2023 00:13:24 +0000 Subject: [PATCH 1/5] my great change --- CommAlg.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CommAlg.lean b/CommAlg.lean index e99d3a6..6d1a3cc 100644 --- a/CommAlg.lean +++ b/CommAlg.lean @@ -1 +1,3 @@ +import Mathlib + def hello := "world" \ No newline at end of file From 3ed659a6ad224ae848b43dde097bbf0ad09e30bc Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Sat, 10 Jun 2023 00:21:01 +0000 Subject: [PATCH 2/5] test push --- CommAlg.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/CommAlg.lean b/CommAlg.lean index 6d1a3cc..ab7e3a6 100644 --- a/CommAlg.lean +++ b/CommAlg.lean @@ -1,3 +1,5 @@ import Mathlib -def hello := "world" \ No newline at end of file +def hello := "world" + +#print "hi" \ No newline at end of file From 437ad08ebd2b88c7786e434bd21ab6524235f944 Mon Sep 17 00:00:00 2001 From: Andre Date: Wed, 14 Jun 2023 01:37:10 -0400 Subject: [PATCH 3/5] fixed hilbertpoly --- comm_alg/test.lean | 137 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 137 insertions(+) create mode 100644 comm_alg/test.lean diff --git a/comm_alg/test.lean b/comm_alg/test.lean new file mode 100644 index 0000000..64650dc --- /dev/null +++ b/comm_alg/test.lean @@ -0,0 +1,137 @@ +import Mathlib.Order.KrullDimension +import Mathlib.Order.JordanHolder +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Order.Height +import Mathlib.RingTheory.Ideal.Basic +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.LinearAlgebra.Finsupp +import Mathlib.RingTheory.GradedAlgebra.Basic +import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal +import Mathlib.Algebra.Module.GradedModule +import Mathlib.RingTheory.Ideal.AssociatedPrime +import Mathlib.RingTheory.Noetherian +import Mathlib.RingTheory.Artinian +import Mathlib.Algebra.Module.GradedModule +import Mathlib.RingTheory.Noetherian +import Mathlib.RingTheory.Finiteness +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.RingTheory.FiniteType +import Mathlib.Order.Height +import Mathlib.RingTheory.PrincipalIdealDomain +import Mathlib.RingTheory.DedekindDomain.Basic +import Mathlib.RingTheory.Ideal.Quotient +import Mathlib.RingTheory.Localization.AtPrime +import Mathlib.Order.ConditionallyCompleteLattice.Basic +import Mathlib.Algebra.DirectSum.Ring +import Mathlib.RingTheory.Ideal.LocalRing + +-- 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.")) + +-- @[BH, 1.5.6 (b)(ii)] +lemma ss (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] + [DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] (p : associatedPrimes (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) : true := by + sorry +-- Ideal.IsHomogeneous 𝒜 p + + + + +noncomputable def length ( A : Type _) (M : Type _) + [CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < ⊤} + + +def HomogeneousPrime { A σ : Type _} [CommRing A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ) [GradedRing 𝒜] (I : Ideal A):= (Ideal.IsPrime I) ∧ (Ideal.IsHomogeneous 𝒜 I) +def HomogeneousMax { A σ : Type _} [CommRing A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ) [GradedRing 𝒜] (I : Ideal A):= (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] + +open GradedMonoid.GSmul +open DirectSum + +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) + +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)) ) + +-- 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 + + + + +@[simp] +def PolyType (f : ℤ → ℤ) (d : ℕ) := ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), ∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly ∧ d = Polynomial.degree Poly + +-- @[BH, 4.1.3] +theorem hilbert_polynomial (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 + +-- @ +lemma Graded_quotient (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)][DirectSum.GCommRing 𝒜] + : true := by + sorry + + +-- @Existence of a chain of submodules of graded submoduels of 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)) + : true := by + sorry +#print Exist_chain_of_graded_submodules +#print Finset \ No newline at end of file From 88a243d26df0919ac1bd36d1a0810f3007a98a0d Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Wed, 14 Jun 2023 18:20:41 +0000 Subject: [PATCH 4/5] new homogeneous --- CommAlg/monalisa.lean | 87 ++++++++++++++++--------------------------- 1 file changed, 32 insertions(+), 55 deletions(-) diff --git a/CommAlg/monalisa.lean b/CommAlg/monalisa.lean index d3a272e..e815cb2 100644 --- a/CommAlg/monalisa.lean +++ b/CommAlg/monalisa.lean @@ -1,8 +1,5 @@ import Mathlib.Order.KrullDimension -import Mathlib.Order.JordanHolder import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic -import Mathlib.Order.Height -import Mathlib.RingTheory.Ideal.Basic import Mathlib.RingTheory.Ideal.Operations import Mathlib.LinearAlgebra.Finsupp import Mathlib.RingTheory.GradedAlgebra.Basic @@ -11,11 +8,6 @@ import Mathlib.Algebra.Module.GradedModule import Mathlib.RingTheory.Ideal.AssociatedPrime import Mathlib.RingTheory.Noetherian import Mathlib.RingTheory.Artinian -import Mathlib.Algebra.Module.GradedModule -import Mathlib.RingTheory.Noetherian -import Mathlib.RingTheory.Finiteness -import Mathlib.RingTheory.Ideal.Operations -import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic import Mathlib.RingTheory.FiniteType import Mathlib.Order.Height import Mathlib.RingTheory.PrincipalIdealDomain @@ -25,27 +17,12 @@ import Mathlib.RingTheory.Localization.AtPrime import Mathlib.Order.ConditionallyCompleteLattice.Basic import Mathlib.Algebra.DirectSum.Ring import Mathlib.RingTheory.Ideal.LocalRing -import Mathlib +--import Mathlib import Mathlib.Algebra.MonoidAlgebra.Basic import Mathlib.Data.Finset.Sort -import Mathlib.Order.Height -import Mathlib.Order.KrullDimension import Mathlib.Order.JordanHolder -import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic -import Mathlib.Order.Height import Mathlib.RingTheory.Ideal.Basic -import Mathlib.RingTheory.Ideal.Operations -import Mathlib.LinearAlgebra.Finsupp -import Mathlib.RingTheory.GradedAlgebra.Basic -import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal -import Mathlib.Algebra.Module.GradedModule -import Mathlib.RingTheory.Ideal.AssociatedPrime -import Mathlib.RingTheory.Noetherian -import Mathlib.RingTheory.Artinian -import Mathlib.Algebra.Module.GradedModule -import Mathlib.RingTheory.Noetherian import Mathlib.RingTheory.Finiteness -import Mathlib.RingTheory.Ideal.Operations @@ -53,11 +30,14 @@ import Mathlib.RingTheory.Ideal.Operations noncomputable def length ( A : Type _) (M : Type _) [CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < ⊤} - -def HomogeneousPrime { A σ : Type _} [CommRing A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ) [GradedRing 𝒜] (I : Ideal A):= (Ideal.IsPrime I) ∧ (Ideal.IsHomogeneous 𝒜 I) + 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 -def HomogeneousMax { A σ : Type _} [CommRing A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ) [GradedRing 𝒜] (I : Ideal A):= (Ideal.IsMaximal I) ∧ (Ideal.IsHomogeneous 𝒜 I) +def HomogeneousPrime (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (I : Ideal (⨁ i, 𝒜 i)):= (Ideal.IsPrime I) ∧ (Ideal.IsHomogeneous' 𝒜 I) + + +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 @@ -67,6 +47,7 @@ open GradedMonoid.GSmul open DirectSum + 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) @@ -88,32 +69,10 @@ instance tada3 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGr letI := Module.compHom (⨁ j, 𝓜 j) (ofZeroRingHom 𝒜) exact Dfinsupp.single_injective.module (𝒜 0) (of 𝓜 i) (mylem 𝒜 𝓜 i) - -- (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) - -noncomputable def dummyhil_function (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] - [DirectSum.GCommRing 𝒜] - [DirectSum.Gmodule 𝒜 𝓜] (hilb : ℤ → ℕ∞) := ∀ i, hilb i = (length (𝒜 0) (𝓜 i)) - - -lemma hilbertz (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] - [DirectSum.GCommRing 𝒜] - [DirectSum.Gmodule 𝒜 𝓜] - (finlen : ∀ i, (length (𝒜 0) (𝓜 i)) < ⊤ ) : ℤ → ℤ := by - intro i - let h := dummyhil_function 𝒜 𝓜 - simp at h - let n : ℤ → ℕ := fun i ↦ WithTop.untop _ (finlen i).ne - have hn : ∀ i, (n i : ℕ∞) = length (𝒜 0) (𝓜 i) := fun i ↦ WithTop.coe_untop _ _ - have' := hn i - exact ((n i) : ℤ ) - - 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) @@ -121,20 +80,38 @@ 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 𝒜] -- [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 +def PolyType (f : ℤ → ℤ) (d : ℕ ) := ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), ∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly ∧ d = Polynomial.degree Poly -theorem hilbert_polynomial (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] +theorem hilbert_polynomial (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 : ∃ d : ℕ , dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = d):True := sorry +[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 --- Semiring A] --- variable [SetLike σ A] \ No newline at end of file +theorem hilbert_polynomial_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 : ℤ → ℤ) +: 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 + From a1888c51e6da1b9bc49a00000f2cd2a2a6554319 Mon Sep 17 00:00:00 2001 From: Andre Date: Wed, 14 Jun 2023 15:07:21 -0400 Subject: [PATCH 5/5] removed imports --- CommAlg/monalisa.lean | 22 ---------------------- 1 file changed, 22 deletions(-) diff --git a/CommAlg/monalisa.lean b/CommAlg/monalisa.lean index e815cb2..717e95a 100644 --- a/CommAlg/monalisa.lean +++ b/CommAlg/monalisa.lean @@ -1,31 +1,9 @@ import Mathlib.Order.KrullDimension import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic -import Mathlib.RingTheory.Ideal.Operations -import Mathlib.LinearAlgebra.Finsupp -import Mathlib.RingTheory.GradedAlgebra.Basic -import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal import Mathlib.Algebra.Module.GradedModule import Mathlib.RingTheory.Ideal.AssociatedPrime -import Mathlib.RingTheory.Noetherian import Mathlib.RingTheory.Artinian -import Mathlib.RingTheory.FiniteType import Mathlib.Order.Height -import Mathlib.RingTheory.PrincipalIdealDomain -import Mathlib.RingTheory.DedekindDomain.Basic -import Mathlib.RingTheory.Ideal.Quotient -import Mathlib.RingTheory.Localization.AtPrime -import Mathlib.Order.ConditionallyCompleteLattice.Basic -import Mathlib.Algebra.DirectSum.Ring -import Mathlib.RingTheory.Ideal.LocalRing ---import Mathlib -import Mathlib.Algebra.MonoidAlgebra.Basic -import Mathlib.Data.Finset.Sort -import Mathlib.Order.JordanHolder -import Mathlib.RingTheory.Ideal.Basic -import Mathlib.RingTheory.Finiteness - - - noncomputable def length ( A : Type _) (M : Type _) [CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < ⊤}