From 7173aefe8d9e171bac69d087b87a9276d30ba70b Mon Sep 17 00:00:00 2001
From: GTBarkley <barkleygrant@gmail.com>
Date: Wed, 14 Jun 2023 17:43:16 +0000
Subject: [PATCH 1/6] changed type of 1 in dim_le_one_of_dimLEOne

---
 CommAlg/krull.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index 06e6d0d..27c3d7e 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -197,7 +197,8 @@ height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain'
 
 /-- The converse of this is false, because the definition of "dimension ≤ 1" in mathlib
   applies only to dimension zero rings and domains of dimension 1. -/
-lemma dim_le_one_of_dimLEOne :  Ring.DimensionLEOne R → krullDim R ≤ (1 : ℕ) := by
+lemma dim_le_one_of_dimLEOne :  Ring.DimensionLEOne R → krullDim R ≤ 1 := by
+  show _ → ((_ : WithBot ℕ∞) ≤ (1 : ℕ))
   rw [krullDim_le_iff R 1]
   intro H p
   apply le_of_not_gt

From 3c4cfeab65b8d9d4d1c07282cf30596f3d017231 Mon Sep 17 00:00:00 2001
From: GTBarkley <barkleygrant@gmail.com>
Date: Wed, 14 Jun 2023 20:28:19 +0000
Subject: [PATCH 2/6] proved dim_le_zero_iff

---
 CommAlg/grant.lean | 42 ++++++++++++++++++++
 CommAlg/krull.lean | 97 +++++++++++++++++++++++++++++++++-------------
 2 files changed, 111 insertions(+), 28 deletions(-)

diff --git a/CommAlg/grant.lean b/CommAlg/grant.lean
index c12b189..76a470c 100644
--- a/CommAlg/grant.lean
+++ b/CommAlg/grant.lean
@@ -171,6 +171,48 @@ lemma dim_le_one_of_dimLEOne :  Ring.DimensionLEOne R → krullDim R ≤ (1 : 
   apply (IsCoatom.lt_iff H.out).mp
   exact hc2
   --refine Iff.mp radical_eq_top (?_ (id (Eq.symm hc3))) 
+
+lemma not_maximal_of_lt_prime {p : Ideal R} {q : Ideal R} (hq : IsPrime q) (h : p < q) : ¬IsMaximal p := by
+  intro hp
+  apply IsPrime.ne_top hq
+  apply (IsCoatom.lt_iff hp.out).mp
+  exact h
+
+lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
+  show ((_ : WithBot ℕ∞) ≤ (0 : ℕ)) ↔ _
+  rw [krullDim_le_iff R 0]
+  constructor <;> intro h I
+  . contrapose! h
+    have ⟨𝔪, h𝔪⟩ := I.asIdeal.exists_le_maximal (IsPrime.ne_top I.IsPrime)
+    let 𝔪p := (⟨𝔪, IsMaximal.isPrime h𝔪.1⟩ : PrimeSpectrum R)
+    have hstrct : I < 𝔪p := by
+      apply lt_of_le_of_ne h𝔪.2
+      intro hcontr
+      rw [hcontr] at h
+      exact h h𝔪.1
+    use 𝔪p
+    show (_ : WithBot ℕ∞) > (0 : ℕ∞)
+    rw [_root_.lt_height_iff'']
+    use [I]
+    constructor
+    . exact List.chain'_singleton _
+    . constructor
+      . intro I' hI'
+        simp at hI'
+        rwa [hI']
+      . simp
+  . contrapose! h
+    change (_ : WithBot ℕ∞) > (0 : ℕ∞) at h
+    rw [_root_.lt_height_iff''] at h
+    obtain ⟨c, _, hc2, hc3⟩ := h
+    norm_cast at hc3
+    rw [List.length_eq_one] at hc3
+    obtain ⟨𝔮, h𝔮⟩ := hc3
+    use 𝔮
+    specialize hc2 𝔮 (h𝔮 ▸ (List.mem_singleton.mpr rfl))
+    apply not_maximal_of_lt_prime _ I.IsPrime
+    exact hc2
+
 end Krull
 
 section iSupWithBot
diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index 27c3d7e..d58a065 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -65,6 +65,34 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) :=
     exact I.2.1
   . simp
 
+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
+    . exact (not_le.mpr h) le_top
+    . tauto
+  have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by
+    symm
+    show (n + 1 ≤ m ↔ _ )
+    apply ENat.add_one_le_iff
+    exact ENat.coe_ne_top _
+  rw [this]
+  unfold Ideal.height
+  show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞))
+  rw [{J | J < 𝔭}.le_chainHeight_iff]
+  show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
+  constructor <;> rintro ⟨c, hc⟩ <;> use c
+  . tauto
+  . change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc
+    norm_cast at hc
+    tauto
+
+lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
+height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
+  show (_ < _) ↔ _
+  rw [WithBot.coe_lt_coe]
+  exact lt_height_iff'
+
 #check height_le_krullDim
 --some propositions that would be nice to be able to eventually
 
