From c8797956abb9c28e2a3eaa97e25a5b926b4cbc40 Mon Sep 17 00:00:00 2001
From: Andre <espietandre@gmail.com>
Date: Fri, 16 Jun 2023 15:11:07 -0400
Subject: [PATCH 1/8] golfed foo

---
 CommAlg/final_poly_type.lean | 39 ++++++------------------------------
 1 file changed, 6 insertions(+), 33 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 85b01a2..07b7bf4 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -194,45 +194,18 @@ lemma Δ_1_ (f : ℤ → ℤ) (d : ℕ) : PolyType (Δ f 1) d → PolyType f (d
   sorry
 
 
-lemma foo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d)  := by
+lemma foo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → 
+    (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d)  := by
   induction' d with d hd
-
   -- Base case
-  · intro f
-    intro h
-    rcases h with ⟨c, N, hh⟩
-    rw [PolyType_0]
-    use c
-    use N
-    tauto
-
+  · rintro f ⟨c, N, hh⟩; rw [PolyType_0 f]; exact ⟨c, N, hh⟩
   -- Induction step
-  · intro f
-    intro h
-    rcases h with ⟨c, N, h⟩
-    have this : PolyType f (d + 1) := by
-      rcases h with ⟨H,c0⟩
-      let g := (Δ f 1)
-      have this1 : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ g d) (n) = c) ∧ c ≠ 0) := by
-        use c; use N
-        constructor
-        · intro n
-          specialize H n
-          intro h
-          have this : Δ f (d + 1) n = c := by tauto
-          rw [←this]
-          rw [Δ_1_s_equiv_Δ_s_1] 
-        · tauto 
-      have this2 : PolyType g d := by
-        apply hd
-        tauto
-      exact Δ_1_ f d this2
-    exact this
+  · exact fun f ⟨c, N, ⟨H, c0⟩⟩ =>
+      Δ_1_ f d (hd (Δ f 1) ⟨c, N, fun n h => by rw [← H n h, Δ_1_s_equiv_Δ_s_1], c0⟩)
 
 -- [BH, 4.1.2] (a) => (b)
 -- Δ^d f (n) = c for some nonzero integer c for n >> 0 → f is of polynomial type d
-lemma a_to_b (f : ℤ → ℤ) (d : ℕ) : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → PolyType f d := by
-  sorry
+lemma a_to_b (f : ℤ → ℤ) (d : ℕ) : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → PolyType f d := fun h => (foo d f) h
 
 -- [BH, 4.1.2] (a) <= (b)
 -- f is of polynomial type d → Δ^d f (n) = c for some nonzero integer c for n >> 0

From 3e8aafd23d5e659f989faa2f8acc167fa78dd913 Mon Sep 17 00:00:00 2001
From: Andre <espietandre@gmail.com>
Date: Fri, 16 Jun 2023 15:17:43 -0400
Subject: [PATCH 2/8] golfed delta_

---
 CommAlg/final_poly_type.lean | 13 +++----------
 1 file changed, 3 insertions(+), 10 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 07b7bf4..8bc6b9e 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -53,8 +53,6 @@ noncomputable section
 def PolyType (f : ℤ → ℤ) (d : ℕ) := ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly) ∧ d = Polynomial.degree Poly
 section
 
-#check PolyType
-
 example (f : ℤ → ℤ) (hf : ∀ x, f x = x ^ 2) : PolyType f 2 := by
   unfold PolyType
   sorry
@@ -132,8 +130,8 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
 
 -- Δ of 0 times preserves the function
 lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by rfl
-  --simp only [Δ]
--- Δ of 1 times decreaes the polynomial type by one
+
+-- Δ of 1 times decreaes the polynomial type by one --can be golfed
 lemma Δ_1 (f : ℤ → ℤ) (d : ℕ) : PolyType f (d + 1) → PolyType (Δ f 1) d := by
   intro h
   simp only [PolyType, Δ, Int.cast_sub, exists_and_right]
@@ -186,20 +184,15 @@ lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d 
 
 -- The "reverse" of Δ of 1 times increases the polynomial type by one
 lemma Δ_1_ (f : ℤ → ℤ) (d : ℕ) : PolyType (Δ f 1) d → PolyType f (d + 1) := by
-  intro h
+  rintro ⟨P, N, ⟨h1, h2⟩⟩ 
   simp only [PolyType, Nat.cast_add, Nat.cast_one, exists_and_right]
-  rcases h with ⟨P, N, h⟩
-  rcases h with ⟨h1, h2⟩
   let G := fun (q : ℤ) => f (N)
   sorry
 
