From a941cce12f21b0bd94757a669c1d73f5677c60a5 Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Tue, 13 Jun 2023 14:26:19 -0700 Subject: [PATCH 1/2] 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 50aa1b07a8a3dbfb712765e822db7a368bcdbce3 Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Tue, 13 Jun 2023 20:58:32 -0700 Subject: [PATCH 2/2] 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