From 5bbb84f5f1eb52e30d6c67fa60dc4577e4f3ee05 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Fri, 9 Jun 2023 17:40:22 -0700 Subject: [PATCH 01/80] 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 48a7a31ec3409cad2f876ed856190170fcb84109 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Sat, 10 Jun 2023 03:13:59 +0000 Subject: [PATCH 02/80] 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 03/80] 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 04/80] 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 05/80] 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 b0b3bdceb390c0abc77a121e3e4d92db3a2c3d9a Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Sat, 10 Jun 2023 06:58:23 -0700 Subject: [PATCH 06/80] 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 07/80] 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 08/80] 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 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 09/80] 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 10/80] 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 11/80] 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 12/80] 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 13/80] 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 14/80] 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 15/80] 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 16/80] 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 17/80] 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 From 193afadecba936cb17e63196d69676ba4d9f5cbe Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Sat, 10 Jun 2023 20:58:29 -0700 Subject: [PATCH 18/80] add things in gitignore --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 20c60d7..e254e15 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ /build /lake-packages/* +.DS_Store \ No newline at end of file From d0071924df883d186c0b805e6b9007656d9f36f5 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Sat, 10 Jun 2023 21:04:25 -0700 Subject: [PATCH 19/80] add stuff --- .DS_Store | Bin 0 -> 6148 bytes 1 file changed, 0 insertions(+), 0 deletions(-) create mode 100644 .DS_Store diff --git a/.DS_Store b/.DS_Store new file mode 100644 index 0000000000000000000000000000000000000000..6d98085373769dd4c6eebf58c63f4db066814689 GIT binary patch literal 6148 zcmeHKyH3ME5S%3`EYYM)dB4CPoTBgrd_V$;L}TOv(YxZi_%vo81(Bf(O*Cum&E4M4 zS)St73&3_C=LcW|V4yqV(}$(`zWc)NDq=)B&p6;2BVNz%r*V<}d%(E^PMGk<=Li2~ znnvH0NdYM!1*Cu!kOEg#pvvoTf7MfUm=ur#x1fOE4~_2F3+KeRIygiNKwL8%#(DG- z#O48FFPsw@p;=OiNwsP*Ea{B5%Ik%5V$xyNd|18Nszb4OJI`;C4(o{;rGON;RA80M zjo1H2`XBxOB}pqOAO&tp0bB2%_B(!3)z-zwd97{qBi(bp=x&?`g+r8MVw7Vpyc};M cDf61ox!()t#Go@CbfSI+To;)X_-_Ti0jAm&VE_OC literal 0 HcmV?d00001 From 29ed7e50387e618af32faebe3bd5bc2bf08cbd7d Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Sat, 10 Jun 2023 21:10:01 -0700 Subject: [PATCH 20/80] test --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 20c60d7..e254e15 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ /build /lake-packages/* +.DS_Store \ No newline at end of file From 53ce99993ecf4436abfb4b89cec26e068dd846f2 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Sat, 10 Jun 2023 21:10:36 -0700 Subject: [PATCH 21/80] test --- test.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 test.md diff --git a/test.md b/test.md new file mode 100644 index 0000000..af2a4c4 --- /dev/null +++ b/test.md @@ -0,0 +1 @@ +Just checking out \ No newline at end of file From 8c0b286765ec910ae7c25acd2149043ab464f8ce Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Sat, 10 Jun 2023 21:26:45 -0700 Subject: [PATCH 22/80] delete test --- test.md | 1 - 1 file changed, 1 deletion(-) delete mode 100644 test.md diff --git a/test.md b/test.md deleted file mode 100644 index af2a4c4..0000000 --- a/test.md +++ /dev/null @@ -1 +0,0 @@ -Just checking out \ No newline at end of file From 8b28694f0e09b0f63c8a6419c34fa4c7a844d132 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Sun, 11 Jun 2023 06:00:13 +0000 Subject: [PATCH 23/80] comparing definitions of height --- comm_alg/grant.lean | 29 ++++++++++++++++++++++++----- 1 file changed, 24 insertions(+), 5 deletions(-) diff --git a/comm_alg/grant.lean b/comm_alg/grant.lean index 86c05fc..2814919 100644 --- a/comm_alg/grant.lean +++ b/comm_alg/grant.lean @@ -1,12 +1,31 @@ import Mathlib.Order.KrullDimension +import Mathlib.Order.JordanHolder import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Order.Height -def hello : IO Unit := do - IO.println "Hello, World!" - -#eval hello #check (p q : PrimeSpectrum _) → (p ≤ q) #check Preorder (PrimeSpectrum _) -#check krullDim (PrimeSpectrum _) \ No newline at end of file +-- Dimension of a ring +#check krullDim (PrimeSpectrum _) + +-- Length of a module +#check krullDim (Submodule _ _) + +#check JordanHolderLattice + + +variable {α : Type _} [Preorder α] (s : Set α) + +-- there should be a coercion from WithTop ℕ to WithBot (WithTop ℕ) but it doesn't seem to work +-- it looks like this might be because someone changed the instance from CoeCT to Coe during the port +lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop ℕ)) = krullDim s := by + intro hs + unfold Set.chainHeight + unfold krullDim + have hKrullSome : ∃n, krullDim s = some n := by + + sorry + -- norm_cast + sorry \ No newline at end of file From e65513322c59ffc53029c17124a6ab692ca82bb3 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Sun, 11 Jun 2023 06:49:28 +0000 Subject: [PATCH 24/80] function relating the offbrand notions of chain --- comm_alg/grant.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/comm_alg/grant.lean b/comm_alg/grant.lean index 2814919..de3e50f 100644 --- a/comm_alg/grant.lean +++ b/comm_alg/grant.lean @@ -18,6 +18,14 @@ import Mathlib.Order.Height variable {α : Type _} [Preorder α] (s : Set α) +def finFun_to_list {n : ℕ} : (Fin n → α) → List α := by sorry + +def series_to_chain : StrictSeries s → s.subchain +| ⟨length, toFun, strictMono⟩ => + ⟨ finFun_to_list (fun x => toFun x), + sorry⟩ + + -- there should be a coercion from WithTop ℕ to WithBot (WithTop ℕ) but it doesn't seem to work -- it looks like this might be because someone changed the instance from CoeCT to Coe during the port lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop ℕ)) = krullDim s := by From dc034c2b09fec19599f1344946a715c33e502af4 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Sun, 11 Jun 2023 12:33:18 +0000 Subject: [PATCH 25/80] added preliminary def of krullDimGE --- comm_alg/grant.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/comm_alg/grant.lean b/comm_alg/grant.lean index de3e50f..92b1716 100644 --- a/comm_alg/grant.lean +++ b/comm_alg/grant.lean @@ -36,4 +36,7 @@ lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop sorry -- norm_cast - sorry \ No newline at end of file + sorry + +def krullDimGE (R : Type _) [CommRing R] (n : ℕ) := + ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 \ No newline at end of file From dcc992588214751fc5e29b036b8baf724dadbef9 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Mon, 12 Jun 2023 04:02:16 +0000 Subject: [PATCH 26/80] wrote some characterizations of bounding krull --- comm_alg/grant.lean | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/comm_alg/grant.lean b/comm_alg/grant.lean index 92b1716..8586fa3 100644 --- a/comm_alg/grant.lean +++ b/comm_alg/grant.lean @@ -28,6 +28,7 @@ def series_to_chain : StrictSeries s → s.subchain -- there should be a coercion from WithTop ℕ to WithBot (WithTop ℕ) but it doesn't seem to work -- it looks like this might be because someone changed the instance from CoeCT to Coe during the port +-- actually it looks like we can coerce to WithBot (ℕ∞) fine lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop ℕ)) = krullDim s := by intro hs unfold Set.chainHeight @@ -38,5 +39,23 @@ 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 \ No newline at end of file + ∃ 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 + + +-- #check ((4 : ℕ∞) : WithBot (WithTop ℕ)) +#check ( (Set.chainHeight s) : WithBot (ℕ∞)) \ No newline at end of file From a8b295fa0ece8e299144984ad67209a5ecb5d45f Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Sun, 11 Jun 2023 21:02:46 -0700 Subject: [PATCH 27/80] corrected definition of height, krull dim --- comm_alg/krull.lean | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/comm_alg/krull.lean b/comm_alg/krull.lean index 2a5af42..431b8f6 100644 --- a/comm_alg/krull.lean +++ b/comm_alg/krull.lean @@ -4,6 +4,7 @@ import Mathlib.RingTheory.PrincipalIdealDomain import Mathlib.RingTheory.DedekindDomain.Basic import Mathlib.RingTheory.Ideal.Quotient import Mathlib.RingTheory.Localization.AtPrime +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic /- This file contains the definitions of height of an ideal, and the krull dimension of a commutative ring. @@ -15,22 +16,24 @@ import Mathlib.RingTheory.Localization.AtPrime developed. -/ -variable {R : Type _} [CommRing R] (I : Ideal R) +namespace Ideal -namespace ideal +variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) -noncomputable def height : ℕ∞ := Set.chainHeight {J | J ≤ I ∧ J.IsPrime} +noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J ≤ I} - 1 -noncomputable def krull_dim (R : Type _) [CommRing R] := height (⊤ : Ideal R) +noncomputable def krull_dim (R : Type) [CommRing R]: WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I --some propositions that would be nice to be able to eventually -lemma dim_eq_zero_iff_field : krull_dim R = 0 ↔ IsField R := sorry +lemma dim_eq_zero_iff_field : krull_dim R = 0 ↔ IsField R := by 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_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krull_dim R ≤ 1 := by + rw [dim_le_one_iff] + exact Ring.DimensionLEOne.principal_ideal_ring R lemma dim_le_dim_polynomial_add_one [Nontrivial R] : krull_dim R ≤ krull_dim (Polynomial R) + 1 := sorry @@ -38,7 +41,7 @@ lemma dim_le_dim_polynomial_add_one [Nontrivial R] : 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_eq_dim_localization : + height I = krull_dim (Localization.AtPrime I.asIdeal) := sorry -lemma height_add_dim_quotient_le_dim : height I + krull_dim (R ⧸ I) ≤ krull_dim R := sorry \ No newline at end of file +lemma height_add_dim_quotient_le_dim : height I + krull_dim (R ⧸ I.asIdeal) ≤ krull_dim R := sorry \ No newline at end of file From 12fd0191134b40681c263bf3fe1200f0a9f78752 Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Sun, 11 Jun 2023 21:03:13 -0700 Subject: [PATCH 28/80] added to resources --- comm_alg/resources.lean | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/comm_alg/resources.lean b/comm_alg/resources.lean index eae7c89..adcce3a 100644 --- a/comm_alg/resources.lean +++ b/comm_alg/resources.lean @@ -9,6 +9,8 @@ import Mathlib.RingTheory.Noetherian import Mathlib.RingTheory.Artinian import Mathlib.Order.Height import Mathlib.RingTheory.MvPolynomial.Basic +import Mathlib.RingTheory.Ideal.Over +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M] @@ -44,4 +46,14 @@ variable (I : Ideal R) #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 +--hopefully there's good communication between them + + +--There's a preliminary version of the going up theorem +#check Ideal.exists_ideal_over_prime_of_isIntegral + +--Theorems relating primes of a ring to primes of its localization +#check PrimeSpectrum.localization_comap_injective +#check PrimeSpectrum.localization_comap_range +--Theorems relating primes of a ring to primes of a quotient +#check PrimeSpectrum.range_comap_of_surjective \ No newline at end of file From 6528571d32a0f95c1f8db340662e117285c9c002 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Mon, 12 Jun 2023 04:15:30 +0000 Subject: [PATCH 29/80] adjusted height definition --- comm_alg/krull.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/comm_alg/krull.lean b/comm_alg/krull.lean index 431b8f6..5204b9a 100644 --- a/comm_alg/krull.lean +++ b/comm_alg/krull.lean @@ -20,7 +20,7 @@ namespace Ideal variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) -noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J ≤ I} - 1 +noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} noncomputable def krull_dim (R : Type) [CommRing R]: WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I From 41922be785ca3dceecac7ceb95c7d8bb9ffefbc6 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Sun, 11 Jun 2023 21:18:21 -0700 Subject: [PATCH 30/80] new: Added some definitions about short exact sequences --- comm_alg/resources.lean | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/comm_alg/resources.lean b/comm_alg/resources.lean index adcce3a..5fbc3d6 100644 --- a/comm_alg/resources.lean +++ b/comm_alg/resources.lean @@ -11,6 +11,7 @@ import Mathlib.Order.Height import Mathlib.RingTheory.MvPolynomial.Basic import Mathlib.RingTheory.Ideal.Over import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Algebra.Homology.ShortExact.Abelian variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M] @@ -56,4 +57,22 @@ variable (I : Ideal R) #check PrimeSpectrum.localization_comap_injective #check PrimeSpectrum.localization_comap_range --Theorems relating primes of a ring to primes of a quotient -#check PrimeSpectrum.range_comap_of_surjective \ No newline at end of file +#check PrimeSpectrum.range_comap_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 +open CategoryTheory CategoryTheory.Limits CategoryTheory.Preadditive + +variable {𝒜 : Type _} [Category 𝒜] [Abelian 𝒜] +variable {A B C A': 𝒜} {f : A ⟶ B} {g : B ⟶ C} + +#check ShortExact +#check ShortExact f g +-- There are some notion of splitting as well +#check Splitting +#check LeftSplit +#check LeftSplit f g +-- And there is a theorem that left split implies splitting +#check LeftSplit.splitting +-- Similar things are there for RightSplit as well \ No newline at end of file From 16b933aeacf3aac0585695505e8c44a501863127 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Sun, 11 Jun 2023 21:41:21 -0700 Subject: [PATCH 31/80] just the statement --- comm_alg/jayden(krull-dim-zero).lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 comm_alg/jayden(krull-dim-zero).lean diff --git a/comm_alg/jayden(krull-dim-zero).lean b/comm_alg/jayden(krull-dim-zero).lean new file mode 100644 index 0000000..0e9b32f --- /dev/null +++ b/comm_alg/jayden(krull-dim-zero).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 dim_zero_Noetherian_is_Artinian (R : Type _) (IsNoetherianRing R) (krull_dim R = 0) : IsArtinianRing R := by sorry + +-- Use Stacks project proof since it's broken into lemmas + + + + + + From 9bac6f9aad370e7e9325672aba2e6a96c9c7fc52 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Sun, 11 Jun 2023 23:30:10 -0700 Subject: [PATCH 32/80] new: Added some more theorems about ses --- comm_alg/resources.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/comm_alg/resources.lean b/comm_alg/resources.lean index 5fbc3d6..bb30ae3 100644 --- a/comm_alg/resources.lean +++ b/comm_alg/resources.lean @@ -65,7 +65,7 @@ variable (I : Ideal R) open CategoryTheory CategoryTheory.Limits CategoryTheory.Preadditive variable {𝒜 : Type _} [Category 𝒜] [Abelian 𝒜] -variable {A B C A': 𝒜} {f : A ⟶ B} {g : B ⟶ C} +variable {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} {h : LeftSplit f g} {h' : RightSplit f g} #check ShortExact #check ShortExact f g @@ -75,4 +75,9 @@ variable {A B C A': 𝒜} {f : A ⟶ B} {g : B ⟶ C} #check LeftSplit f g -- And there is a theorem that left split implies splitting #check LeftSplit.splitting --- Similar things are there for RightSplit as well \ No newline at end of file +#check LeftSplit.splitting h +-- Similar things are there for RightSplit as well +#check RightSplit.splitting +#check RightSplit.splitting h' +-- There's also a theorem about ismorphisms between short exact sequences +#check isIso_of_shortExact_of_isIso_of_isIso From 6d4b9b0f60663df52862416f24a8ee4555db4ae9 Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Mon, 12 Jun 2023 09:49:40 -0700 Subject: [PATCH 33/80] updated krull_dim name, addd krullDim_le_iff --- comm_alg/krull.lean | 28 ++++++++++++++++++++-------- 1 file changed, 20 insertions(+), 8 deletions(-) diff --git a/comm_alg/krull.lean b/comm_alg/krull.lean index 5204b9a..1bd2829 100644 --- a/comm_alg/krull.lean +++ b/comm_alg/krull.lean @@ -5,6 +5,7 @@ import Mathlib.RingTheory.DedekindDomain.Basic import Mathlib.RingTheory.Ideal.Quotient import Mathlib.RingTheory.Localization.AtPrime import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Order.ConditionallyCompleteLattice.Basic /- This file contains the definitions of height of an ideal, and the krull dimension of a commutative ring. @@ -22,26 +23,37 @@ variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} -noncomputable def krull_dim (R : Type) [CommRing R]: WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I +noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I + +lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl +lemma krullDim_def (R : Type) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl +lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl + +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) --some propositions that would be nice to be able to eventually -lemma dim_eq_zero_iff_field : krull_dim R = 0 ↔ IsField R := by sorry +lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry #check Ring.DimensionLEOne -lemma dim_le_one_iff : krull_dim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry +lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry -lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krull_dim R ≤ 1 := by +lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1 := by rw [dim_le_one_iff] exact Ring.DimensionLEOne.principal_ideal_ring R lemma dim_le_dim_polynomial_add_one [Nontrivial R] : - krull_dim R ≤ krull_dim (Polynomial R) + 1 := sorry + krullDim R ≤ krullDim (Polynomial R) + 1 := sorry lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : - krull_dim R = krull_dim (Polynomial R) + 1 := sorry + krullDim R = krullDim (Polynomial R) + 1 := sorry lemma height_eq_dim_localization : - height I = krull_dim (Localization.AtPrime I.asIdeal) := sorry + height I = krullDim (Localization.AtPrime I.asIdeal) := sorry -lemma height_add_dim_quotient_le_dim : height I + krull_dim (R ⧸ I.asIdeal) ≤ krull_dim R := sorry \ No newline at end of file +lemma height_add_dim_quotient_le_dim : height I + krullDim (R ⧸ I.asIdeal) ≤ krullDim R := sorry \ No newline at end of file From 3b13474cec8bf6de0de201bd8de51149a348848c Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Mon, 12 Jun 2023 10:13:44 -0700 Subject: [PATCH 34/80] add lemmas --- comm_alg/jayden(krull-dim-zero).lean | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/comm_alg/jayden(krull-dim-zero).lean b/comm_alg/jayden(krull-dim-zero).lean index 0e9b32f..7be91c5 100644 --- a/comm_alg/jayden(krull-dim-zero).lean +++ b/comm_alg/jayden(krull-dim-zero).lean @@ -1,12 +1,25 @@ import Mathlib.RingTheory.Ideal.Basic import Mathlib.RingTheory.Noetherian +import Mathlib.Order.KrullDimension import Mathlib.RingTheory.Artinian import Mathlib.RingTheory.Ideal.Quotient import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic -lemma dim_zero_Noetherian_is_Artinian (R : Type _) (IsNoetherianRing R) (krull_dim R = 0) : IsArtinianRing R := by sorry +variable {R : Type _} [CommRing R] --- Use Stacks project proof since it's broken into lemmas +-- 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 + +-- The following is Stacks Lemma 10.53.6 +lemma IsArtinian_iff_finite_length : IsArtinianRing R ↔ ∃ n : ℕ, length R R ≤ n := by sorry From 6b46181b725d6ecfcc602df3f7ebf6242fa48c5a Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Mon, 12 Jun 2023 10:22:57 -0700 Subject: [PATCH 35/80] 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 36/80] 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 37/80] 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 38/80] 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 39/80] 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 40/80] 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 41/80] 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 e22b18e7c5964baf74ee825a0144a0b10379657c Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Mon, 12 Jun 2023 20:57:49 +0000 Subject: [PATCH 42/80] TESTMOna --- comm_alg/krull.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/comm_alg/krull.lean b/comm_alg/krull.lean index 2a5af42..1067e63 100644 --- a/comm_alg/krull.lean +++ b/comm_alg/krull.lean @@ -41,4 +41,4 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : 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 +lemma height_add_dim_quotient_le_dim : height I + krull_dim (R ⧸ I) ≤ krull_dim R := sorry From 871f38239c89e357335caa4b36e65494a07b7b48 Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Mon, 12 Jun 2023 20:59:28 +0000 Subject: [PATCH 43/80] TESTMOna --- comm_alg/Defhil.lean | 41 +++++++++++++++++++++++++++++++++++++++++ comm_alg/hilpol.lean | 14 ++++++++++++++ 2 files changed, 55 insertions(+) create mode 100644 comm_alg/Defhil.lean create mode 100644 comm_alg/hilpol.lean diff --git a/comm_alg/Defhil.lean b/comm_alg/Defhil.lean new file mode 100644 index 0000000..63c140a --- /dev/null +++ b/comm_alg/Defhil.lean @@ -0,0 +1,41 @@ +import Mathlib + +variable {R : Type _} (M A B C : Type _) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B] [AddCommGroup C] [Module R C] +variable (A' B' C' : ModuleCat R) +#check ModuleCat.of R A + +example : Module R A' := inferInstance + +#check ModuleCat.of R B + +example : Module R B' := inferInstance + +#check ModuleCat.of R C + +example : Module R C' := inferInstance + +namespace CategoryTheory + +noncomputable instance abelian : Abelian (ModuleCat.{v} R) := inferInstance +noncomputable instance haszero : Limits.HasZeroMorphisms (ModuleCat.{v} R) := inferInstance + +#check (A B : Submodule _ _) → (A ≤ B) + +#check Preorder (Submodule _ _) + +#check krullDim (Submodule _ _) + +noncomputable def length := krullDim (Submodule R M) + +open ZeroObject + +namespace HasZeroMorphisms + +open LinearMap + +#check length M + +#check ModuleCat.of R + +lemma length_additive_shortexact {f : A ⟶ B} {g : B ⟶ C} (h : ShortExact f g) : length B = length A + length C := sorry + diff --git a/comm_alg/hilpol.lean b/comm_alg/hilpol.lean new file mode 100644 index 0000000..957bade --- /dev/null +++ b/comm_alg/hilpol.lean @@ -0,0 +1,14 @@ +import Mathlib + + +--class GradedRing + +variable [GradedRing S] + +namespace DirectSum + +namespace ideal + +def S_+ := ⊕ (i ≥ 0) S_i + +lemma A set of homogeneous elements fi∈S+ generates S as an algebra over S0 ↔ they generate S+ as an ideal of S. \ No newline at end of file From cf0052a11221b47b8bea05b402fcd15a611cf4ad Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Mon, 12 Jun 2023 14:14:39 -0700 Subject: [PATCH 44/80] update lemmas --- comm_alg/jayden(krull-dim-zero).lean | 44 ++++++++++++++++++++++++---- 1 file changed, 38 insertions(+), 6 deletions(-) diff --git a/comm_alg/jayden(krull-dim-zero).lean b/comm_alg/jayden(krull-dim-zero).lean index 7be91c5..e084f18 100644 --- a/comm_alg/jayden(krull-dim-zero).lean +++ b/comm_alg/jayden(krull-dim-zero).lean @@ -1,28 +1,60 @@ import Mathlib.RingTheory.Ideal.Basic +import Mathlib.RingTheory.JacobsonIdeal import Mathlib.RingTheory.Noetherian 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 -variable {R : Type _} [CommRing R] +import Mathlib.Order.Height +import Mathlib.RingTheory.DedekindDomain.Basic +import Mathlib.RingTheory.Localization.AtPrime +import Mathlib.Order.ConditionallyCompleteLattice.Basic --- Repeats the definition by Monalisa -noncomputable def length : krullDim (Submodule _ _) +-- copy from krull.lean; the name of Krull dimension for rings is changed to krullDim' since krullDim already exists in the librrary +namespace Ideal +variable (R : Type _) [CommRing R] (I : PrimeSpectrum R) --- The following is Stacks Lemma 10.60.5 +noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} + +noncomputable def krullDim' (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height R I +-- copy ends + +-- 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 ∧ krull_dim R = 0 ↔ IsArtinianRing R := by + IsNoetherianRing R ∧ krullDim' R = 0 ↔ IsArtinianRing R := by sorry #check IsNoetherianRing --- The following is Stacks Lemma 10.53.6 +#check krullDim + +-- Repeats the definition of the length of a module by Monalisa +variable (M : Type _) [AddCommMonoid M] [Module R M] + +noncomputable def length := krullDim (Submodule R M) + +#check length +-- Stacks Lemma 10.53.6: R is Artinian iff R has finite length as an R-mod lemma IsArtinian_iff_finite_length : IsArtinianRing R ↔ ∃ n : ℕ, length R R ≤ n := by sorry +-- Stacks Lemma 10.53.3: R is Artinian iff R has finitely many maximal ideals +lemma IsArtinian_iff_finite_max_ideal : IsArtinianRing R ↔ Finite (MaximalSpectrum R) := by sorry + +-- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent +lemma Jacobson_of_Artinian_is_nilpotent : Is +-- how to use namespace + +namespace something + +end something + +open something From 58450c56be897479198a42f517fff39a7008b7e4 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Mon, 12 Jun 2023 14:21:59 -0700 Subject: [PATCH 45/80] renamed thngs --- {comm_alg => CommAlg}/jayden(krull-dim-zero).lean | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename {comm_alg => CommAlg}/jayden(krull-dim-zero).lean (100%) 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 From 8b2be97b5a4f597de327d00598bfafc20c9504a1 Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Mon, 12 Jun 2023 14:27:09 -0700 Subject: [PATCH 46/80] 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 From bbaf335924f1f71bf2bf911823687a4324d311bb Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Mon, 12 Jun 2023 16:06:48 -0700 Subject: [PATCH 47/80] new: Working proof of dim_field_eq_zero --- CommAlg/sayantan.lean | 67 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 67 insertions(+) create mode 100644 CommAlg/sayantan.lean diff --git a/CommAlg/sayantan.lean b/CommAlg/sayantan.lean new file mode 100644 index 0000000..553fa4f --- /dev/null +++ b/CommAlg/sayantan.lean @@ -0,0 +1,67 @@ +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 +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Order.ConditionallyCompleteLattice.Basic +-- import Mathlib.Data.ENat.Lattice +-- import Mathlib.Order.OrderIsoNat +-- import Mathlib.Tactic.TFAE + +namespace Ideal + +-- def foo : List Nat := [1, 2, 3, 4, 5] + +-- #check List.Chain' + +-- example : List.Chain' (· < ·) foo := by +-- repeat { constructor; norm_num } + + + +example (x : Nat) : List.Chain' (· < ·) [x] := by + constructor + + + +variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) + +noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} + +noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I + +lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl +lemma krullDim_def (R : Type) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl +lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl + +variable {K : Type _} [Field K] + +lemma dim_field_eq_zero : krullDim K = 0 := by + have prime_bot (P : Ideal K) : IsPrime P ↔ P = ⊥ := by + constructor + · intro primeP + obtain T := eq_bot_or_top P + have : ¬P = ⊤ := IsPrime.ne_top primeP + tauto + · intro botP + rw [botP] + exact bot_prime + unfold krullDim + have height_zero : ∀ P : PrimeSpectrum K, height P = 0 := by + intro P + unfold height + simp + by_contra spec + change _ ≠ _ at spec + rw [← Set.nonempty_iff_ne_empty] at spec + obtain ⟨J, JlP : J < P⟩ := spec + have P0 : IsPrime P.asIdeal := P.IsPrime + have J0 : IsPrime J.asIdeal := J.IsPrime + rw [prime_bot] at P0 J0 + have : J.asIdeal = P.asIdeal := Eq.trans J0 (Eq.symm P0) + have JeqP : J = P := PrimeSpectrum.ext J P this + have JneqP : J ≠ P := ne_of_lt JlP + contradiction + simp [height_zero] From 0a8fd3ef7cedb909dd11e28001f66bd4ef24379a Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Mon, 12 Jun 2023 23:09:47 +0000 Subject: [PATCH 48/80] Test --- comm_alg/Defhil.lean | 34 +++++++++++----------------------- comm_alg/hilpol.lean | 41 ++++++++++++++++++++++++++++++++++------- 2 files changed, 45 insertions(+), 30 deletions(-) diff --git a/comm_alg/Defhil.lean b/comm_alg/Defhil.lean index 63c140a..65da0c6 100644 --- a/comm_alg/Defhil.lean +++ b/comm_alg/Defhil.lean @@ -1,23 +1,15 @@ import Mathlib +import Mathlib.RingTheory.Ideal.Basic +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.LinearAlgebra.Finsupp +import Mathlib.RingTheory.GradedAlgebra.Basic +import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal + + + variable {R : Type _} (M A B C : Type _) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B] [AddCommGroup C] [Module R C] -variable (A' B' C' : ModuleCat R) -#check ModuleCat.of R A -example : Module R A' := inferInstance - -#check ModuleCat.of R B - -example : Module R B' := inferInstance - -#check ModuleCat.of R C - -example : Module R C' := inferInstance - -namespace CategoryTheory - -noncomputable instance abelian : Abelian (ModuleCat.{v} R) := inferInstance -noncomputable instance haszero : Limits.HasZeroMorphisms (ModuleCat.{v} R) := inferInstance #check (A B : Submodule _ _) → (A ≤ B) @@ -25,17 +17,13 @@ noncomputable instance haszero : Limits.HasZeroMorphisms (ModuleCat.{v} R) := in #check krullDim (Submodule _ _) -noncomputable def length := krullDim (Submodule R M) - -open ZeroObject - -namespace HasZeroMorphisms +noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < ⊤} open LinearMap #check length M -#check ModuleCat.of R -lemma length_additive_shortexact {f : A ⟶ B} {g : B ⟶ C} (h : ShortExact f g) : length B = length A + length C := sorry + +--lemma length_additive_shortexact {f : A ⟶ B} {g : B ⟶ C} (h : ShortExact f g) : length B = length A + length C := sorry diff --git a/comm_alg/hilpol.lean b/comm_alg/hilpol.lean index 957bade..0aab559 100644 --- a/comm_alg/hilpol.lean +++ b/comm_alg/hilpol.lean @@ -1,14 +1,41 @@ -import Mathlib +import Mathlib.Order.KrullDimension +import Mathlib.Order.JordanHolder +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Order.Height +import Mathlib.RingTheory.Ideal.Basic +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.LinearAlgebra.Finsupp +import Mathlib.RingTheory.GradedAlgebra.Basic +import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal +import Mathlib.Algebra.Module.GradedModule +import Mathlib.RingTheory.Ideal.AssociatedPrime +import Mathlib.RingTheory.Noetherian +variable {ι σ R A : Type _} ---class GradedRing +section HomogeneousDef -variable [GradedRing S] +variable [Semiring A] -namespace DirectSum +variable [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ) -namespace ideal +variable [GradedRing 𝒜] -def S_+ := ⊕ (i ≥ 0) S_i +variable (I : HomogeneousIdeal 𝒜) -lemma A set of homogeneous elements fi∈S+ generates S as an algebra over S0 ↔ they generate S+ as an ideal of S. \ No newline at end of file +-- def Ideal.IsHomogeneous : Prop := +-- ∀ (i : ι) ⦃r : A⦄, r ∈ I → (DirectSum.decompose 𝒜 r i : A) ∈ I +-- #align ideal.is_homogeneous Ideal.IsHomogeneous + +-- structure HomogeneousIdeal extends Submodule A A where +-- is_homogeneous' : Ideal.IsHomogeneous 𝒜 toSubmodule + +--#check Ideal.IsPrime hI + +def HomogeneousPrime (I : Ideal A):= Ideal.IsPrime I + +def HomogeneousMax (I : Ideal A):= Ideal.IsMaximal I + +--theorem monotone_stabilizes_iff_noetherian : +-- (∀ f : ℕ →o Submodule R M, ∃ n, ∀ m, n ≤ m → f n = f m) ↔ IsNoetherian R M := by +-- rw [isNoetherian_iff_wellFounded, WellFounded.monotone_chain_condition] \ No newline at end of file From a41873ac1b52a51eaafa29caf112f8827185ea92 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Mon, 12 Jun 2023 16:25:02 -0700 Subject: [PATCH 49/80] change: Refactoring --- CommAlg/sayantan.lean | 28 +++++++++------------------- 1 file changed, 9 insertions(+), 19 deletions(-) diff --git a/CommAlg/sayantan.lean b/CommAlg/sayantan.lean index 553fa4f..90bf5d5 100644 --- a/CommAlg/sayantan.lean +++ b/CommAlg/sayantan.lean @@ -9,18 +9,8 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic -- import Mathlib.Data.ENat.Lattice -- import Mathlib.Order.OrderIsoNat -- import Mathlib.Tactic.TFAE - namespace Ideal --- def foo : List Nat := [1, 2, 3, 4, 5] - --- #check List.Chain' - --- example : List.Chain' (· < ·) foo := by --- repeat { constructor; norm_num } - - - example (x : Nat) : List.Chain' (· < ·) [x] := by constructor @@ -36,10 +26,8 @@ lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := r lemma krullDim_def (R : Type) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl -variable {K : Type _} [Field K] - -lemma dim_field_eq_zero : krullDim K = 0 := by - have prime_bot (P : Ideal K) : IsPrime P ↔ P = ⊥ := by +@[simp] +lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by constructor · intro primeP obtain T := eq_bot_or_top P @@ -48,9 +36,8 @@ lemma dim_field_eq_zero : krullDim K = 0 := by · intro botP rw [botP] exact bot_prime - unfold krullDim - have height_zero : ∀ P : PrimeSpectrum K, height P = 0 := by - intro P + +lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : height P = 0 := by unfold height simp by_contra spec @@ -59,9 +46,12 @@ lemma dim_field_eq_zero : krullDim K = 0 := by obtain ⟨J, JlP : J < P⟩ := spec have P0 : IsPrime P.asIdeal := P.IsPrime have J0 : IsPrime J.asIdeal := J.IsPrime - rw [prime_bot] at P0 J0 + rw [field_prime_bot] at P0 J0 have : J.asIdeal = P.asIdeal := Eq.trans J0 (Eq.symm P0) have JeqP : J = P := PrimeSpectrum.ext J P this have JneqP : J ≠ P := ne_of_lt JlP contradiction - simp [height_zero] + +lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by + unfold krullDim + simp [field_prime_height_zero] From 5cb0f77d2f22c5adf957dcacc198be6cf8066751 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Mon, 12 Jun 2023 20:03:43 -0700 Subject: [PATCH 50/80] update --- CommAlg/jayden(krull-dim-zero).lean | 40 ++++++++++++++++------------- 1 file changed, 22 insertions(+), 18 deletions(-) diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean index 0646bcb..bdb3bf9 100644 --- a/CommAlg/jayden(krull-dim-zero).lean +++ b/CommAlg/jayden(krull-dim-zero).lean @@ -4,15 +4,15 @@ import Mathlib.RingTheory.Noetherian import Mathlib.Order.KrullDimension import Mathlib.RingTheory.Artinian import Mathlib.RingTheory.Ideal.Quotient +import Mathlib.RingTheory.Nilpotent import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic - import Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal import Mathlib.Data.Finite.Defs - import Mathlib.Order.Height import Mathlib.RingTheory.DedekindDomain.Basic import Mathlib.RingTheory.Localization.AtPrime import Mathlib.Order.ConditionallyCompleteLattice.Basic +import Mathlib.Algebra.Ring.Pi -- copy from krull.lean; the name of Krull dimension for rings is changed to krullDim' since krullDim already exists in the librrary namespace Ideal @@ -26,21 +26,9 @@ 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 + IsNoetherianRing R ∧ krullDim' R = 0 ↔ IsArtinianRing R := by sorry -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 #check krullDim @@ -58,7 +46,25 @@ lemma IsArtinian_iff_finite_length : IsArtinianRing R ↔ ∃ n : ℕ, length R lemma IsArtinian_iff_finite_max_ideal : IsArtinianRing R ↔ Finite (MaximalSpectrum R) := by sorry -- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent -lemma Jacobson_of_Artinian_is_nilpotent : Is +lemma Jacobson_of_Artinian_is_nilpotent : IsArtinianRing R → IsNilpotent (Ideal.jacobson (⊤ : Ideal R)) := by sorry + + +-- Stacks Definition 10.32.1: An ideal is locally nilpotent +-- if every element is nilpotent +namespace Ideal +class IsLocallyNilpotent (I : Ideal R) : Prop := + h : ∀ x ∈ I, IsNilpotent x + +end Ideal + +#check Ideal.IsLocallyNilpotent + +-- Stacks Lemma 10.53.5: If R has finitely many maximal ideals and +-- locally nilpotent Jacobson radical, then R is the product of its localizations at +-- its maximal ideals. Also, all primes are maximal + +lemma product_of_localization_at_maximal_ideal : Finite (MaximalSpectrum R) + ∧ Ideal.IsLocallyNilpotent (Ideal.jacobson (⊤ : Ideal R)) → Localization.AtPrime R I @@ -70,8 +76,6 @@ 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 From eb01e5506a234fa5084c04b301879aec28e2d121 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Mon, 12 Jun 2023 20:48:42 -0700 Subject: [PATCH 51/80] add more stuff --- CommAlg/jayden(krull-dim-zero).lean | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean index bdb3bf9..3651102 100644 --- a/CommAlg/jayden(krull-dim-zero).lean +++ b/CommAlg/jayden(krull-dim-zero).lean @@ -13,6 +13,7 @@ import Mathlib.RingTheory.DedekindDomain.Basic import Mathlib.RingTheory.Localization.AtPrime import Mathlib.Order.ConditionallyCompleteLattice.Basic import Mathlib.Algebra.Ring.Pi +import Mathlib.Topology.NoetherianSpace -- copy from krull.lean; the name of Krull dimension for rings is changed to krullDim' since krullDim already exists in the librrary namespace Ideal @@ -36,7 +37,8 @@ lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : -- Repeats the definition of the length of a module by Monalisa variable (M : Type _) [AddCommMonoid M] [Module R M] -noncomputable def length := krullDim (Submodule R M) +-- change the definition of length +noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < ⊤} #check length -- Stacks Lemma 10.53.6: R is Artinian iff R has finite length as an R-mod @@ -64,9 +66,24 @@ end Ideal -- its maximal ideals. Also, all primes are maximal lemma product_of_localization_at_maximal_ideal : Finite (MaximalSpectrum R) - ∧ Ideal.IsLocallyNilpotent (Ideal.jacobson (⊤ : Ideal R)) → Localization.AtPrime R I + ∧ Ideal.IsLocallyNilpotent (Ideal.jacobson (⊤ : Ideal R)) → Pi.commRing (MaximalSpectrum R) Localization.AtPrime R I + := by sorry +-- Haven't finished this. + +-- Stacks Lemma 10.31.5: R is Noetherian iff Spec(R) is a Noetherian space +lemma ring_Noetherian_iff_spec_Noetherian : IsNoetherianRing R + ↔ TopologicalSpace.NoetherianSpace (PrimeSpectrum R) := by sorry +-- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible : +-- Every closed subset of a noetherian space is a finite union +-- of irreducible closed subsets. +-- Stacks Lemma 10.26.1 (Should already exists) +-- (1) The closure of a prime P is V(P) +-- (2) the irreducible closed subsets are V(P) for P prime +-- (3) the irreducible components are V(P) for P minimal prime + +-- Stacks Lemma 10.32.5: R Noetherian. I,J ideals. If J ⊂ √I, then J ^ n ⊂ I for some n -- how to use namespace From b3a11a6e44865996fcb1ca9f211e0ddde154949b Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Tue, 13 Jun 2023 04:23:17 +0000 Subject: [PATCH 52/80] proved height_ge_iff' --- CommAlg/grant.lean | 58 ++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 53 insertions(+), 5 deletions(-) diff --git a/CommAlg/grant.lean b/CommAlg/grant.lean index 2f3c634..2261f25 100644 --- a/CommAlg/grant.lean +++ b/CommAlg/grant.lean @@ -17,6 +17,8 @@ import CommAlg.krull #check JordanHolderLattice +section Chains + variable {α : Type _} [Preorder α] (s : Set α) def finFun_to_list {n : ℕ} : (Fin n → α) → List α := by sorry @@ -26,7 +28,6 @@ def series_to_chain : StrictSeries s → s.subchain ⟨ finFun_to_list (fun x => toFun x), sorry⟩ - -- there should be a coercion from WithTop ℕ to WithBot (WithTop ℕ) but it doesn't seem to work -- it looks like this might be because someone changed the instance from CoeCT to Coe during the port -- actually it looks like we can coerce to WithBot (ℕ∞) fine @@ -40,15 +41,62 @@ lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop -- norm_cast sorry +end Chains + +section Krull + +variable (R : Type _) [CommRing R] (M : Type _) [AddCommGroup M] [Module R M] + open Ideal -lemma krullDim_le_iff' (R : Type _) [CommRing R] : +-- chain of primes +#check height + +-- lemma height_ge_iff {𝔭 : PrimeSpectrum R} {n : ℕ∞} : +-- height 𝔭 ≥ n ↔ := sorry + +lemma height_ge_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : +height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by + rcases n with _ | n + . constructor <;> intro h <;> exfalso + . exact (not_le.mpr h) le_top + . -- change ∃c, _ ∧ _ ∧ ((List.length c : ℕ∞) = ⊤ + 1) at h + -- rw [WithTop.top_add] at h + tauto + have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by + symm + show (n + 1 ≤ m ↔ _ ) + apply ENat.add_one_le_iff + exact ENat.coe_ne_top _ + rw [this] + unfold Ideal.height + show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞)) + rw [{J | J < 𝔭}.le_chainHeight_iff] + show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _ + have h := fun (c : List (PrimeSpectrum R)) => (@WithTop.coe_eq_coe _ (List.length c) n) + constructor <;> rintro ⟨c, hc⟩ <;> use c --<;> tauto--<;> exact ⟨hc.1, by tauto⟩ + . --rw [and_assoc] + -- show _ ∧ _ ∧ _ + --exact ⟨hc.1, _⟩ + tauto + . change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc + norm_cast at hc + tauto + +lemma krullDim_le_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : Ideal.krullDim R ≤ n ↔ (∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1) := by sorry -lemma krullDim_ge_iff' (R : Type _) [CommRing R] : +lemma krullDim_ge_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : Ideal.krullDim R ≥ n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 := sorry - +#check (sorry : False) +#check (sorryAx) +#check (4 : WithBot ℕ∞) +#check List.sum -- #check ((4 : ℕ∞) : WithBot (WithTop ℕ)) -#check ( (Set.chainHeight s) : WithBot (ℕ∞)) \ No newline at end of file +-- #check ( (Set.chainHeight s) : WithBot (ℕ∞)) + +variable (P : PrimeSpectrum R) + +#check {J | J < P}.le_chainHeight_iff (n := 4) From 6bbeb7e36d15abf34012208ff301eda1d461efea Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Mon, 12 Jun 2023 21:55:06 -0700 Subject: [PATCH 53/80] new: Made some progress on the other side of dim_eq_zero_iff_field --- CommAlg/sayantan.lean | 28 +++++++++++++++++++++------- 1 file changed, 21 insertions(+), 7 deletions(-) diff --git a/CommAlg/sayantan.lean b/CommAlg/sayantan.lean index 90bf5d5..b2fc79a 100644 --- a/CommAlg/sayantan.lean +++ b/CommAlg/sayantan.lean @@ -6,9 +6,7 @@ import Mathlib.RingTheory.Ideal.Quotient import Mathlib.RingTheory.Localization.AtPrime import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic import Mathlib.Order.ConditionallyCompleteLattice.Basic --- import Mathlib.Data.ENat.Lattice --- import Mathlib.Order.OrderIsoNat --- import Mathlib.Tactic.TFAE + namespace Ideal example (x : Nat) : List.Chain' (· < ·) [x] := by @@ -17,9 +15,7 @@ example (x : Nat) : List.Chain' (· < ·) [x] := by variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) - noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} - noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl @@ -48,10 +44,28 @@ lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : heig have J0 : IsPrime J.asIdeal := J.IsPrime rw [field_prime_bot] at P0 J0 have : J.asIdeal = P.asIdeal := Eq.trans J0 (Eq.symm P0) - have JeqP : J = P := PrimeSpectrum.ext J P this - have JneqP : J ≠ P := ne_of_lt JlP + have : J = P := PrimeSpectrum.ext J P this + have : J ≠ P := ne_of_lt JlP contradiction lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by unfold krullDim simp [field_prime_height_zero] + +lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by + unfold krullDim at h + simp [height] at h + by_contra x + rw [Ring.not_isField_iff_exists_prime] at x + obtain ⟨P, ⟨h, primeP⟩⟩ := x + have PgtBot : P > ⊥ := Ne.bot_lt h + sorry + +lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by + constructor + · exact isField.dim_zero + · intro fieldD + have : Field D := IsField.toField fieldD + -- Not exactly sure why this is failing + -- apply @dim_field_eq_zero D _ + sorry From 6a0a3768f8a5f5b13845b21d36e4b41cde7c06e1 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Tue, 13 Jun 2023 05:01:18 +0000 Subject: [PATCH 54/80] proved krullDim_nonneg_of_nontrivial --- CommAlg/grant.lean | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/CommAlg/grant.lean b/CommAlg/grant.lean index 2261f25..ef2cc9f 100644 --- a/CommAlg/grant.lean +++ b/CommAlg/grant.lean @@ -73,7 +73,7 @@ height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞)) rw [{J | J < 𝔭}.le_chainHeight_iff] show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _ - have h := fun (c : List (PrimeSpectrum R)) => (@WithTop.coe_eq_coe _ (List.length c) n) + -- have h := fun (c : List (PrimeSpectrum R)) => (@WithTop.coe_eq_coe _ (List.length c) n) constructor <;> rintro ⟨c, hc⟩ <;> use c --<;> tauto--<;> exact ⟨hc.1, by tauto⟩ . --rw [and_assoc] -- show _ ∧ _ ∧ _ @@ -83,6 +83,11 @@ height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ norm_cast at hc tauto +lemma krullDim_nonneg_of_nontrivial [Nontrivial R] : ∃ n : ℕ∞, Ideal.krullDim R = n := by + have h := dim_eq_bot_iff.not.mpr (not_subsingleton R) + lift (Ideal.krullDim R) to ℕ∞ using h with k + use k + lemma krullDim_le_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : Ideal.krullDim R ≤ n ↔ (∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1) := by sorry @@ -90,6 +95,8 @@ lemma krullDim_le_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : lemma krullDim_ge_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : Ideal.krullDim R ≥ n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 := sorry + + #check (sorry : False) #check (sorryAx) #check (4 : WithBot ℕ∞) From e3a7639399596c8dc532b35eec70f2e19df8cf11 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Mon, 12 Jun 2023 23:58:40 -0700 Subject: [PATCH 55/80] new: Made some progress on the isField.dim_zero lemma --- CommAlg/sayantan.lean | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/CommAlg/sayantan.lean b/CommAlg/sayantan.lean index b2fc79a..6140db5 100644 --- a/CommAlg/sayantan.lean +++ b/CommAlg/sayantan.lean @@ -57,9 +57,19 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) simp [height] at h by_contra x rw [Ring.not_isField_iff_exists_prime] at x - obtain ⟨P, ⟨h, primeP⟩⟩ := x - have PgtBot : P > ⊥ := Ne.bot_lt h - sorry + obtain ⟨P, ⟨h1, primeP⟩⟩ := x + have PgtBot : P > ⊥ := Ne.bot_lt h1 + have pos_height : ↑(Set.chainHeight {J | J < P}) > 0 := by + have : ⊥ ∈ {J | J < P} := PgtBot + have : {J | J < P}.Nonempty := Set.nonempty_of_mem this + -- have : {J | J < P} ≠ ∅ := Set.Nonempty.ne_empty this + rw [←Set.one_le_chainHeight_iff] at this + exact Iff.mp ENat.one_le_iff_pos this + have zero_height : ↑(Set.chainHeight {J | J < P}) = 0 := by + -- Probably need to use Sup_le or something here + sorry + have : ↑(Set.chainHeight {J | J < P}) ≠ 0 := Iff.mp pos_iff_ne_zero pos_height + contradiction lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by constructor From afeeeb506fe6801f158593d292ff32dc636c3a3f Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Tue, 13 Jun 2023 19:11:44 +0000 Subject: [PATCH 56/80] proved dim_eq_bot_iff --- CommAlg/grant.lean | 40 ++++++++++++++++++++++++++++++++-------- 1 file changed, 32 insertions(+), 8 deletions(-) diff --git a/CommAlg/grant.lean b/CommAlg/grant.lean index ef2cc9f..7951c54 100644 --- a/CommAlg/grant.lean +++ b/CommAlg/grant.lean @@ -52,10 +52,10 @@ open Ideal -- chain of primes #check height --- lemma height_ge_iff {𝔭 : PrimeSpectrum R} {n : ℕ∞} : --- height 𝔭 ≥ n ↔ := sorry +lemma lt_height_iff {𝔭 : PrimeSpectrum R} {n : ℕ∞} : + height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c ∈ {I : PrimeSpectrum R | I < 𝔭}.subchain ∧ c.length = n + 1 := sorry -lemma height_ge_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : +lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by rcases n with _ | n . constructor <;> intro h <;> exfalso @@ -88,13 +88,37 @@ lemma krullDim_nonneg_of_nontrivial [Nontrivial R] : ∃ n : ℕ∞, Ideal.krull lift (Ideal.krullDim R) to ℕ∞ using h with k use k -lemma krullDim_le_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : - Ideal.krullDim R ≤ n ↔ (∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1) := by - sorry +-- lemma krullDim_le_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : +-- Ideal.krullDim R ≤ n ↔ (∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1) := by +-- sorry -lemma krullDim_ge_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : - Ideal.krullDim R ≥ n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 := sorry +-- lemma krullDim_ge_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : +-- Ideal.krullDim R ≥ n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 := sorry +lemma prime_elim_of_subsingleton (x : PrimeSpectrum R) [Subsingleton R] : False := + x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : R)) x.1.zero_mem + +lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by + constructor + . contrapose + rw [not_isEmpty_iff, ←not_nontrivial_iff_subsingleton, not_not] + apply PrimeSpectrum.instNonemptyPrimeSpectrum + . intro h + by_contra hneg + rw [not_isEmpty_iff] at hneg + rcases hneg with ⟨a, ha⟩ + exact prime_elim_of_subsingleton R ⟨a, ha⟩ + +lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by + unfold Ideal.krullDim + rw [←primeSpectrum_empty_iff, iSup_eq_bot] + constructor <;> intro h + . rw [←not_nonempty_iff] + rintro ⟨a, ha⟩ + specialize h ⟨a, ha⟩ + tauto + . rw [h.forall_iff] + trivial #check (sorry : False) From f63286aff8ebf58f6a463b92068573ea4d9aa9d1 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Tue, 13 Jun 2023 20:34:02 +0000 Subject: [PATCH 57/80] moved dim_eq_bot_iff to krull.lean --- CommAlg/grant.lean | 7 ++++--- CommAlg/krull.lean | 26 +++++++++++++++++++++++++- 2 files changed, 29 insertions(+), 4 deletions(-) diff --git a/CommAlg/grant.lean b/CommAlg/grant.lean index 7951c54..ce5041d 100644 --- a/CommAlg/grant.lean +++ b/CommAlg/grant.lean @@ -95,7 +95,7 @@ lemma krullDim_nonneg_of_nontrivial [Nontrivial R] : ∃ n : ℕ∞, Ideal.krull -- lemma krullDim_ge_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : -- Ideal.krullDim R ≥ n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 := sorry -lemma prime_elim_of_subsingleton (x : PrimeSpectrum R) [Subsingleton R] : False := +lemma primeSpectrum_empty_of_subsingleton (x : PrimeSpectrum R) [Subsingleton R] : False := x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : R)) x.1.zero_mem lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by @@ -107,15 +107,16 @@ lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by_contra hneg rw [not_isEmpty_iff] at hneg rcases hneg with ⟨a, ha⟩ - exact prime_elim_of_subsingleton R ⟨a, ha⟩ + exact primeSpectrum_empty_of_subsingleton R ⟨a, ha⟩ +/-- A ring has Krull dimension -∞ if and only if it is the zero ring -/ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by unfold Ideal.krullDim rw [←primeSpectrum_empty_iff, iSup_eq_bot] constructor <;> intro h . rw [←not_nonempty_iff] rintro ⟨a, ha⟩ - specialize h ⟨a, ha⟩ + -- specialize h ⟨a, ha⟩ tauto . rw [h.forall_iff] trivial diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 9b4c785..c021d74 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -62,7 +62,31 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := #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 primeSpectrum_empty_of_subsingleton (x : PrimeSpectrum R) [Subsingleton R] : False := + x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : R)) x.1.zero_mem + +lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by + constructor + . contrapose + rw [not_isEmpty_iff, ←not_nontrivial_iff_subsingleton, not_not] + apply PrimeSpectrum.instNonemptyPrimeSpectrum + . intro h + by_contra hneg + rw [not_isEmpty_iff] at hneg + rcases hneg with ⟨a, ha⟩ + exact primeSpectrum_empty_of_subsingleton ⟨a, ha⟩ + +/-- A ring has Krull dimension -∞ if and only if it is the zero ring -/ +lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by + unfold Ideal.krullDim + rw [←primeSpectrum_empty_iff, iSup_eq_bot] + constructor <;> intro h + . rw [←not_nonempty_iff] + rintro ⟨a, ha⟩ + specialize h ⟨a, ha⟩ + tauto + . rw [h.forall_iff] + trivial lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry From dedb9711c76e58717d6a2c15693ec2e16069cfe6 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 14:08:04 -0700 Subject: [PATCH 58/80] update: Finally, the proof of dim_eq_zero_iff_field is complete --- CommAlg/sayantan.lean | 39 ++++++++++++++++++++------------------- 1 file changed, 20 insertions(+), 19 deletions(-) diff --git a/CommAlg/sayantan.lean b/CommAlg/sayantan.lean index 6140db5..7656924 100644 --- a/CommAlg/sayantan.lean +++ b/CommAlg/sayantan.lean @@ -9,11 +9,6 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic namespace Ideal -example (x : Nat) : List.Chain' (· < ·) [x] := by - constructor - - - variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I @@ -52,30 +47,36 @@ lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by unfold krullDim simp [field_prime_height_zero] +noncomputable +instance : CompleteLattice (WithBot ℕ∞) := + inferInstanceAs <| CompleteLattice (WithBot (WithTop ℕ)) + lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by unfold krullDim at h simp [height] at h by_contra x rw [Ring.not_isField_iff_exists_prime] at x obtain ⟨P, ⟨h1, primeP⟩⟩ := x - have PgtBot : P > ⊥ := Ne.bot_lt h1 - have pos_height : ↑(Set.chainHeight {J | J < P}) > 0 := by - have : ⊥ ∈ {J | J < P} := PgtBot - have : {J | J < P}.Nonempty := Set.nonempty_of_mem this - -- have : {J | J < P} ≠ ∅ := Set.Nonempty.ne_empty this + let P' : PrimeSpectrum D := PrimeSpectrum.mk P primeP + have h2 : P' ≠ ⊥ := by + by_contra a + have : P = ⊥ := by rwa [PrimeSpectrum.ext_iff] at a + contradiction + have PgtBot : P' > ⊥ := Ne.bot_lt h2 + have pos_height : ¬ ↑(Set.chainHeight {J | J < P'}) ≤ 0 := by + have : ⊥ ∈ {J | J < P'} := PgtBot + have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this rw [←Set.one_le_chainHeight_iff] at this - exact Iff.mp ENat.one_le_iff_pos this - have zero_height : ↑(Set.chainHeight {J | J < P}) = 0 := by - -- Probably need to use Sup_le or something here - sorry - have : ↑(Set.chainHeight {J | J < P}) ≠ 0 := Iff.mp pos_iff_ne_zero pos_height + exact not_le_of_gt (Iff.mp ENat.one_le_iff_pos this) + have zero_height : (Set.chainHeight {J | J < P'}) ≤ 0 := by + have : (⨆ (I : PrimeSpectrum D), (Set.chainHeight {J | J < I} : WithBot ℕ∞)) ≤ 0 := h.le + rw [iSup_le_iff] at this + exact Iff.mp WithBot.coe_le_zero (this P') contradiction lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by constructor · exact isField.dim_zero · intro fieldD - have : Field D := IsField.toField fieldD - -- Not exactly sure why this is failing - -- apply @dim_field_eq_zero D _ - sorry + let h : Field D := IsField.toField fieldD + exact dim_field_eq_zero \ No newline at end of file From db1875067783ee57b4013b8c5ce54d335a9c63ac Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 14:11:13 -0700 Subject: [PATCH 59/80] Renamed a file --- CommAlg/{sayantan.lean => sayantan(dim_eq_zero_iff_field).lean} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename CommAlg/{sayantan.lean => sayantan(dim_eq_zero_iff_field).lean} (99%) diff --git a/CommAlg/sayantan.lean b/CommAlg/sayantan(dim_eq_zero_iff_field).lean similarity index 99% rename from CommAlg/sayantan.lean rename to CommAlg/sayantan(dim_eq_zero_iff_field).lean index 7656924..35f197f 100644 --- a/CommAlg/sayantan.lean +++ b/CommAlg/sayantan(dim_eq_zero_iff_field).lean @@ -79,4 +79,4 @@ lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = · exact isField.dim_zero · intro fieldD let h : Field D := IsField.toField fieldD - exact dim_field_eq_zero \ No newline at end of file + exact dim_field_eq_zero From 5f241e80f164fb255953686d33c21d4a12cd1df1 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 14:16:53 -0700 Subject: [PATCH 60/80] Added a comment --- CommAlg/krull.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index c021d74..e8941a3 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -88,7 +88,7 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by . rw [h.forall_iff] trivial -lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry +lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry -- It's been done in another file #check Ring.DimensionLEOne lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry From 4c7b6b3022d7707e4897e43cadbf9bef95689b2e Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Tue, 13 Jun 2023 14:17:59 -0700 Subject: [PATCH 61/80] two new sorried statements --- CommAlg/krull.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 9b4c785..a85f6b5 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -45,6 +45,12 @@ lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) : lemma krullDim_le_iff' (R : Type) [CommRing R] (n : ℕ∞) : krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞) +lemma le_krullDim_iff (R : Type) [CommRing R] (n : ℕ) : + n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry + +lemma le_krullDim_iff' (R : Type) [CommRing R] (n : ℕ∞) : + n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry + @[simp] lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R := le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I From a941cce12f21b0bd94757a669c1d73f5677c60a5 Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Tue, 13 Jun 2023 14:26:19 -0700 Subject: [PATCH 62/80] changed all rings from Type to Type _ --- CommAlg/krull.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 440ea66..2a87c16 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -25,11 +25,11 @@ variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} -noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I +noncomputable def krullDim (R : Type _) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl -lemma krullDim_def (R : Type) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl -lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl +lemma krullDim_def (R : Type _) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl +lemma krullDim_def' (R : Type _) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice @@ -39,16 +39,16 @@ lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ show J' < J exact lt_of_lt_of_le hJ' I_le_J -lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) : +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 : ℕ∞) : +lemma krullDim_le_iff' (R : Type _) [CommRing R] (n : ℕ∞) : krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞) -lemma le_krullDim_iff (R : Type) [CommRing R] (n : ℕ) : +lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) : n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry -lemma le_krullDim_iff' (R : Type) [CommRing R] (n : ℕ∞) : +lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) : n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry @[simp] From 3730100c86de0fed1adf2df212d98d84af084ef7 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 14:35:10 -0700 Subject: [PATCH 63/80] Moved dim_eq_zero_iff_field to the main file --- CommAlg/krull.lean | 60 +++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 59 insertions(+), 1 deletion(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index e8941a3..4e069a2 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -88,7 +88,65 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by . rw [h.forall_iff] trivial -lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry -- It's been done in another file +@[simp] +lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by + constructor + · intro primeP + obtain T := eq_bot_or_top P + have : ¬P = ⊤ := IsPrime.ne_top primeP + tauto + · intro botP + rw [botP] + exact bot_prime + +lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : height P = 0 := by + unfold height + simp + by_contra spec + change _ ≠ _ at spec + rw [← Set.nonempty_iff_ne_empty] at spec + obtain ⟨J, JlP : J < P⟩ := spec + have P0 : IsPrime P.asIdeal := P.IsPrime + have J0 : IsPrime J.asIdeal := J.IsPrime + rw [field_prime_bot] at P0 J0 + have : J.asIdeal = P.asIdeal := Eq.trans J0 (Eq.symm P0) + have : J = P := PrimeSpectrum.ext J P this + have : J ≠ P := ne_of_lt JlP + contradiction + +lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by + unfold krullDim + simp [field_prime_height_zero] + +lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by + unfold krullDim at h + simp [height] at h + by_contra x + rw [Ring.not_isField_iff_exists_prime] at x + obtain ⟨P, ⟨h1, primeP⟩⟩ := x + let P' : PrimeSpectrum D := PrimeSpectrum.mk P primeP + have h2 : P' ≠ ⊥ := by + by_contra a + have : P = ⊥ := by rwa [PrimeSpectrum.ext_iff] at a + contradiction + have PgtBot : P' > ⊥ := Ne.bot_lt h2 + have pos_height : ¬ ↑(Set.chainHeight {J | J < P'}) ≤ 0 := by + have : ⊥ ∈ {J | J < P'} := PgtBot + have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this + rw [←Set.one_le_chainHeight_iff] at this + exact not_le_of_gt (Iff.mp ENat.one_le_iff_pos this) + have nonpos_height : (Set.chainHeight {J | J < P'}) ≤ 0 := by + have : (⨆ (I : PrimeSpectrum D), (Set.chainHeight {J | J < I} : WithBot ℕ∞)) ≤ 0 := h.le + rw [iSup_le_iff] at this + exact Iff.mp WithBot.coe_le_zero (this P') + contradiction + +lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by + constructor + · exact isField.dim_zero + · intro fieldD + let h : Field D := IsField.toField fieldD + exact dim_field_eq_zero #check Ring.DimensionLEOne lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry From 7b8c0ba127128bfb3bd11221291139e087978e03 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 14:35:46 -0700 Subject: [PATCH 64/80] Made very small changes --- CommAlg/sayantan(dim_eq_zero_iff_field).lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CommAlg/sayantan(dim_eq_zero_iff_field).lean b/CommAlg/sayantan(dim_eq_zero_iff_field).lean index 35f197f..fd712f0 100644 --- a/CommAlg/sayantan(dim_eq_zero_iff_field).lean +++ b/CommAlg/sayantan(dim_eq_zero_iff_field).lean @@ -68,7 +68,7 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this rw [←Set.one_le_chainHeight_iff] at this exact not_le_of_gt (Iff.mp ENat.one_le_iff_pos this) - have zero_height : (Set.chainHeight {J | J < P'}) ≤ 0 := by + have nonpos_height : (Set.chainHeight {J | J < P'}) ≤ 0 := by have : (⨆ (I : PrimeSpectrum D), (Set.chainHeight {J | J < I} : WithBot ℕ∞)) ≤ 0 := h.le rw [iSup_le_iff] at this exact Iff.mp WithBot.coe_le_zero (this P') From 1ed0a5499c1d1203fd54eda9cddecc76c154cdd1 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Tue, 13 Jun 2023 21:43:06 +0000 Subject: [PATCH 65/80] added krullDim_nonneg_of_nontrivial to krull --- CommAlg/krull.lean | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 440ea66..c355b30 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -39,7 +39,7 @@ lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ show J' < J exact lt_of_lt_of_le hJ' I_le_J -lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) : +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 : ℕ∞) : @@ -94,6 +94,11 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by . rw [h.forall_iff] trivial +lemma krullDim_nonneg_of_nontrivial [Nontrivial R] : ∃ n : ℕ∞, Ideal.krullDim R = n := by + have h := dim_eq_bot_iff.not.mpr (not_subsingleton R) + lift (Ideal.krullDim R) to ℕ∞ using h with k + use k + lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry #check Ring.DimensionLEOne From 81bc507768b55b8829cd82edb811d20b3375ef26 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Tue, 13 Jun 2023 15:03:28 -0700 Subject: [PATCH 66/80] keep working --- .DS_Store | Bin 6148 -> 6148 bytes 1 file changed, 0 insertions(+), 0 deletions(-) diff --git a/.DS_Store b/.DS_Store index 6d98085373769dd4c6eebf58c63f4db066814689..4d3a1f281d5e07d2e291de80d019305e81afbbf8 100644 GIT binary patch delta 18 acmZoMXfc?uV&ldz_K6Lgo7p-3@&f=#eg{YZ delta 20 ccmZoMXfc?uf{}6K#xVAY4IG= Date: Tue, 13 Jun 2023 16:00:58 -0700 Subject: [PATCH 67/80] added two lemmas --- CommAlg/sameer(artinian-rings).lean | 59 +++++++++++++++++++++++++++-- 1 file changed, 56 insertions(+), 3 deletions(-) diff --git a/CommAlg/sameer(artinian-rings).lean b/CommAlg/sameer(artinian-rings).lean index 381680b..e6bb667 100644 --- a/CommAlg/sameer(artinian-rings).lean +++ b/CommAlg/sameer(artinian-rings).lean @@ -3,13 +3,66 @@ import Mathlib.RingTheory.Noetherian import Mathlib.RingTheory.Artinian import Mathlib.RingTheory.Ideal.Quotient import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.RingTheory.DedekindDomain.DVR + + +lemma FieldisArtinian (R : Type _) [CommRing R] (IsField : ):= by sorry + + +lemma ArtinianDomainIsField (R : Type _) [CommRing R] [IsDomain R] +(IsArt : IsArtinianRing R) : IsField (R) := by +-- Assume P is nonzero and R is Artinian +-- Localize at P; Then R_P is Artinian; +-- Assume R_P is not a field +-- Then Jacobson Radical of R_P is nilpotent so it's maximal ideal is nilpotent +-- Maximal ideal is zero since local ring is a domain +-- a contradiction since P is nonzero +-- Therefore, R is a field +have maxIdeal := Ideal.exists_maximal R +obtain ⟨m,hm⟩ := maxIdeal +have h:= Ideal.primeCompl_le_nonZeroDivisors m +have artRP : IsDomain _ := IsLocalization.isDomain_localization h +have h' : IsArtinianRing (Localization (Ideal.primeCompl m)) := inferInstance +have h' : IsNilpotent (Ideal.jacobson (⊥ : Ideal (Localization + (Ideal.primeCompl m)))):= IsArtinianRing.isNilpotent_jacobson_bot +have := LocalRing.jacobson_eq_maximalIdeal (⊥ : Ideal (Localization + (Ideal.primeCompl m))) bot_ne_top +rw [this] at h' +have := IsNilpotent.eq_zero h' +rw [Ideal.zero_eq_bot, ← LocalRing.isField_iff_maximalIdeal_eq] at this +by_contra h'' +--by_cases h'' : m = ⊥ +have := Ring.ne_bot_of_isMaximal_of_not_isField hm h'' +have := IsLocalization.AtPrime.not_isField R this (Localization (Ideal.primeCompl m)) +contradiction -lemma quotientRing_is_Artinian (R : Type _) [CommRing R] (I : Ideal R) (IsArt : IsArtinianRing R): -IsArtinianRing (R⧸I) := by sorry #check Ideal.IsPrime +#check IsDomain + +lemma isArtinianRing_of_quotient_of_artinian (R : Type _) [CommRing R] + (I : Ideal R) (IsArt : IsArtinianRing R) : IsArtinianRing (R ⧸ I) := + isArtinian_of_tower R (isArtinian_of_quotient_of_artinian R R I IsArt) + +lemma IsPrimeMaximal (R : Type _) [CommRing R] (P : Ideal R) +(IsArt : IsArtinianRing R) (isPrime : Ideal.IsPrime P) : Ideal.IsMaximal P := +by +-- if R is Artinian and P is prime then R/P is Integral Domain +-- which is Artinian Domain +-- R⧸P is a field by the above lemma +-- P is maximal + + have : IsDomain (R⧸P) := Ideal.Quotient.isDomain P + have artRP : IsArtinianRing (R⧸P) := by + exact isArtinianRing_of_quotient_of_artinian R P IsArt + + +-- Then R/I is Artinian + -- have' : IsArtinianRing R ∧ Ideal.IsPrime I → IsDomain (R⧸I) := by + +-- R⧸I.IsArtinian → monotone_stabilizes_iff_artinian.R⧸I + -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 From 55ea06c1419d46c5399997a0a67c6d619d5b5d2c Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Tue, 13 Jun 2023 17:21:42 -0700 Subject: [PATCH 68/80] add more stuff --- CommAlg/jayden(krull-dim-zero).lean | 203 +++++++++++++++++++--------- 1 file changed, 138 insertions(+), 65 deletions(-) diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean index 3651102..6f282ba 100644 --- a/CommAlg/jayden(krull-dim-zero).lean +++ b/CommAlg/jayden(krull-dim-zero).lean @@ -1,97 +1,170 @@ import Mathlib.RingTheory.Ideal.Basic +import Mathlib.RingTheory.Ideal.Operations import Mathlib.RingTheory.JacobsonIdeal import Mathlib.RingTheory.Noetherian import Mathlib.Order.KrullDimension import Mathlib.RingTheory.Artinian import Mathlib.RingTheory.Ideal.Quotient import Mathlib.RingTheory.Nilpotent -import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic import Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian import Mathlib.Data.Finite.Defs import Mathlib.Order.Height import Mathlib.RingTheory.DedekindDomain.Basic import Mathlib.RingTheory.Localization.AtPrime import Mathlib.Order.ConditionallyCompleteLattice.Basic import Mathlib.Algebra.Ring.Pi -import Mathlib.Topology.NoetherianSpace +import Mathlib.RingTheory.Finiteness + --- copy from krull.lean; the name of Krull dimension for rings is changed to krullDim' since krullDim already exists in the librrary namespace Ideal -variable (R : Type _) [CommRing R] (I : PrimeSpectrum R) +variable (R : Type _) [CommRing R] (P : PrimeSpectrum R) -noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} - -noncomputable def krullDim' (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height R I --- copy ends - --- 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 sorry - - -#check IsNoetherianRing - -#check krullDim - --- Repeats the definition of the length of a module by Monalisa -variable (M : Type _) [AddCommMonoid M] [Module R M] - --- change the definition of length -noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < ⊤} - -#check length --- Stacks Lemma 10.53.6: R is Artinian iff R has finite length as an R-mod -lemma IsArtinian_iff_finite_length : IsArtinianRing R ↔ ∃ n : ℕ, length R R ≤ n := by sorry - --- Stacks Lemma 10.53.3: R is Artinian iff R has finitely many maximal ideals -lemma IsArtinian_iff_finite_max_ideal : IsArtinianRing R ↔ Finite (MaximalSpectrum R) := by sorry - --- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent -lemma Jacobson_of_Artinian_is_nilpotent : IsArtinianRing R → IsNilpotent (Ideal.jacobson (⊤ : Ideal R)) := by sorry - - --- Stacks Definition 10.32.1: An ideal is locally nilpotent --- if every element is nilpotent -namespace Ideal -class IsLocallyNilpotent (I : Ideal R) : Prop := - h : ∀ x ∈ I, IsNilpotent x - -end Ideal - -#check Ideal.IsLocallyNilpotent - --- Stacks Lemma 10.53.5: If R has finitely many maximal ideals and --- locally nilpotent Jacobson radical, then R is the product of its localizations at --- its maximal ideals. Also, all primes are maximal - -lemma product_of_localization_at_maximal_ideal : Finite (MaximalSpectrum R) - ∧ Ideal.IsLocallyNilpotent (Ideal.jacobson (⊤ : Ideal R)) → Pi.commRing (MaximalSpectrum R) Localization.AtPrime R I - := by sorry --- Haven't finished this. - --- Stacks Lemma 10.31.5: R is Noetherian iff Spec(R) is a Noetherian space -lemma ring_Noetherian_iff_spec_Noetherian : IsNoetherianRing R - ↔ TopologicalSpace.NoetherianSpace (PrimeSpectrum R) := by sorry --- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible : --- Every closed subset of a noetherian space is a finite union --- of irreducible closed subsets. +noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < P} +noncomputable def krullDim (R : Type) [CommRing R] : + WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height R I -- Stacks Lemma 10.26.1 (Should already exists) -- (1) The closure of a prime P is V(P) -- (2) the irreducible closed subsets are V(P) for P prime -- (3) the irreducible components are V(P) for P minimal prime --- Stacks Lemma 10.32.5: R Noetherian. I,J ideals. If J ⊂ √I, then J ^ n ⊂ I for some n +-- Stacks Definition 10.32.1: An ideal is locally nilpotent +-- if every element is nilpotent +class IsLocallyNilpotent (I : Ideal R) : Prop := + h : ∀ x ∈ I, IsNilpotent x +#check Ideal.IsLocallyNilpotent +end Ideal + + +-- Repeats the definition of the length of a module by Monalisa +variable (R : Type _) [CommRing R] (I J : Ideal R) +variable (M : Type _) [AddCommMonoid M] [Module R M] + +-- change the definition of length of a module +namespace Module +noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < ⊤} +end Module + +-- Stacks Lemma 10.31.5: R is Noetherian iff Spec(R) is a Noetherian space +example [IsNoetherianRing R] : + TopologicalSpace.NoetherianSpace (PrimeSpectrum R) := + inferInstance + +instance ring_Noetherian_of_spec_Noetherian + [TopologicalSpace.NoetherianSpace (PrimeSpectrum R)] : + IsNoetherianRing R where + noetherian := by sorry + +lemma ring_Noetherian_iff_spec_Noetherian : IsNoetherianRing R + ↔ TopologicalSpace.NoetherianSpace (PrimeSpectrum R) := by + constructor + intro RisNoetherian + -- how do I apply an instance to prove one direction? + + +-- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible : +-- Every closed subset of a noetherian space is a finite union +-- of irreducible closed subsets. + +-- Stacks Lemma 10.32.5: R Noetherian. I,J ideals. +-- If J ⊂ √I, then J ^ n ⊂ I for some n. In particular, locally nilpotent +-- and nilpotent are the same for Noetherian rings +lemma containment_radical_power_containment : + IsNoetherianRing R ∧ J ≤ Ideal.radical I → ∃ n : ℕ, J ^ n ≤ I := by + rintro ⟨RisNoetherian, containment⟩ + rw [isNoetherianRing_iff_ideal_fg] at RisNoetherian + specialize RisNoetherian (Ideal.radical I) + rcases RisNoetherian with ⟨S, Sgenerates⟩ + + -- how to I get a generating set? + +-- Stacks Lemma 10.52.6: I is a maximal ideal and IM = 0. Then length of M is +-- + +-- Stacks Lemma 10.52.8: I is a finitely generated maximal ideal of R. +-- M is a finite R-mod and I^nM=0. Then length of M is finite. +lemma power_zero_finite_length : Ideal.FG I → Ideal.IsMaximal I → Module.Finite R M + → (∃ n : ℕ, (I ^ n) • (⊤ : Submodule R M) = 0) + → (∃ m : ℕ, Module.length R M ≤ m) := by + intro IisFG IisMaximal MisFinite power + rcases power with ⟨n, npower⟩ + -- how do I get a generating set? + + +-- Stacks Lemma 10.53.3: R is Artinian iff R has finitely many maximal ideals +lemma IsArtinian_iff_finite_max_ideal : + IsArtinianRing R ↔ Finite (MaximalSpectrum R) := by sorry + +-- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent +lemma Jacobson_of_Artinian_is_nilpotent : + IsArtinianRing R → IsNilpotent (Ideal.jacobson (⊤ : Ideal R)) := by sorry + +-- Stacks Lemma 10.53.5: If R has finitely many maximal ideals and +-- locally nilpotent Jacobson radical, then R is the product of its localizations at +-- its maximal ideals. Also, all primes are maximal + +-- lemma product_of_localization_at_maximal_ideal : Finite (MaximalSpectrum R) +-- ∧ + +def jaydensRing : Type _ := sorry + -- ∀ I : MaximalSpectrum R, Localization.AtPrime R I + +instance : CommRing jaydensRing := sorry -- this should come for free, don't even need to state it + +def foo : jaydensRing ≃+* R where + toFun := _ + invFun := _ + left_inv := _ + right_inv := _ + map_mul' := _ + map_add' := _ + -- Ideal.IsLocallyNilpotent (Ideal.jacobson (⊤ : Ideal R)) → + -- Pi.commRing (MaximalSpectrum R) Localization.AtPrime R I + -- := by sorry +-- Haven't finished this. + +-- Stacks Lemma 10.53.6: R is Artinian iff R has finite length as an R-mod +lemma IsArtinian_iff_finite_length : + IsArtinianRing R ↔ (∃ n : ℕ, Module.length R R ≤ n) := by sorry + +-- Lemma: if R has finite length as R-mod, then R is Noetherian +lemma finite_length_is_Noetherian : + (∃ n : ℕ, Module.length R R ≤ n) → IsNoetherianRing R := by sorry + +-- Lemma: if R is Artinian then all the prime ideals are maximal +lemma primes_of_Artinian_are_maximal : + IsArtinianRing R → Ideal.IsPrime I → Ideal.IsMaximal I := by sorry + +-- Lemma: Krull dimension of a ring is the supremum of height of maximal ideals + + +-- 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 ∧ Ideal.krullDim R = 0 ↔ IsArtinianRing R := by + constructor + sorry + intro RisArtinian + constructor + apply finite_length_is_Noetherian + rwa [IsArtinian_iff_finite_length] at RisArtinian + sorry + + + + + + + + + + --- how to use namespace -namespace something -end something -open something From 23064c442b509a300c75e215dffc266f065d5ea0 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 19:55:50 -0700 Subject: [PATCH 69/80] Little bit of golfing --- CommAlg/krull.lean | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 78e2a36..24251ab 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -130,8 +130,6 @@ lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by simp [field_prime_height_zero] lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by - unfold krullDim at h - simp [height] at h by_contra x rw [Ring.not_isField_iff_exists_prime] at x obtain ⟨P, ⟨h1, primeP⟩⟩ := x @@ -140,16 +138,16 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) by_contra a have : P = ⊥ := by rwa [PrimeSpectrum.ext_iff] at a contradiction - have PgtBot : P' > ⊥ := Ne.bot_lt h2 - have pos_height : ¬ ↑(Set.chainHeight {J | J < P'}) ≤ 0 := by - have : ⊥ ∈ {J | J < P'} := PgtBot + have pos_height : ¬ (height P') ≤ 0 := by + have : ⊥ ∈ {J | J < P'} := Ne.bot_lt h2 have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this + unfold height rw [←Set.one_le_chainHeight_iff] at this exact not_le_of_gt (Iff.mp ENat.one_le_iff_pos this) - have nonpos_height : (Set.chainHeight {J | J < P'}) ≤ 0 := by - have : (⨆ (I : PrimeSpectrum D), (Set.chainHeight {J | J < I} : WithBot ℕ∞)) ≤ 0 := h.le - rw [iSup_le_iff] at this - exact Iff.mp WithBot.coe_le_zero (this P') + have nonpos_height : height P' ≤ 0 := by + have := height_le_krullDim P' + rw [h] at this + aesop contradiction lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by @@ -167,10 +165,10 @@ lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1 exact Ring.DimensionLEOne.principal_ideal_ring R lemma dim_le_dim_polynomial_add_one [Nontrivial R] : - krullDim R ≤ krullDim (Polynomial R) + 1 := sorry + krullDim R + 1 ≤ krullDim (Polynomial R) := sorry lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : - krullDim R = krullDim (Polynomial R) + 1 := sorry + krullDim R + 1 = krullDim (Polynomial R) := sorry lemma height_eq_dim_localization : height I = krullDim (Localization.AtPrime I.asIdeal) := sorry From 06a491b8437fa18bddee734ecbaaad74ad1636dd Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 19:58:28 -0700 Subject: [PATCH 70/80] del: Deleted temp working file --- CommAlg/sayantan(dim_eq_zero_iff_field).lean | 82 -------------------- 1 file changed, 82 deletions(-) delete mode 100644 CommAlg/sayantan(dim_eq_zero_iff_field).lean diff --git a/CommAlg/sayantan(dim_eq_zero_iff_field).lean b/CommAlg/sayantan(dim_eq_zero_iff_field).lean deleted file mode 100644 index fd712f0..0000000 --- a/CommAlg/sayantan(dim_eq_zero_iff_field).lean +++ /dev/null @@ -1,82 +0,0 @@ -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 -import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic -import Mathlib.Order.ConditionallyCompleteLattice.Basic - -namespace Ideal - -variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) -noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} -noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I - -lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl -lemma krullDim_def (R : Type) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl -lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl - -@[simp] -lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by - constructor - · intro primeP - obtain T := eq_bot_or_top P - have : ¬P = ⊤ := IsPrime.ne_top primeP - tauto - · intro botP - rw [botP] - exact bot_prime - -lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : height P = 0 := by - unfold height - simp - by_contra spec - change _ ≠ _ at spec - rw [← Set.nonempty_iff_ne_empty] at spec - obtain ⟨J, JlP : J < P⟩ := spec - have P0 : IsPrime P.asIdeal := P.IsPrime - have J0 : IsPrime J.asIdeal := J.IsPrime - rw [field_prime_bot] at P0 J0 - have : J.asIdeal = P.asIdeal := Eq.trans J0 (Eq.symm P0) - have : J = P := PrimeSpectrum.ext J P this - have : J ≠ P := ne_of_lt JlP - contradiction - -lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by - unfold krullDim - simp [field_prime_height_zero] - -noncomputable -instance : CompleteLattice (WithBot ℕ∞) := - inferInstanceAs <| CompleteLattice (WithBot (WithTop ℕ)) - -lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by - unfold krullDim at h - simp [height] at h - by_contra x - rw [Ring.not_isField_iff_exists_prime] at x - obtain ⟨P, ⟨h1, primeP⟩⟩ := x - let P' : PrimeSpectrum D := PrimeSpectrum.mk P primeP - have h2 : P' ≠ ⊥ := by - by_contra a - have : P = ⊥ := by rwa [PrimeSpectrum.ext_iff] at a - contradiction - have PgtBot : P' > ⊥ := Ne.bot_lt h2 - have pos_height : ¬ ↑(Set.chainHeight {J | J < P'}) ≤ 0 := by - have : ⊥ ∈ {J | J < P'} := PgtBot - have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this - rw [←Set.one_le_chainHeight_iff] at this - exact not_le_of_gt (Iff.mp ENat.one_le_iff_pos this) - have nonpos_height : (Set.chainHeight {J | J < P'}) ≤ 0 := by - have : (⨆ (I : PrimeSpectrum D), (Set.chainHeight {J | J < I} : WithBot ℕ∞)) ≤ 0 := h.le - rw [iSup_le_iff] at this - exact Iff.mp WithBot.coe_le_zero (this P') - contradiction - -lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by - constructor - · exact isField.dim_zero - · intro fieldD - let h : Field D := IsField.toField fieldD - exact dim_field_eq_zero From 2c3d2d84a374a1ac81dd7777fed50cfc28d086a5 Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Wed, 14 Jun 2023 03:03:10 +0000 Subject: [PATCH 71/80] TEST --- .docker/test.lean | 133 +++++++++++++++++++++++++++++++++++++++++++ comm_alg/Defhil.lean | 29 ---------- comm_alg/hilpol.lean | 41 ------------- 3 files changed, 133 insertions(+), 70 deletions(-) create mode 100644 .docker/test.lean delete mode 100644 comm_alg/Defhil.lean delete mode 100644 comm_alg/hilpol.lean diff --git a/.docker/test.lean b/.docker/test.lean new file mode 100644 index 0000000..a851192 --- /dev/null +++ b/.docker/test.lean @@ -0,0 +1,133 @@ +import Mathlib.Order.KrullDimension +import Mathlib.Order.JordanHolder +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Order.Height +import Mathlib.RingTheory.Ideal.Basic +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.LinearAlgebra.Finsupp +import Mathlib.RingTheory.GradedAlgebra.Basic +import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal +import Mathlib.Algebra.Module.GradedModule +import Mathlib.RingTheory.Ideal.AssociatedPrime +import Mathlib.RingTheory.Noetherian +import Mathlib.RingTheory.Artinian +import Mathlib.Algebra.Module.GradedModule +import Mathlib.RingTheory.Noetherian +import Mathlib.RingTheory.Finiteness +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.RingTheory.FiniteType +import Mathlib.Order.Height +import Mathlib.RingTheory.PrincipalIdealDomain +import Mathlib.RingTheory.DedekindDomain.Basic +import Mathlib.RingTheory.Ideal.Quotient +import Mathlib.RingTheory.Localization.AtPrime +import Mathlib.Order.ConditionallyCompleteLattice.Basic +import Mathlib.Algebra.DirectSum.Ring +import Mathlib.RingTheory.Ideal.LocalRing +import Mathlib +import Mathlib.Algebra.MonoidAlgebra.Basic +import Mathlib.Data.Finset.Sort +import Mathlib.Order.Height +import Mathlib.Order.KrullDimension +import Mathlib.Order.JordanHolder +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Order.Height +import Mathlib.RingTheory.Ideal.Basic +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.LinearAlgebra.Finsupp +import Mathlib.RingTheory.GradedAlgebra.Basic +import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal +import Mathlib.Algebra.Module.GradedModule +import Mathlib.RingTheory.Ideal.AssociatedPrime +import Mathlib.RingTheory.Noetherian +import Mathlib.RingTheory.Artinian +import Mathlib.Algebra.Module.GradedModule +import Mathlib.RingTheory.Noetherian +import Mathlib.RingTheory.Finiteness +import Mathlib.RingTheory.Ideal.Operations + + + + +noncomputable def length ( A : Type _) (M : Type _) + [CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < ⊤} + + +def HomogeneousPrime { A σ : Type _} [CommRing A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ) [GradedRing 𝒜] (I : Ideal A):= (Ideal.IsPrime I) ∧ (Ideal.IsHomogeneous 𝒜 I) + + +def HomogeneousMax { A σ : Type _} [CommRing A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ) [GradedRing 𝒜] (I : Ideal A):= (Ideal.IsMaximal I) ∧ (Ideal.IsHomogeneous 𝒜 I) + +--theorem monotone_stabilizes_iff_noetherian : +-- (∀ f : ℕ →o Submodule R M, ∃ n, ∀ m, n ≤ m → f n = f m) ↔ IsNoetherian R M := by +-- rw [isNoetherian_iff_wellFounded, WellFounded.monotone_chain_condition] + +open GradedMonoid.GSmul + +open DirectSum + +instance tada1 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] + [DirectSum.Gmodule 𝒜 𝓜] (i : ℤ ) : SMul (𝒜 0) (𝓜 i) + where smul x y := @Eq.rec ℤ (0+i) (fun a _ => 𝓜 a) (GradedMonoid.GSmul.smul x y) i (zero_add i) + +lemma mylem (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] + [h : DirectSum.Gmodule 𝒜 𝓜] (i : ℤ) (a : 𝒜 0) (m : 𝓜 i) : + of _ _ (a • m) = of _ _ a • of _ _ m := by + refine' Eq.trans _ (Gmodule.of_smul_of 𝒜 𝓜 a m).symm + refine' of_eq_of_gradedMonoid_eq _ + exact Sigma.ext (zero_add _).symm <| eq_rec_heq _ _ + +instance tada2 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] + [h : DirectSum.Gmodule 𝒜 𝓜] (i : ℤ ) : SMulWithZero (𝒜 0) (𝓜 i) := by + letI := SMulWithZero.compHom (⨁ i, 𝓜 i) (of 𝒜 0).toZeroHom + exact Function.Injective.smulWithZero (of 𝓜 i).toZeroHom Dfinsupp.single_injective (mylem 𝒜 𝓜 i) + +instance tada3 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] + [h : DirectSum.Gmodule 𝒜 𝓜] (i : ℤ ): Module (𝒜 0) (𝓜 i) := by + letI := Module.compHom (⨁ j, 𝓜 j) (ofZeroRingHom 𝒜) + exact Dfinsupp.single_injective.module (𝒜 0) (of 𝓜 i) (mylem 𝒜 𝓜 i) + +noncomputable def hilbert_function (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] + [DirectSum.GCommRing 𝒜] + [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) + : ℤ → ℕ∞ := fun i => (length (𝒜 0) (𝓜 i)) + +lemma hilbertz (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] + [DirectSum.GCommRing 𝒜] + [DirectSum.Gmodule 𝒜 𝓜] + (finlen : ∀ i, (length (𝒜 0) (𝓜 i)) < ⊤ ) : ℤ → ℤ := by + intro i + let h := hilbert_function 𝒜 𝓜 + simp at h + let n : ℤ → ℕ := fun i ↦ WithTop.untop _ (finlen i).ne + have hn : ∀ i, (n i : ℕ∞) = length (𝒜 0) (𝓜 i) := fun i ↦ WithTop.coe_untop _ _ + have' := hn i + exact ((n i) : ℤ ) + + + +noncomputable def dimensionring { A: Type _} + [CommRing A] := krullDim (PrimeSpectrum A) + + +noncomputable def dimensionmodule ( A : Type _) (M : Type _) + [CommRing A] [AddCommGroup M] [Module A M] := krullDim (PrimeSpectrum (A ⧸ ((⊤ : Submodule A M).annihilator)) ) + +-- lemma graded_local (𝒜 : ℤ → Type _) [SetLike (⨁ i, 𝒜 i)] (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] +-- [DirectSum.GCommRing 𝒜] +-- [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) : ∃ ( I : Ideal ((⨁ i, 𝒜 i))),(HomogeneousMax 𝒜 I) := sorry + + +def PolyType (f : ℤ → ℤ) (d : ℕ) := ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), ∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly ∧ d = Polynomial.degree Poly + + + +theorem hilbert_polynomial (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] +[DirectSum.GCommRing 𝒜] +[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) (fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) +(findim : ∃ d : ℕ , dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = d):True := sorry + +-- Semiring A] + +-- variable [SetLike σ A] \ No newline at end of file diff --git a/comm_alg/Defhil.lean b/comm_alg/Defhil.lean deleted file mode 100644 index 65da0c6..0000000 --- a/comm_alg/Defhil.lean +++ /dev/null @@ -1,29 +0,0 @@ -import Mathlib -import Mathlib.RingTheory.Ideal.Basic -import Mathlib.RingTheory.Ideal.Operations -import Mathlib.LinearAlgebra.Finsupp -import Mathlib.RingTheory.GradedAlgebra.Basic -import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal - - - - -variable {R : Type _} (M A B C : Type _) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B] [AddCommGroup C] [Module R C] - - -#check (A B : Submodule _ _) → (A ≤ B) - -#check Preorder (Submodule _ _) - -#check krullDim (Submodule _ _) - -noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < ⊤} - -open LinearMap - -#check length M - - - ---lemma length_additive_shortexact {f : A ⟶ B} {g : B ⟶ C} (h : ShortExact f g) : length B = length A + length C := sorry - diff --git a/comm_alg/hilpol.lean b/comm_alg/hilpol.lean deleted file mode 100644 index 0aab559..0000000 --- a/comm_alg/hilpol.lean +++ /dev/null @@ -1,41 +0,0 @@ -import Mathlib.Order.KrullDimension -import Mathlib.Order.JordanHolder -import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic -import Mathlib.Order.Height -import Mathlib.RingTheory.Ideal.Basic -import Mathlib.RingTheory.Ideal.Operations -import Mathlib.LinearAlgebra.Finsupp -import Mathlib.RingTheory.GradedAlgebra.Basic -import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal -import Mathlib.Algebra.Module.GradedModule -import Mathlib.RingTheory.Ideal.AssociatedPrime -import Mathlib.RingTheory.Noetherian - -variable {ι σ R A : Type _} - -section HomogeneousDef - -variable [Semiring A] - -variable [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ) - -variable [GradedRing 𝒜] - -variable (I : HomogeneousIdeal 𝒜) - --- def Ideal.IsHomogeneous : Prop := --- ∀ (i : ι) ⦃r : A⦄, r ∈ I → (DirectSum.decompose 𝒜 r i : A) ∈ I --- #align ideal.is_homogeneous Ideal.IsHomogeneous - --- structure HomogeneousIdeal extends Submodule A A where --- is_homogeneous' : Ideal.IsHomogeneous 𝒜 toSubmodule - ---#check Ideal.IsPrime hI - -def HomogeneousPrime (I : Ideal A):= Ideal.IsPrime I - -def HomogeneousMax (I : Ideal A):= Ideal.IsMaximal I - ---theorem monotone_stabilizes_iff_noetherian : --- (∀ f : ℕ →o Submodule R M, ∃ n, ∀ m, n ≤ m → f n = f m) ↔ IsNoetherian R M := by --- rw [isNoetherian_iff_wellFounded, WellFounded.monotone_chain_condition] \ No newline at end of file From d30702fb10a79ca854f1feb58037082377e0529a Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Wed, 14 Jun 2023 03:45:23 +0000 Subject: [PATCH 72/80] updated def --- .docker/test.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.docker/test.lean b/.docker/test.lean index a851192..888270c 100644 --- a/.docker/test.lean +++ b/.docker/test.lean @@ -88,10 +88,11 @@ instance tada3 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGr letI := Module.compHom (⨁ j, 𝓜 j) (ofZeroRingHom 𝒜) exact Dfinsupp.single_injective.module (𝒜 0) (of 𝓜 i) (mylem 𝒜 𝓜 i) + -- (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) + noncomputable def hilbert_function (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] - [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) - : ℤ → ℕ∞ := fun i => (length (𝒜 0) (𝓜 i)) + [DirectSum.Gmodule 𝒜 𝓜] (hilb : ℤ → ℕ∞) := ∀ i, hilb i = (length (𝒜 0) (𝓜 i)) lemma hilbertz (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] From 50aa1b07a8a3dbfb712765e822db7a368bcdbce3 Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Tue, 13 Jun 2023 20:58:32 -0700 Subject: [PATCH 73/80] moved krullDim_nonneg_of_nontrivial to krull.lean --- CommAlg/krull.lean | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 2a87c16..4e5ac3a 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -94,6 +94,17 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by . rw [h.forall_iff] trivial +lemma krullDim_nonneg_of_nontrivial (R : Type _) [CommRing R] [Nontrivial R] : ∃ n : ℕ∞, Ideal.krullDim R = n := by + have h := dim_eq_bot_iff.not.mpr (not_subsingleton R) + lift (Ideal.krullDim R) to ℕ∞ using h with k + use k + +lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by + constructor <;> intro h + . intro I + sorry + . sorry + lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry #check Ring.DimensionLEOne @@ -104,10 +115,10 @@ lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1 exact Ring.DimensionLEOne.principal_ideal_ring R lemma dim_le_dim_polynomial_add_one [Nontrivial R] : - krullDim R ≤ krullDim (Polynomial R) + 1 := sorry + krullDim R + 1 ≤ krullDim (Polynomial R) := sorry lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : - krullDim R = krullDim (Polynomial R) + 1 := sorry + krullDim R + 1 = krullDim (Polynomial R) := sorry lemma height_eq_dim_localization : height I = krullDim (Localization.AtPrime I.asIdeal) := sorry From 4d2aeea2c2739003c9b15337115a8bc96840671f Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Tue, 13 Jun 2023 21:17:54 -0700 Subject: [PATCH 74/80] more updates --- CommAlg/jayden(krull-dim-zero).lean | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean index 6f282ba..523eb90 100644 --- a/CommAlg/jayden(krull-dim-zero).lean +++ b/CommAlg/jayden(krull-dim-zero).lean @@ -77,12 +77,25 @@ lemma containment_radical_power_containment : rintro ⟨RisNoetherian, containment⟩ rw [isNoetherianRing_iff_ideal_fg] at RisNoetherian specialize RisNoetherian (Ideal.radical I) - rcases RisNoetherian with ⟨S, Sgenerates⟩ + -- rcases RisNoetherian with ⟨S, Sgenerates⟩ + have containment2 : ∃ n : ℕ, (Ideal.radical I) ^ n ≤ I := by + apply Ideal.exists_radical_pow_le_of_fg I RisNoetherian + cases' containment2 with n containment2' + have containment3 : J ^ n ≤ (Ideal.radical I) ^ n := by + apply Ideal.pow_mono containment + use n + apply le_trans containment3 containment2' +-- The above can be proven using the following quicker theorem that is in the wrong place. +-- Ideal.exists_pow_le_of_le_radical_of_fG - -- how to I get a generating set? -- Stacks Lemma 10.52.6: I is a maximal ideal and IM = 0. Then length of M is --- +-- the same as the dimension as a vector space over R/I, +lemma length_eq_dim_if_maximal_annihilates {I : Ideal R} [Ideal.IsMaximal I] + : I • (⊤ : Submodule R M) = 0 + → Module.length R M = Module.rank R⧸I M⧸(I • (⊤ : Submodule R M)) := by sorry + +-- Does lean know that M/IM is a R/I module? -- Stacks Lemma 10.52.8: I is a finitely generated maximal ideal of R. -- M is a finite R-mod and I^nM=0. Then length of M is finite. From b6bbf7af8c1d08ac35f49898d632f4cedb1d8f9a Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Wed, 14 Jun 2023 04:49:17 +0000 Subject: [PATCH 75/80] udpated def final --- .docker/test.lean | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/.docker/test.lean b/.docker/test.lean index 888270c..d3a272e 100644 --- a/.docker/test.lean +++ b/.docker/test.lean @@ -90,16 +90,17 @@ instance tada3 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGr -- (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) -noncomputable def hilbert_function (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] +noncomputable def dummyhil_function (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] (hilb : ℤ → ℕ∞) := ∀ i, hilb i = (length (𝒜 0) (𝓜 i)) + lemma hilbertz (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] (finlen : ∀ i, (length (𝒜 0) (𝓜 i)) < ⊤ ) : ℤ → ℤ := by intro i - let h := hilbert_function 𝒜 𝓜 + let h := dummyhil_function 𝒜 𝓜 simp at h let n : ℤ → ℕ := fun i ↦ WithTop.untop _ (finlen i).ne have hn : ∀ i, (n i : ℕ∞) = length (𝒜 0) (𝓜 i) := fun i ↦ WithTop.coe_untop _ _ @@ -107,6 +108,11 @@ lemma hilbertz (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGr exact ((n i) : ℤ ) +noncomputable def hilbert_function (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] + [DirectSum.GCommRing 𝒜] + [DirectSum.Gmodule 𝒜 𝓜] (hilb : ℤ → ℤ) := ∀ i, hilb i = (ENat.toNat (length (𝒜 0) (𝓜 i))) + + noncomputable def dimensionring { A: Type _} [CommRing A] := krullDim (PrimeSpectrum A) From 869ce6aa9f79faf4a6ed950f9f6f326af774274f Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Wed, 14 Jun 2023 04:51:49 +0000 Subject: [PATCH 76/80] proved dim_le_one_of_dimLEOne --- CommAlg/grant.lean | 102 +++++++++++++++++++++++++++++++++++++++++++-- CommAlg/krull.lean | 50 ++++++++++++++++++++++ 2 files changed, 148 insertions(+), 4 deletions(-) diff --git a/CommAlg/grant.lean b/CommAlg/grant.lean index ce5041d..c12b189 100644 --- a/CommAlg/grant.lean +++ b/CommAlg/grant.lean @@ -83,6 +83,16 @@ height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ norm_cast at hc tauto +lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : +height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by + show (_ < _) ↔ _ + rw [WithBot.coe_lt_coe] + exact lt_height_iff' _ + +lemma height_le_iff {𝔭 : PrimeSpectrum R} {n : ℕ∞} : + height 𝔭 ≤ n ↔ ∀ c : List (PrimeSpectrum R), c ∈ {I : PrimeSpectrum R | I < 𝔭}.subchain ∧ c.length = n + 1 := by + sorry + lemma krullDim_nonneg_of_nontrivial [Nontrivial R] : ∃ n : ℕ∞, Ideal.krullDim R = n := by have h := dim_eq_bot_iff.not.mpr (not_subsingleton R) lift (Ideal.krullDim R) to ℕ∞ using h with k @@ -116,19 +126,103 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by constructor <;> intro h . rw [←not_nonempty_iff] rintro ⟨a, ha⟩ - -- specialize h ⟨a, ha⟩ + specialize h ⟨a, ha⟩ tauto . rw [h.forall_iff] trivial - #check (sorry : False) #check (sorryAx) #check (4 : WithBot ℕ∞) #check List.sum +#check (_ ∈ (_ : List _)) +variable (α : Type ) +#synth Membership α (List α) +#check bot_lt_iff_ne_bot -- #check ((4 : ℕ∞) : WithBot (WithTop ℕ)) -- #check ( (Set.chainHeight s) : WithBot (ℕ∞)) -variable (P : PrimeSpectrum R) +/-- The converse of this is false, because the definition of "dimension ≤ 1" in mathlib + applies only to dimension zero rings and domains of dimension 1. -/ +lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ (1 : ℕ) := by + rw [krullDim_le_iff R 1] + -- unfold Ring.DimensionLEOne + intro H p + -- have Hp := H p.asIdeal + -- have Hp := fun h => (Hp h) p.IsPrime + apply le_of_not_gt + intro h + rcases ((lt_height_iff'' R).mp h) with ⟨c, ⟨hc1, hc2, hc3⟩⟩ + norm_cast at hc3 + rw [List.chain'_iff_get] at hc1 + specialize hc1 0 (by rw [hc3]; simp) + -- generalize hq0 : List.get _ _ = q0 at hc1 + set q0 : PrimeSpectrum R := List.get c { val := 0, isLt := _ } + set q1 : PrimeSpectrum R := List.get c { val := 1, isLt := _ } + -- have hq0 : q0 ∈ c := List.get_mem _ _ _ + -- have hq1 : q1 ∈ c := List.get_mem _ _ _ + specialize hc2 q1 (List.get_mem _ _ _) + -- have aa := (bot_le : (⊥ : Ideal R) ≤ q0.asIdeal) + change q0.asIdeal < q1.asIdeal at hc1 + have q1nbot := Trans.trans (bot_le : ⊥ ≤ q0.asIdeal) hc1 + specialize H q1.asIdeal (bot_lt_iff_ne_bot.mp q1nbot) q1.IsPrime + -- change q1.asIdeal < p.asIdeal at hc2 + apply IsPrime.ne_top p.IsPrime + apply (IsCoatom.lt_iff H.out).mp + exact hc2 + --refine Iff.mp radical_eq_top (?_ (id (Eq.symm hc3))) +end Krull -#check {J | J < P}.le_chainHeight_iff (n := 4) +section iSupWithBot + +variable {α : Type _} [CompleteSemilatticeSup α] {I : Type _} (f : I → α) + +#synth SupSet (WithBot ℕ∞) + +protected lemma WithBot.iSup_ge_coe_iff {a : α} : + (a ≤ ⨆ i : I, (f i : WithBot α) ) ↔ ∃ i : I, f i ≥ a := by + rw [WithBot.coe_le_iff] + sorry + +end iSupWithBot + +section myGreatElab +open Lean Meta Elab + +syntax (name := lhsStx) "lhs% " term:max : term +syntax (name := rhsStx) "rhs% " term:max : term + +@[term_elab lhsStx, term_elab rhsStx] +def elabLhsStx : Term.TermElab := fun stx expectedType? => + match stx with + | `(lhs% $t) => do + let (lhs, _, eq) ← mkExpected expectedType? + discard <| Term.elabTermEnsuringType t eq + return lhs + | `(rhs% $t) => do + let (_, rhs, eq) ← mkExpected expectedType? + discard <| Term.elabTermEnsuringType t eq + return rhs + | _ => throwUnsupportedSyntax +where + mkExpected expectedType? := do + let α ← + if let some expectedType := expectedType? then + pure expectedType + else + mkFreshTypeMVar + let lhs ← mkFreshExprMVar α + let rhs ← mkFreshExprMVar α + let u ← getLevel α + let eq := mkAppN (.const ``Eq [u]) #[α, lhs, rhs] + return (lhs, rhs, eq) + +#check lhs% (add_comm 1 2) +#check rhs% (add_comm 1 2) +#check lhs% (add_comm _ _ : _ = 1 + 2) + +example (x y : α) (h : x = y) : lhs% h = rhs% h := h + +def lhsOf {α : Sort _} {x y : α} (h : x = y) : α := x + +#check lhsOf (add_comm 1 2) \ No newline at end of file diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 78e2a36..6f65a93 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -160,8 +160,58 @@ lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = exact dim_field_eq_zero #check Ring.DimensionLEOne +-- This lemma is false! lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry +lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : +height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by + rcases n with _ | n + . constructor <;> intro h <;> exfalso + . exact (not_le.mpr h) le_top + . tauto + have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by + symm + show (n + 1 ≤ m ↔ _ ) + apply ENat.add_one_le_iff + exact ENat.coe_ne_top _ + rw [this] + unfold Ideal.height + show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞)) + rw [{J | J < 𝔭}.le_chainHeight_iff] + show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _ + constructor <;> rintro ⟨c, hc⟩ <;> use c + . tauto + . change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc + norm_cast at hc + tauto + +lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : +height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by + show (_ < _) ↔ _ + rw [WithBot.coe_lt_coe] + exact lt_height_iff' + +/-- The converse of this is false, because the definition of "dimension ≤ 1" in mathlib + applies only to dimension zero rings and domains of dimension 1. -/ +lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ (1 : ℕ) := by + rw [krullDim_le_iff R 1] + intro H p + apply le_of_not_gt + intro h + rcases (lt_height_iff''.mp h) with ⟨c, ⟨hc1, hc2, hc3⟩⟩ + norm_cast at hc3 + rw [List.chain'_iff_get] at hc1 + specialize hc1 0 (by rw [hc3]; simp) + set q0 : PrimeSpectrum R := List.get c { val := 0, isLt := _ } + set q1 : PrimeSpectrum R := List.get c { val := 1, isLt := _ } + specialize hc2 q1 (List.get_mem _ _ _) + change q0.asIdeal < q1.asIdeal at hc1 + have q1nbot := Trans.trans (bot_le : ⊥ ≤ q0.asIdeal) hc1 + specialize H q1.asIdeal (bot_lt_iff_ne_bot.mp q1nbot) q1.IsPrime + apply IsPrime.ne_top p.IsPrime + apply (IsCoatom.lt_iff H.out).mp + exact hc2 + lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1 := by rw [dim_le_one_iff] exact Ring.DimensionLEOne.principal_ideal_ring R From 7c91fd8d3133e1ca2f53716f7a9e9e622b536b77 Mon Sep 17 00:00:00 2001 From: Andre Date: Wed, 14 Jun 2023 01:38:51 -0400 Subject: [PATCH 77/80] fixed hilbertpoly --- comm_alg/test.lean | 137 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 137 insertions(+) create mode 100644 comm_alg/test.lean diff --git a/comm_alg/test.lean b/comm_alg/test.lean new file mode 100644 index 0000000..64650dc --- /dev/null +++ b/comm_alg/test.lean @@ -0,0 +1,137 @@ +import Mathlib.Order.KrullDimension +import Mathlib.Order.JordanHolder +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Order.Height +import Mathlib.RingTheory.Ideal.Basic +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.LinearAlgebra.Finsupp +import Mathlib.RingTheory.GradedAlgebra.Basic +import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal +import Mathlib.Algebra.Module.GradedModule +import Mathlib.RingTheory.Ideal.AssociatedPrime +import Mathlib.RingTheory.Noetherian +import Mathlib.RingTheory.Artinian +import Mathlib.Algebra.Module.GradedModule +import Mathlib.RingTheory.Noetherian +import Mathlib.RingTheory.Finiteness +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.RingTheory.FiniteType +import Mathlib.Order.Height +import Mathlib.RingTheory.PrincipalIdealDomain +import Mathlib.RingTheory.DedekindDomain.Basic +import Mathlib.RingTheory.Ideal.Quotient +import Mathlib.RingTheory.Localization.AtPrime +import Mathlib.Order.ConditionallyCompleteLattice.Basic +import Mathlib.Algebra.DirectSum.Ring +import Mathlib.RingTheory.Ideal.LocalRing + +-- Setting for "library_search" +set_option maxHeartbeats 0 +macro "ls" : tactic => `(tactic|library_search) + +-- New tactic "obviously" +macro "obviously" : tactic => + `(tactic| ( + first + | dsimp; simp; done; dbg_trace "it was dsimp simp" + | simp; done; dbg_trace "it was simp" + | tauto; done; dbg_trace "it was tauto" + | simp; tauto; done; dbg_trace "it was simp tauto" + | rfl; done; dbg_trace "it was rfl" + | norm_num; done; dbg_trace "it was norm_num" + | /-change (@Eq ℝ _ _);-/ linarith; done; dbg_trace "it was linarith" + -- | gcongr; done + | ring; done; dbg_trace "it was ring" + | trivial; done; dbg_trace "it was trivial" + -- | nlinarith; done + | fail "No, this is not obvious.")) + +-- @[BH, 1.5.6 (b)(ii)] +lemma ss (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] + [DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] (p : associatedPrimes (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) : true := by + sorry +-- Ideal.IsHomogeneous 𝒜 p + + + + +noncomputable def length ( A : Type _) (M : Type _) + [CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < ⊤} + + +def HomogeneousPrime { A σ : Type _} [CommRing A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ) [GradedRing 𝒜] (I : Ideal A):= (Ideal.IsPrime I) ∧ (Ideal.IsHomogeneous 𝒜 I) +def HomogeneousMax { A σ : Type _} [CommRing A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ) [GradedRing 𝒜] (I : Ideal A):= (Ideal.IsMaximal I) ∧ (Ideal.IsHomogeneous 𝒜 I) + +--theorem monotone_stabilizes_iff_noetherian : +-- (∀ f : ℕ →o Submodule R M, ∃ n, ∀ m, n ≤ m → f n = f m) ↔ IsNoetherian R M := by +-- rw [isNoetherian_iff_wellFounded, WellFounded.monotone_chain_condition] + +open GradedMonoid.GSmul +open DirectSum + +instance tada1 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] + [DirectSum.Gmodule 𝒜 𝓜] (i : ℤ ) : SMul (𝒜 0) (𝓜 i) + where smul x y := @Eq.rec ℤ (0+i) (fun a _ => 𝓜 a) (GradedMonoid.GSmul.smul x y) i (zero_add i) + +lemma mylem (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] + [h : DirectSum.Gmodule 𝒜 𝓜] (i : ℤ) (a : 𝒜 0) (m : 𝓜 i) : + of _ _ (a • m) = of _ _ a • of _ _ m := by + refine' Eq.trans _ (Gmodule.of_smul_of 𝒜 𝓜 a m).symm + refine' of_eq_of_gradedMonoid_eq _ + exact Sigma.ext (zero_add _).symm <| eq_rec_heq _ _ + +instance tada2 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] + [h : DirectSum.Gmodule 𝒜 𝓜] (i : ℤ ) : SMulWithZero (𝒜 0) (𝓜 i) := by + letI := SMulWithZero.compHom (⨁ i, 𝓜 i) (of 𝒜 0).toZeroHom + exact Function.Injective.smulWithZero (of 𝓜 i).toZeroHom Dfinsupp.single_injective (mylem 𝒜 𝓜 i) + +instance tada3 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] + [h : DirectSum.Gmodule 𝒜 𝓜] (i : ℤ ): Module (𝒜 0) (𝓜 i) := by + letI := Module.compHom (⨁ j, 𝓜 j) (ofZeroRingHom 𝒜) + exact Dfinsupp.single_injective.module (𝒜 0) (of 𝓜 i) (mylem 𝒜 𝓜 i) + +noncomputable def hilbert_function (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] + [DirectSum.GCommRing 𝒜] + [DirectSum.Gmodule 𝒜 𝓜] (hilb : ℤ → ℤ) := ∀ i, hilb i = (ENat.toNat (length (𝒜 0) (𝓜 i))) + +noncomputable def dimensionring { A: Type _} + [CommRing A] := krullDim (PrimeSpectrum A) + + +noncomputable def dimensionmodule ( A : Type _) (M : Type _) + [CommRing A] [AddCommGroup M] [Module A M] := krullDim (PrimeSpectrum (A ⧸ ((⊤ : Submodule A M).annihilator)) ) + +-- lemma graded_local (𝒜 : ℤ → Type _) [SetLike (⨁ i, 𝒜 i)] (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] +-- [DirectSum.GCommRing 𝒜] +-- [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) : ∃ ( I : Ideal ((⨁ i, 𝒜 i))),(HomogeneousMax 𝒜 I) := sorry + + + + +@[simp] +def PolyType (f : ℤ → ℤ) (d : ℕ) := ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), ∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly ∧ d = Polynomial.degree Poly + +-- @[BH, 4.1.3] +theorem hilbert_polynomial (d : ℕ) (d1 : 1 ≤ d) (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] +[DirectSum.GCommRing 𝒜] +[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) +(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) +(findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = d) (hilb : ℤ → ℤ) + (Hhilb: hilbert_function 𝒜 𝓜 hilb) +: PolyType hilb (d - 1) := by + sorry + +-- @ +lemma Graded_quotient (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)][DirectSum.GCommRing 𝒜] + : true := by + sorry + + +-- @Existence of a chain of submodules of graded submoduels of f.g graded R-mod M +lemma Exist_chain_of_graded_submodules (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] + [DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] (fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) + : true := by + sorry +#print Exist_chain_of_graded_submodules +#print Finset \ No newline at end of file From 56cefd9b53ab50541dbd3c088febe0ffd6894d6d Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 22:54:57 -0700 Subject: [PATCH 78/80] Made some progress on dim_eq_dim_polynomial_add_one --- ...yantan(dim_eq_dim_polynomial_add_one).lean | 46 +++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean diff --git a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean new file mode 100644 index 0000000..a9269a2 --- /dev/null +++ b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean @@ -0,0 +1,46 @@ +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 +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Order.ConditionallyCompleteLattice.Basic + +namespace Ideal + +variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) +noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} +noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I + +lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl +lemma krullDim_def (R : Type) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl +lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl + +noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice + +lemma dim_le_dim_polynomial_add_one [Nontrivial R] : + krullDim R + 1 ≤ krullDim (Polynomial R) := sorry -- Others are working on it + +-- private lemma sum_succ_of_succ_sum {ι : Type} (a : ℕ∞) [inst : Nonempty ι] : +-- (⨆ (x : ι), a + 1) = (⨆ (x : ι), a) + 1 := by +-- have : a + 1 = (⨆ (x : ι), a) + 1 := by rw [ciSup_const] +-- have : a + 1 = (⨆ (x : ι), a + 1) := Eq.symm ciSup_const +-- simp + +lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : + krullDim R + 1 = krullDim (Polynomial R) := by + rw [le_antisymm_iff] + constructor + · exact dim_le_dim_polynomial_add_one + · unfold krullDim + have htPBdd : ∀ (P : PrimeSpectrum (Polynomial R)), (height P: WithBot ℕ∞) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by + intro P + unfold height + sorry + have : (⨆ (I : PrimeSpectrum R), ↑(height I) + 1) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by + have : ∀ P : PrimeSpectrum R, ↑(height P) + 1 ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := + fun _ ↦ add_le_add_right (le_iSup height _) 1 + apply iSup_le + exact this + sorry \ No newline at end of file From 39c06f39fde230c4750f93fcfa86297bac41a65d Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Wed, 14 Jun 2023 10:22:14 -0700 Subject: [PATCH 79/80] Develop dim_eq_dim_polynomial_add_one a bit more, with a sorried section --- ...yantan(dim_eq_dim_polynomial_add_one).lean | 22 ++++++++++++------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean index a9269a2..ea6f7cd 100644 --- a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean +++ b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean @@ -34,13 +34,19 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : constructor · exact dim_le_dim_polynomial_add_one · unfold krullDim - have htPBdd : ∀ (P : PrimeSpectrum (Polynomial R)), (height P: WithBot ℕ∞) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by + have htPBdd : ∀ (P : PrimeSpectrum (Polynomial R)), (height P : WithBot ℕ∞) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by intro P - unfold height - sorry - have : (⨆ (I : PrimeSpectrum R), ↑(height I) + 1) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by - have : ∀ P : PrimeSpectrum R, ↑(height P) + 1 ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := - fun _ ↦ add_le_add_right (le_iSup height _) 1 + have : ∃ (I : PrimeSpectrum R), (height P : WithBot ℕ∞) ≤ ↑(height I + 1) := by + sorry + obtain ⟨I, IP⟩ := this + have : (↑(height I + 1) : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum R), ↑(height I + 1) := by + apply @le_iSup (WithBot ℕ∞) _ _ _ I + apply ge_trans this IP + have oneOut : (⨆ (I : PrimeSpectrum R), (height I : WithBot ℕ∞) + 1) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by + have : ∀ P : PrimeSpectrum R, (height P : WithBot ℕ∞) + 1 ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := + fun P ↦ (by apply add_le_add_right (@le_iSup (WithBot ℕ∞) _ _ _ P) 1) apply iSup_le - exact this - sorry \ No newline at end of file + apply this + simp + intro P + exact ge_trans oneOut (htPBdd P) From 0f3f18ef09b2d4e756d39d307aae344dbcc0d33d Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Wed, 14 Jun 2023 17:38:40 +0000 Subject: [PATCH 80/80] moved files into CommAlg --- comm_alg/test.lean => CommAlg/hilbertpolynomial.lean | 0 .docker/test.lean => CommAlg/monalisa.lean | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename comm_alg/test.lean => CommAlg/hilbertpolynomial.lean (100%) rename .docker/test.lean => CommAlg/monalisa.lean (100%) diff --git a/comm_alg/test.lean b/CommAlg/hilbertpolynomial.lean similarity index 100% rename from comm_alg/test.lean rename to CommAlg/hilbertpolynomial.lean diff --git a/.docker/test.lean b/CommAlg/monalisa.lean similarity index 100% rename from .docker/test.lean rename to CommAlg/monalisa.lean