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