-
 lemma foo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → 
     (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d)  := by
   induction' d with d hd
-  -- Base case
   · rintro f ⟨c, N, hh⟩; rw [PolyType_0 f]; exact ⟨c, N, hh⟩
-  -- Induction step
   · exact fun f ⟨c, N, ⟨H, c0⟩⟩ =>
       Δ_1_ f d (hd (Δ f 1) ⟨c, N, fun n h => by rw [← H n h, Δ_1_s_equiv_Δ_s_1], c0⟩)
 

From 24d2f8e1f082b81dcebe9db0cefe17c1c00b81e5 Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Fri, 16 Jun 2023 12:20:24 -0700
Subject: [PATCH 3/8] finish poly_shifting

---
 CommAlg/final_poly_type.lean | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 85b01a2..6c9e556 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -15,6 +15,7 @@ macro "obviously" : tactic =>
         | 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"
+        | norm_cast; done; dbg_trace "it was norm_cast"
         | /-change (@Eq ℝ _ _);-/ linarith; done; dbg_trace "it was linarith"
         -- | gcongr; done
         | ring; done; dbg_trace "it was ring"
@@ -84,7 +85,7 @@ lemma Polynomial_shifting (F : Polynomial ℚ) (s : ℚ) : ∃ (G : Polynomial 
   sorry
 
 -- Shifting doesn't change the polynomial type
-lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s : ℤ) (hfg : ∀ (n : ℤ), f (n + s) = g (n)) : PolyType g d := by
+lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s : ℕ) (hfg : ∀ (n : ℤ), f (n + s) = g (n)) : PolyType g d := by
   simp only [PolyType]
   rcases hf with ⟨F, hh⟩
   rcases hh with ⟨N,s1, s2⟩
@@ -97,9 +98,15 @@ lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s :
   · intro n
     specialize s1 (n + s)
     intro hN
-    have this1 : f (n + s) = Polynomial.eval (n + s : ℚ) F := by
-      sorry
-    sorry
+    have this1 : f (n + s) = Polynomial.eval (n + (s : ℚ)) F := by
+      have this2 : N ≤ n + s := by linarith
+      have this3 : ↑(f (n + ↑s)) = Polynomial.eval (↑(n + ↑s)) F := by tauto
+      rw [this3]
+      norm_cast
+    specialize hfg n
+    rw [←hfg, this1]
+    specialize h1 n
+    tauto
   · rw [h2, s2]
 
 -- PolyType 0 = constant function
@@ -241,6 +248,9 @@ lemma b_to_a (f : ℤ → ℤ) (d : ℕ) (poly : PolyType f d) :
   rw [←PolyType_0]; exact Δ_d_PolyType_d_to_PolyType_0 f d poly
 
 end
+
+
+
 -- @Additive lemma of length for a SES
 -- Given a SES 0 → A → B → C → 0, then length (A) - length (B) + length (C) = 0 
 section

From cb4e0ead26d54fd6e615dbc1a576fbd8bf7dcbef Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Fri, 16 Jun 2023 13:16:46 -0700
Subject: [PATCH 4/8] trivial change

