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

CommAlg/jayden(krull-dim-zero).lean

@@ -15,6 +15,9 @@ import Mathlib.RingTheory.Localization.AtPrime
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Algebra.Ring.Pi
 import Mathlib.RingTheory.Finiteness
+import Mathlib.Util.PiNotation
+
+open PiNotation
 
 
 namespace Ideal
@@ -26,6 +29,8 @@ noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J <
 noncomputable def krullDim (R : Type) [CommRing R] :
      WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height R I
 
+--variable {R}
+
 -- 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
@@ -33,7 +38,7 @@ noncomputable def krullDim (R : Type) [CommRing R] :
 
 -- Stacks Definition 10.32.1: An ideal is locally nilpotent
 -- if every element is nilpotent
-class IsLocallyNilpotent (I : Ideal R) : Prop :=
+class IsLocallyNilpotent {R : Type _} [CommRing R] (I : Ideal R) : Prop :=
     h : ∀ x ∈ I, IsNilpotent x
 #check Ideal.IsLocallyNilpotent
 end Ideal
@@ -89,6 +94,10 @@ lemma containment_radical_power_containment :
 -- Ideal.exists_pow_le_of_le_radical_of_fG
 
 
+-- Stacks Lemma 10.52.5: R → S is a ring map.  M is an S-mod. 
+-- Then length_R M ≥ length_S M. 
+-- Stacks Lemma 10.52.5': equality holds if R → S is surjective.
+
 -- Stacks Lemma 10.52.6: I is a maximal ideal and IM = 0. Then length of M is
 -- the same as the dimension as a vector space over R/I,
 lemma length_eq_dim_if_maximal_annihilates {I : Ideal R} [Ideal.IsMaximal I] 
@@ -96,48 +105,53 @@ lemma length_eq_dim_if_maximal_annihilates {I : Ideal R} [Ideal.IsMaximal I]
      → Module.length R M = Module.rank R⧸I M⧸(I • (⊤ : Submodule R M)) := by sorry
 
 -- Does lean know that M/IM is a R/I module?
+-- Use 10.52.5
 
 -- 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⟩
+lemma power_zero_finite_length [Ideal.IsMaximal I] (h₁ : Ideal.FG I) [Module.Finite R M]
+    (h₂ : (∃ n : ℕ, (I ^ n) • (⊤ : Submodule R M) = 0)) :
+     (∃ m : ℕ, Module.length R M ≤ m) := by sorry
+    -- 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
+lemma Artinian_has_finite_max_ideal 
+    [IsArtinianRing R] : Finite (MaximalSpectrum R) := by 
+    by_contra infinite
+    simp only [not_finite_iff_infinite] at infinite
+    
 
 -- 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
+lemma Jacobson_of_Artinian_is_nilpotent 
+    [IsArtinianRing R] : IsNilpotent (Ideal.jacobson (⊥ : Ideal R)) := by 
+    have J := Ideal.jacobson (⊥ : Ideal R)
+    
 
 -- 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
+abbrev Prod_of_localization :=
+  Π I : MaximalSpectrum R, Localization.AtPrime I.1
 
--- lemma product_of_localization_at_maximal_ideal : Finite (MaximalSpectrum R)
---      ∧ 
+-- instance : CommRing (Prod_of_localization R) := by
+--   unfold Prod_of_localization
+--   infer_instance
      
-def jaydensRing : Type _ := sorry
-  -- ∀ I : MaximalSpectrum R, Localization.AtPrime R I
+def foo : Prod_of_localization R →+* R where
+  toFun := sorry
+  invFun := sorry
+  left_inv := sorry
+  right_inv := sorry
+  map_mul' := sorry
+  map_add' := sorry
 
-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.
+def product_of_localization_at_maximal_ideal [Finite (MaximalSpectrum R)]
+    (h : Ideal.IsLocallyNilpotent (Ideal.jacobson (⊥ : Ideal R))) :
+    Prod_of_localization R ≃+* 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 : 
@@ -148,8 +162,8 @@ 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 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
 

CommAlg/krull.lean

@@ -63,7 +63,7 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) :=
     apply height_le_of_le
     apply le_maximalIdeal
     exact I.2.1
-  . simp
+  . simp only [height_le_krullDim]
 
 #check height_le_krullDim
 --some propositions that would be nice to be able to eventually
@@ -135,7 +135,7 @@ 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
+lemma domain_dim_zero.isField {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
@@ -156,9 +156,9 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0)
     aesop
   contradiction
 
-lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
+lemma domain_dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
   constructor
-  · exact isField.dim_zero
+  · exact domain_dim_zero.isField
   · intro fieldD
     let h : Field D := IsField.toField fieldD
     exact dim_field_eq_zero
