From 01bce563a54a421dd25d2ef8143ec319bc38de6e Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Thu, 15 Jun 2023 19:33:24 -0700
Subject: [PATCH 1/3] One side of poly_over_field

---
 CommAlg/sayantan(poly_over_field).lean | 45 ++++++++++++++++++++++++++
 1 file changed, 45 insertions(+)
 create mode 100644 CommAlg/sayantan(poly_over_field).lean

diff --git a/CommAlg/sayantan(poly_over_field).lean b/CommAlg/sayantan(poly_over_field).lean
new file mode 100644
index 0000000..5379c52
--- /dev/null
+++ b/CommAlg/sayantan(poly_over_field).lean
@@ -0,0 +1,45 @@
+import CommAlg.krull
+import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.RingTheory.FiniteType
+import Mathlib.Order.Height
+import Mathlib.RingTheory.PrincipalIdealDomain
+import Mathlib.RingTheory.DedekindDomain.Basic
+import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Ideal.MinimalPrime
+import Mathlib.RingTheory.Localization.AtPrime
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
+
+namespace Ideal
+
+lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullDim (Polynomial K) = 1 := by
+  -- unfold krullDim
+  rw [le_antisymm_iff]
+  constructor
+  · sorry
+  · suffices : ∃I : PrimeSpectrum (Polynomial K), 1 ≤ (height I : WithBot ℕ∞)
+    · obtain ⟨I, h⟩ := this
+      have :  (height I : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum (Polynomial K)), ↑(height I) := by
+        apply @le_iSup (WithBot ℕ∞) _ _ _ I
+      exact le_trans h this
+    have primeX : Prime Polynomial.X := @Polynomial.prime_X K _ _
+    let X := @Polynomial.X K _
+    have : IsPrime (span {X}) := by
+      refine Iff.mpr (span_singleton_prime ?hp) primeX
+      exact Polynomial.X_ne_zero
+    let P := PrimeSpectrum.mk (span {X}) this
+    unfold height
+    use P
+    have : ⊥ ∈ {J | J < P} := by
+      simp only [Set.mem_setOf_eq]
+      rw [bot_lt_iff_ne_bot]
+      suffices : P.asIdeal ≠ ⊥
+      · by_contra x
+        rw [PrimeSpectrum.ext_iff] at x
+        contradiction
+      by_contra x
+      simp only [span_singleton_eq_bot] at x
+      have := @Polynomial.X_ne_zero K _ _
+      contradiction
+    have : {J | J < P}.Nonempty := Set.nonempty_of_mem this
+    rwa [←Set.one_le_chainHeight_iff, ←WithBot.one_le_coe] at this

From e9fbb1a521ee4e39ea091544e35a44ccc7847f5c Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Thu, 15 Jun 2023 19:34:20 -0700
Subject: [PATCH 2/3] Minor changes

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

diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index bd9edb4..1c70814 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -86,7 +86,7 @@ lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) :
           fun _ ↦ (WithBot.coe_le rfl).mpr (H1 _)
       rw [←iSup_le_iff] at H1
       have : ((n : ℕ∞) : WithBot ℕ∞) ≤ (((n  - 1 : ℕ) : ℕ∞) : WithBot ℕ∞) := le_trans H H1
-      norm_cast at  this
+      norm_cast at this
       have that : n - 1 < n := by refine Nat.sub_lt h (by norm_num)
       apply lt_irrefl (n-1) (trans that this)
   · rintro ⟨I, h⟩
@@ -278,7 +278,7 @@ lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim
     have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this
     unfold height
     rw [←Set.one_le_chainHeight_iff] at this
-    exact not_le_of_gt (Iff.mp ENat.one_le_iff_pos this)
+    exact not_le_of_gt (ENat.one_le_iff_pos.mp this)
   have nonpos_height : height P' ≤ 0 := by
     have := height_le_krullDim P'
     rw [h] at this

From eb1e6118a05c375ee5d07150f9eedaede254e80c Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Thu, 15 Jun 2023 19:36:02 -0700
Subject: [PATCH 3/3] Some changes to dim_eq_dim_poly_add_one

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

diff --git a/CommAlg/sayantan(poly_over_field).lean b/CommAlg/sayantan(poly_over_field).lean
index 5379c52..987fe93 100644
--- a/CommAlg/sayantan(poly_over_field).lean
+++ b/CommAlg/sayantan(poly_over_field).lean
@@ -16,7 +16,8 @@ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullD
   -- unfold krullDim
   rw [le_antisymm_iff]
   constructor
-  · sorry
+  · 
+    sorry
   · suffices : ∃I : PrimeSpectrum (Polynomial K), 1 ≤ (height I : WithBot ℕ∞)
     · obtain ⟨I, h⟩ := this
       have :  (height I : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum (Polynomial K)), ↑(height I) := by