From e22b18e7c5964baf74ee825a0144a0b10379657c Mon Sep 17 00:00:00 2001
From: monula95 dutta <monula95@gmail.com>
Date: Mon, 12 Jun 2023 20:57:49 +0000
Subject: [PATCH 01/13] TESTMOna

---
 comm_alg/krull.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/comm_alg/krull.lean b/comm_alg/krull.lean
index 2a5af42..1067e63 100644
--- a/comm_alg/krull.lean
+++ b/comm_alg/krull.lean
@@ -41,4 +41,4 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
 lemma height_eq_dim_localization [Ideal.IsPrime I] :
   height I = krull_dim (Localization.AtPrime I) := sorry
 
-lemma height_add_dim_quotient_le_dim : height I + krull_dim (R ⧸ I) ≤ krull_dim R := sorry
\ No newline at end of file
+lemma height_add_dim_quotient_le_dim : height I + krull_dim (R ⧸ I) ≤ krull_dim R := sorry

From 871f38239c89e357335caa4b36e65494a07b7b48 Mon Sep 17 00:00:00 2001
From: monula95 dutta <monula95@gmail.com>
Date: Mon, 12 Jun 2023 20:59:28 +0000
Subject: [PATCH 02/13] TESTMOna

---
 comm_alg/Defhil.lean | 41 +++++++++++++++++++++++++++++++++++++++++
 comm_alg/hilpol.lean | 14 ++++++++++++++
 2 files changed, 55 insertions(+)
 create mode 100644 comm_alg/Defhil.lean
 create mode 100644 comm_alg/hilpol.lean

diff --git a/comm_alg/Defhil.lean b/comm_alg/Defhil.lean
new file mode 100644
index 0000000..63c140a
--- /dev/null
+++ b/comm_alg/Defhil.lean
@@ -0,0 +1,41 @@
+import Mathlib
+
+variable {R : Type _} (M A B C : Type _) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B] [AddCommGroup C] [Module R C]
+variable (A' B' C' : ModuleCat R)
+#check ModuleCat.of R A
+
+example : Module R A' := inferInstance
+
+#check ModuleCat.of R B
+
+example : Module R B' := inferInstance
+
+#check ModuleCat.of R C
+
+example : Module R C' := inferInstance
+
+namespace CategoryTheory
+
+noncomputable instance abelian : Abelian (ModuleCat.{v} R) := inferInstance
+noncomputable instance haszero : Limits.HasZeroMorphisms (ModuleCat.{v} R) := inferInstance
+
+#check (A B : Submodule _ _) → (A ≤ B)
+
+#check Preorder (Submodule _ _)
+
+#check krullDim (Submodule _ _)
+
+noncomputable def length := krullDim (Submodule R M) 
+ 
+open ZeroObject
+
+namespace HasZeroMorphisms
+
+open LinearMap
+
+#check length M
+
+#check ModuleCat.of R
+
+lemma length_additive_shortexact {f : A ⟶ B} {g : B ⟶ C} (h : ShortExact f g) : length B = length A + length C := sorry
+
diff --git a/comm_alg/hilpol.lean b/comm_alg/hilpol.lean
new file mode 100644
index 0000000..957bade
--- /dev/null
+++ b/comm_alg/hilpol.lean
@@ -0,0 +1,14 @@
+import Mathlib
+
+
+--class GradedRing 
+
+variable [GradedRing S]
+
+namespace DirectSum
+
+namespace ideal
+
+def S_+ := ⊕ (i ≥ 0) S_i
+
+lemma  A set of homogeneous elements fi∈S+ generates S as an algebra over S0 ↔ they generate S+ as an ideal of S.
\ No newline at end of file

From 0a8fd3ef7cedb909dd11e28001f66bd4ef24379a Mon Sep 17 00:00:00 2001
From: monula95 dutta <monula95@gmail.com>
Date: Mon, 12 Jun 2023 23:09:47 +0000
Subject: [PATCH 03/13] Test

---
 comm_alg/Defhil.lean | 34 +++++++++++-----------------------
 comm_alg/hilpol.lean | 41 ++++++++++++++++++++++++++++++++++-------
 2 files changed, 45 insertions(+), 30 deletions(-)

diff --git a/comm_alg/Defhil.lean b/comm_alg/Defhil.lean
index 63c140a..65da0c6 100644
--- a/comm_alg/Defhil.lean
+++ b/comm_alg/Defhil.lean
@@ -1,23 +1,15 @@
 import Mathlib
+import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.LinearAlgebra.Finsupp
+import Mathlib.RingTheory.GradedAlgebra.Basic
+import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal
+
+
+
 
 variable {R : Type _} (M A B C : Type _) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B] [AddCommGroup C] [Module R C]
-variable (A' B' C' : ModuleCat R)
-#check ModuleCat.of R A
 
-example : Module R A' := inferInstance
-
-#check ModuleCat.of R B
-
-example : Module R B' := inferInstance
-
-#check ModuleCat.of R C
-
-example : Module R C' := inferInstance
-
-namespace CategoryTheory
-
-noncomputable instance abelian : Abelian (ModuleCat.{v} R) := inferInstance
-noncomputable instance haszero : Limits.HasZeroMorphisms (ModuleCat.{v} R) := inferInstance
 
 #check (A B : Submodule _ _) → (A ≤ B)
 
@@ -25,17 +17,13 @@ noncomputable instance haszero : Limits.HasZeroMorphisms (ModuleCat.{v} R) := in
 
 #check krullDim (Submodule _ _)
 
-noncomputable def length := krullDim (Submodule R M) 
- 
-open ZeroObject
-
-namespace HasZeroMorphisms
+noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < ⊤}
 
 open LinearMap
 
 #check length M
 
-#check ModuleCat.of R
 
-lemma length_additive_shortexact {f : A ⟶ B} {g : B ⟶ C} (h : ShortExact f g) : length B = length A + length C := sorry
+
+--lemma length_additive_shortexact {f : A ⟶ B} {g : B ⟶ C} (h : ShortExact f g) : length B = length A + length C := sorry
 
diff --git a/comm_alg/hilpol.lean b/comm_alg/hilpol.lean
index 957bade..0aab559 100644
--- a/comm_alg/hilpol.lean
+++ b/comm_alg/hilpol.lean
@@ -1,14 +1,41 @@
-import Mathlib
+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
 
+variable {ι σ R A : Type _}
 
---class GradedRing 
+section HomogeneousDef
 
-variable [GradedRing S]
+variable [Semiring A]
 
-namespace DirectSum
+variable [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ)
 
-namespace ideal
+variable [GradedRing 𝒜]
 
-def S_+ := ⊕ (i ≥ 0) S_i
+variable (I : HomogeneousIdeal 𝒜)
 
-lemma  A set of homogeneous elements fi∈S+ generates S as an algebra over S0 ↔ they generate S+ as an ideal of S.
\ No newline at end of file
+-- def Ideal.IsHomogeneous : Prop :=
+-- ∀ (i : ι) ⦃r : A⦄, r ∈ I → (DirectSum.decompose 𝒜 r i : A) ∈ I
+-- #align ideal.is_homogeneous Ideal.IsHomogeneous
+
+-- structure HomogeneousIdeal extends Submodule A A where
+-- is_homogeneous' : Ideal.IsHomogeneous 𝒜 toSubmodule
+
+--#check Ideal.IsPrime hI
+
+def HomogeneousPrime (I : Ideal A):= Ideal.IsPrime I
+
+def HomogeneousMax (I : Ideal A):= Ideal.IsMaximal 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]
\ No newline at end of file

From 2c3d2d84a374a1ac81dd7777fed50cfc28d086a5 Mon Sep 17 00:00:00 2001
From: monula95 dutta <monula95@gmail.com>
Date: Wed, 14 Jun 2023 03:03:10 +0000
Subject: [PATCH 04/13] TEST