@@ -226,7 +226,11 @@ lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
 lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
   krullDim R + 1 = krullDim (Polynomial R) := sorry
 
+lemma dim_mvPolynomial [Field K] (n : ℕ) : krullDim (MvPolynomial (Fin n) K) = n := sorry
+
 lemma height_eq_dim_localization :
   height I = krullDim (Localization.AtPrime I.asIdeal) := sorry
 
+lemma dim_quotient_le_dim : height I + krullDim (R ⧸ I.asIdeal) ≤ krullDim R := sorry
+
 lemma height_add_dim_quotient_le_dim : height I + krullDim (R ⧸ I.asIdeal) ≤ krullDim R := sorry

CommAlg/sameer(artinian-rings).lean

@@ -6,7 +6,9 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import Mathlib.RingTheory.DedekindDomain.DVR
 
 
-lemma FieldisArtinian (R : Type _) [CommRing R] (IsField : ):= by sorry
+lemma FieldisArtinian (R : Type _) [CommRing R] (h: IsField R) : 
+  IsArtinianRing R := by sorry
+
 
 
 lemma ArtinianDomainIsField (R : Type _) [CommRing R] [IsDomain R]
@@ -47,8 +49,7 @@ lemma isArtinianRing_of_quotient_of_artinian (R : Type _) [CommRing R]
 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 
+-- if R is Artinian and P is prime then R/P is Artinian Domain 
 -- R⧸P is a field by the above lemma
 -- P is maximal
 
@@ -56,13 +57,13 @@ by
   have artRP : IsArtinianRing (R⧸P) := by
     exact isArtinianRing_of_quotient_of_artinian R P IsArt
   
+  have artRPField : IsField (R⧸P) := by
+    exact ArtinianDomainIsField (R⧸P) artRP
+  
+  have h := Ideal.Quotient.maximal_of_isField P artRPField
+  exact h
   
 -- Then R/I is Artinian 
  --  have' : IsArtinianRing R ∧ Ideal.IsPrime I → IsDomain (R⧸I) := by
 
 -- R⧸I.IsArtinian → monotone_stabilizes_iff_artinian.R⧸I
-
-
-
-
--- Use Stacks project proof since it's broken into lemmas

CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean

@@ -22,11 +22,7 @@ noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.c
 lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
   krullDim R + 1 ≤ krullDim (Polynomial R) := sorry -- Others are working on it
 
--- private lemma sum_succ_of_succ_sum {ι : Type} (a : ℕ∞) [inst : Nonempty ι] :
---       (⨆ (x : ι), a + 1) = (⨆ (x : ι), a) + 1 := by
---   have : a + 1 = (⨆ (x : ι), a) + 1 := by rw [ciSup_const]
---   have : a + 1 = (⨆ (x : ι), a + 1) := Eq.symm ciSup_const
---   simp
+lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := sorry -- Already done in main file
 
 lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
   krullDim R + 1 = krullDim (Polynomial R) := by
@@ -37,16 +33,30 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
     have htPBdd : ∀ (P : PrimeSpectrum (Polynomial R)), (height P : WithBot ℕ∞) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by
       intro P
       have : ∃ (I : PrimeSpectrum R), (height P : WithBot ℕ∞) ≤ ↑(height I + 1) := by
+        have : ∃ M, Ideal.IsMaximal M ∧ P.asIdeal ≤ M := by
+          apply exists_le_maximal
+          apply IsPrime.ne_top
+          apply P.IsPrime
+        obtain ⟨M, maxM, PleM⟩ := this
+        let P' : PrimeSpectrum (Polynomial R) := PrimeSpectrum.mk M (IsMaximal.isPrime maxM)
+        have PleP' : P ≤ P' := PleM
+        have : height P ≤ height P' := height_le_of_le PleP'
+        simp only [WithBot.coe_le_coe]
+        have : ∃ (I : PrimeSpectrum R), height P' ≤ height I + 1 := by
+
           sorry
+        obtain ⟨I, h⟩ := this
+        use I
+        exact ge_trans h this
       obtain ⟨I, IP⟩ := this
       have : (↑(height I + 1) : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum R), ↑(height I + 1) := by
         apply @le_iSup (WithBot ℕ∞) _ _ _ I
-      apply ge_trans this IP
+      exact ge_trans this IP
     have oneOut : (⨆ (I : PrimeSpectrum R), (height I : WithBot ℕ∞) + 1) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by
       have : ∀ P : PrimeSpectrum R, (height P : WithBot ℕ∞) + 1 ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 :=
         fun P ↦ (by apply add_le_add_right (@le_iSup (WithBot ℕ∞) _ _ _ P) 1)
       apply iSup_le
       apply this
-    simp
+    simp only [iSup_le_iff]
     intro P
     exact ge_trans oneOut (htPBdd P)