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/18] 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/18] 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/18] 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 a941cce12f21b0bd94757a669c1d73f5677c60a5 Mon Sep 17 00:00:00 2001
From: leopoldmayer <leomayer@uw.edu>
Date: Tue, 13 Jun 2023 14:26:19 -0700
Subject: [PATCH 04/18] changed all rings from Type to Type _

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

diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index 440ea66..2a87c16 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -25,11 +25,11 @@ variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
 
 noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I}
 
-noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I
+noncomputable def krullDim (R : Type _) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I
 
 lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl
-lemma krullDim_def (R : Type) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl
-lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl
+lemma krullDim_def (R : Type _) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl
+lemma krullDim_def' (R : Type _) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl
 
 noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice
 
@@ -39,16 +39,16 @@ lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤
   show J' < J
   exact lt_of_lt_of_le hJ' I_le_J
 
-lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) :
+lemma krullDim_le_iff (R : Type _) [CommRing R] (n : ℕ) :
   krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞)
 
-lemma krullDim_le_iff' (R : Type) [CommRing R] (n : ℕ∞) :
+lemma krullDim_le_iff' (R : Type _) [CommRing R] (n : ℕ∞) :
   krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞)
 
-lemma le_krullDim_iff (R : Type) [CommRing R] (n : ℕ) :
+lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) :
   n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry
 
-lemma le_krullDim_iff' (R : Type) [CommRing R] (n : ℕ∞) :
+lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) :
   n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry
 
 @[simp]

From 81bc507768b55b8829cd82edb811d20b3375ef26 Mon Sep 17 00:00:00 2001
From: poincare-duality <jidongw@uoregon.edu>
Date: Tue, 13 Jun 2023 15:03:28 -0700
Subject: [PATCH 05/18] keep working

---
 .DS_Store | Bin 6148 -> 6148 bytes
 1 file changed, 0 insertions(+), 0 deletions(-)

diff --git a/.DS_Store b/.DS_Store
index 6d98085373769dd4c6eebf58c63f4db066814689..4d3a1f281d5e07d2e291de80d019305e81afbbf8 100644
GIT binary patch
delta 18
acmZoMXfc?uV&ldz_K6Lgo7p-3@&f=#eg{YZ

delta 20
ccmZoMXfc?uf{}6K#xVAY4IG=<IsWnk08Z5hNdN!<


From 55ea06c1419d46c5399997a0a67c6d619d5b5d2c Mon Sep 17 00:00:00 2001
From: poincare-duality <jidongw@uoregon.edu>
Date: Tue, 13 Jun 2023 17:21:42 -0700
Subject: [PATCH 06/18] add more stuff

---
 CommAlg/jayden(krull-dim-zero).lean | 203 +++++++++++++++++++---------
 1 file changed, 138 insertions(+), 65 deletions(-)

diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean
index 3651102..6f282ba 100644
--- a/CommAlg/jayden(krull-dim-zero).lean
+++ b/CommAlg/jayden(krull-dim-zero).lean
@@ -1,97 +1,170 @@
 import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.Ideal.Operations
 import Mathlib.RingTheory.JacobsonIdeal
 import Mathlib.RingTheory.Noetherian
 import Mathlib.Order.KrullDimension
 import Mathlib.RingTheory.Artinian
 import Mathlib.RingTheory.Ideal.Quotient
 import Mathlib.RingTheory.Nilpotent
-import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian
 import Mathlib.Data.Finite.Defs
 import Mathlib.Order.Height
 import Mathlib.RingTheory.DedekindDomain.Basic
 import Mathlib.RingTheory.Localization.AtPrime
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Algebra.Ring.Pi
-import Mathlib.Topology.NoetherianSpace
+import Mathlib.RingTheory.Finiteness
+
 
--- copy from krull.lean; the name of Krull dimension for rings is changed to krullDim' since krullDim already exists in the librrary
 namespace Ideal
 
-variable (R : Type _) [CommRing R] (I : PrimeSpectrum R)
+variable (R : Type _) [CommRing R] (P : PrimeSpectrum R)
 
-noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I}
-
-noncomputable def krullDim' (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height R I
--- copy ends
-
--- Stacks Lemma 10.60.5: R is Artinian iff R is Noetherian of dimension 0
-lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : 
-    IsNoetherianRing R ∧ krullDim' R = 0 ↔ IsArtinianRing R := by sorry
-
-
-#check IsNoetherianRing
-
-#check krullDim
-
--- Repeats the definition of the length of a module by Monalisa
-variable (M : Type _) [AddCommMonoid M] [Module R M]
-
--- change the definition of length
-noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < ⊤}
-
-#check length
--- Stacks Lemma 10.53.6: R is Artinian iff R has finite length as an R-mod
-lemma IsArtinian_iff_finite_length : IsArtinianRing R ↔ ∃ n : ℕ, length R R ≤ n := by sorry 
-
--- Stacks Lemma 10.53.3: R is Artinian iff R has finitely many maximal ideals
-lemma IsArtinian_iff_finite_max_ideal : IsArtinianRing R ↔ Finite (MaximalSpectrum R) := by sorry
-
--- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent
-lemma Jacobson_of_Artinian_is_nilpotent : IsArtinianRing R → IsNilpotent (Ideal.jacobson (⊤ : Ideal R)) := by sorry
-
-
--- Stacks Definition 10.32.1: An ideal is locally nilpotent
--- if every element is nilpotent
-namespace Ideal
-class IsLocallyNilpotent (I : Ideal R) : Prop :=
-    h : ∀ x ∈ I, IsNilpotent x
-
-end Ideal
-
-#check Ideal.IsLocallyNilpotent
-
--- Stacks Lemma 10.53.5: If R has finitely many maximal ideals and 
--- locally nilpotent Jacobson radical, then R is the product of its localizations at 
--- its maximal ideals. Also, all primes are maximal
-
-lemma product_of_localization_at_maximal_ideal : Finite (MaximalSpectrum R)
-     ∧ Ideal.IsLocallyNilpotent (Ideal.jacobson (⊤ : Ideal R)) → Pi.commRing (MaximalSpectrum R) Localization.AtPrime R I
-      := by sorry
--- Haven't finished this.
-
--- Stacks Lemma 10.31.5: R is Noetherian iff Spec(R) is a Noetherian space
-lemma ring_Noetherian_iff_spec_Noetherian : IsNoetherianRing R 
-    ↔ TopologicalSpace.NoetherianSpace (PrimeSpectrum R) := by sorry
--- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible :
--- Every closed subset of a noetherian space is a finite union 
--- of irreducible closed subsets.
+noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < P}
 
+noncomputable def krullDim (R : Type) [CommRing R] :
+     WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height R I
 
 -- Stacks Lemma 10.26.1 (Should already exists)
 -- (1) The closure of a prime P is V(P)
 -- (2) the irreducible closed subsets are V(P) for P prime
 -- (3) the irreducible components are V(P) for P minimal prime
 
