From c5a522392cd703af6637fa8dfd87d88d42477e7a Mon Sep 17 00:00:00 2001
From: GTBarkley <barkleygrant@gmail.com>
Date: Mon, 12 Jun 2023 17:44:27 +0000
Subject: [PATCH] renamed comm_alg folder so imports work

---
 {comm_alg => CommAlg}/grant.lean              | 24 ++++++++-----------
 .../jayden(krull-dim-zero).lean               |  0
 {comm_alg => CommAlg}/krull.lean              |  0
 {comm_alg => CommAlg}/resources.lean          |  0
 lakefile.lean                                 | 13 ++++------
 5 files changed, 15 insertions(+), 22 deletions(-)
 rename {comm_alg => CommAlg}/grant.lean (68%)
 rename {comm_alg => CommAlg}/jayden(krull-dim-zero).lean (100%)
 rename {comm_alg => CommAlg}/krull.lean (100%)
 rename {comm_alg => CommAlg}/resources.lean (100%)

diff --git a/comm_alg/grant.lean b/CommAlg/grant.lean
similarity index 68%
rename from comm_alg/grant.lean
rename to CommAlg/grant.lean
index 8586fa3..e1ea335 100644
--- a/comm_alg/grant.lean
+++ b/CommAlg/grant.lean
@@ -2,6 +2,7 @@ import Mathlib.Order.KrullDimension
 import Mathlib.Order.JordanHolder
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import Mathlib.Order.Height
+import CommAlg.krull
 
 
 #check (p q : PrimeSpectrum _) → (p ≤ q)
@@ -10,6 +11,9 @@ import Mathlib.Order.Height
 -- Dimension of a ring
 #check krullDim (PrimeSpectrum _)
 
+
+#check Set.chainHeight {M' : Submodule _ _ | M' < _}
+
 -- Length of a module
 #check krullDim (Submodule _ _)
 
@@ -39,22 +43,14 @@ 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
-
-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
+lemma krullDim_le_iff' (R : Type _) [CommRing R] : 
+  Ideal.krullDim R ≤ n ↔ (∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1) := by
+    sorry
+
+lemma krullDim_ge_iff' (R : Type _) [CommRing R] : 
+  Ideal.krullDim R ≥ n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 := sorry
 
 
 -- #check ((4 : ℕ∞) : WithBot (WithTop ℕ))
diff --git a/comm_alg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean
similarity index 100%
rename from comm_alg/jayden(krull-dim-zero).lean
rename to CommAlg/jayden(krull-dim-zero).lean
diff --git a/comm_alg/krull.lean b/CommAlg/krull.lean
similarity index 100%
rename from comm_alg/krull.lean
rename to CommAlg/krull.lean
diff --git a/comm_alg/resources.lean b/CommAlg/resources.lean
similarity index 100%
rename from comm_alg/resources.lean
rename to CommAlg/resources.lean
diff --git a/lakefile.lean b/lakefile.lean
index 6cad1c5..6a57a84 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -1,14 +1,11 @@
 import Lake
 open Lake DSL
 
-package «comm_alg» {
-  -- add any package configuration options here
-}
+package comm_alg
+
+@[default_target]
+lean_lib CommAlg where
+  moreLeanArgs := #["-Dpp.unicode.fun=true"] -- pretty-prints `fun a ↦ b`
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"
-
-@[default_target]
-lean_lib «CommAlg» {
-  -- add any library configuration options here
-}