From cf0052a11221b47b8bea05b402fcd15a611cf4ad Mon Sep 17 00:00:00 2001
From: poincare-duality <jidongw@uoregon.edu>
Date: Mon, 12 Jun 2023 14:14:39 -0700
Subject: [PATCH 1/2] update lemmas

---
 comm_alg/jayden(krull-dim-zero).lean | 44 ++++++++++++++++++++++++----
 1 file changed, 38 insertions(+), 6 deletions(-)

diff --git a/comm_alg/jayden(krull-dim-zero).lean b/comm_alg/jayden(krull-dim-zero).lean
index 7be91c5..e084f18 100644
--- a/comm_alg/jayden(krull-dim-zero).lean
+++ b/comm_alg/jayden(krull-dim-zero).lean
@@ -1,28 +1,60 @@
 import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.JacobsonIdeal
 import Mathlib.RingTheory.Noetherian
 import Mathlib.Order.KrullDimension
 import Mathlib.RingTheory.Artinian
 import Mathlib.RingTheory.Ideal.Quotient
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal
+import Mathlib.Data.Finite.Defs
 
-variable {R : Type _} [CommRing R]
+import Mathlib.Order.Height
+import Mathlib.RingTheory.DedekindDomain.Basic
+import Mathlib.RingTheory.Localization.AtPrime
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
 
--- Repeats the definition by Monalisa
-noncomputable def length : krullDim (Submodule _ _)
+-- 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)
 
--- The following is Stacks Lemma 10.60.5
+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 ∧ krull_dim R = 0 ↔ IsArtinianRing R := by 
+    IsNoetherianRing R ∧ krullDim' R = 0 ↔ IsArtinianRing R := by 
   sorry
 
 #check IsNoetherianRing
 
--- The following is Stacks Lemma 10.53.6
+#check krullDim
+
+-- Repeats the definition of the length of a module by Monalisa
+variable (M : Type _) [AddCommMonoid M] [Module R M]
+
+noncomputable def length := krullDim (Submodule R 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 : Is
 
 
 
+-- how to use namespace
+
+namespace something
+
+end something
+
+open something
 
 

From 58450c56be897479198a42f517fff39a7008b7e4 Mon Sep 17 00:00:00 2001
From: poincare-duality <jidongw@uoregon.edu>
Date: Mon, 12 Jun 2023 14:21:59 -0700
Subject: [PATCH 2/2] renamed thngs

---
 {comm_alg => CommAlg}/jayden(krull-dim-zero).lean | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename {comm_alg => CommAlg}/jayden(krull-dim-zero).lean (100%)

diff --git a/comm_alg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean
similarity index 100%
rename from comm_alg/jayden(krull-dim-zero).lean
rename to CommAlg/jayden(krull-dim-zero).lean