From b0b3bdceb390c0abc77a121e3e4d92db3a2c3d9a Mon Sep 17 00:00:00 2001
From: leopoldmayer <leomayer@uw.edu>
Date: Sat, 10 Jun 2023 06:58:23 -0700
Subject: [PATCH 1/3] removed unnecessary file

---
 CommAlg.lean | 1 -
 1 file changed, 1 deletion(-)
 delete mode 100644 CommAlg.lean

diff --git a/CommAlg.lean b/CommAlg.lean
deleted file mode 100644
index e99d3a6..0000000
--- a/CommAlg.lean
+++ /dev/null
@@ -1 +0,0 @@
-def hello := "world"
\ No newline at end of file

From 97d219fe2162cf2c1d08aa7d5fa65364a8768f8b Mon Sep 17 00:00:00 2001
From: leopoldmayer <leomayer@uw.edu>
Date: Sat, 10 Jun 2023 07:27:37 -0700
Subject: [PATCH 2/3] added resources file to dump useful links

---
 comm_alg/resources.lean | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 comm_alg/resources.lean

diff --git a/comm_alg/resources.lean b/comm_alg/resources.lean
new file mode 100644
index 0000000..feb671a
--- /dev/null
+++ b/comm_alg/resources.lean
@@ -0,0 +1,40 @@
+/-
+We don't want to reinvent the wheel, but finding
+things in Mathlib can be pretty annoying. This is
+a temporary file intended to be a dumping ground for
+useful lemmas and definitions
+-/
+import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.Noetherian
+import Mathlib.RingTheory.Artinian
+import Mathlib.Order.Height
+
+variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M]
+
+--ideals are defined
+#check Ideal R
+
+variable (I : Ideal R)
+
+--as are prime and maximal (they are defined as typeclasses)
+#check (I.IsPrime)
+#check (I.IsMaximal)
+
+--a module being Noetherian is also a class
+#check IsNoetherian M
+#check IsNoetherian I
+
+--a ring is Noetherian if it is Noetherian as a module over itself
+#check IsNoetherianRing R
+
+--ditto for Artinian
+#check IsArtinian M
+#check IsArtinianRing R
+
+--I can't find the theorem that an Artinian ring is noetherian. That could be a good
+--thing to add at some point
+
+
+
+--Here's the main defintion that will be helpful
+#check Set.chainHeight
\ No newline at end of file

From 1fd4e29c875d0640d120ab17b9e97e753e878128 Mon Sep 17 00:00:00 2001
From: leopoldmayer <leomayer@uw.edu>
Date: Sat, 10 Jun 2023 08:13:10 -0700
Subject: [PATCH 3/3] added statements of lemmas we'd like to prove

---
 comm_alg/krull.lean     | 44 +++++++++++++++++++++++++++++++++++++++++
 comm_alg/resources.lean |  9 ++++++++-
 2 files changed, 52 insertions(+), 1 deletion(-)
 create mode 100644 comm_alg/krull.lean

diff --git a/comm_alg/krull.lean b/comm_alg/krull.lean
new file mode 100644
index 0000000..2a5af42
--- /dev/null
+++ b/comm_alg/krull.lean
@@ -0,0 +1,44 @@
+import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.Order.Height
+import Mathlib.RingTheory.PrincipalIdealDomain
+import Mathlib.RingTheory.DedekindDomain.Basic
+import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Localization.AtPrime
+
+/- This file contains the definitions of height of an ideal, and the krull
+  dimension of a commutative ring.
+  There are also sorried statements of many of the theorems that would be
+  really nice to prove.
+  I'm imagining for this file to ultimately contain basic API for height and
+  krull dimension, and the theorems will probably end up other files,
+  depending on how long the proofs are, and what extra API needs to be
+  developed.
+-/
+
+variable {R : Type _} [CommRing R] (I : Ideal R)
+
+namespace ideal
+
+noncomputable def height : ℕ∞ := Set.chainHeight {J | J ≤ I ∧ J.IsPrime}
+
+noncomputable def krull_dim (R : Type _) [CommRing R] := height (⊤ : Ideal R)
+
+--some propositions that would be nice to be able to eventually
+
+lemma dim_eq_zero_iff_field : krull_dim R = 0 ↔ IsField R := sorry
+
+#check Ring.DimensionLEOne
+lemma dim_le_one_iff : krull_dim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry
+
+lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krull_dim R ≤ 1 := sorry
+
+lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
+  krull_dim R ≤ krull_dim (Polynomial R) + 1 := sorry
+
+lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
+  krull_dim R = krull_dim (Polynomial R) + 1 := sorry
+
+lemma height_eq_dim_localization [Ideal.IsPrime I] :
+  height I = krull_dim (Localization.AtPrime I) := sorry
+
+lemma height_add_dim_quotient_le_dim : height I + krull_dim (R ⧸ I) ≤ krull_dim R := sorry
\ No newline at end of file
diff --git a/comm_alg/resources.lean b/comm_alg/resources.lean
index feb671a..eae7c89 100644
--- a/comm_alg/resources.lean
+++ b/comm_alg/resources.lean
@@ -8,6 +8,7 @@ import Mathlib.RingTheory.Ideal.Basic
 import Mathlib.RingTheory.Noetherian
 import Mathlib.RingTheory.Artinian
 import Mathlib.Order.Height
+import Mathlib.RingTheory.MvPolynomial.Basic
 
 variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M]
 
@@ -37,4 +38,10 @@ variable (I : Ideal R)
 
 
 --Here's the main defintion that will be helpful
-#check Set.chainHeight
\ No newline at end of file
+#check Set.chainHeight
+
+--this is the polynomial ring R[x]
+#check Polynomial R
+--this is the polynomial ring with variables indexed by ℕ
+#check MvPolynomial ℕ R
+--hopefully there's good communication between them
\ No newline at end of file