---
 CommAlg/final_poly_type.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 9388083..85e322f 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -5,7 +5,7 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 set_option maxHeartbeats 0
 macro "ls" : tactic => `(tactic|library_search)
 
--- New tactic "obviously"
+-- From Kyle : New tactic "obviously"
 macro "obviously" : tactic =>
   `(tactic| (
       first

From 3588faa23ce477c043cce51f800dc1a471120dce Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Fri, 16 Jun 2023 14:34:28 -0700
Subject: [PATCH 5/8] add something in Polynomial_shifting

---
 CommAlg/final_poly_type.lean | 28 +++++++++++++++++++++++++++-
 1 file changed, 27 insertions(+), 1 deletion(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 85e322f..2820552 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -80,7 +80,33 @@ lemma Poly_constant (F : Polynomial ℚ) (c : ℚ) :
 
 -- Get the polynomial G (X) = F (X + s) from the polynomial F(X)
 lemma Polynomial_shifting (F : Polynomial ℚ) (s : ℚ) : ∃ (G : Polynomial ℚ), (∀ (x : ℚ), Polynomial.eval x G = Polynomial.eval (x + s) F) ∧ (Polynomial.degree G = Polynomial.degree F) := by  
-  sorry
+  let Shift := (Polynomial.monomial 1 (1 : ℚ)) + (Polynomial.C s)
+  let G := Polynomial.comp Shift F
+  use G
+  constructor
+  · intro t
+    have this : Polynomial.eval t G = Polynomial.eval (Polynomial.eval t Shift) F:= by
+      sorry
+    have this1 : Polynomial.eval t Shift = t + s := by
+      dsimp; simp
+    rw [this1] at this
+    exact this
+  · have this : Polynomial.degree G = (Polynomial.degree F) * (Polynomial.degree Shift) := by
+      sorry
+    have Shift_degree : Polynomial.degree Shift = 1 := by
+      have this2 : Polynomial.degree (Polynomial.monomial 1 (1 : ℚ)) = 1 := by
+        have this3 : (1 : ℚ) ≠ 0 := by norm_num
+        exact Polynomial.degree_monomial 1 this3
+      have this1 : Polynomial.degree Shift = (Polynomial.degree (Polynomial.monomial 1 (1 : ℚ))) + (Polynomial.degree (Polynomial.C s)) := by
+        sorry
+      have this3 : Polynomial.degree (Polynomial.C s) = 0 := by
+        sorry
+      rw [this1, this2, this3]
+      trivial
+    rw [Shift_degree] at this
+    rw [this]
+    norm_num
+
 
 -- Shifting doesn't change the polynomial type
 lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s : ℕ) (hfg : ∀ (n : ℤ), f (n + s) = g (n)) : PolyType g d := by

From 01fb5fbd8b6d10e488ed72800c0838664dfe8446 Mon Sep 17 00:00:00 2001
From: Andre <espietandre@gmail.com>
Date: Fri, 16 Jun 2023 17:37:02 -0400
Subject: [PATCH 6/8] finished refactoring

---
 CommAlg/final_poly_type.lean | 51 ++++++++++++++----------------------
 1 file changed, 19 insertions(+), 32 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 9388083..449da0d 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -5,7 +5,7 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 set_option maxHeartbeats 0
 macro "ls" : tactic => `(tactic|library_search)
 
--- New tactic "obviously"
+-- From Kyle : New tactic "obviously"
 macro "obviously" : tactic =>
   `(tactic| (
       first
@@ -41,7 +41,7 @@ example : Polynomial.eval (100 : ℚ) F = (2 : ℚ) := by
   refine Iff.mpr (Rat.ext_iff (Polynomial.eval 100 F) 2) ?_
   simp only [Rat.ofNat_num, Rat.ofNat_den]
   rw [F]
-  simp
+  simp [simp]
 
 -- Treat polynomial f ∈ ℚ[X] as a function f : ℚ → ℚ
 
@@ -51,7 +51,9 @@ end section
 noncomputable section
 -- Polynomial type of degree d
 @[simp]
-def PolyType (f : ℤ → ℤ) (d : ℕ) := ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly) ∧ d = Polynomial.degree Poly
+def PolyType (f : ℤ → ℤ) (d : ℕ) := 
+  ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly) ∧ 
+    d = Polynomial.degree Poly
 section
 
 example (f : ℤ → ℤ) (hf : ∀ x, f x = x ^ 2) : PolyType f 2 := by
@@ -68,43 +70,30 @@ def Δ : (ℤ → ℤ) → ℕ → (ℤ → ℤ)
 
 -- (NO need to prove another direction) Constant polynomial function = constant function
 lemma Poly_constant (F : Polynomial ℚ) (c : ℚ) : 
-  (F = Polynomial.C (c : ℚ)) ↔ (∀ r : ℚ, (Polynomial.eval r F) = (c : ℚ)) := by
+    (F = Polynomial.C (c : ℚ)) ↔ (∀ r : ℚ, (Polynomial.eval r F) = (c : ℚ)) := by
   constructor
-  · intro h
-    rintro r
+  · intro h r
     refine Iff.mpr (Rat.ext_iff (Polynomial.eval r F) c) ?_
     simp only [Rat.ofNat_num, Rat.ofNat_den]
-    rw [h]
-    simp
+    simp [h]
   · sorry
 
 -- Get the polynomial G (X) = F (X + s) from the polynomial F(X)
-lemma Polynomial_shifting (F : Polynomial ℚ) (s : ℚ) : ∃ (G : Polynomial ℚ), (∀ (x : ℚ), Polynomial.eval x G = Polynomial.eval (x + s) F) ∧ (Polynomial.degree G = Polynomial.degree F) := by  
+lemma Polynomial_shifting (F : Polynomial ℚ) (s : ℚ) : ∃ (G : Polynomial ℚ), (∀ (x : ℚ), 
+    Polynomial.eval x G = Polynomial.eval (x + s) F) ∧ 
+    (Polynomial.degree G = Polynomial.degree F) := by  
   sorry
 
 -- Shifting doesn't change the polynomial type
-lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s : ℕ) (hfg : ∀ (n : ℤ), f (n + s) = g (n)) : PolyType g d := by
-  simp only [PolyType]
-  rcases hf with ⟨F, hh⟩
-  rcases hh with ⟨N,s1, s2⟩
-  have this : ∃ (G : Polynomial ℚ), (∀ (x : ℚ), Polynomial.eval x G = Polynomial.eval (x + s) F) ∧ (Polynomial.degree G = Polynomial.degree F) := by
-    exact Polynomial_shifting F s
-  rcases this with ⟨Poly, h1, h2⟩
-  use Poly
-  use N
-  constructor
-  · intro n
-    specialize s1 (n + s)
-    intro hN
+lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s : ℕ) 
+    (hfg : ∀ (n : ℤ), f (n + s) = g (n)) : PolyType g d := by
+  rcases hf with ⟨F, ⟨N, s1, s2⟩⟩
+  rcases (Polynomial_shifting F s) with ⟨Poly, h1, h2⟩
+  use Poly, N; constructor
+  · intro n hN
     have this1 : f (n + s) = Polynomial.eval (n + (s : ℚ)) F := by
