From d0a6d8605e8a8b38a7e6cc9ea2312a2641015d8a Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Fri, 16 Jun 2023 09:54:07 -0700 Subject: [PATCH 1/6] golfed imports --- CommAlg/polynomial.lean | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/CommAlg/polynomial.lean b/CommAlg/polynomial.lean index 8dd886a..e7380b0 100644 --- a/CommAlg/polynomial.lean +++ b/CommAlg/polynomial.lean @@ -1,13 +1,3 @@ -import Mathlib.RingTheory.Ideal.Operations -import Mathlib.RingTheory.FiniteType -import Mathlib.Order.Height -import Mathlib.RingTheory.Polynomial.Quotient -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 CommAlg.krull section ChainLemma @@ -132,7 +122,6 @@ lemma ht_adjoin_x_eq_ht_add_one [Nontrivial R] (I : PrimeSpectrum R) : height I apply hl.2 exact hb -#check (⊤ : ℕ∞) /- dim R + 1 ≤ dim R[X] -/ From f76ff450e7ceda65f3d21c1003d6a38ed0a0abc9 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Fri, 16 Jun 2023 11:22:21 -0700 Subject: [PATCH 2/6] Modified some types to make them implicit --- CommAlg/krull.lean | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 7d4a31c..e26837f 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -49,10 +49,12 @@ 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 : ℕ) : +@[simp] +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 : ℕ∞) : +@[simp] +lemma krullDim_le_iff' {R : Type _} [CommRing R] {n : ℕ∞} : krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞) @[simp] @@ -91,7 +93,8 @@ lemma height_bot_eq {D: Type _} [CommRing D] [IsDomain D] : height (⊥ : PrimeS /-- The Krull dimension of a ring being ≥ n is equivalent to there being an ideal of height ≥ n. -/ -lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) : +@[simp] +lemma le_krullDim_iff {R : Type _} [CommRing R] {n : ℕ} : n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by constructor · unfold krullDim @@ -246,7 +249,7 @@ lemma not_maximal_of_lt_prime {p : Ideal R} {q : Ideal R} (hq : IsPrime q) (h : /-- Krull dimension is ≤ 0 if and only if all primes are maximal. -/ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by show ((_ : WithBot ℕ∞) ≤ (0 : ℕ)) ↔ _ - rw [krullDim_le_iff R 0] + rw [krullDim_le_iff] constructor <;> intro h I . contrapose! h have ⟨𝔪, h𝔪⟩ := I.asIdeal.exists_le_maximal (IsPrime.ne_top I.IsPrime) @@ -353,7 +356,7 @@ lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry applies only to dimension zero rings and domains of dimension 1. -/ lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ 1 := by show _ → ((_ : WithBot ℕ∞) ≤ (1 : ℕ)) - rw [krullDim_le_iff R 1] + rw [krullDim_le_iff] intro H p apply le_of_not_gt intro h @@ -375,7 +378,7 @@ lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1 exact Ring.DimensionLEOne.principal_ideal_ring R /-- The ring of polynomials over a field has dimension one. -/ -lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullDim (Polynomial K) = 1 := by +lemma polynomial_over_field_dim_one {K : Type _} [Nontrivial K] [Field K] : krullDim (Polynomial K) = 1 := by rw [le_antisymm_iff] let X := @Polynomial.X K _ constructor From c5f0eb20815dff5d68ae0fa7a50c55a9b9c00282 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Fri, 16 Jun 2023 11:37:19 -0700 Subject: [PATCH 3/6] Add the whole proof back since I just noticed that I had replaced them by sorried statements --- CommAlg/krull.lean | 59 +++++++++++++++++++++++++- CommAlg/sayantan(poly_over_field).lean | 3 +- 2 files changed, 59 insertions(+), 3 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index e26837f..574ffc5 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -377,12 +377,67 @@ lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1 rw [dim_le_one_iff] exact Ring.DimensionLEOne.principal_ideal_ring R +private lemma singleton_bot_chainHeight_one {α : Type} [Preorder α] [Bot α] : Set.chainHeight {(⊥ : α)} ≤ 1 := by + unfold Set.chainHeight + simp only [iSup_le_iff, Nat.cast_le_one] + intro L h + unfold Set.subchain at h + simp only [Set.mem_singleton_iff, Set.mem_setOf_eq] at h + rcases L with (_ | ⟨a,L⟩) + . simp only [List.length_nil, zero_le] + rcases L with (_ | ⟨b,L⟩) + . simp only [List.length_singleton, le_refl] + simp only [List.chain'_cons, List.find?, List.mem_cons, forall_eq_or_imp] at h + rcases h with ⟨⟨h1, _⟩, ⟨rfl, rfl, _⟩⟩ + exact absurd h1 (lt_irrefl _) + /-- The ring of polynomials over a field has dimension one. -/ -lemma polynomial_over_field_dim_one {K : Type _} [Nontrivial K] [Field K] : krullDim (Polynomial K) = 1 := by +lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullDim (Polynomial K) = 1 := by rw [le_antisymm_iff] let X := @Polynomial.X K _ constructor - · exact dim_le_one_of_pid + · unfold krullDim + apply @iSup_le (WithBot ℕ∞) _ _ _ _ + intro I + have PIR : IsPrincipalIdealRing (Polynomial K) := by infer_instance + by_cases I = ⊥ + · rw [← height_bot_iff_bot] at h + simp only [WithBot.coe_le_one, ge_iff_le] + rw [h] + exact bot_le + · push_neg at h + have : I.asIdeal ≠ ⊥ := by + by_contra a + have : I = ⊥ := PrimeSpectrum.ext I ⊥ a + contradiction + have maxI := IsPrime.to_maximal_ideal this + have sngletn : ∀P, P ∈ {J | J < I} ↔ P = ⊥ := by + intro P + constructor + · intro H + simp only [Set.mem_setOf_eq] at H + by_contra x + push_neg at x + have : P.asIdeal ≠ ⊥ := by + by_contra a + have : P = ⊥ := PrimeSpectrum.ext P ⊥ a + contradiction + have maxP := IsPrime.to_maximal_ideal this + have IneTop := IsMaximal.ne_top maxI + have : P ≤ I := le_of_lt H + rw [←PrimeSpectrum.asIdeal_le_asIdeal] at this + have : P.asIdeal = I.asIdeal := Ideal.IsMaximal.eq_of_le maxP IneTop this + have : P = I := PrimeSpectrum.ext P I this + replace H : P ≠ I := ne_of_lt H + contradiction + · intro pBot + simp only [Set.mem_setOf_eq, pBot] + exact lt_of_le_of_ne bot_le h.symm + replace sngletn : {J | J < I} = {⊥} := Set.ext sngletn + unfold height + rw [sngletn] + simp only [WithBot.coe_le_one, ge_iff_le] + exact singleton_bot_chainHeight_one · suffices : ∃I : PrimeSpectrum (Polynomial K), 1 ≤ (height I : WithBot ℕ∞) · obtain ⟨I, h⟩ := this have : (height I : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum (Polynomial K)), ↑(height I) := by diff --git a/CommAlg/sayantan(poly_over_field).lean b/CommAlg/sayantan(poly_over_field).lean index 48aa955..d7c1369 100644 --- a/CommAlg/sayantan(poly_over_field).lean +++ b/CommAlg/sayantan(poly_over_field).lean @@ -22,7 +22,8 @@ private lemma singleton_bot_chainHeight_one {α : Type} [Preorder α] [Bot α] : exact absurd h1 (lt_irrefl _) /-- The ring of polynomials over a field has dimension one. -/ -lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullDim (Polynomial K) = 1 := by +-- It's the exact same lemma as in krull.lean, added ' to avoid conflict +lemma polynomial_over_field_dim_one' {K : Type} [Nontrivial K] [Field K] : krullDim (Polynomial K) = 1 := by rw [le_antisymm_iff] let X := @Polynomial.X K _ constructor From 19b490ab9e3f64dc28f7f7f294ac13c7156540e7 Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Fri, 16 Jun 2023 11:43:00 -0700 Subject: [PATCH 4/6] some golfing, one new lemma --- CommAlg/krull.lean | 78 ++++++++++++++++++---------------------------- 1 file changed, 31 insertions(+), 47 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index e24aa0f..78c9a9b 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -127,9 +127,19 @@ lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) : #check ENat.recTopCoe -/- terrible place for this lemma. Also this probably exists somewhere +/- terrible place for these two lemmas. Also this probably exists somewhere Also this is a terrible proof -/ +lemma eq_top_iff' (n : ℕ∞) : n = ⊤ ↔ ∀ m : ℕ, m ≤ n := by + refine' ⟨fun a b => _, fun h => _⟩ + . rw [a]; exact le_top + . induction' n using ENat.recTopCoe with n + . rfl + . exfalso + apply not_lt_of_ge (h (n + 1)) + norm_cast + norm_num + lemma eq_top_iff (n : WithBot ℕ∞) : n = ⊤ ↔ ∀ m : ℕ, m ≤ n := by aesop induction' n using WithBot.recBotCoe with n @@ -147,47 +157,30 @@ lemma eq_top_iff (n : WithBot ℕ∞) : n = ⊤ ↔ ∀ m : ℕ, m ≤ n := by lemma krullDim_eq_top_iff (R : Type _) [CommRing R] : krullDim R = ⊤ ↔ ∀ (n : ℕ), ∃ I : PrimeSpectrum R, n ≤ height I := by - simp [eq_top_iff, le_krullDim_iff] + simp_rw [eq_top_iff, le_krullDim_iff] change (∀ (m : ℕ), ∃ I, ((m : ℕ∞) : WithBot ℕ∞) ≤ height I) ↔ _ simp [WithBot.coe_le_coe] - /-- The Krull dimension of a local ring is the height of its maximal ideal. -/ 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 + exact WithBot.coe_mono <| height_le_of_le <| le_maximalIdeal I.2.1 . simp only [height_le_krullDim] /-- The height of a prime `𝔭` is greater than `n` if and only if there is a chain of primes less than `𝔭` with length `n + 1`. -/ lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : n < height 𝔭 ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by - match n with - | ⊤ => - constructor <;> intro h <;> exfalso - . exact (not_le.mpr h) le_top - . tauto - | (n : ℕ) => - have (m : ℕ∞) : n < m ↔ (n + 1 : ℕ∞) ≤ m := by - symm - show (n + 1 ≤ m ↔ _ ) - apply ENat.add_one_le_iff - exact ENat.coe_ne_top _ - rw [this] - unfold Ideal.height + induction' n using ENat.recTopCoe with n + . simp + . rw [←(ENat.add_one_le_iff <| ENat.coe_ne_top _)] show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞)) - rw [{J | J < 𝔭}.le_chainHeight_iff] + rw [Ideal.height, Set.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 + norm_cast + simp_rw [and_assoc] /-- Form of `lt_height_iff''` for rewriting with the height coerced to `WithBot ℕ∞`. -/ lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : @@ -199,30 +192,24 @@ lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : --some propositions that would be nice to be able to eventually /-- The prime spectrum of the zero ring is empty. -/ -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_of_subsingleton [Subsingleton R] : IsEmpty <| PrimeSpectrum R where + false x := x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : R)) x.1.zero_mem /-- A CommRing has empty prime spectrum if and only if it is the zero ring. -/ lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by - constructor - . contrapose - rw [not_isEmpty_iff, ←not_nontrivial_iff_subsingleton, not_not] + 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⟩ + . intro hneg h + exact hneg primeSpectrum_empty_of_subsingleton /-- 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] + rw [Ideal.krullDim, ←primeSpectrum_empty_iff, iSup_eq_bot] constructor <;> intro h . rw [←not_nonempty_iff] rintro ⟨a, ha⟩ - specialize h ⟨a, ha⟩ - tauto + cases h ⟨a, ha⟩ . rw [h.forall_iff] trivial @@ -290,13 +277,10 @@ lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum /-- In a field, the unique prime ideal is the zero ideal. -/ @[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] + refine' ⟨fun primeP => Or.elim (eq_bot_or_top P) _ _, fun botP => _⟩ + · intro P_top; exact P_top + . intro P_bot; exact False.elim (primeP.ne_top P_bot) + · rw [botP] exact bot_prime /-- In a field, all primes have height 0. -/ From db3bf05878ac9caf0863ecb9323b00de44aa3433 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Fri, 16 Jun 2023 13:02:25 -0700 Subject: [PATCH 5/6] Some minor renames and changes --- CommAlg/krull.lean | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 574ffc5..b31f7cf 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -63,11 +63,10 @@ lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R := /-- In a domain, the height of a prime ideal is Bot (0 in this case) iff it's the Bot ideal. -/ @[simp] -lemma height_bot_iff_bot {D: Type _} [CommRing D] [IsDomain D] {P : PrimeSpectrum D} : height P = ⊥ ↔ P = ⊥ := by +lemma height_zero_iff_bot {D: Type _} [CommRing D] [IsDomain D] {P : PrimeSpectrum D} : height P = 0 ↔ P = ⊥ := by constructor · intro h unfold height at h - rw [bot_eq_zero] at h simp only [Set.chainHeight_eq_zero_iff] at h apply eq_bot_of_minimal intro I @@ -87,10 +86,6 @@ lemma height_bot_iff_bot {D: Type _} [CommRing D] [IsDomain D] {P : PrimeSpectru have := not_lt_of_lt JneP contradiction -@[simp] -lemma height_bot_eq {D: Type _} [CommRing D] [IsDomain D] : height (⊥ : PrimeSpectrum D) = ⊥ := by - rw [height_bot_iff_bot] - /-- The Krull dimension of a ring being ≥ n is equivalent to there being an ideal of height ≥ n. -/ @[simp] @@ -307,16 +302,16 @@ lemma field_prime_bot {K: Type _} [Field K] {P : Ideal K} : IsPrime P ↔ P = exact bot_prime /-- In a field, all primes have height 0. -/ -lemma field_prime_height_bot {K: Type _} [Nontrivial K] [Field K] (P : PrimeSpectrum K) : height P = ⊥ := by +lemma field_prime_height_zero {K: Type _} [Nontrivial K] [Field K] (P : PrimeSpectrum K) : height P = 0 := by have : IsPrime P.asIdeal := P.IsPrime rw [field_prime_bot] at this have : P = ⊥ := PrimeSpectrum.ext P ⊥ this - rwa [height_bot_iff_bot] + rwa [height_zero_iff_bot] /-- The Krull dimension of a field is 0. -/ lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by unfold krullDim - simp only [field_prime_height_bot, ciSup_unique] + simp only [field_prime_height_zero, ciSup_unique] /-- A domain with Krull dimension 0 is a field. -/ lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by @@ -377,7 +372,7 @@ lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1 rw [dim_le_one_iff] exact Ring.DimensionLEOne.principal_ideal_ring R -private lemma singleton_bot_chainHeight_one {α : Type} [Preorder α] [Bot α] : Set.chainHeight {(⊥ : α)} ≤ 1 := by +private lemma singleton_chainHeight_le_one {α : Type _} {x : α} [Preorder α] : Set.chainHeight {x} ≤ 1 := by unfold Set.chainHeight simp only [iSup_le_iff, Nat.cast_le_one] intro L h @@ -401,7 +396,7 @@ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullD intro I have PIR : IsPrincipalIdealRing (Polynomial K) := by infer_instance by_cases I = ⊥ - · rw [← height_bot_iff_bot] at h + · rw [← height_zero_iff_bot] at h simp only [WithBot.coe_le_one, ge_iff_le] rw [h] exact bot_le @@ -437,7 +432,7 @@ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullD unfold height rw [sngletn] simp only [WithBot.coe_le_one, ge_iff_le] - exact singleton_bot_chainHeight_one + exact singleton_chainHeight_le_one · suffices : ∃I : PrimeSpectrum (Polynomial K), 1 ≤ (height I : WithBot ℕ∞) · obtain ⟨I, h⟩ := this have : (height I : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum (Polynomial K)), ↑(height I) := by From fc6fac87a2cc440539b382b1e1d129590ff3bd57 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Fri, 16 Jun 2023 14:37:06 -0700 Subject: [PATCH 6/6] Is it too late to say sorry --- CommAlg/jayden(krull-dim-zero).lean | 67 ++++++++++++++++++++++++----- 1 file changed, 56 insertions(+), 11 deletions(-) diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean index 15dd150..921d6f8 100644 --- a/CommAlg/jayden(krull-dim-zero).lean +++ b/CommAlg/jayden(krull-dim-zero).lean @@ -16,6 +16,7 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic import Mathlib.Algebra.Ring.Pi import Mathlib.RingTheory.Finiteness import Mathlib.Util.PiNotation +import Mathlib.RingTheory.Ideal.MinimalPrime import CommAlg.krull open PiNotation @@ -43,6 +44,8 @@ class IsLocallyNilpotent {R : Type _} [CommRing R] (I : Ideal R) : Prop := #check Ideal.IsLocallyNilpotent end Ideal +def RingJacobson (R) [Ring R] := Ideal.jacobson (⊥ : Ideal R) + -- 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] @@ -169,15 +172,15 @@ abbrev Prod_of_localization := def foo : Prod_of_localization R →+* R where toFun := sorry -- invFun := sorry - left_inv := sorry - right_inv := sorry + --left_inv := sorry + --right_inv := sorry map_mul' := sorry map_add' := sorry def product_of_localization_at_maximal_ideal [Finite (MaximalSpectrum R)] - (h : Ideal.IsLocallyNilpotent (Ideal.jacobson (⊥ : Ideal R))) : - Prod_of_localization R ≃+* R := by sorry + (h : Ideal.IsLocallyNilpotent (RingJacobson R)) : + R ≃+* Prod_of_localization 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 : @@ -193,18 +196,61 @@ lemma primes_of_Artinian_are_maximal -- Lemma: Krull dimension of a ring is the supremum of height of maximal ideals +-- Lemma: X is an irreducible component of Spec(R) ↔ X = V(I) for I a minimal prime +lemma irred_comp_minmimal_prime (X) : + X ∈ irreducibleComponents (PrimeSpectrum R) + ↔ ∃ (P : minimalPrimes R), X = PrimeSpectrum.zeroLocus P := by + sorry + +-- Lemma: localization of Noetherian ring is Noetherian +-- lemma localization_of_Noetherian_at_prime [IsNoetherianRing R] +-- (atprime: Ideal.IsPrime I) : +-- IsNoetherianRing (Localization.AtPrime I) := by sorry + + -- Stacks Lemma 10.60.5: R is Artinian iff R is Noetherian of dimension 0 -lemma dim_le_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : - IsNoetherianRing R ∧ Ideal.krullDim R ≤ 0 ↔ IsArtinianRing R := by - constructor +lemma Artinian_if_dim_le_zero_Noetherian (R : Type _) [CommRing R] : + IsNoetherianRing R ∧ Ideal.krullDim R ≤ 0 → IsArtinianRing R := by rintro ⟨RisNoetherian, dimzero⟩ rw [ring_Noetherian_iff_spec_Noetherian] at RisNoetherian + have := fun X => (irred_comp_minmimal_prime R X).mp + choose F hf using this let Z := irreducibleComponents (PrimeSpectrum R) - have Zfinite : Set.Finite Z := by + -- have Zfinite : Set.Finite Z := by -- apply TopologicalSpace.NoetherianSpace.finite_irreducibleComponents ?_ + -- sorry + --let P := fun + rw [← ring_Noetherian_iff_spec_Noetherian] at RisNoetherian + have PrimeIsMaximal : ∀ X : Z, Ideal.IsMaximal (F X X.2).1 := by + intro X + have prime : Ideal.IsPrime (F X X.2).1 := (F X X.2).2.1.1 + rw [Ideal.dim_le_zero_iff] at dimzero + exact dimzero ⟨_, prime⟩ + have JacLocallyNil : Ideal.IsLocallyNilpotent (RingJacobson R) := by sorry + let Loc := fun X : Z ↦ Localization.AtPrime (F X.1 X.2).1 + have LocNoetherian : ∀ X, IsNoetherianRing (Loc X) := by + intro X sorry - - sorry + -- apply IsLocalization.isNoetherianRing (F X.1 X.2).1 (Loc X) RisNoetherian + have Locdimzero : ∀ X, Ideal.krullDim (Loc X) ≤ 0 := by sorry + have powerannihilates : ∀ X, ∃ n : ℕ, + ((F X.1 X.2).1) ^ n • (⊤: Submodule R (Loc X)) = 0 := by sorry + have LocFinitelength : ∀ X, ∃ n : ℕ, Module.length R (Loc X) ≤ n := by + intro X + have idealfg : Ideal.FG (F X.1 X.2).1 := by + rw [isNoetherianRing_iff_ideal_fg] at RisNoetherian + specialize RisNoetherian (F X.1 X.2).1 + exact RisNoetherian + have modulefg : Module.Finite R (Loc X) := by sorry -- not sure if this is true + specialize PrimeIsMaximal X + specialize powerannihilates X + apply power_zero_finite_length R (F X.1 X.2).1 (Loc X) idealfg powerannihilates + have RingFinitelength : ∃ n : ℕ, Module.length R R ≤ n := by sorry + rw [IsArtinian_iff_finite_length] + exact RingFinitelength + +lemma dim_le_zero_Noetherian_if_Artinian (R : Type _) [CommRing R] : + IsArtinianRing R → IsNoetherianRing R ∧ Ideal.krullDim R ≤ 0 := by intro RisArtinian constructor apply finite_length_is_Noetherian @@ -213,7 +259,6 @@ lemma dim_le_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : intro I apply primes_of_Artinian_are_maximal --- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible :