From 8b2be97b5a4f597de327d00598bfafc20c9504a1 Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Mon, 12 Jun 2023 14:27:09 -0700 Subject: [PATCH] added some lemmas --- CommAlg/krull.lean | 30 +++++++++++++++++++++++++++--- 1 file changed, 27 insertions(+), 3 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 228f0b1..9b4c785 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -19,6 +19,7 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic -/ namespace Ideal +open LocalRing variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) @@ -32,10 +33,33 @@ lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpe noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice -lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) : - iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) ≤ n ↔ - ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞) +lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := by + apply Set.chainHeight_mono + intro J' hJ' + show J' < J + exact lt_of_lt_of_le hJ' I_le_J +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 : ℕ∞) : + krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞) + +@[simp] +lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R := + le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I + +lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := by + apply le_antisymm + . rw [krullDim_le_iff'] + intro I + apply WithBot.coe_mono + apply height_le_of_le + apply le_maximalIdeal + exact I.2.1 + . simp + +#check height_le_krullDim --some propositions that would be nice to be able to eventually lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := sorry