@@ -99,6 +127,47 @@ lemma krullDim_nonneg_of_nontrivial (R : Type _) [CommRing R] [Nontrivial R] : 
   lift (Ideal.krullDim R) to ℕ∞ using h with k
   use k
 
+lemma not_maximal_of_lt_prime {p : Ideal R} {q : Ideal R} (hq : IsPrime q) (h : p < q) : ¬IsMaximal p := by
+  intro hp
+  apply IsPrime.ne_top hq
+  apply (IsCoatom.lt_iff hp.out).mp
+  exact h
+
+lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
+  show ((_ : WithBot ℕ∞) ≤ (0 : ℕ)) ↔ _
+  rw [krullDim_le_iff R 0]
+  constructor <;> intro h I
+  . contrapose! h
+    have ⟨𝔪, h𝔪⟩ := I.asIdeal.exists_le_maximal (IsPrime.ne_top I.IsPrime)
+    let 𝔪p := (⟨𝔪, IsMaximal.isPrime h𝔪.1⟩ : PrimeSpectrum R)
+    have hstrct : I < 𝔪p := by
+      apply lt_of_le_of_ne h𝔪.2
+      intro hcontr
+      rw [hcontr] at h
+      exact h h𝔪.1
+    use 𝔪p
+    show (_ : WithBot ℕ∞) > (0 : ℕ∞)
+    rw [lt_height_iff'']
+    use [I]
+    constructor
+    . exact List.chain'_singleton _
+    . constructor
+      . intro I' hI'
+        simp at hI'
+        rwa [hI']
+      . simp
+  . contrapose! h
+    change (_ : WithBot ℕ∞) > (0 : ℕ∞) at h
+    rw [lt_height_iff''] at h
+    obtain ⟨c, _, hc2, hc3⟩ := h
+    norm_cast at hc3
+    rw [List.length_eq_one] at hc3
+    obtain ⟨𝔮, h𝔮⟩ := hc3
+    use 𝔮
+    specialize hc2 𝔮 (h𝔮 ▸ (List.mem_singleton.mpr rfl))
+    apply not_maximal_of_lt_prime I.IsPrime
+    exact hc2
+
 lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
   constructor <;> intro h
   . intro I
@@ -167,34 +236,6 @@ lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D =
 -- This lemma is false!
 lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry
 
-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
-    . exact (not_le.mpr h) le_top
-    . tauto
-  have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by
-    symm
-    show (n + 1 ≤ m ↔ _ )
-    apply ENat.add_one_le_iff
-    exact ENat.coe_ne_top _
-  rw [this]
-  unfold Ideal.height
-  show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞))
-  rw [{J | J < 𝔭}.le_chainHeight_iff]
-  show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
-  constructor <;> rintro ⟨c, hc⟩ <;> use c
-  . tauto
-  . change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc
-    norm_cast at hc
-    tauto
-
-lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
-height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
-  show (_ < _) ↔ _
-  rw [WithBot.coe_lt_coe]
-  exact lt_height_iff'
-
 /-- The converse of this is false, because the definition of "dimension ≤ 1" in mathlib
   applies only to dimension zero rings and domains of dimension 1. -/
 lemma dim_le_one_of_dimLEOne :  Ring.DimensionLEOne R → krullDim R ≤ 1 := by

From 0773a97fb544e404b0f7dfcc2707d08f6b79104e Mon Sep 17 00:00:00 2001
From: Andre <espietandre@gmail.com>
Date: Wed, 14 Jun 2023 16:28:25 -0400
Subject: [PATCH 3/6] reduced imports poly_type

---
 CommAlg/poly_type.lean | 20 +-------------------
 1 file changed, 1 insertion(+), 19 deletions(-)

diff --git a/CommAlg/poly_type.lean b/CommAlg/poly_type.lean
index ab3b4c1..52fa754 100644
--- a/CommAlg/poly_type.lean
+++ b/CommAlg/poly_type.lean
@@ -1,24 +1,6 @@
-import Mathlib
-import Mathlib.Algebra.MonoidAlgebra.Basic
-import Mathlib.Data.Finset.Sort
 import Mathlib.Order.Height
-import Mathlib.Order.KrullDimension
-import Mathlib.Order.JordanHolder
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
-import Mathlib.Order.Height
-import Mathlib.RingTheory.Ideal.Basic
-import Mathlib.RingTheory.Ideal.Operations
-import Mathlib.LinearAlgebra.Finsupp
-import Mathlib.RingTheory.GradedAlgebra.Basic
-import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal
-import Mathlib.Algebra.Module.GradedModule
-import Mathlib.RingTheory.Ideal.AssociatedPrime
-import Mathlib.RingTheory.Noetherian
-import Mathlib.RingTheory.Artinian
-import Mathlib.Algebra.Module.GradedModule
-import Mathlib.RingTheory.Noetherian
-import Mathlib.RingTheory.Finiteness
-import Mathlib.RingTheory.Ideal.Operations
+
 
 -- Setting for "library_search"
 set_option maxHeartbeats 0

