From 1ed0a5499c1d1203fd54eda9cddecc76c154cdd1 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Tue, 13 Jun 2023 21:43:06 +0000 Subject: [PATCH] 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