Merge branch 'main' of github.com:GTBarkley/comm_alg into main

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
 
 
 

CommAlg/krull.lean

@@ -105,7 +105,63 @@ lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum
     sorry
   . sorry
   
-lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry
+@[simp]
+lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by
+      constructor
+      · intro primeP
+        obtain T := eq_bot_or_top P
+        have : ¬P = ⊤ := IsPrime.ne_top primeP
+        tauto
+      · intro botP
+        rw [botP]
+        exact bot_prime
+
+lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : height P = 0 := by
+    unfold height
+    simp
+    by_contra spec
+    change _ ≠ _ at spec
+    rw [← Set.nonempty_iff_ne_empty] at spec
+    obtain ⟨J, JlP : J < P⟩ := spec
+    have P0 : IsPrime P.asIdeal := P.IsPrime
+    have J0 : IsPrime J.asIdeal := J.IsPrime
+    rw [field_prime_bot] at P0 J0
+    have : J.asIdeal = P.asIdeal := Eq.trans J0 (Eq.symm P0)
+    have : J = P := PrimeSpectrum.ext J P this
+    have : J ≠ P := ne_of_lt JlP
+    contradiction
+
+lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by
+  unfold krullDim
+  simp [field_prime_height_zero]
+
+lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by
+  by_contra x
+  rw [Ring.not_isField_iff_exists_prime] at x
+  obtain ⟨P, ⟨h1, primeP⟩⟩ := x
+  let P' : PrimeSpectrum D := PrimeSpectrum.mk P primeP
+  have h2 : P' ≠ ⊥ := by
+    by_contra a
+    have : P = ⊥ := by rwa [PrimeSpectrum.ext_iff] at a
+    contradiction
+  have pos_height : ¬ (height P') ≤ 0  := by
+    have : ⊥ ∈ {J | J < P'} := Ne.bot_lt h2
+    have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this
+    unfold height
+    rw [←Set.one_le_chainHeight_iff] at this
+    exact not_le_of_gt (Iff.mp ENat.one_le_iff_pos this)
+  have nonpos_height : height P' ≤ 0 := by
+    have := height_le_krullDim P'
+    rw [h] at this
+    aesop
+  contradiction
+
+lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
+  constructor
+  · exact isField.dim_zero
+  · intro fieldD
+    let h : Field D := IsField.toField fieldD
+    exact dim_field_eq_zero
 
 #check Ring.DimensionLEOne
 lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry

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

CommAlg/sayantan(dim_eq_zero_iff_field).lean

@@ -68,7 +68,7 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0)
     have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this
     rw [←Set.one_le_chainHeight_iff] at this
     exact not_le_of_gt (Iff.mp ENat.one_le_iff_pos this)
-  have zero_height : (Set.chainHeight {J | J < P'}) ≤ 0 := by
+  have nonpos_height : (Set.chainHeight {J | J < P'}) ≤ 0 := by
     have : (⨆ (I : PrimeSpectrum D), (Set.chainHeight {J | J < I} : WithBot ℕ∞)) ≤ 0 := h.le
     rw [iSup_le_iff] at this
     exact Iff.mp WithBot.coe_le_zero (this P')