From cf7f08df3eed4c8138e985e069a1d998083cf3c6 Mon Sep 17 00:00:00 2001
From: monula95 dutta <monula95@gmail.com>
Date: Wed, 14 Jun 2023 20:31:39 +0000
Subject: [PATCH 4/6] added associated prime graded

---
 CommAlg/monalisa.lean | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/CommAlg/monalisa.lean b/CommAlg/monalisa.lean
index 357578b..43cb907 100644
--- a/CommAlg/monalisa.lean
+++ b/CommAlg/monalisa.lean
@@ -4,6 +4,8 @@ import Mathlib.Algebra.Module.GradedModule
 import Mathlib.RingTheory.Ideal.AssociatedPrime
 import Mathlib.RingTheory.Artinian
 import Mathlib.Order.Height
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
+import Mathlib.RingTheory.FiniteType
 
 noncomputable def length ( A : Type _) (M : Type _)
  [CommRing A] [AddCommGroup M] [Module A M] :=  Set.chainHeight {M' : Submodule A M | M' < ⊤}
@@ -87,19 +89,15 @@ theorem hilbert_polynomial_0 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [
 : true := by
   sorry
 
-lemma ass_graded (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) 
-[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
-[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜]
-(p : associatedPrimes (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) : (HomogeneousMax 𝒜 p) := by
-sorry
-
 lemma Associated_prime_of_graded_is_graded
 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) 
 [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
 [DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜]
 (p : associatedPrimes (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
-  : (Ideal.IsHomogeneous' 𝒜 p) ∧ ((∃ (i : ℤ ), ∃ (x :  𝒜 i), p = (Submodule.span (⨁ i, 𝒜 i) {DirectSum.of x i}).annihilator)) := by
+  : (Ideal.IsHomogeneous' 𝒜 p) ∧ ((∃ (i : ℤ ), ∃ (x :  𝒜 i), p = (Submodule.span (⨁ i, 𝒜 i) {DirectSum.of _ i x}).annihilator)) := by
   sorry
 
 
-def standard_graded (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (I : Ideal (⨁ i, 𝒜 i)) := (⨁ i, 𝒜 i)
+-- def standard_graded {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (n : ℕ) :
+--     Prop :=
+--   ∃ J, Ideal.IsHomogeneous' 𝒜 J (J :Nonempty ((⨁ i, 𝒜 i) ≃+* (MvPolynomial (Fin n) (𝒜 0)) ⧸ J)

From a62a8bfe4d73b3c5bfa77168fe6f8b13f6b55f46 Mon Sep 17 00:00:00 2001
From: Andre <espietandre@gmail.com>
Date: Wed, 14 Jun 2023 16:37:08 -0400
Subject: [PATCH 5/6] removed two imports

---
 CommAlg/monalisa.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/CommAlg/monalisa.lean b/CommAlg/monalisa.lean
index 43cb907..68579da 100644
--- a/CommAlg/monalisa.lean
+++ b/CommAlg/monalisa.lean
@@ -4,8 +4,6 @@ import Mathlib.Algebra.Module.GradedModule
 import Mathlib.RingTheory.Ideal.AssociatedPrime
 import Mathlib.RingTheory.Artinian
 import Mathlib.Order.Height
-import Mathlib.Order.ConditionallyCompleteLattice.Basic
-import Mathlib.RingTheory.FiniteType
 
 noncomputable def length ( A : Type _) (M : Type _)
  [CommRing A] [AddCommGroup M] [Module A M] :=  Set.chainHeight {M' : Submodule A M | M' < ⊤}

From 46908891497cd2510c470a563e127b48843a2b76 Mon Sep 17 00:00:00 2001
From: GTBarkley <barkleygrant@gmail.com>
Date: Wed, 14 Jun 2023 21:35:36 +0000
Subject: [PATCH 6/6] proved dim_eq_zero_iff

---
 CommAlg/krull.lean | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index d58a065..b2d0230 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -169,11 +169,16 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal
     exact hc2
 
 lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
-  constructor <;> intro h
-  . intro I
-    sorry
-  . sorry
-  
+  rw [←dim_le_zero_iff]
+  obtain ⟨n, hn⟩ := krullDim_nonneg_of_nontrivial R
+  have : n ≥ 0 := zero_le n
+  change _ ≤ _ at this
+  rw [←WithBot.coe_le_coe,←hn] at this
+  change (0 : WithBot ℕ∞) ≤ _ at this
+  constructor <;> intro h'
+  rw [h']
+  exact le_antisymm h' this
+
 @[simp]
 lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by
       constructor