From 6a0a3768f8a5f5b13845b21d36e4b41cde7c06e1 Mon Sep 17 00:00:00 2001
From: GTBarkley <barkleygrant@gmail.com>
Date: Tue, 13 Jun 2023 05:01:18 +0000
Subject: [PATCH] proved krullDim_nonneg_of_nontrivial

---
 CommAlg/grant.lean | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/CommAlg/grant.lean b/CommAlg/grant.lean
index 2261f25..ef2cc9f 100644
--- a/CommAlg/grant.lean
+++ b/CommAlg/grant.lean
@@ -73,7 +73,7 @@ height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀
   show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞))
   rw [{J | J < 𝔭}.le_chainHeight_iff]
   show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
-  have h := fun (c : List (PrimeSpectrum R)) => (@WithTop.coe_eq_coe _ (List.length c) n) 
+  -- have h := fun (c : List (PrimeSpectrum R)) => (@WithTop.coe_eq_coe _ (List.length c) n) 
   constructor <;> rintro ⟨c, hc⟩ <;> use c --<;> tauto--<;> exact ⟨hc.1, by tauto⟩
   . --rw [and_assoc]
     -- show _ ∧ _ ∧ _
@@ -83,6 +83,11 @@ height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀
     norm_cast at hc
     tauto
 
+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 krullDim_le_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : 
   Ideal.krullDim R ≤ n ↔ (∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1) := by
     sorry
@@ -90,6 +95,8 @@ lemma krullDim_le_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} :
 lemma krullDim_ge_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : 
   Ideal.krullDim R ≥ n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 := sorry
 
+
+
 #check (sorry : False)
 #check (sorryAx)
 #check (4 : WithBot ℕ∞)