From e93a53bd67732c7b09ea41d2d5a60b573b8724b4 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Thu, 15 Jun 2023 15:18:22 -0700 Subject: [PATCH] Proved le_krullDim_iff --- CommAlg/krull.lean | 54 ++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 47 insertions(+), 7 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index a559b1d..bd9edb4 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -19,6 +19,11 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic developed. -/ +lemma lt_bot_eq_WithBot_bot [PartialOrder α] [OrderBot α] {a : WithBot α} (h : a < (⊥ : α)) : a = ⊥ := by + cases a + . rfl + . cases h.not_le (WithBot.coe_le_coe.2 bot_le) + namespace Ideal open LocalRing @@ -46,16 +51,51 @@ 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 : ℕ) : - n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry - -lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) : - n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry - @[simp] lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R := le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I +lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) : + n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by + constructor + · unfold krullDim + intro H + by_contra H1 + push_neg at H1 + by_cases n ≤ 0 + · rw [Nat.le_zero] at h + rw [h] at H H1 + have : ∀ (I : PrimeSpectrum R), ↑(height I) = (⊥ : WithBot ℕ∞) := by + intro I + specialize H1 I + exact lt_bot_eq_WithBot_bot H1 + rw [←iSup_eq_bot] at this + have := le_of_le_of_eq H this + rw [le_bot_iff] at this + exact WithBot.coe_ne_bot this + · push_neg at h + have : (n: ℕ∞) > 0 := Nat.cast_pos.mpr h + replace H1 : ∀ (I : PrimeSpectrum R), height I ≤ n - 1 := by + intro I + specialize H1 I + apply ENat.le_of_lt_add_one + rw [←ENat.coe_one, ←ENat.coe_sub, ←ENat.coe_add, tsub_add_cancel_of_le] + exact WithBot.coe_lt_coe.mp H1 + exact h + replace H1 : ∀ (I : PrimeSpectrum R), (height I : WithBot ℕ∞) ≤ ↑(n - 1):= + fun _ ↦ (WithBot.coe_le rfl).mpr (H1 _) + rw [←iSup_le_iff] at H1 + have : ((n : ℕ∞) : WithBot ℕ∞) ≤ (((n - 1 : ℕ) : ℕ∞) : WithBot ℕ∞) := le_trans H H1 + norm_cast at this + have that : n - 1 < n := by refine Nat.sub_lt h (by norm_num) + apply lt_irrefl (n-1) (trans that this) + · rintro ⟨I, h⟩ + have : height I ≤ krullDim R := by apply height_le_krullDim + exact le_trans h this + +lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) : + n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry + /-- The Krull dimension of a local ring is the height of its maximal ideal. -/ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := by apply le_antisymm @@ -250,7 +290,7 @@ lemma domain_dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krull constructor · exact domain_dim_zero.isField · intro fieldD - let h : Field D := IsField.toField fieldD + let h : Field D := fieldD.toField exact dim_field_eq_zero #check Ring.DimensionLEOne