-      have this2 : N ≤ n + s := by linarith
-      have this3 : ↑(f (n + ↑s)) = Polynomial.eval (↑(n + ↑s)) F := by tauto
-      rw [this3]
-      norm_cast
-    specialize hfg n
-    rw [←hfg, this1]
-    specialize h1 n
-    tauto
+      rw [s1 (n + s) (by linarith)]; norm_cast
+    rw [←hfg n, this1]; exact (h1 n).symm
   · rw [h2, s2]
 
 -- PolyType 0 = constant function
@@ -215,8 +204,6 @@ lemma b_to_a (f : ℤ → ℤ) (d : ℕ) (poly : PolyType f d) :
 
 end
 
-
-
 -- @Additive lemma of length for a SES
 -- Given a SES 0 → A → B → C → 0, then length (A) - length (B) + length (C) = 0 
 section

From fc6fac87a2cc440539b382b1e1d129590ff3bd57 Mon Sep 17 00:00:00 2001
From: poincare-duality <jidongw@uoregon.edu>
Date: Fri, 16 Jun 2023 14:37:06 -0700
Subject: [PATCH 7/8] Is it too late to say sorry

---
 CommAlg/jayden(krull-dim-zero).lean | 67 ++++++++++++++++++++++++-----
 1 file changed, 56 insertions(+), 11 deletions(-)

diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean
index 15dd150..921d6f8 100644
--- a/CommAlg/jayden(krull-dim-zero).lean
+++ b/CommAlg/jayden(krull-dim-zero).lean
@@ -16,6 +16,7 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Algebra.Ring.Pi
 import Mathlib.RingTheory.Finiteness
 import Mathlib.Util.PiNotation
+import Mathlib.RingTheory.Ideal.MinimalPrime
 import CommAlg.krull
 
 open PiNotation
@@ -43,6 +44,8 @@ class IsLocallyNilpotent {R : Type _} [CommRing R] (I : Ideal R) : Prop :=
 #check Ideal.IsLocallyNilpotent
 end Ideal
 
+def RingJacobson (R) [Ring R] := Ideal.jacobson (⊥ : Ideal R)
+
 -- 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]
@@ -169,15 +172,15 @@ abbrev Prod_of_localization :=
 def foo : Prod_of_localization R →+* R where
   toFun := sorry
   -- invFun := sorry
-  left_inv := sorry
-  right_inv := sorry
+  --left_inv := sorry
+  --right_inv := sorry
   map_mul' := sorry
   map_add' := sorry
 
 
 def product_of_localization_at_maximal_ideal [Finite (MaximalSpectrum R)]
-    (h : Ideal.IsLocallyNilpotent (Ideal.jacobson (⊥ : Ideal R))) :
-    Prod_of_localization R ≃+* R := by sorry
+    (h : Ideal.IsLocallyNilpotent (RingJacobson R)) :
+    R ≃+* Prod_of_localization R := by sorry
 
 -- Stacks Lemma 10.53.6: R is Artinian iff R has finite length as an R-mod
 lemma IsArtinian_iff_finite_length : 
@@ -193,18 +196,61 @@ lemma primes_of_Artinian_are_maximal
 
 -- Lemma: Krull dimension of a ring is the supremum of height of maximal ideals
 
