From 5bbb84f5f1eb52e30d6c67fa60dc4577e4f3ee05 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Fri, 9 Jun 2023 17:40:22 -0700 Subject: [PATCH 1/9] Give it a try --- CommAlg.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/CommAlg.lean b/CommAlg.lean index e99d3a6..cef13f8 100644 --- a/CommAlg.lean +++ b/CommAlg.lean @@ -1 +1,4 @@ -def hello := "world" \ No newline at end of file +import Mathlib.Tactic +def hello := "world" + +-- Thank Grant for setting this up. \ No newline at end of file From 094826ab4259ac0f566697174e0f7c71703d19d9 Mon Sep 17 00:00:00 2001 From: monula95 <135654233+monula95@users.noreply.github.com> Date: Sat, 10 Jun 2023 10:18:47 -0700 Subject: [PATCH 2/9] Update README.md --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 9fe7965..1d265b5 100644 --- a/README.md +++ b/README.md @@ -29,3 +29,5 @@ 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 + +Definition of a graded ring From 36fbac8502a95e9e3694805c77daf8414256d3c9 Mon Sep 17 00:00:00 2001 From: Monalisa Dutta <135654233+monula95@users.noreply.github.com> Date: Sat, 10 Jun 2023 10:27:04 -0700 Subject: [PATCH 3/9] Update README.md --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 1d265b5..b7d24b8 100644 --- a/README.md +++ b/README.md @@ -31,3 +31,5 @@ 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 Definition of a graded ring + +Definition of a graded module From 56880e2c266568cfc31a2821702c5cb3ea30870b Mon Sep 17 00:00:00 2001 From: Monalisa Dutta <135654233+monula95@users.noreply.github.com> Date: Sat, 10 Jun 2023 11:48:40 -0700 Subject: [PATCH 4/9] Update README.md --- README.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/README.md b/README.md index b7d24b8..c3f58ab 100644 --- a/README.md +++ b/README.md @@ -30,6 +30,4 @@ 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 -Definition of a graded ring - Definition of a graded module From 223660606bcd4f57d19b7ad87ba3a98a3bc63da6 Mon Sep 17 00:00:00 2001 From: GTBarkley <67718465+GTBarkley@users.noreply.github.com> Date: Sat, 10 Jun 2023 15:21:22 -0400 Subject: [PATCH 5/9] added bullets and the definition of an ideal from mathlib --- README.md | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 9fe7965..25599bc 100644 --- a/README.md +++ b/README.md @@ -6,19 +6,22 @@ We start the commutative algebra project with a list of important definitions an 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 +- Definitions of an ideal, prime ideal, and maximal ideal: +```lean +def Mathlib.RingTheory.Ideal.Basic.Ideal (R : Type u) [Semiring R] := Submodule R R +``` -Definition of a Spec of a ring +- Definition of a Spec of a ring -Definition of a Noetherian and Artinian rings +- Definition of a Noetherian and Artinian rings -Definitions of a local ring and quotient ring +- Definitions of a local ring and quotient ring -Definition of the chain of prime ideals and the length of these chains +- 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) +- Definition of the Krull dimension (supremum of the lengh of chain of prime ideal) -Definition of the height of prime ideal (dimension of A_p) +- Definition of the height of prime ideal (dimension of A_p) Give Examples of each of the above cases for a particular instances of ring From c95b28d69cacbf61ac8307b9ff656113bd615d43 Mon Sep 17 00:00:00 2001 From: GTBarkley <67718465+GTBarkley@users.noreply.github.com> Date: Sat, 10 Jun 2023 18:19:33 -0400 Subject: [PATCH 6/9] add more mathlib refs to readme --- README.md | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 6a76379..d3e6216 100644 --- a/README.md +++ b/README.md @@ -11,21 +11,28 @@ Feel free to add, modify, and expand this file. Below are starting points for th def Mathlib.RingTheory.Ideal.Basic.Ideal (R : Type u) [Semiring R] := Submodule R R ``` -- Definition of a Spec of a ring +- Definition of a Spec of a ring: `Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic.PrimeSpectrum` -- Definition of a Noetherian and Artinian rings +- Definition of a Noetherian and Artinian rings: +```lean +class Mathlib.RingTheory.Noetherian.IsNoetherian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop +``` - Definitions of a local ring and quotient ring - 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) +- Definition of the Krull dimension (supremum of the lengh of chain of prime ideal): `Mathlib.Order.KrullDimension.krullDim` + +- Definition of the height of prime ideal (dimension of A_p): `Mathlib.Order.KrullDimension.height` -- Definition of the height of prime ideal (dimension of A_p) Give Examples of each of the above cases for a particular instances of ring -Theorem 0: Hilbert Basis Theorem +Theorem 0: Hilbert Basis Theorem: +```lean +instance isNoetherianRing [Finite σ] [IsNoetherianRing R] : IsNoetherianRing (MvPolynomial σ R) +``` Theorem 1: If A is a nonzero ring, then dim A[t] >= dim A +1 From 9a08a5927441d3c59831b1a5e07629b68a51f782 Mon Sep 17 00:00:00 2001 From: GTBarkley <67718465+GTBarkley@users.noreply.github.com> Date: Sat, 10 Jun 2023 18:40:48 -0400 Subject: [PATCH 7/9] added more references to readme --- README.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index d3e6216..058a6e8 100644 --- a/README.md +++ b/README.md @@ -9,6 +9,8 @@ Feel free to add, modify, and expand this file. Below are starting points for th - 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` @@ -31,7 +33,7 @@ Give Examples of each of the above cases for a particular instances of ring Theorem 0: Hilbert Basis Theorem: ```lean -instance isNoetherianRing [Finite σ] [IsNoetherianRing R] : IsNoetherianRing (MvPolynomial σ R) +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 From 506fd9b4d6591a7f26143f7ed2355f1e64c07a4b Mon Sep 17 00:00:00 2001 From: GTBarkley <67718465+GTBarkley@users.noreply.github.com> Date: Sat, 10 Jun 2023 18:53:44 -0400 Subject: [PATCH 8/9] added more references to mathlib to readme --- README.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 058a6e8..3c5bba6 100644 --- a/README.md +++ b/README.md @@ -18,9 +18,14 @@ class IsMaximal (I : Ideal α) : Prop - 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 +- 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 From c2a362500f33980d5d83de3386e3d5f420199461 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Sat, 10 Jun 2023 16:09:51 -0700 Subject: [PATCH 9/9] 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