Merge branch 'GTBarkley:main' into main

CommAlg/grant.lean

@@ -17,6 +17,8 @@ import CommAlg.krull
 #check JordanHolderLattice
 
 
+section Chains
+
 variable {α : Type _} [Preorder α] (s : Set α)
 
 def finFun_to_list {n : ℕ} : (Fin n → α) → List α := by sorry
@@ -26,7 +28,6 @@ def series_to_chain : StrictSeries s → s.subchain
     ⟨ finFun_to_list (fun x => toFun x),
       sorry⟩
 
-
 -- there should be a coercion from WithTop ℕ to WithBot (WithTop ℕ) but it doesn't seem to work
 -- it looks like this might be because someone changed the instance from CoeCT to Coe during the port
 -- actually it looks like we can coerce to WithBot (ℕ∞) fine
@@ -40,15 +41,62 @@ lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop
   -- norm_cast
   sorry
 
+end Chains
+
+section Krull
+
+variable (R : Type _) [CommRing R] (M : Type _) [AddCommGroup M] [Module R M]
+
 open Ideal
 
-lemma krullDim_le_iff' (R : Type _) [CommRing R] : 
+-- chain of primes 
+#check height 
+
+-- lemma height_ge_iff {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
+--   height 𝔭 ≥ n ↔ := sorry
+
+lemma height_ge_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
+height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
+  rcases n with _ | n
+  . constructor <;> intro h <;> exfalso
+    . exact (not_le.mpr h) le_top
+    . -- change ∃c, _ ∧ _ ∧ ((List.length c : ℕ∞) = ⊤ + 1) at h
+      -- rw [WithTop.top_add] at h
+      tauto
+  have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by
+    symm
+    show (n + 1 ≤ m ↔ _ )
+    apply ENat.add_one_le_iff
+    exact ENat.coe_ne_top _
+  rw [this]
+  unfold Ideal.height
+  show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞))
+  rw [{J | J < 𝔭}.le_chainHeight_iff]
+  show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
+  have h := fun (c : List (PrimeSpectrum R)) => (@WithTop.coe_eq_coe _ (List.length c) n) 
+  constructor <;> rintro ⟨c, hc⟩ <;> use c --<;> tauto--<;> exact ⟨hc.1, by tauto⟩
+  . --rw [and_assoc]
+    -- show _ ∧ _ ∧ _
+    --exact ⟨hc.1, _⟩
+    tauto
+  . change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc
+    norm_cast at hc
+    tauto
+
+lemma krullDim_le_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : 
   Ideal.krullDim R ≤ n ↔ (∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1) := by
     sorry
 
-lemma krullDim_ge_iff' (R : Type _) [CommRing R] : 
+lemma krullDim_ge_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : 
   Ideal.krullDim R ≥ n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 := sorry
 
-
+#check (sorry : False)
+#check (sorryAx)
+#check (4 : WithBot ℕ∞)
+#check List.sum
 -- #check ((4 : ℕ∞) : WithBot (WithTop ℕ))
-#check ( (Set.chainHeight s) : WithBot (ℕ∞))
+-- #check ( (Set.chainHeight s) : WithBot (ℕ∞))
+
+variable (P : PrimeSpectrum R)
+
+#check {J | J < P}.le_chainHeight_iff (n := 4)

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

@@ -4,15 +4,16 @@ 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
+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
@@ -26,21 +27,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
@@ -48,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
@@ -58,9 +48,42 @@ 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)) → 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
 
@@ -70,8 +93,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