From fd5bd05f0109488dd5eb4d4c85c957654c01d41b Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Mon, 12 Jun 2023 13:03:35 -0700 Subject: [PATCH] golf, added dim_eq_bot_iff --- CommAlg/krull.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 1bd2829..228f0b1 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -1,4 +1,5 @@ -import Mathlib.RingTheory.Ideal.Basic +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.RingTheory.FiniteType import Mathlib.Order.Height import Mathlib.RingTheory.PrincipalIdealDomain import Mathlib.RingTheory.DedekindDomain.Basic @@ -33,11 +34,12 @@ noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.c lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) : iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) ≤ n ↔ - ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := by - convert @iSup_le_iff (WithBot ℕ∞) (PrimeSpectrum R) inferInstance _ (↑n) + ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞) --some propositions that would be nice to be able to eventually +lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := sorry + lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry #check Ring.DimensionLEOne