From b0b3bdceb390c0abc77a121e3e4d92db3a2c3d9a Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Sat, 10 Jun 2023 06:58:23 -0700 Subject: [PATCH 1/5] removed unnecessary file --- CommAlg.lean | 1 - 1 file changed, 1 deletion(-) delete mode 100644 CommAlg.lean diff --git a/CommAlg.lean b/CommAlg.lean deleted file mode 100644 index e99d3a6..0000000 --- a/CommAlg.lean +++ /dev/null @@ -1 +0,0 @@ -def hello := "world" \ No newline at end of file From 97d219fe2162cf2c1d08aa7d5fa65364a8768f8b Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Sat, 10 Jun 2023 07:27:37 -0700 Subject: [PATCH 2/5] added resources file to dump useful links --- comm_alg/resources.lean | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 comm_alg/resources.lean diff --git a/comm_alg/resources.lean b/comm_alg/resources.lean new file mode 100644 index 0000000..feb671a --- /dev/null +++ b/comm_alg/resources.lean @@ -0,0 +1,40 @@ +/- +We don't want to reinvent the wheel, but finding +things in Mathlib can be pretty annoying. This is +a temporary file intended to be a dumping ground for +useful lemmas and definitions +-/ +import Mathlib.RingTheory.Ideal.Basic +import Mathlib.RingTheory.Noetherian +import Mathlib.RingTheory.Artinian +import Mathlib.Order.Height + +variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M] + +--ideals are defined +#check Ideal R + +variable (I : Ideal R) + +--as are prime and maximal (they are defined as typeclasses) +#check (I.IsPrime) +#check (I.IsMaximal) + +--a module being Noetherian is also a class +#check IsNoetherian M +#check IsNoetherian I + +--a ring is Noetherian if it is Noetherian as a module over itself +#check IsNoetherianRing R + +--ditto for Artinian +#check IsArtinian M +#check IsArtinianRing R + +--I can't find the theorem that an Artinian ring is noetherian. That could be a good +--thing to add at some point + + + +--Here's the main defintion that will be helpful +#check Set.chainHeight \ No newline at end of file From 1fd4e29c875d0640d120ab17b9e97e753e878128 Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Sat, 10 Jun 2023 08:13:10 -0700 Subject: [PATCH 3/5] added statements of lemmas we'd like to prove --- comm_alg/krull.lean | 44 +++++++++++++++++++++++++++++++++++++++++ comm_alg/resources.lean | 9 ++++++++- 2 files changed, 52 insertions(+), 1 deletion(-) create mode 100644 comm_alg/krull.lean diff --git a/comm_alg/krull.lean b/comm_alg/krull.lean new file mode 100644 index 0000000..2a5af42 --- /dev/null +++ b/comm_alg/krull.lean @@ -0,0 +1,44 @@ +import Mathlib.RingTheory.Ideal.Basic +import Mathlib.Order.Height +import Mathlib.RingTheory.PrincipalIdealDomain +import Mathlib.RingTheory.DedekindDomain.Basic +import Mathlib.RingTheory.Ideal.Quotient +import Mathlib.RingTheory.Localization.AtPrime + +/- This file contains the definitions of height of an ideal, and the krull + dimension of a commutative ring. + There are also sorried statements of many of the theorems that would be + really nice to prove. + I'm imagining for this file to ultimately contain basic API for height and + krull dimension, and the theorems will probably end up other files, + depending on how long the proofs are, and what extra API needs to be + developed. +-/ + +variable {R : Type _} [CommRing R] (I : Ideal R) + +namespace ideal + +noncomputable def height : ℕ∞ := Set.chainHeight {J | J ≤ I ∧ J.IsPrime} + +noncomputable def krull_dim (R : Type _) [CommRing R] := height (⊤ : Ideal R) + +--some propositions that would be nice to be able to eventually + +lemma dim_eq_zero_iff_field : krull_dim R = 0 ↔ IsField R := sorry + +#check Ring.DimensionLEOne +lemma dim_le_one_iff : krull_dim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry + +lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krull_dim R ≤ 1 := sorry + +lemma dim_le_dim_polynomial_add_one [Nontrivial R] : + krull_dim R ≤ krull_dim (Polynomial R) + 1 := sorry + +lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : + krull_dim R = krull_dim (Polynomial R) + 1 := sorry + +lemma height_eq_dim_localization [Ideal.IsPrime I] : + height I = krull_dim (Localization.AtPrime I) := sorry + +lemma height_add_dim_quotient_le_dim : height I + krull_dim (R ⧸ I) ≤ krull_dim R := sorry \ No newline at end of file diff --git a/comm_alg/resources.lean b/comm_alg/resources.lean index feb671a..eae7c89 100644 --- a/comm_alg/resources.lean +++ b/comm_alg/resources.lean @@ -8,6 +8,7 @@ import Mathlib.RingTheory.Ideal.Basic import Mathlib.RingTheory.Noetherian import Mathlib.RingTheory.Artinian import Mathlib.Order.Height +import Mathlib.RingTheory.MvPolynomial.Basic variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M] @@ -37,4 +38,10 @@ variable (I : Ideal R) --Here's the main defintion that will be helpful -#check Set.chainHeight \ No newline at end of file +#check Set.chainHeight + +--this is the polynomial ring R[x] +#check Polynomial R +--this is the polynomial ring with variables indexed by ℕ +#check MvPolynomial ℕ R +--hopefully there's good communication between them \ No newline at end of file From c2a362500f33980d5d83de3386e3d5f420199461 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Sat, 10 Jun 2023 16:09:51 -0700 Subject: [PATCH 4/5] add things to do --- README.md | 54 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 54 insertions(+) create mode 100644 README.md diff --git a/README.md b/README.md new file mode 100644 index 0000000..8ffbe34 --- /dev/null +++ b/README.md @@ -0,0 +1,54 @@ +# Commutative algebra in Lean + +Welcome to the repository for adding definitions and theorems related to Krull dimension and Hilbert polynomials to mathlib. + +We start the commutative algebra project with a list of important definitions and theorems and go from there. + +Feel free to add, modify, and expand this file. Below are starting points for the project: + +- Definitions of an ideal, prime ideal, and maximal ideal: +```lean +def Mathlib.RingTheory.Ideal.Basic.Ideal (R : Type u) [Semiring R] := Submodule R R +class Mathlib.RingTheory.Ideal.Basic.IsPrime (I : Ideal α) : Prop +class IsMaximal (I : Ideal α) : Prop +``` + +- Definition of a Spec of a ring: `Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic.PrimeSpectrum` + +- Definition of a Noetherian and Artinian rings: +```lean +class Mathlib.RingTheory.Noetherian.IsNoetherian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop +class Mathlib.RingTheory.Artinian.IsArtinian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop +``` +- Definition of a polynomial ring: `Mathlib.RingTheory.Polynomial.Basic` + +- Definitions of a local ring and quotient ring: `Mathlib.RingTheory.Ideal.Quotient.?` +```lean +class Mathlib.RingTheory.Ideal.LocalRing.LocalRing (R : Type u) [Semiring R] extends Nontrivial R : Prop +``` + +- Definition of the chain of prime ideals and the length of these chains + +- Definition of the Krull dimension (supremum of the lengh of chain of prime ideal): `Mathlib.Order.KrullDimension.krullDim` + +- Krull dimension of a module + +- Definition of the height of prime ideal (dimension of A_p): `Mathlib.Order.KrullDimension.height` + + +Give Examples of each of the above cases for a particular instances of ring + +Theorem 0: Hilbert Basis Theorem: +```lean +theorem Mathlib.RingTheory.Polynomial.Basic.Polynomial.isNoetherianRing [inst : IsNoetherianRing R] : IsNoetherianRing R[X] +``` + +Theorem 1: If A is a nonzero ring, then dim A[t] >= dim A +1 + +Theorem 2: If A is a nonzero noetherian ring, then dim A[t] = dim A + 1 + +Theorem 3: If A is nonzero ring then dim A_p + dim A/p <= dim A + +Lemma 0: A ring is artinian iff it is noetherian of dimension 0. + +Definition of a graded module From 868f098749083d5c870f5e98af8b5205fbdadb90 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Sun, 11 Jun 2023 00:36:27 +0000 Subject: [PATCH 5/5] checked preliminary definition of Krull dimension --- comm_alg/grant.lean | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/comm_alg/grant.lean b/comm_alg/grant.lean index 80e5d39..86c05fc 100644 --- a/comm_alg/grant.lean +++ b/comm_alg/grant.lean @@ -1,6 +1,12 @@ -import Mathlib.Analysis.Seminorm +import Mathlib.Order.KrullDimension +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic def hello : IO Unit := do IO.println "Hello, World!" -#eval hello \ No newline at end of file +#eval hello + +#check (p q : PrimeSpectrum _) → (p ≤ q) +#check Preorder (PrimeSpectrum _) + +#check krullDim (PrimeSpectrum _) \ No newline at end of file