---
 .docker/test.lean    | 133 +++++++++++++++++++++++++++++++++++++++++++
 comm_alg/Defhil.lean |  29 ----------
 comm_alg/hilpol.lean |  41 -------------
 3 files changed, 133 insertions(+), 70 deletions(-)
 create mode 100644 .docker/test.lean
 delete mode 100644 comm_alg/Defhil.lean
 delete mode 100644 comm_alg/hilpol.lean

diff --git a/.docker/test.lean b/.docker/test.lean
new file mode 100644
index 0000000..a851192
--- /dev/null
+++ b/.docker/test.lean
@@ -0,0 +1,133 @@
+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
+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
+
+
+
+
+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 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
+  : ℤ → ℕ∞ := fun 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 := hilbert_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 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
+
+
+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)]
+[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
+
+-- Semiring A]
+
+-- variable [SetLike σ A]
\ No newline at end of file
diff --git a/comm_alg/Defhil.lean b/comm_alg/Defhil.lean
deleted file mode 100644
index 65da0c6..0000000
--- a/comm_alg/Defhil.lean
+++ /dev/null
@@ -1,29 +0,0 @@
-import Mathlib
-import Mathlib.RingTheory.Ideal.Basic
-import Mathlib.RingTheory.Ideal.Operations
-import Mathlib.LinearAlgebra.Finsupp
-import Mathlib.RingTheory.GradedAlgebra.Basic
-import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal
-
-
-
-
-variable {R : Type _} (M A B C : Type _) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B] [AddCommGroup C] [Module R C]
-
-
-#check (A B : Submodule _ _) → (A ≤ B)
-
-#check Preorder (Submodule _ _)
-
-#check krullDim (Submodule _ _)
-
-noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < ⊤}
-
-open LinearMap
-
-#check length M
-
-
-
---lemma length_additive_shortexact {f : A ⟶ B} {g : B ⟶ C} (h : ShortExact f g) : length B = length A + length C := sorry
-
diff --git a/comm_alg/hilpol.lean b/comm_alg/hilpol.lean
deleted file mode 100644
index 0aab559..0000000
--- a/comm_alg/hilpol.lean
+++ /dev/null
@@ -1,41 +0,0 @@
-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
-
-variable {ι σ R A : Type _}
-
-section HomogeneousDef
-
-variable [Semiring A]
-
-variable [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ)
-
-variable [GradedRing 𝒜]
-
-variable (I : HomogeneousIdeal 𝒜)
-
--- def Ideal.IsHomogeneous : Prop :=
--- ∀ (i : ι) ⦃r : A⦄, r ∈ I → (DirectSum.decompose 𝒜 r i : A) ∈ I
--- #align ideal.is_homogeneous Ideal.IsHomogeneous
-
--- structure HomogeneousIdeal extends Submodule A A where
--- is_homogeneous' : Ideal.IsHomogeneous 𝒜 toSubmodule
-
---#check Ideal.IsPrime hI
-
-def HomogeneousPrime (I : Ideal A):= Ideal.IsPrime I
-
-def HomogeneousMax (I : Ideal A):= Ideal.IsMaximal 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]
\ No newline at end of file

From d30702fb10a79ca854f1feb58037082377e0529a Mon Sep 17 00:00:00 2001
From: monula95 dutta <monula95@gmail.com>
Date: Wed, 14 Jun 2023 03:45:23 +0000
Subject: [PATCH 05/13] updated def

---
 .docker/test.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/.docker/test.lean b/.docker/test.lean
