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] 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