From 5cb0f77d2f22c5adf957dcacc198be6cf8066751 Mon Sep 17 00:00:00 2001
From: poincare-duality <jidongw@uoregon.edu>
Date: Mon, 12 Jun 2023 20:03:43 -0700
Subject: [PATCH 1/2] update
---
CommAlg/jayden(krull-dim-zero).lean | 40 ++++++++++++++++-------------
1 file changed, 22 insertions(+), 18 deletions(-)
diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean
index 0646bcb..bdb3bf9 100644
--- a/CommAlg/jayden(krull-dim-zero).lean
+++ b/CommAlg/jayden(krull-dim-zero).lean
@@ -4,15 +4,15 @@ 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.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
-- copy from krull.lean; the name of Krull dimension for rings is changed to krullDim' since krullDim already exists in the librrary
namespace Ideal
@@ -26,21 +26,9 @@ noncomputable def krullDim' (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I :
-- 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
+ IsNoetherianRing R ∧ krullDim' R = 0 ↔ IsArtinianRing R := by sorry
-variable {R : Type _} [CommRing R]
-
--- Repeats the definition by Monalisa
-noncomputable def length : krullDim (Submodule _ _)
-
-
--- The following is Stacks Lemma 10.60.5
-lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] :
- IsNoetherianRing R ∧ krull_dim R = 0 ↔ IsArtinianRing R := by
-
- sorry
-
#check IsNoetherianRing
#check krullDim
@@ -58,7 +46,25 @@ lemma IsArtinian_iff_finite_length : IsArtinianRing R ↔ ∃ n : ℕ, length R
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
+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)) → Localization.AtPrime R I
@@ -70,8 +76,6 @@ end something
open something
--- The following is Stacks Lemma 10.53.6
-lemma IsArtinian_iff_finite_length : IsArtinianRing R ↔ ∃ n : ℕ, length R R ≤ n := by sorry
From eb01e5506a234fa5084c04b301879aec28e2d121 Mon Sep 17 00:00:00 2001
From: poincare-duality <jidongw@uoregon.edu>
Date: Mon, 12 Jun 2023 20:48:42 -0700
Subject: [PATCH 2/2] add more stuff
---
CommAlg/jayden(krull-dim-zero).lean | 21 +++++++++++++++++++--
1 file changed, 19 insertions(+), 2 deletions(-)
diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean
index bdb3bf9..3651102 100644
--- a/CommAlg/jayden(krull-dim-zero).lean
+++ b/CommAlg/jayden(krull-dim-zero).lean
@@ -13,6 +13,7 @@ import Mathlib.RingTheory.DedekindDomain.Basic
import Mathlib.RingTheory.Localization.AtPrime
import Mathlib.Order.ConditionallyCompleteLattice.Basic
import Mathlib.Algebra.Ring.Pi
+import Mathlib.Topology.NoetherianSpace
-- copy from krull.lean; the name of Krull dimension for rings is changed to krullDim' since krullDim already exists in the librrary
namespace Ideal
@@ -36,7 +37,8 @@ lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] :
-- 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)
+-- 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
@@ -64,9 +66,24 @@ end Ideal
-- its maximal ideals. Also, all primes are maximal
lemma product_of_localization_at_maximal_ideal : Finite (MaximalSpectrum R)
- ∧ Ideal.IsLocallyNilpotent (Ideal.jacobson (⊤ : Ideal R)) → Localization.AtPrime R I
+ ∧ 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.
+-- 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
-- how to use namespace