index a851192..888270c 100644
--- a/.docker/test.lean
+++ b/.docker/test.lean
@@ -88,10 +88,11 @@ 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 hilbert_function (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
   [DirectSum.GCommRing 𝒜]
-  [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
-  : ℤ → ℕ∞ := fun i => (length (𝒜 0) (𝓜 i))
+  [DirectSum.Gmodule 𝒜 𝓜] (hilb : ℤ → ℕ∞) := ∀ i, hilb i = (length (𝒜 0) (𝓜 i))
 
 lemma hilbertz (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
   [DirectSum.GCommRing 𝒜]

From b6bbf7af8c1d08ac35f49898d632f4cedb1d8f9a Mon Sep 17 00:00:00 2001
From: monula95 dutta <monula95@gmail.com>
Date: Wed, 14 Jun 2023 04:49:17 +0000
Subject: [PATCH 06/13] udpated def final

---
 .docker/test.lean | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/.docker/test.lean b/.docker/test.lean
index 888270c..d3a272e 100644
--- a/.docker/test.lean
+++ b/.docker/test.lean
@@ -90,16 +90,17 @@ instance tada3 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGr
 
   -- (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
 
-noncomputable def hilbert_function (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
+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 := hilbert_function 𝒜 𝓜
+  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 _ _
@@ -107,6 +108,11 @@ lemma hilbertz (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGr
   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)

From 7c91fd8d3133e1ca2f53716f7a9e9e622b536b77 Mon Sep 17 00:00:00 2001
From: Andre <espietandre@gmail.com>
Date: Wed, 14 Jun 2023 01:38:51 -0400
Subject: [PATCH 07/13] 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 39c06f39fde230c4750f93fcfa86297bac41a65d Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Wed, 14 Jun 2023 10:22:14 -0700
Subject: [PATCH 08/13] Develop dim_eq_dim_polynomial_add_one a bit more, with
 a sorried section

---
 ...yantan(dim_eq_dim_polynomial_add_one).lean | 22 ++++++++++++-------
 1 file changed, 14 insertions(+), 8 deletions(-)

diff --git a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean
index a9269a2..ea6f7cd 100644
--- a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean
+++ b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean
@@ -34,13 +34,19 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
   constructor
   · exact dim_le_dim_polynomial_add_one
   · unfold krullDim
-    have htPBdd : ∀ (P : PrimeSpectrum (Polynomial R)), (height P: WithBot ℕ∞) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by
+    have htPBdd : ∀ (P : PrimeSpectrum (Polynomial R)), (height P : WithBot ℕ∞) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by
       intro P
-      unfold height
-      sorry
-    have : (⨆ (I : PrimeSpectrum R), ↑(height I) + 1) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by
-      have : ∀ P : PrimeSpectrum R, ↑(height P) + 1 ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 :=
-        fun _ ↦ add_le_add_right (le_iSup height _) 1
+      have : ∃ (I : PrimeSpectrum R), (height P : WithBot ℕ∞) ≤ ↑(height I + 1) := by
+        sorry
+      obtain ⟨I, IP⟩ := this
+      have : (↑(height I + 1) : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum R), ↑(height I + 1) := by
+        apply @le_iSup (WithBot ℕ∞) _ _ _ I
+      apply ge_trans this IP
+    have oneOut : (⨆ (I : PrimeSpectrum R), (height I : WithBot ℕ∞) + 1) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by
+      have : ∀ P : PrimeSpectrum R, (height P : WithBot ℕ∞) + 1 ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 :=
+        fun P ↦ (by apply add_le_add_right (@le_iSup (WithBot ℕ∞) _ _ _ P) 1)
       apply iSup_le
-      exact this
-    sorry
\ No newline at end of file
+      apply this
+    simp
+    intro P
+    exact ge_trans oneOut (htPBdd P)

From 0f3f18ef09b2d4e756d39d307aae344dbcc0d33d Mon Sep 17 00:00:00 2001
From: monula95 dutta <monula95@gmail.com>
Date: Wed, 14 Jun 2023 17:38:40 +0000
Subject: [PATCH 09/13] moved files into CommAlg

---
 comm_alg/test.lean => CommAlg/hilbertpolynomial.lean | 0
 .docker/test.lean => CommAlg/monalisa.lean           | 0
 2 files changed, 0 insertions(+), 0 deletions(-)
 rename comm_alg/test.lean => CommAlg/hilbertpolynomial.lean (100%)
 rename .docker/test.lean => CommAlg/monalisa.lean (100%)

diff --git a/comm_alg/test.lean b/CommAlg/hilbertpolynomial.lean
similarity index 100%
rename from comm_alg/test.lean
rename to CommAlg/hilbertpolynomial.lean
diff --git a/.docker/test.lean b/CommAlg/monalisa.lean
similarity index 100%
rename from .docker/test.lean
rename to CommAlg/monalisa.lean

From 50515d9ed8e2aa115ef83b43df1e0f9c3bec3cb3 Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Wed, 14 Jun 2023 11:02:02 -0700
Subject: [PATCH 10/13] Completed most of the simple part

---
 .../sayantan(dim_eq_dim_polynomial_add_one).lean  | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean
index ea6f7cd..485ee3b 100644
--- a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean
+++ b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean
@@ -22,11 +22,7 @@ noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.c
 lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
   krullDim R + 1 ≤ krullDim (Polynomial R) := sorry -- Others are working on it
 
--- private lemma sum_succ_of_succ_sum {ι : Type} (a : ℕ∞) [inst : Nonempty ι] :
---       (⨆ (x : ι), a + 1) = (⨆ (x : ι), a) + 1 := by
---   have : a + 1 = (⨆ (x : ι), a) + 1 := by rw [ciSup_const]
---   have : a + 1 = (⨆ (x : ι), a + 1) := Eq.symm ciSup_const
---   simp
+lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := sorry -- Already done in main file
 
 lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
   krullDim R + 1 = krullDim (Polynomial R) := by
@@ -37,6 +33,15 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
     have htPBdd : ∀ (P : PrimeSpectrum (Polynomial R)), (height P : WithBot ℕ∞) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by
       intro P
       have : ∃ (I : PrimeSpectrum R), (height P : WithBot ℕ∞) ≤ ↑(height I + 1) := by
+        have : ∃ M, Ideal.IsMaximal M ∧ P.asIdeal ≤ M := by
+          apply exists_le_maximal
+          apply IsPrime.ne_top
+          apply P.IsPrime
+        obtain ⟨M, maxM, PleM⟩ := this
+        let P' : PrimeSpectrum (Polynomial R) := PrimeSpectrum.mk M (IsMaximal.isPrime maxM)
+        have PleP' : P ≤ P' := PleM
+        have : height P ≤ height P' := height_le_of_le PleP'
+        simp only [WithBot.coe_le_coe]
         sorry
       obtain ⟨I, IP⟩ := this
       have : (↑(height I + 1) : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum R), ↑(height I + 1) := by

From a2f481c7db196d982765165911022adaf6ea03e8 Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Wed, 14 Jun 2023 11:12:33 -0700
Subject: [PATCH 11/13] Turn some simp into simp only

---
 CommAlg/krull.lean                                   |  2 +-
 CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean | 11 ++++++++---
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index 06e6d0d..1e720c0 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -63,7 +63,7 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) :=
     apply height_le_of_le
     apply le_maximalIdeal
     exact I.2.1
-  . simp
+  . simp only [height_le_krullDim]
 
 #check height_le_krullDim
 --some propositions that would be nice to be able to eventually
diff --git a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean
index 485ee3b..089c4b5 100644
--- a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean
+++ b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean
@@ -42,16 +42,21 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
         have PleP' : P ≤ P' := PleM
         have : height P ≤ height P' := height_le_of_le PleP'
         simp only [WithBot.coe_le_coe]
-        sorry
+        have : ∃ (I : PrimeSpectrum R), height P' ≤ height I + 1 := by
+
+          sorry
+        obtain ⟨I, h⟩ := this
+        use I
+        exact ge_trans h this
       obtain ⟨I, IP⟩ := this
       have : (↑(height I + 1) : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum R), ↑(height I + 1) := by
         apply @le_iSup (WithBot ℕ∞) _ _ _ I
-      apply ge_trans this IP
+      exact ge_trans this IP
     have oneOut : (⨆ (I : PrimeSpectrum R), (height I : WithBot ℕ∞) + 1) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by
       have : ∀ P : PrimeSpectrum R, (height P : WithBot ℕ∞) + 1 ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 :=
         fun P ↦ (by apply add_le_add_right (@le_iSup (WithBot ℕ∞) _ _ _ P) 1)
       apply iSup_le
       apply this
-    simp
+    simp only [iSup_le_iff]
     intro P
     exact ge_trans oneOut (htPBdd P)

From ae8bf07ee7b82901b157fb81d018120f8f52c804 Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Wed, 14 Jun 2023 11:23:29 -0700
Subject: [PATCH 12/13] Make the lemma names a little more descriptive

---
 CommAlg/krull.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index 1e720c0..ec94d36 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -135,7 +135,7 @@ lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by
   unfold krullDim
   simp [field_prime_height_zero]
 
-lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by
+lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by
   by_contra x
   rw [Ring.not_isField_iff_exists_prime] at x
   obtain ⟨P, ⟨h1, primeP⟩⟩ := x
@@ -156,9 +156,9 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0)
     aesop
   contradiction
 
-lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
+lemma domain_dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
   constructor
-  · exact isField.dim_zero
+  · exact domain_dim_zero.isField
   · intro fieldD
     let h : Field D := IsField.toField fieldD
     exact dim_field_eq_zero

From a3e4746b134035c75432a84847659973e8189f73 Mon Sep 17 00:00:00 2001
From: Sameer Savkar <sameersavkar@gmail.com>
Date: Wed, 14 Jun 2023 11:50:29 -0700
Subject: [PATCH 13/13] wrote proofs of 2 lemmas

---
 CommAlg/sameer(artinian-rings).lean | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/CommAlg/sameer(artinian-rings).lean b/CommAlg/sameer(artinian-rings).lean
index e6bb667..417cc96 100644
--- a/CommAlg/sameer(artinian-rings).lean
+++ b/CommAlg/sameer(artinian-rings).lean
@@ -6,7 +6,9 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import Mathlib.RingTheory.DedekindDomain.DVR
 
 
-lemma FieldisArtinian (R : Type _) [CommRing R] (IsField : ):= by sorry
+lemma FieldisArtinian (R : Type _) [CommRing R] (h: IsField R) : 
+  IsArtinianRing R := by sorry
+
 
 
 lemma ArtinianDomainIsField (R : Type _) [CommRing R] [IsDomain R]
@@ -47,8 +49,7 @@ lemma isArtinianRing_of_quotient_of_artinian (R : Type _) [CommRing R]
 lemma IsPrimeMaximal (R : Type _) [CommRing R] (P : Ideal R) 
 (IsArt : IsArtinianRing R) (isPrime : Ideal.IsPrime P) : Ideal.IsMaximal P := 
 by 
--- if R is Artinian and P is prime then R/P is Integral Domain 
--- which is Artinian Domain 
+-- if R is Artinian and P is prime then R/P is Artinian Domain 
 -- R⧸P is a field by the above lemma
 -- P is maximal
 
@@ -56,13 +57,13 @@ by
   have artRP : IsArtinianRing (R⧸P) := by
     exact isArtinianRing_of_quotient_of_artinian R P IsArt
   
-
+  have artRPField : IsField (R⧸P) := by
+    exact ArtinianDomainIsField (R⧸P) artRP
+  
+  have h := Ideal.Quotient.maximal_of_isField P artRPField
+  exact h
+  
 -- Then R/I is Artinian 
  --  have' : IsArtinianRing R ∧ Ideal.IsPrime I → IsDomain (R⧸I) := by
 
 -- R⧸I.IsArtinian → monotone_stabilizes_iff_artinian.R⧸I
-
-
-
-
--- Use Stacks project proof since it's broken into lemmas