add more stuff

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 height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < P}
-
-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 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