+-- Lemma: X is an irreducible component of Spec(R) ↔ X = V(I) for I a minimal prime
+lemma irred_comp_minmimal_prime (X) : 
+    X ∈ irreducibleComponents (PrimeSpectrum R) 
+      ↔ ∃ (P : minimalPrimes R), X = PrimeSpectrum.zeroLocus P := by
+      sorry
+
+-- Lemma: localization of Noetherian ring is Noetherian
+-- lemma localization_of_Noetherian_at_prime [IsNoetherianRing R]
+--      (atprime: Ideal.IsPrime I) :
+--     IsNoetherianRing (Localization.AtPrime I) := by sorry
+
+
 -- Stacks Lemma 10.60.5: R is Artinian iff R is Noetherian of dimension 0
-lemma dim_le_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : 
-    IsNoetherianRing R ∧ Ideal.krullDim R ≤ 0 ↔ IsArtinianRing R := by 
-    constructor
+lemma Artinian_if_dim_le_zero_Noetherian (R : Type _) [CommRing R] : 
+    IsNoetherianRing R ∧ Ideal.krullDim R ≤ 0 → IsArtinianRing R := by
     rintro ⟨RisNoetherian, dimzero⟩  
     rw [ring_Noetherian_iff_spec_Noetherian] at RisNoetherian
+    have := fun X => (irred_comp_minmimal_prime R X).mp
+    choose F hf using this
     let Z := irreducibleComponents (PrimeSpectrum R)
-    have Zfinite : Set.Finite Z := by
+    -- have Zfinite : Set.Finite Z := by
       -- apply TopologicalSpace.NoetherianSpace.finite_irreducibleComponents ?_
+      -- sorry
+    --let P := fun 
+    rw [← ring_Noetherian_iff_spec_Noetherian] at RisNoetherian
+    have PrimeIsMaximal : ∀ X : Z, Ideal.IsMaximal (F X X.2).1 := by
+      intro X
+      have prime : Ideal.IsPrime (F X X.2).1 := (F X X.2).2.1.1
+      rw [Ideal.dim_le_zero_iff] at dimzero
+      exact dimzero ⟨_, prime⟩
+    have JacLocallyNil : Ideal.IsLocallyNilpotent (RingJacobson R) := by sorry 
+    let Loc := fun X : Z ↦ Localization.AtPrime (F X.1 X.2).1 
+    have LocNoetherian : ∀ X, IsNoetherianRing (Loc X) := by 
+      intro X
       sorry
-    
-    sorry
+      -- apply IsLocalization.isNoetherianRing (F X.1 X.2).1 (Loc X) RisNoetherian
+    have Locdimzero : ∀ X, Ideal.krullDim (Loc X) ≤ 0 := by sorry
+    have powerannihilates : ∀ X, ∃ n : ℕ, 
+      ((F X.1 X.2).1) ^ n • (⊤: Submodule R (Loc X)) = 0 := by sorry
+    have LocFinitelength : ∀ X, ∃ n : ℕ, Module.length R (Loc X) ≤ n := by
+      intro X
+      have idealfg : Ideal.FG (F X.1 X.2).1 := by
+        rw [isNoetherianRing_iff_ideal_fg] at RisNoetherian
+        specialize RisNoetherian (F X.1 X.2).1
+        exact RisNoetherian
+      have modulefg : Module.Finite R (Loc X) := by sorry -- not sure if this is true
+      specialize PrimeIsMaximal X
+      specialize powerannihilates X
+      apply power_zero_finite_length R (F X.1 X.2).1 (Loc X) idealfg powerannihilates
+    have RingFinitelength : ∃ n : ℕ, Module.length R R ≤ n := by sorry
+    rw [IsArtinian_iff_finite_length]
+    exact RingFinitelength
+
+lemma dim_le_zero_Noetherian_if_Artinian (R : Type _) [CommRing R] : 
+    IsArtinianRing R → IsNoetherianRing R ∧ Ideal.krullDim R ≤ 0 := by 
     intro RisArtinian
     constructor
     apply finite_length_is_Noetherian
@@ -213,7 +259,6 @@ lemma dim_le_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] :
     intro I
     apply primes_of_Artinian_are_maximal
 
--- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible :
 
 
 

From dbdb06fb587de57a84f7b8a453b04706bc76a485 Mon Sep 17 00:00:00 2001
From: Andre <espietandre@gmail.com>
Date: Fri, 16 Jun 2023 17:42:48 -0400
Subject: [PATCH 8/8] removed a comment

---
 CommAlg/final_poly_type.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index e96aae3..dd35253 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -5,7 +5,6 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 set_option maxHeartbeats 0
 macro "ls" : tactic => `(tactic|library_search)
 
--- From Kyle : New tactic "obviously"
 -- From Kyle : New tactic "obviously"
 macro "obviously" : tactic =>
   `(tactic| (