From 1f4505f8ab7e3d2c28ab8b2f998eaca461855dad Mon Sep 17 00:00:00 2001
From: Sameer Savkar <sameersavkar@gmail.com>
Date: Tue, 13 Jun 2023 16:00:58 -0700
Subject: [PATCH] added two lemmas

---
 CommAlg/sameer(artinian-rings).lean | 59 +++++++++++++++++++++++++++--
 1 file changed, 56 insertions(+), 3 deletions(-)

diff --git a/CommAlg/sameer(artinian-rings).lean b/CommAlg/sameer(artinian-rings).lean
index 381680b..e6bb667 100644
--- a/CommAlg/sameer(artinian-rings).lean
+++ b/CommAlg/sameer(artinian-rings).lean
@@ -3,13 +3,66 @@ import Mathlib.RingTheory.Noetherian
 import Mathlib.RingTheory.Artinian
 import Mathlib.RingTheory.Ideal.Quotient
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.RingTheory.DedekindDomain.DVR
+
+
+lemma FieldisArtinian (R : Type _) [CommRing R] (IsField : ):= by sorry
+
+
+lemma ArtinianDomainIsField (R : Type _) [CommRing R] [IsDomain R]
+(IsArt : IsArtinianRing R) : IsField (R) := by 
+-- Assume P is nonzero and R is Artinian
+-- Localize at P; Then R_P is Artinian; 
+-- Assume R_P is not a field 
+-- Then Jacobson Radical of R_P is nilpotent so it's maximal ideal is nilpotent
+-- Maximal ideal is zero since local ring is a domain
+-- a contradiction since P is nonzero
+-- Therefore, R is a field
+have maxIdeal := Ideal.exists_maximal R
+obtain ⟨m,hm⟩ := maxIdeal
+have h:= Ideal.primeCompl_le_nonZeroDivisors m 
+have artRP : IsDomain _ := IsLocalization.isDomain_localization h
+have h' : IsArtinianRing (Localization (Ideal.primeCompl m)) := inferInstance
+have h' : IsNilpotent (Ideal.jacobson (⊥ : Ideal (Localization 
+  (Ideal.primeCompl m)))):= IsArtinianRing.isNilpotent_jacobson_bot
+have := LocalRing.jacobson_eq_maximalIdeal (⊥ : Ideal (Localization 
+  (Ideal.primeCompl m))) bot_ne_top
+rw [this] at h'
+have := IsNilpotent.eq_zero h'
+rw [Ideal.zero_eq_bot, ← LocalRing.isField_iff_maximalIdeal_eq] at this
+by_contra h''
+--by_cases h'' : m = ⊥
+have := Ring.ne_bot_of_isMaximal_of_not_isField hm h'' 
+have := IsLocalization.AtPrime.not_isField R this (Localization (Ideal.primeCompl m))
+contradiction
 
-lemma quotientRing_is_Artinian (R : Type _) [CommRing R] (I : Ideal R) (IsArt : IsArtinianRing R): 
-IsArtinianRing (R⧸I) := by sorry
 
 #check Ideal.IsPrime
+#check IsDomain
+
+lemma isArtinianRing_of_quotient_of_artinian (R : Type _) [CommRing R]
+    (I : Ideal R) (IsArt : IsArtinianRing R) : IsArtinianRing (R ⧸ I) :=
+  isArtinian_of_tower R (isArtinian_of_quotient_of_artinian R R I IsArt)
+
+lemma IsPrimeMaximal (R : Type _) [CommRing R] (P : Ideal R) 
+(IsArt : IsArtinianRing R) (isPrime : Ideal.IsPrime P) : Ideal.IsMaximal P := 
+by 
+-- if R is Artinian and P is prime then R/P is Integral Domain 
+-- which is Artinian Domain 
+-- R⧸P is a field by the above lemma
+-- P is maximal
+
+  have : IsDomain (R⧸P) := Ideal.Quotient.isDomain P
+  have artRP : IsArtinianRing (R⧸P) := by
+    exact isArtinianRing_of_quotient_of_artinian R P IsArt
+  
+
+-- Then R/I is Artinian 
+ --  have' : IsArtinianRing R ∧ Ideal.IsPrime I → IsDomain (R⧸I) := by
+
+-- R⧸I.IsArtinian → monotone_stabilizes_iff_artinian.R⧸I
+
 
-lemma IsPrimeMaximal (R : Type _) [CommRing R] (I : Ideal R) (IsArt : IsArtinianRing R) (isPrime : Ideal.IsPrime I) : Ideal.IsMaximal I := by sorry
 
 
 -- Use Stacks project proof since it's broken into lemmas