--- Stacks Lemma 10.32.5: R Noetherian. I,J ideals. If J ⊂ √I, then J ^ n ⊂ I for some n  
+-- Stacks Definition 10.32.1: An ideal is locally nilpotent
+-- if every element is nilpotent
+class IsLocallyNilpotent (I : Ideal R) : Prop :=
+    h : ∀ x ∈ I, IsNilpotent x
+#check Ideal.IsLocallyNilpotent
+end Ideal
+
+
+-- Repeats the definition of the length of a module by Monalisa
+variable (R : Type _) [CommRing R] (I J : Ideal R)
+variable (M : Type _) [AddCommMonoid M] [Module R M]
+
+-- change the definition of length of a module
+namespace Module
+noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < ⊤}
+end Module
+
+-- Stacks Lemma 10.31.5: R is Noetherian iff Spec(R) is a Noetherian space
+example [IsNoetherianRing R] :
+    TopologicalSpace.NoetherianSpace (PrimeSpectrum R) :=
+  inferInstance
+
+instance ring_Noetherian_of_spec_Noetherian
+    [TopologicalSpace.NoetherianSpace (PrimeSpectrum R)] :
+    IsNoetherianRing R where
+  noetherian := by sorry
+
+lemma ring_Noetherian_iff_spec_Noetherian : IsNoetherianRing R 
+    ↔ TopologicalSpace.NoetherianSpace (PrimeSpectrum R) := by
+    constructor
+    intro RisNoetherian
+    -- how do I apply an instance to prove one direction?
+
+
+-- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible :
+-- Every closed subset of a noetherian space is a finite union 
+-- of irreducible closed subsets.
+
+-- Stacks Lemma 10.32.5: R Noetherian. I,J ideals.
+--  If J ⊂ √I, then J ^ n ⊂ I for some n. In particular, locally nilpotent
+-- and nilpotent are the same for Noetherian rings
+lemma containment_radical_power_containment : 
+    IsNoetherianRing R ∧ J ≤ Ideal.radical I → ∃ n : ℕ, J ^ n ≤ I :=  by 
+    rintro ⟨RisNoetherian, containment⟩ 
+    rw [isNoetherianRing_iff_ideal_fg] at RisNoetherian
+    specialize RisNoetherian (Ideal.radical I)
+    rcases RisNoetherian with ⟨S, Sgenerates⟩
+
+    -- how to I get a generating set?
+
+-- Stacks Lemma 10.52.6: I is a maximal ideal and IM = 0. Then length of M is
+-- 
+
+-- Stacks Lemma 10.52.8: I is a finitely generated maximal ideal of R.
+-- M is a finite R-mod and I^nM=0. Then length of M is finite.
+lemma power_zero_finite_length : Ideal.FG I → Ideal.IsMaximal I → Module.Finite R M
+    → (∃ n : ℕ, (I ^ n) • (⊤ : Submodule R M) = 0)
+    → (∃ m : ℕ, Module.length R M ≤ m) := by
+    intro IisFG IisMaximal MisFinite power
+    rcases power with ⟨n, npower⟩
+    -- how do I get a generating set?
+
+
+-- Stacks Lemma 10.53.3: R is Artinian iff R has finitely many maximal ideals
+lemma IsArtinian_iff_finite_max_ideal : 
+    IsArtinianRing R ↔ Finite (MaximalSpectrum R) := by sorry
+
+-- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent
+lemma Jacobson_of_Artinian_is_nilpotent : 
+    IsArtinianRing R → IsNilpotent (Ideal.jacobson (⊤ : Ideal R)) := by sorry
+
+-- Stacks Lemma 10.53.5: If R has finitely many maximal ideals and 
+-- locally nilpotent Jacobson radical, then R is the product of its localizations at 
+-- its maximal ideals. Also, all primes are maximal
+
+-- lemma product_of_localization_at_maximal_ideal : Finite (MaximalSpectrum R)
+--      ∧ 
+
+def jaydensRing : Type _ := sorry
+  -- ∀ I : MaximalSpectrum R, Localization.AtPrime R I
+
+instance : CommRing jaydensRing := sorry -- this should come for free, don't even need to state it
+
+def foo : jaydensRing ≃+* R where
+  toFun := _
+  invFun := _
+  left_inv := _
+  right_inv := _
+  map_mul' := _
+  map_add' := _
+      -- Ideal.IsLocallyNilpotent (Ideal.jacobson (⊤ : Ideal R)) → 
+      --  Pi.commRing (MaximalSpectrum R) Localization.AtPrime R I
+      -- := by sorry
+-- Haven't finished this.
+
+-- Stacks Lemma 10.53.6: R is Artinian iff R has finite length as an R-mod
+lemma IsArtinian_iff_finite_length : 
+    IsArtinianRing R ↔ (∃ n : ℕ, Module.length R R ≤ n) := by sorry 
+
+-- Lemma: if R has finite length as R-mod, then R is Noetherian
+lemma finite_length_is_Noetherian : 
+    (∃ n : ℕ, Module.length R R ≤ n) → IsNoetherianRing R := by sorry 
+
+-- Lemma: if R is Artinian then all the prime ideals are maximal
+lemma primes_of_Artinian_are_maximal : 
+    IsArtinianRing R → Ideal.IsPrime I → Ideal.IsMaximal I := by sorry
+
+-- Lemma: Krull dimension of a ring is the supremum of height of maximal ideals
+
+
+-- Stacks Lemma 10.60.5: R is Artinian iff R is Noetherian of dimension 0
+lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : 
+    IsNoetherianRing R ∧ Ideal.krullDim R = 0 ↔ IsArtinianRing R := by 
+    constructor
+    sorry
+    intro RisArtinian
+    constructor
+    apply finite_length_is_Noetherian
+    rwa [IsArtinian_iff_finite_length] at RisArtinian
+    sorry
+
+
+
+
+    
+
+
+
+
+
 
