Merge branch 'main' into jayden

.gitignore

@@ -1,3 +1,4 @@
 /build
 /lake-packages/*
 .DS_Store
+.cache/

CommAlg/grant.lean

@@ -2,6 +2,7 @@ import Mathlib.Order.KrullDimension
 import Mathlib.Order.JordanHolder
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import Mathlib.Order.Height
+import CommAlg.krull
 
 
 #check (p q : PrimeSpectrum _) → (p ≤ q)
@@ -39,22 +40,14 @@ lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop
   -- norm_cast
   sorry
 
-namespace Ideal
-noncomputable def krullDim (R : Type _) [CommRing R] := 
-  Set.chainHeight (Set.univ : Set (PrimeSpectrum R))
-
-def krullDimGE (R : Type _) [CommRing R] (n : ℕ) :=
-  ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1
-
-def krullDimLE (R : Type _) [CommRing R] (n : ℕ) :=
-  ∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1
-
-end Ideal
-
 open Ideal
 
-lemma krullDim_le (R : Type _) [CommRing R] : krullDimLE R n ↔ Ideal.krullDim R ≤ n := sorry
-lemma krullDim_ge (R : Type _) [CommRing R] : krullDimGE R n ↔ Ideal.krullDim R ≥ n := sorry
+lemma krullDim_le_iff' (R : Type _) [CommRing R] : 
+  Ideal.krullDim R ≤ n ↔ (∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1) := by
+    sorry
+
+lemma krullDim_ge_iff' (R : Type _) [CommRing R] : 
+  Ideal.krullDim R ≥ n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 := sorry
 
 
 -- #check ((4 : ℕ∞) : WithBot (WithTop ℕ))

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

@@ -5,6 +5,7 @@ import Mathlib.Order.KrullDimension
 import Mathlib.RingTheory.Artinian
 import Mathlib.RingTheory.Ideal.Quotient
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal
 import Mathlib.Data.Finite.Defs
 
@@ -26,6 +27,18 @@ 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 
+
+
+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
@@ -57,4 +70,10 @@ 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 
+
+
+
+
 

CommAlg/krull.lean

@@ -1,4 +1,5 @@
-import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.RingTheory.FiniteType
 import Mathlib.Order.Height
 import Mathlib.RingTheory.PrincipalIdealDomain
 import Mathlib.RingTheory.DedekindDomain.Basic
@@ -18,6 +19,7 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic
 -/
 
 namespace Ideal
+open LocalRing
 
 variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
 
@@ -31,13 +33,37 @@ lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpe
 
 noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice
 
-lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) :
-  iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) ≤ n ↔
-  ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := by
-    convert @iSup_le_iff (WithBot ℕ∞) (PrimeSpectrum R) inferInstance _ (↑n)
+lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := by
+  apply Set.chainHeight_mono
+  intro J' hJ'
+  show J' < J
+  exact lt_of_lt_of_le hJ' I_le_J
 
+lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) :
+  krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞)
+
+lemma krullDim_le_iff' (R : Type) [CommRing R] (n : ℕ∞) :
+  krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞)
+
+@[simp]
+lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R := 
+  le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I
+
+lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := by
+  apply le_antisymm
+  . rw [krullDim_le_iff']
+    intro I
+    apply WithBot.coe_mono
+    apply height_le_of_le
+    apply le_maximalIdeal
+    exact I.2.1
+  . simp
+
+#check height_le_krullDim
 --some propositions that would be nice to be able to eventually
 
+lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := sorry
+
 lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry
 
 #check Ring.DimensionLEOne

CommAlg/resources.lean

@@ -7,6 +7,7 @@ useful lemmas and definitions
 import Mathlib.RingTheory.Ideal.Basic
 import Mathlib.RingTheory.Noetherian
 import Mathlib.RingTheory.Artinian
+import Mathlib.RingTheory.FiniteType
 import Mathlib.Order.Height
 import Mathlib.RingTheory.MvPolynomial.Basic
 import Mathlib.RingTheory.Ideal.Over
@@ -59,6 +60,11 @@ variable (I : Ideal R)
 --Theorems relating primes of a ring to primes of a quotient
 #check PrimeSpectrum.range_comap_of_surjective
 
+--There's a lot of theorems about finite-type algebras
+#check Algebra.FiniteType.polynomial
+#check Algebra.FiniteType.mvPolynomial
+#check Algebra.FiniteType.of_surjective
+
 -- There is a notion of short exact sequences but the number of theorems are lacking
 -- For example, I couldn't find anything saying that for a ses 0 -> A -> B -> C -> 0
 -- of R-modules, A and C being FG implies that B is FG

CommAlg/sameer(artinian-rings).lean

@@ -0,0 +1,15 @@
+import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.Noetherian
+import Mathlib.RingTheory.Artinian
+import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+
+lemma quotientRing_is_Artinian (R : Type _) [CommRing R] (I : Ideal R) (IsArt : IsArtinianRing R): 
+IsArtinianRing (R⧸I) := by sorry
+
+#check Ideal.IsPrime
+
+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