From 5f241e80f164fb255953686d33c21d4a12cd1df1 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 14:16:53 -0700 Subject: [PATCH 1/8] 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 3730100c86de0fed1adf2df212d98d84af084ef7 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 14:35:10 -0700 Subject: [PATCH 2/8] 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 3/8] 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 4/8] 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 5/8] 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 6/8] 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 7/8] 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 8/8] 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