--- how to use namespace
 
-namespace something
 
-end something
 
-open something
 
 
 

From 23064c442b509a300c75e215dffc266f065d5ea0 Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Tue, 13 Jun 2023 19:55:50 -0700
Subject: [PATCH 07/18] Little bit of golfing

---
 CommAlg/krull.lean | 20 +++++++++-----------
 1 file changed, 9 insertions(+), 11 deletions(-)

diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index 78e2a36..24251ab 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -130,8 +130,6 @@ lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by
   simp [field_prime_height_zero]
 
 lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by
-  unfold krullDim at h
-  simp [height] at h
   by_contra x
   rw [Ring.not_isField_iff_exists_prime] at x
   obtain ⟨P, ⟨h1, primeP⟩⟩ := x
@@ -140,16 +138,16 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0)
     by_contra a
     have : P = ⊥ := by rwa [PrimeSpectrum.ext_iff] at a
     contradiction
-  have PgtBot : P' > ⊥ := Ne.bot_lt h2
-  have pos_height : ¬ ↑(Set.chainHeight {J | J < P'}) ≤ 0  := by
-    have : ⊥ ∈ {J | J < P'} := PgtBot
+  have pos_height : ¬ (height P') ≤ 0  := by
+    have : ⊥ ∈ {J | J < P'} := Ne.bot_lt h2
     have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this
+    unfold height
     rw [←Set.one_le_chainHeight_iff] at this
     exact not_le_of_gt (Iff.mp ENat.one_le_iff_pos this)
-  have nonpos_height : (Set.chainHeight {J | J < P'}) ≤ 0 := by
-    have : (⨆ (I : PrimeSpectrum D), (Set.chainHeight {J | J < I} : WithBot ℕ∞)) ≤ 0 := h.le
-    rw [iSup_le_iff] at this
-    exact Iff.mp WithBot.coe_le_zero (this P')
+  have nonpos_height : height P' ≤ 0 := by
+    have := height_le_krullDim P'
+    rw [h] at this
+    aesop
   contradiction
 
 lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
@@ -167,10 +165,10 @@ lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1
   exact Ring.DimensionLEOne.principal_ideal_ring R
 
 lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
-  krullDim R ≤ krullDim (Polynomial R) + 1 := sorry
+  krullDim R + 1 ≤ krullDim (Polynomial R) := sorry
 
 lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
-  krullDim R = krullDim (Polynomial R) + 1 := sorry
+  krullDim R + 1 = krullDim (Polynomial R) := sorry
 
 lemma height_eq_dim_localization :
   height I = krullDim (Localization.AtPrime I.asIdeal) := sorry

From 06a491b8437fa18bddee734ecbaaad74ad1636dd Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Tue, 13 Jun 2023 19:58:28 -0700
Subject: [PATCH 08/18] del: Deleted temp working file

---
 CommAlg/sayantan(dim_eq_zero_iff_field).lean | 82 --------------------
 1 file changed, 82 deletions(-)
 delete mode 100644 CommAlg/sayantan(dim_eq_zero_iff_field).lean

diff --git a/CommAlg/sayantan(dim_eq_zero_iff_field).lean b/CommAlg/sayantan(dim_eq_zero_iff_field).lean
deleted file mode 100644
index fd712f0..0000000
--- a/CommAlg/sayantan(dim_eq_zero_iff_field).lean
+++ /dev/null
@@ -1,82 +0,0 @@
-import Mathlib.RingTheory.Ideal.Basic
-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.AlgebraicGeometry.PrimeSpectrum.Basic
-import Mathlib.Order.ConditionallyCompleteLattice.Basic
-
-namespace Ideal
-
-variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
-noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I}
-noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I
-
-lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl
-lemma krullDim_def (R : Type) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl
-lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl
-
-@[simp]
-lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by
-      constructor
-      · intro primeP
-        obtain T := eq_bot_or_top P
-        have : ¬P = ⊤ := IsPrime.ne_top primeP
-        tauto
-      · intro botP
-        rw [botP]
-        exact bot_prime
-
-lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : height P = 0 := by
-    unfold height
-    simp
-    by_contra spec
-    change _ ≠ _ at spec
-    rw [← Set.nonempty_iff_ne_empty] at spec
-    obtain ⟨J, JlP : J < P⟩ := spec
-    have P0 : IsPrime P.asIdeal := P.IsPrime
-    have J0 : IsPrime J.asIdeal := J.IsPrime
-    rw [field_prime_bot] at P0 J0
-    have : J.asIdeal = P.asIdeal := Eq.trans J0 (Eq.symm P0)
-    have : J = P := PrimeSpectrum.ext J P this
-    have : J ≠ P := ne_of_lt JlP
-    contradiction
-
-lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by
-  unfold krullDim
-  simp [field_prime_height_zero]
-
-noncomputable
-instance : CompleteLattice (WithBot ℕ∞) :=
-  inferInstanceAs <| CompleteLattice (WithBot (WithTop ℕ))
-
-lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by
-  unfold krullDim at h
-  simp [height] at h
-  by_contra x
-  rw [Ring.not_isField_iff_exists_prime] at x
-  obtain ⟨P, ⟨h1, primeP⟩⟩ := x
-  let P' : PrimeSpectrum D := PrimeSpectrum.mk P primeP
-  have h2 : P' ≠ ⊥ := by
-    by_contra a
-    have : P = ⊥ := by rwa [PrimeSpectrum.ext_iff] at a
-    contradiction
-  have PgtBot : P' > ⊥ := Ne.bot_lt h2
-  have pos_height : ¬ ↑(Set.chainHeight {J | J < P'}) ≤ 0  := by
-    have : ⊥ ∈ {J | J < P'} := PgtBot
-    have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this
-    rw [←Set.one_le_chainHeight_iff] at this
-    exact not_le_of_gt (Iff.mp ENat.one_le_iff_pos this)
-  have nonpos_height : (Set.chainHeight {J | J < P'}) ≤ 0 := by
-    have : (⨆ (I : PrimeSpectrum D), (Set.chainHeight {J | J < I} : WithBot ℕ∞)) ≤ 0 := h.le
-    rw [iSup_le_iff] at this
-    exact Iff.mp WithBot.coe_le_zero (this P')
-  contradiction
-
-lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
-  constructor
-  · exact isField.dim_zero
-  · intro fieldD
-    let h : Field D := IsField.toField fieldD
-    exact dim_field_eq_zero

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 09/18] 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 10/18] 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 50aa1b07a8a3dbfb712765e822db7a368bcdbce3 Mon Sep 17 00:00:00 2001
From: leopoldmayer <leomayer@uw.edu>
Date: Tue, 13 Jun 2023 20:58:32 -0700
Subject: [PATCH 11/18] moved krullDim_nonneg_of_nontrivial to krull.lean

---
 CommAlg/krull.lean | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index 2a87c16..4e5ac3a 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -94,6 +94,17 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
   . rw [h.forall_iff]
     trivial
 
+lemma krullDim_nonneg_of_nontrivial (R : Type _) [CommRing R] [Nontrivial R] : ∃ n : ℕ∞, Ideal.krullDim R = n := by
+  have h := dim_eq_bot_iff.not.mpr (not_subsingleton R)
+  lift (Ideal.krullDim R) to ℕ∞ using h with k
+  use k
+
+lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
+  constructor <;> intro h
+  . intro I
+    sorry
+  . sorry
+
 lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry
 
 #check Ring.DimensionLEOne
@@ -104,10 +115,10 @@ lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1
   exact Ring.DimensionLEOne.principal_ideal_ring R
 
 lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
-  krullDim R ≤ krullDim (Polynomial R) + 1 := sorry
+  krullDim R + 1 ≤ krullDim (Polynomial R) := sorry
 
 lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
-  krullDim R = krullDim (Polynomial R) + 1 := sorry
+  krullDim R + 1 = krullDim (Polynomial R) := sorry
 
 lemma height_eq_dim_localization :
   height I = krullDim (Localization.AtPrime I.asIdeal) := sorry

From 4d2aeea2c2739003c9b15337115a8bc96840671f Mon Sep 17 00:00:00 2001
From: poincare-duality <jidongw@uoregon.edu>
Date: Tue, 13 Jun 2023 21:17:54 -0700
Subject: [PATCH 12/18] more updates

---
 CommAlg/jayden(krull-dim-zero).lean | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean
index 6f282ba..523eb90 100644
--- a/CommAlg/jayden(krull-dim-zero).lean
+++ b/CommAlg/jayden(krull-dim-zero).lean
@@ -77,12 +77,25 @@ lemma containment_radical_power_containment :
     rintro ⟨RisNoetherian, containment⟩ 
     rw [isNoetherianRing_iff_ideal_fg] at RisNoetherian
     specialize RisNoetherian (Ideal.radical I)
-    rcases RisNoetherian with ⟨S, Sgenerates⟩
+    -- rcases RisNoetherian with ⟨S, Sgenerates⟩
+    have containment2 : ∃ n : ℕ,  (Ideal.radical I) ^ n ≤ I := by
+      apply Ideal.exists_radical_pow_le_of_fg I RisNoetherian
+    cases' containment2 with n containment2'
+    have containment3 : J ^ n ≤ (Ideal.radical I) ^ n := by 
+      apply Ideal.pow_mono containment
+    use n
+    apply le_trans containment3 containment2'
+-- The above can be proven using the following quicker theorem that is in the wrong place.
+-- Ideal.exists_pow_le_of_le_radical_of_fG
 
-    -- how to I get a generating set?
 
 -- Stacks Lemma 10.52.6: I is a maximal ideal and IM = 0. Then length of M is
--- 
+-- the same as the dimension as a vector space over R/I,
+lemma length_eq_dim_if_maximal_annihilates {I : Ideal R} [Ideal.IsMaximal I] 
+    : I • (⊤ : Submodule R M) = 0
+     → Module.length R M = Module.rank R⧸I M⧸(I • (⊤ : Submodule R M)) := by sorry
+
+-- Does lean know that M/IM is a R/I module?
 
 -- Stacks Lemma 10.52.8: I is a finitely generated maximal ideal of R.
 -- M is a finite R-mod and I^nM=0. Then length of M is finite.

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 13/18] 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 869ce6aa9f79faf4a6ed950f9f6f326af774274f Mon Sep 17 00:00:00 2001
From: GTBarkley <barkleygrant@gmail.com>
Date: Wed, 14 Jun 2023 04:51:49 +0000
Subject: [PATCH 14/18] proved dim_le_one_of_dimLEOne

---
 CommAlg/grant.lean | 102 +++++++++++++++++++++++++++++++++++++++++++--
 CommAlg/krull.lean |  50 ++++++++++++++++++++++
 2 files changed, 148 insertions(+), 4 deletions(-)

diff --git a/CommAlg/grant.lean b/CommAlg/grant.lean
index ce5041d..c12b189 100644
--- a/CommAlg/grant.lean
+++ b/CommAlg/grant.lean
@@ -83,6 +83,16 @@ height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀
     norm_cast at hc
     tauto
 
+lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
+height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
+  show (_ < _) ↔ _
+  rw [WithBot.coe_lt_coe]
+  exact lt_height_iff' _
+
+lemma height_le_iff {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
+  height 𝔭 ≤ n ↔ ∀ c : List (PrimeSpectrum R), c ∈ {I : PrimeSpectrum R | I < 𝔭}.subchain ∧ c.length = n + 1 := by
+  sorry
+
 lemma krullDim_nonneg_of_nontrivial [Nontrivial R] : ∃ n : ℕ∞, Ideal.krullDim R = n := by
   have h := dim_eq_bot_iff.not.mpr (not_subsingleton R)
   lift (Ideal.krullDim R) to ℕ∞ using h with k
@@ -116,19 +126,103 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
   constructor <;> intro h
   . rw [←not_nonempty_iff]
     rintro ⟨a, ha⟩
-    -- specialize h ⟨a, ha⟩
+    specialize h ⟨a, ha⟩
     tauto
   . rw [h.forall_iff]
     trivial
 
-
 #check (sorry : False)
 #check (sorryAx)
 #check (4 : WithBot ℕ∞)
 #check List.sum
+#check (_ ∈ (_ : List _))
+variable (α : Type ) 
+#synth Membership α (List α)
+#check bot_lt_iff_ne_bot
 -- #check ((4 : ℕ∞) : WithBot (WithTop ℕ))
 -- #check ( (Set.chainHeight s) : WithBot (ℕ∞))
 
-variable (P : PrimeSpectrum R)
+/-- The converse of this is false, because the definition of "dimension ≤ 1" in mathlib
+  applies only to dimension zero rings and domains of dimension 1. -/
+lemma dim_le_one_of_dimLEOne :  Ring.DimensionLEOne R → krullDim R ≤ (1 : ℕ) := by
+  rw [krullDim_le_iff R 1]
+  -- unfold Ring.DimensionLEOne
+  intro H p
+  -- have Hp := H p.asIdeal
+  -- have Hp := fun h => (Hp h) p.IsPrime
+  apply le_of_not_gt
+  intro h
+  rcases ((lt_height_iff'' R).mp h) with ⟨c, ⟨hc1, hc2, hc3⟩⟩
+  norm_cast at hc3
+  rw [List.chain'_iff_get] at hc1
+  specialize hc1 0 (by rw [hc3]; simp)
+  -- generalize hq0 : List.get _ _ = q0 at hc1
+  set q0 : PrimeSpectrum R := List.get c { val := 0, isLt := _ }
+  set q1 : PrimeSpectrum R := List.get c { val := 1, isLt := _ } 
+  -- have hq0 : q0 ∈ c := List.get_mem _ _ _ 
+  -- have hq1 : q1 ∈ c := List.get_mem _ _ _
+  specialize hc2 q1 (List.get_mem _ _ _)
+  -- have aa := (bot_le : (⊥ : Ideal R) ≤ q0.asIdeal)
+  change q0.asIdeal < q1.asIdeal at hc1
+  have q1nbot := Trans.trans (bot_le : ⊥ ≤ q0.asIdeal) hc1
+  specialize H q1.asIdeal (bot_lt_iff_ne_bot.mp q1nbot) q1.IsPrime
+  -- change q1.asIdeal < p.asIdeal at hc2
+  apply IsPrime.ne_top p.IsPrime
+  apply (IsCoatom.lt_iff H.out).mp
+  exact hc2
+  --refine Iff.mp radical_eq_top (?_ (id (Eq.symm hc3))) 
+end Krull
 
-#check {J | J < P}.le_chainHeight_iff (n := 4)
+section iSupWithBot
+
+variable {α : Type _} [CompleteSemilatticeSup α] {I : Type _} (f : I → α)
+
+#synth SupSet (WithBot ℕ∞)
+
+protected lemma WithBot.iSup_ge_coe_iff {a : α} : 
+  (a ≤ ⨆ i : I, (f i : WithBot α) ) ↔ ∃ i : I, f i ≥ a := by
+  rw [WithBot.coe_le_iff]
+  sorry
+
+end iSupWithBot
+
+section myGreatElab
+open Lean Meta Elab
+
+syntax (name := lhsStx) "lhs% " term:max : term
+syntax (name := rhsStx) "rhs% " term:max : term
+
+@[term_elab lhsStx, term_elab rhsStx]
+def elabLhsStx : Term.TermElab := fun stx expectedType? =>
+  match stx with
+  | `(lhs% $t) => do
+    let (lhs, _, eq) ← mkExpected expectedType?
+    discard <| Term.elabTermEnsuringType t eq
+    return lhs
+  | `(rhs% $t) => do
+    let (_, rhs, eq) ← mkExpected expectedType?
+    discard <| Term.elabTermEnsuringType t eq
+    return rhs
+  | _ => throwUnsupportedSyntax
+where
+  mkExpected expectedType? := do
+    let α ←
+      if let some expectedType := expectedType? then
+        pure expectedType
+      else
+        mkFreshTypeMVar
+    let lhs ← mkFreshExprMVar α
+    let rhs ← mkFreshExprMVar α
+    let u ← getLevel α
+    let eq := mkAppN (.const ``Eq [u]) #[α, lhs, rhs]
+    return (lhs, rhs, eq)
+
+#check lhs% (add_comm 1 2)
+#check rhs% (add_comm 1 2)
+#check lhs% (add_comm _ _ : _ = 1 + 2)
+
+example (x y : α) (h : x = y) : lhs% h = rhs% h := h
+
+def lhsOf {α : Sort _} {x y : α} (h : x = y) : α := x
+
+#check lhsOf (add_comm 1 2)
\ No newline at end of file
diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index 78e2a36..6f65a93 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -160,8 +160,58 @@ lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D =
     exact dim_field_eq_zero
 
 #check Ring.DimensionLEOne
+-- This lemma is false!
 lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry
 
+lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
+height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
+  rcases n with _ | n
+  . constructor <;> intro h <;> exfalso
+    . exact (not_le.mpr h) le_top
+    . tauto
+  have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by
+    symm
+    show (n + 1 ≤ m ↔ _ )
+    apply ENat.add_one_le_iff
+    exact ENat.coe_ne_top _
+  rw [this]
+  unfold Ideal.height
+  show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞))
+  rw [{J | J < 𝔭}.le_chainHeight_iff]
+  show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
+  constructor <;> rintro ⟨c, hc⟩ <;> use c
+  . tauto
+  . change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc
+    norm_cast at hc
+    tauto
+
+lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
+height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
+  show (_ < _) ↔ _
+  rw [WithBot.coe_lt_coe]
+  exact lt_height_iff'
+
+/-- The converse of this is false, because the definition of "dimension ≤ 1" in mathlib
+  applies only to dimension zero rings and domains of dimension 1. -/
+lemma dim_le_one_of_dimLEOne :  Ring.DimensionLEOne R → krullDim R ≤ (1 : ℕ) := by
+  rw [krullDim_le_iff R 1]
+  intro H p
+  apply le_of_not_gt
+  intro h
+  rcases (lt_height_iff''.mp h) with ⟨c, ⟨hc1, hc2, hc3⟩⟩
+  norm_cast at hc3
+  rw [List.chain'_iff_get] at hc1
+  specialize hc1 0 (by rw [hc3]; simp)
+  set q0 : PrimeSpectrum R := List.get c { val := 0, isLt := _ }
+  set q1 : PrimeSpectrum R := List.get c { val := 1, isLt := _ } 
+  specialize hc2 q1 (List.get_mem _ _ _)
+  change q0.asIdeal < q1.asIdeal at hc1
+  have q1nbot := Trans.trans (bot_le : ⊥ ≤ q0.asIdeal) hc1
+  specialize H q1.asIdeal (bot_lt_iff_ne_bot.mp q1nbot) q1.IsPrime
+  apply IsPrime.ne_top p.IsPrime
+  apply (IsCoatom.lt_iff H.out).mp
+  exact hc2
+
 lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1 := by
   rw [dim_le_one_iff]
   exact Ring.DimensionLEOne.principal_ideal_ring R

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 15/18] 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 56cefd9b53ab50541dbd3c088febe0ffd6894d6d Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Tue, 13 Jun 2023 22:54:57 -0700
Subject: [PATCH 16/18] Made some progress on dim_eq_dim_polynomial_add_one

---
 ...yantan(dim_eq_dim_polynomial_add_one).lean | 46 +++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean

diff --git a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean
new file mode 100644
index 0000000..a9269a2
--- /dev/null
+++ b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean
@@ -0,0 +1,46 @@
+import Mathlib.RingTheory.Ideal.Basic
+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.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
+
+namespace Ideal
+
+variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
+noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I}
+noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I
+
+lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl
+lemma krullDim_def (R : Type) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl
+lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl
+
+noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice
+
+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 dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
+  krullDim R + 1 = krullDim (Polynomial R) := by
+  rw [le_antisymm_iff]
+  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
+      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
+      apply iSup_le
+      exact this
+    sorry
\ 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 17/18] 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 18/18] 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