From 50515d9ed8e2aa115ef83b43df1e0f9c3bec3cb3 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Wed, 14 Jun 2023 11:02:02 -0700 Subject: [PATCH 1/6] Completed most of the simple part --- .../sayantan(dim_eq_dim_polynomial_add_one).lean | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean index ea6f7cd..485ee3b 100644 --- a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean +++ b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean @@ -22,11 +22,7 @@ noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.c 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 height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := sorry -- Already done in main file lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : krullDim R + 1 = krullDim (Polynomial R) := by @@ -37,6 +33,15 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : have htPBdd : ∀ (P : PrimeSpectrum (Polynomial R)), (height P : WithBot ℕ∞) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by intro P have : ∃ (I : PrimeSpectrum R), (height P : WithBot ℕ∞) ≤ ↑(height I + 1) := by + have : ∃ M, Ideal.IsMaximal M ∧ P.asIdeal ≤ M := by + apply exists_le_maximal + apply IsPrime.ne_top + apply P.IsPrime + obtain ⟨M, maxM, PleM⟩ := this + let P' : PrimeSpectrum (Polynomial R) := PrimeSpectrum.mk M (IsMaximal.isPrime maxM) + have PleP' : P ≤ P' := PleM + have : height P ≤ height P' := height_le_of_le PleP' + simp only [WithBot.coe_le_coe] sorry obtain ⟨I, IP⟩ := this have : (↑(height I + 1) : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum R), ↑(height I + 1) := by From a2f481c7db196d982765165911022adaf6ea03e8 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Wed, 14 Jun 2023 11:12:33 -0700 Subject: [PATCH 2/6] Turn some simp into simp only --- CommAlg/krull.lean | 2 +- CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean | 11 ++++++++--- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 06e6d0d..1e720c0 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -63,7 +63,7 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := apply height_le_of_le apply le_maximalIdeal exact I.2.1 - . simp + . simp only [height_le_krullDim] #check height_le_krullDim --some propositions that would be nice to be able to eventually diff --git a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean index 485ee3b..089c4b5 100644 --- a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean +++ b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean @@ -42,16 +42,21 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : have PleP' : P ≤ P' := PleM have : height P ≤ height P' := height_le_of_le PleP' simp only [WithBot.coe_le_coe] - sorry + have : ∃ (I : PrimeSpectrum R), height P' ≤ height I + 1 := by + + sorry + obtain ⟨I, h⟩ := this + use I + exact ge_trans h this 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 + exact 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 apply this - simp + simp only [iSup_le_iff] intro P exact ge_trans oneOut (htPBdd P) From ae8bf07ee7b82901b157fb81d018120f8f52c804 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Wed, 14 Jun 2023 11:23:29 -0700 Subject: [PATCH 3/6] Make the lemma names a little more descriptive --- CommAlg/krull.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 1e720c0..ec94d36 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -135,7 +135,7 @@ 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 +lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by by_contra x rw [Ring.not_isField_iff_exists_prime] at x obtain ⟨P, ⟨h1, primeP⟩⟩ := x @@ -156,9 +156,9 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) aesop contradiction -lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by +lemma domain_dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by constructor - · exact isField.dim_zero + · exact domain_dim_zero.isField · intro fieldD let h : Field D := IsField.toField fieldD exact dim_field_eq_zero From a3e4746b134035c75432a84847659973e8189f73 Mon Sep 17 00:00:00 2001 From: Sameer Savkar Date: Wed, 14 Jun 2023 11:50:29 -0700 Subject: [PATCH 4/6] wrote proofs of 2 lemmas --- CommAlg/sameer(artinian-rings).lean | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/CommAlg/sameer(artinian-rings).lean b/CommAlg/sameer(artinian-rings).lean index e6bb667..417cc96 100644 --- a/CommAlg/sameer(artinian-rings).lean +++ b/CommAlg/sameer(artinian-rings).lean @@ -6,7 +6,9 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic import Mathlib.RingTheory.DedekindDomain.DVR -lemma FieldisArtinian (R : Type _) [CommRing R] (IsField : ):= by sorry +lemma FieldisArtinian (R : Type _) [CommRing R] (h: IsField R) : + IsArtinianRing R := by sorry + lemma ArtinianDomainIsField (R : Type _) [CommRing R] [IsDomain R] @@ -47,8 +49,7 @@ lemma isArtinianRing_of_quotient_of_artinian (R : Type _) [CommRing R] 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 +-- if R is Artinian and P is prime then R/P is Artinian Domain -- R⧸P is a field by the above lemma -- P is maximal @@ -56,13 +57,13 @@ by have artRP : IsArtinianRing (R⧸P) := by exact isArtinianRing_of_quotient_of_artinian R P IsArt - + have artRPField : IsField (R⧸P) := by + exact ArtinianDomainIsField (R⧸P) artRP + + have h := Ideal.Quotient.maximal_of_isField P artRPField + exact h + -- Then R/I is Artinian -- have' : IsArtinianRing R ∧ Ideal.IsPrime I → IsDomain (R⧸I) := by -- R⧸I.IsArtinian → monotone_stabilizes_iff_artinian.R⧸I - - - - --- Use Stacks project proof since it's broken into lemmas From ebbbfc88c32e21ca47be4e9aa3067c8a9f5005ad Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Wed, 14 Jun 2023 12:02:01 -0700 Subject: [PATCH 5/6] added more sorried statements --- CommAlg/krull.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 06e6d0d..59fd048 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -226,7 +226,11 @@ lemma dim_le_dim_polynomial_add_one [Nontrivial R] : lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : krullDim R + 1 = krullDim (Polynomial R) := sorry +lemma dim_mvPolynomial [Field K] (n : ℕ) : krullDim (MvPolynomial (Fin n) K) = n := sorry + lemma height_eq_dim_localization : height I = krullDim (Localization.AtPrime I.asIdeal) := sorry +lemma dim_quotient_le_dim : height I + krullDim (R ⧸ I.asIdeal) ≤ krullDim R := sorry + lemma height_add_dim_quotient_le_dim : height I + krullDim (R ⧸ I.asIdeal) ≤ krullDim R := sorry \ No newline at end of file From 5485c268498dcac0a15507392d7c1ef3ea7713b1 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Wed, 14 Jun 2023 13:09:23 -0700 Subject: [PATCH 6/6] add more stuff --- CommAlg/jayden(krull-dim-zero).lean | 72 +++++++++++++++++------------ 1 file changed, 43 insertions(+), 29 deletions(-) diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean index 523eb90..06dc873 100644 --- a/CommAlg/jayden(krull-dim-zero).lean +++ b/CommAlg/jayden(krull-dim-zero).lean @@ -15,6 +15,9 @@ import Mathlib.RingTheory.Localization.AtPrime import Mathlib.Order.ConditionallyCompleteLattice.Basic import Mathlib.Algebra.Ring.Pi import Mathlib.RingTheory.Finiteness +import Mathlib.Util.PiNotation + +open PiNotation namespace Ideal @@ -26,6 +29,8 @@ noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height R I +--variable {R} + -- 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 @@ -33,7 +38,7 @@ noncomputable def krullDim (R : Type) [CommRing R] : -- Stacks Definition 10.32.1: An ideal is locally nilpotent -- if every element is nilpotent -class IsLocallyNilpotent (I : Ideal R) : Prop := +class IsLocallyNilpotent {R : Type _} [CommRing R] (I : Ideal R) : Prop := h : ∀ x ∈ I, IsNilpotent x #check Ideal.IsLocallyNilpotent end Ideal @@ -89,6 +94,10 @@ lemma containment_radical_power_containment : -- Ideal.exists_pow_le_of_le_radical_of_fG +-- Stacks Lemma 10.52.5: R → S is a ring map. M is an S-mod. +-- Then length_R M ≥ length_S M. +-- Stacks Lemma 10.52.5': equality holds if R → S is surjective. + -- 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] @@ -96,48 +105,53 @@ lemma length_eq_dim_if_maximal_annihilates {I : Ideal R} [Ideal.IsMaximal I] → 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? +-- Use 10.52.5 -- 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⟩ +lemma power_zero_finite_length [Ideal.IsMaximal I] (h₁ : Ideal.FG I) [Module.Finite R M] + (h₂ : (∃ n : ℕ, (I ^ n) • (⊤ : Submodule R M) = 0)) : + (∃ m : ℕ, Module.length R M ≤ m) := by sorry + -- 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 +lemma Artinian_has_finite_max_ideal + [IsArtinianRing R] : Finite (MaximalSpectrum R) := by + by_contra infinite + simp only [not_finite_iff_infinite] at infinite + -- 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 +lemma Jacobson_of_Artinian_is_nilpotent + [IsArtinianRing R] : IsNilpotent (Ideal.jacobson (⊥ : Ideal R)) := by + have J := Ideal.jacobson (⊥ : Ideal R) + -- 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 +abbrev Prod_of_localization := + Π I : MaximalSpectrum R, Localization.AtPrime I.1 --- lemma product_of_localization_at_maximal_ideal : Finite (MaximalSpectrum R) --- ∧ +-- instance : CommRing (Prod_of_localization R) := by +-- unfold Prod_of_localization +-- infer_instance + +def foo : Prod_of_localization R →+* R where + toFun := sorry + invFun := sorry + left_inv := sorry + right_inv := sorry + map_mul' := sorry + map_add' := sorry -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. +def product_of_localization_at_maximal_ideal [Finite (MaximalSpectrum R)] + (h : Ideal.IsLocallyNilpotent (Ideal.jacobson (⊥ : Ideal R))) : + Prod_of_localization R ≃+* R := by sorry -- Stacks Lemma 10.53.6: R is Artinian iff R has finite length as an R-mod lemma IsArtinian_iff_finite_length : @@ -148,8 +162,8 @@ 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 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