From 6b46181b725d6ecfcc602df3f7ebf6242fa48c5a Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Mon, 12 Jun 2023 10:22:57 -0700 Subject: [PATCH 1/8] found a bunch of good finite-type algebra lemmas --- comm_alg/resources.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/comm_alg/resources.lean b/comm_alg/resources.lean index bb30ae3..2d5d227 100644 --- a/comm_alg/resources.lean +++ b/comm_alg/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 From 8e7ddca721f0f3eb6eca2eb47ac6434ef9328e06 Mon Sep 17 00:00:00 2001 From: Sameer Savkar Date: Mon, 12 Jun 2023 10:34:51 -0700 Subject: [PATCH 2/8] created a new file --- .gitignore | 3 ++- comm_alg/sameer(artinian-rings).lean | 11 +++++++++++ 2 files changed, 13 insertions(+), 1 deletion(-) create mode 100644 comm_alg/sameer(artinian-rings).lean diff --git a/.gitignore b/.gitignore index e254e15..c666579 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ /build /lake-packages/* -.DS_Store \ No newline at end of file +.DS_Store +.cache/ \ No newline at end of file diff --git a/comm_alg/sameer(artinian-rings).lean b/comm_alg/sameer(artinian-rings).lean new file mode 100644 index 0000000..aae0fd7 --- /dev/null +++ b/comm_alg/sameer(artinian-rings).lean @@ -0,0 +1,11 @@ +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 _) (isArtinianRing R) (Ideal I) : IsArtinianRing R := by sorry + +lemma IsPrimeisMaximal (R : Type_) (isArtinianRing R) (Ideal I) : IsPrimeisMaximal R := by sorry + +-- Use Stacks project proof since it's broken into lemmas From 64070acb5c64b3c73b89ef6ae9a3bcc72c2779d9 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Mon, 12 Jun 2023 17:47:09 +0000 Subject: [PATCH 3/8] renamed comm_alg folder so imports work --- {comm_alg => CommAlg}/grant.lean | 0 {comm_alg => CommAlg}/jayden(krull-dim-zero).lean | 0 {comm_alg => CommAlg}/krull.lean | 0 {comm_alg => CommAlg}/resources.lean | 0 4 files changed, 0 insertions(+), 0 deletions(-) rename {comm_alg => CommAlg}/grant.lean (100%) rename {comm_alg => CommAlg}/jayden(krull-dim-zero).lean (100%) rename {comm_alg => CommAlg}/krull.lean (100%) rename {comm_alg => CommAlg}/resources.lean (100%) diff --git a/comm_alg/grant.lean b/CommAlg/grant.lean similarity index 100% rename from comm_alg/grant.lean rename to CommAlg/grant.lean diff --git a/comm_alg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean similarity index 100% rename from comm_alg/jayden(krull-dim-zero).lean rename to CommAlg/jayden(krull-dim-zero).lean diff --git a/comm_alg/krull.lean b/CommAlg/krull.lean similarity index 100% rename from comm_alg/krull.lean rename to CommAlg/krull.lean diff --git a/comm_alg/resources.lean b/CommAlg/resources.lean similarity index 100% rename from comm_alg/resources.lean rename to CommAlg/resources.lean From cdf8cc5e99c3c7f844f6fd874223622d9ecf545e Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Mon, 12 Jun 2023 18:02:03 +0000 Subject: [PATCH 4/8] stated some equivalences for bounding krull dim --- CommAlg/grant.lean | 21 +++++++-------------- 1 file changed, 7 insertions(+), 14 deletions(-) diff --git a/CommAlg/grant.lean b/CommAlg/grant.lean index 8586fa3..2f3c634 100644 --- a/CommAlg/grant.lean +++ b/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 ℕ)) From fd5bd05f0109488dd5eb4d4c85c957654c01d41b Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Mon, 12 Jun 2023 13:03:35 -0700 Subject: [PATCH 5/8] golf, added dim_eq_bot_iff --- CommAlg/krull.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 1bd2829..228f0b1 100644 --- a/CommAlg/krull.lean +++ b/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 @@ -33,11 +34,12 @@ noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.c 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) + ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞) --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 From cbb0c6ce7af913b76cccb7462528aa8d071cc0c5 Mon Sep 17 00:00:00 2001 From: Sameer Savkar Date: Mon, 12 Jun 2023 13:34:09 -0700 Subject: [PATCH 6/8] Defining lemmas --- comm_alg/sameer(artinian-rings).lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/comm_alg/sameer(artinian-rings).lean b/comm_alg/sameer(artinian-rings).lean index aae0fd7..381680b 100644 --- a/comm_alg/sameer(artinian-rings).lean +++ b/comm_alg/sameer(artinian-rings).lean @@ -4,8 +4,12 @@ import Mathlib.RingTheory.Artinian import Mathlib.RingTheory.Ideal.Quotient import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic -lemma quotientRing_is_Artinian (R : Type _) (isArtinianRing R) (Ideal I) : IsArtinianRing R := by sorry +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 -lemma IsPrimeisMaximal (R : Type_) (isArtinianRing R) (Ideal I) : IsPrimeisMaximal R := by sorry -- Use Stacks project proof since it's broken into lemmas From 2ae8926e4c8500205bf476374f05f707e07bfe85 Mon Sep 17 00:00:00 2001 From: Sameer Savkar Date: Mon, 12 Jun 2023 13:38:26 -0700 Subject: [PATCH 7/8] Moved files --- {comm_alg => CommAlg}/sameer(artinian-rings).lean | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename {comm_alg => CommAlg}/sameer(artinian-rings).lean (100%) diff --git a/comm_alg/sameer(artinian-rings).lean b/CommAlg/sameer(artinian-rings).lean similarity index 100% rename from comm_alg/sameer(artinian-rings).lean rename to CommAlg/sameer(artinian-rings).lean From 8b2be97b5a4f597de327d00598bfafc20c9504a1 Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Mon, 12 Jun 2023 14:27:09 -0700 Subject: [PATCH 8/8] added some lemmas --- CommAlg/krull.lean | 30 +++++++++++++++++++++++++++--- 1 file changed, 27 insertions(+), 3 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 228f0b1..9b4c785 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -19,6 +19,7 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic -/ namespace Ideal +open LocalRing variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) @@ -32,10 +33,33 @@ 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 := iSup_le_iff (α := WithBot ℕ∞) +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