From 48a7a31ec3409cad2f876ed856190170fcb84109 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Sat, 10 Jun 2023 03:13:59 +0000 Subject: [PATCH 01/11] add readme --- Readme.md | 3 +++ comm_alg/grant.lean | 6 ++++++ 2 files changed, 9 insertions(+) create mode 100644 Readme.md create mode 100644 comm_alg/grant.lean diff --git a/Readme.md b/Readme.md new file mode 100644 index 0000000..1522392 --- /dev/null +++ b/Readme.md @@ -0,0 +1,3 @@ +# Commutative algebra in Lean + +Welcome to the repository for definitions and theorems related to Krull dimension and Hilbert polynomials. \ No newline at end of file diff --git a/comm_alg/grant.lean b/comm_alg/grant.lean new file mode 100644 index 0000000..80e5d39 --- /dev/null +++ b/comm_alg/grant.lean @@ -0,0 +1,6 @@ +import Mathlib.Analysis.Seminorm + +def hello : IO Unit := do + IO.println "Hello, World!" + +#eval hello \ No newline at end of file From 3a45dc52d7c6a239261e85d1eb29538b7833e64f Mon Sep 17 00:00:00 2001 From: ssavkar1 <134407735+ssavkar1@users.noreply.github.com> Date: Fri, 9 Jun 2023 20:51:11 -0700 Subject: [PATCH 02/11] Create README.md First draft of the Readme file. It is just a list of things to do but need to be more descriptive. --- README.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 README.md diff --git a/README.md b/README.md new file mode 100644 index 0000000..37c6838 --- /dev/null +++ b/README.md @@ -0,0 +1,18 @@ +# comm_alg +SLMath collaboration for adding Krull dimension and Hilbert polynomial to mathlib + +We start the comm algebra project by important definitions and theorems and go from there. +Feel free to add, modify, and expand this file. Below are starting point for the project: + +Definitions of an ideal, prime ideal, and maximal ideal +Definition of a Spec of a ring +Definition of a Noetherian and Artinian rings +Definition of a local ring and quotient ring +Definition of the Krull dimension + +Give examples of each of the above cases for a particular instances of ring + +Theorem 0: Hilbert Basis Theorem +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 From accf75c663385f11f7ac104e4315b6928d8f7e47 Mon Sep 17 00:00:00 2001 From: ssavkar1 <134407735+ssavkar1@users.noreply.github.com> Date: Fri, 9 Jun 2023 21:05:03 -0700 Subject: [PATCH 03/11] Update README.md Formatted the list to make it readable. --- README.md | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 37c6838..f140359 100644 --- a/README.md +++ b/README.md @@ -2,17 +2,29 @@ SLMath collaboration for adding Krull dimension and Hilbert polynomial to mathlib We start the comm algebra project by important definitions and theorems and go from there. + Feel free to add, modify, and expand this file. Below are starting point for the project: Definitions of an ideal, prime ideal, and maximal ideal -Definition of a Spec of a ring -Definition of a Noetherian and Artinian rings -Definition of a local ring and quotient ring -Definition of the Krull dimension -Give examples of each of the above cases for a particular instances of ring +Definition of a Spec of a ring + +Definition of a Noetherian and Artinian rings + +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 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 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 From d736cf81b3ef94a4961226a0a267a098ecc2096d Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Sat, 10 Jun 2023 04:27:40 +0000 Subject: [PATCH 04/11] merged readme files --- README.md | 9 +++++---- Readme.md | 3 --- 2 files changed, 5 insertions(+), 7 deletions(-) delete mode 100644 Readme.md diff --git a/README.md b/README.md index f140359..9fe7965 100644 --- a/README.md +++ b/README.md @@ -1,9 +1,10 @@ -# comm_alg -SLMath collaboration for adding Krull dimension and Hilbert polynomial to mathlib +# Commutative algebra in Lean -We start the comm algebra project by important definitions and theorems and go from there. +Welcome to the repository for adding definitions and theorems related to Krull dimension and Hilbert polynomials to mathlib. -Feel free to add, modify, and expand this file. Below are starting point for the project: +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 diff --git a/Readme.md b/Readme.md deleted file mode 100644 index 1522392..0000000 --- a/Readme.md +++ /dev/null @@ -1,3 +0,0 @@ -# Commutative algebra in Lean - -Welcome to the repository for definitions and theorems related to Krull dimension and Hilbert polynomials. \ 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 05/11] 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 06/11] 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 07/11] 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 08/11] 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 09/11] 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 10/11] 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 11/11] 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