From afeeeb506fe6801f158593d292ff32dc636c3a3f Mon Sep 17 00:00:00 2001
From: GTBarkley <barkleygrant@gmail.com>
Date: Tue, 13 Jun 2023 19:11:44 +0000
Subject: [PATCH 1/2] proved dim_eq_bot_iff

---
 CommAlg/grant.lean | 40 ++++++++++++++++++++++++++++++++--------
 1 file changed, 32 insertions(+), 8 deletions(-)

diff --git a/CommAlg/grant.lean b/CommAlg/grant.lean
index ef2cc9f..7951c54 100644
--- a/CommAlg/grant.lean
+++ b/CommAlg/grant.lean
@@ -52,10 +52,10 @@ open Ideal
 -- chain of primes 
 #check height 
 
--- lemma height_ge_iff {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
---   height 𝔭 ≥ n ↔ := sorry
+lemma lt_height_iff {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
+  height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c ∈ {I : PrimeSpectrum R | I < 𝔭}.subchain ∧ c.length = n + 1 := sorry
 
-lemma height_ge_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
+lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
 height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
   rcases n with _ | n
   . constructor <;> intro h <;> exfalso
@@ -88,13 +88,37 @@ lemma krullDim_nonneg_of_nontrivial [Nontrivial R] : ∃ n : ℕ∞, Ideal.krull
   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
+-- 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
 
-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
+-- 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
 
+lemma prime_elim_of_subsingleton (x : PrimeSpectrum R) [Subsingleton R] : False :=
+  x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : R)) x.1.zero_mem
+
+lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by
+  constructor
+  . contrapose
+    rw [not_isEmpty_iff, ←not_nontrivial_iff_subsingleton, not_not]
+    apply PrimeSpectrum.instNonemptyPrimeSpectrum
+  . intro h
+    by_contra hneg
+    rw [not_isEmpty_iff] at hneg
+    rcases hneg with ⟨a, ha⟩
+    exact prime_elim_of_subsingleton R ⟨a, ha⟩
+
+lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
+  unfold Ideal.krullDim
+  rw [←primeSpectrum_empty_iff, iSup_eq_bot]
+  constructor <;> intro h
+  . rw [←not_nonempty_iff]
+    rintro ⟨a, ha⟩
+    specialize h ⟨a, ha⟩
+    tauto
+  . rw [h.forall_iff]
+    trivial
 
 
 #check (sorry : False)

From f63286aff8ebf58f6a463b92068573ea4d9aa9d1 Mon Sep 17 00:00:00 2001
From: GTBarkley <barkleygrant@gmail.com>
Date: Tue, 13 Jun 2023 20:34:02 +0000
Subject: [PATCH 2/2] moved dim_eq_bot_iff to krull.lean

---
 CommAlg/grant.lean |  7 ++++---
 CommAlg/krull.lean | 26 +++++++++++++++++++++++++-
 2 files changed, 29 insertions(+), 4 deletions(-)

diff --git a/CommAlg/grant.lean b/CommAlg/grant.lean
index 7951c54..ce5041d 100644
--- a/CommAlg/grant.lean
+++ b/CommAlg/grant.lean
@@ -95,7 +95,7 @@ lemma krullDim_nonneg_of_nontrivial [Nontrivial R] : ∃ n : ℕ∞, Ideal.krull
 -- 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
 
-lemma prime_elim_of_subsingleton (x : PrimeSpectrum R) [Subsingleton R] : False :=
+lemma primeSpectrum_empty_of_subsingleton (x : PrimeSpectrum R) [Subsingleton R] : False :=
   x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : R)) x.1.zero_mem
 
 lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by
@@ -107,15 +107,16 @@ lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R :=
     by_contra hneg
     rw [not_isEmpty_iff] at hneg
     rcases hneg with ⟨a, ha⟩
-    exact prime_elim_of_subsingleton R ⟨a, ha⟩
+    exact primeSpectrum_empty_of_subsingleton R ⟨a, ha⟩
 
+/-- A ring has Krull dimension -∞ if and only if it is the zero ring -/
 lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
   unfold Ideal.krullDim
   rw [←primeSpectrum_empty_iff, iSup_eq_bot]
   constructor <;> intro h
   . rw [←not_nonempty_iff]
     rintro ⟨a, ha⟩
-    specialize h ⟨a, ha⟩
+    -- specialize h ⟨a, ha⟩
     tauto
   . rw [h.forall_iff]
     trivial
diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index 9b4c785..c021d74 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -62,7 +62,31 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) :=
 #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
+lemma primeSpectrum_empty_of_subsingleton (x : PrimeSpectrum R) [Subsingleton R] : False :=
+  x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : R)) x.1.zero_mem
+
+lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by
+  constructor
+  . contrapose
+    rw [not_isEmpty_iff, ←not_nontrivial_iff_subsingleton, not_not]
+    apply PrimeSpectrum.instNonemptyPrimeSpectrum
+  . intro h
+    by_contra hneg
+    rw [not_isEmpty_iff] at hneg
+    rcases hneg with ⟨a, ha⟩
+    exact primeSpectrum_empty_of_subsingleton ⟨a, ha⟩
+
+/-- A ring has Krull dimension -∞ if and only if it is the zero ring -/
+lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
+  unfold Ideal.krullDim
+  rw [←primeSpectrum_empty_iff, iSup_eq_bot]
+  constructor <;> intro h
+  . rw [←not_nonempty_iff]
+    rintro ⟨a, ha⟩
+    specialize h ⟨a, ha⟩
+    tauto
+  . rw [h.forall_iff]
+    trivial
 
 lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry