From 8b28694f0e09b0f63c8a6419c34fa4c7a844d132 Mon Sep 17 00:00:00 2001
From: GTBarkley <barkleygrant@gmail.com>
Date: Sun, 11 Jun 2023 06:00:13 +0000
Subject: [PATCH 1/4] comparing definitions of height

---
 comm_alg/grant.lean | 29 ++++++++++++++++++++++++-----
 1 file changed, 24 insertions(+), 5 deletions(-)

diff --git a/comm_alg/grant.lean b/comm_alg/grant.lean
index 86c05fc..2814919 100644
--- a/comm_alg/grant.lean
+++ b/comm_alg/grant.lean
@@ -1,12 +1,31 @@
 import Mathlib.Order.KrullDimension
+import Mathlib.Order.JordanHolder
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.Order.Height
 
-def hello : IO Unit := do
-  IO.println "Hello, World!"
-
-#eval hello
 
 #check (p q : PrimeSpectrum _) → (p ≤ q)
 #check Preorder (PrimeSpectrum _)
 
-#check krullDim (PrimeSpectrum _)
\ No newline at end of file
+-- Dimension of a ring
+#check krullDim (PrimeSpectrum _)
+
+-- Length of a module
+#check krullDim (Submodule _ _)
+
+#check JordanHolderLattice
+
+
+variable {α : Type _} [Preorder α] (s : Set α)
+
+-- there should be a coercion from WithTop ℕ to WithBot (WithTop ℕ) but it doesn't seem to work
+-- it looks like this might be because someone changed the instance from CoeCT to Coe during the port
+lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop ℕ)) = krullDim s := by
+  intro hs
+  unfold Set.chainHeight
+  unfold krullDim
+  have hKrullSome : ∃n, krullDim s = some n := by
+    
+    sorry
+  -- norm_cast
+  sorry
\ No newline at end of file

From e65513322c59ffc53029c17124a6ab692ca82bb3 Mon Sep 17 00:00:00 2001
From: GTBarkley <barkleygrant@gmail.com>
Date: Sun, 11 Jun 2023 06:49:28 +0000
Subject: [PATCH 2/4] function relating the offbrand notions of chain

---
 comm_alg/grant.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/comm_alg/grant.lean b/comm_alg/grant.lean
index 2814919..de3e50f 100644
--- a/comm_alg/grant.lean
+++ b/comm_alg/grant.lean
@@ -18,6 +18,14 @@ import Mathlib.Order.Height
 
 variable {α : Type _} [Preorder α] (s : Set α)
 
+def finFun_to_list {n : ℕ} : (Fin n → α) → List α := by sorry
+
+def series_to_chain : StrictSeries s → s.subchain
+| ⟨length, toFun, strictMono⟩ => 
+    ⟨ finFun_to_list (fun x => toFun x),
+      sorry⟩
+
+
 -- there should be a coercion from WithTop ℕ to WithBot (WithTop ℕ) but it doesn't seem to work
 -- it looks like this might be because someone changed the instance from CoeCT to Coe during the port
 lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop ℕ)) = krullDim s := by

From dc034c2b09fec19599f1344946a715c33e502af4 Mon Sep 17 00:00:00 2001
From: GTBarkley <barkleygrant@gmail.com>
Date: Sun, 11 Jun 2023 12:33:18 +0000
Subject: [PATCH 3/4] added preliminary def of krullDimGE

---
 comm_alg/grant.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/comm_alg/grant.lean b/comm_alg/grant.lean
index de3e50f..92b1716 100644
--- a/comm_alg/grant.lean
+++ b/comm_alg/grant.lean
@@ -36,4 +36,7 @@ lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop 
     
     sorry
   -- norm_cast
-  sorry
\ No newline at end of file
+  sorry
+
+def krullDimGE (R : Type _) [CommRing R] (n : ℕ) :=
+  ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1
\ No newline at end of file

From dcc992588214751fc5e29b036b8baf724dadbef9 Mon Sep 17 00:00:00 2001
From: GTBarkley <barkleygrant@gmail.com>
Date: Mon, 12 Jun 2023 04:02:16 +0000
Subject: [PATCH 4/4] wrote some characterizations of bounding krull

---
 comm_alg/grant.lean | 21 ++++++++++++++++++++-
 1 file changed, 20 insertions(+), 1 deletion(-)

diff --git a/comm_alg/grant.lean b/comm_alg/grant.lean
index 92b1716..8586fa3 100644
--- a/comm_alg/grant.lean
+++ b/comm_alg/grant.lean
@@ -28,6 +28,7 @@ def series_to_chain : StrictSeries s → s.subchain
 
 -- there should be a coercion from WithTop ℕ to WithBot (WithTop ℕ) but it doesn't seem to work
 -- it looks like this might be because someone changed the instance from CoeCT to Coe during the port
+-- actually it looks like we can coerce to WithBot (ℕ∞) fine
 lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop ℕ)) = krullDim s := by
   intro hs
   unfold Set.chainHeight
@@ -38,5 +39,23 @@ lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop 
   -- norm_cast
   sorry
 
+namespace Ideal
+noncomputable def krullDim (R : Type _) [CommRing R] := 
+  Set.chainHeight (Set.univ : Set (PrimeSpectrum R))
+
 def krullDimGE (R : Type _) [CommRing R] (n : ℕ) :=
-  ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1
\ No newline at end of file
+  ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1
+
+def krullDimLE (R : Type _) [CommRing R] (n : ℕ) :=
+  ∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1
+
+end Ideal
+
+open Ideal
+
+lemma krullDim_le (R : Type _) [CommRing R] : krullDimLE R n ↔ Ideal.krullDim R ≤ n := sorry
+lemma krullDim_ge (R : Type _) [CommRing R] : krullDimGE R n ↔ Ideal.krullDim R ≥ n := sorry
+
+
+-- #check ((4 : ℕ∞) : WithBot (WithTop ℕ))
+#check ( (Set.chainHeight s) : WithBot (ℕ∞))
\ No newline at end of file