From a41873ac1b52a51eaafa29caf112f8827185ea92 Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Mon, 12 Jun 2023 16:25:02 -0700
Subject: [PATCH 1/2] change: Refactoring

---
 CommAlg/sayantan.lean | 28 +++++++++-------------------
 1 file changed, 9 insertions(+), 19 deletions(-)

diff --git a/CommAlg/sayantan.lean b/CommAlg/sayantan.lean
index 553fa4f..90bf5d5 100644
--- a/CommAlg/sayantan.lean
+++ b/CommAlg/sayantan.lean
@@ -9,18 +9,8 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic
 -- import Mathlib.Data.ENat.Lattice
 -- import Mathlib.Order.OrderIsoNat
 -- import Mathlib.Tactic.TFAE
-
 namespace Ideal
 
--- def foo : List Nat := [1, 2, 3, 4, 5]
-
--- #check List.Chain'
-
--- example : List.Chain' (· < ·) foo := by
---   repeat { constructor; norm_num }
-  
-  
-
 example (x : Nat) : List.Chain' (· < ·)  [x] := by
   constructor
 
@@ -36,10 +26,8 @@ lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := r
 lemma krullDim_def (R : Type) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl
 lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl
 
-variable {K : Type _} [Field K]
-
-lemma dim_field_eq_zero : krullDim K = 0 := by
-  have prime_bot (P : Ideal K) : IsPrime P ↔ P = ⊥ := by
+@[simp]
+lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by
       constructor
       · intro primeP
         obtain T := eq_bot_or_top P
@@ -48,9 +36,8 @@ lemma dim_field_eq_zero : krullDim K = 0 := by
       · intro botP
         rw [botP]
         exact bot_prime
-  unfold krullDim
-  have height_zero : ∀ P : PrimeSpectrum K, height P = 0 := by
-    intro P
+
+lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : height P = 0 := by
     unfold height
     simp
     by_contra spec
@@ -59,9 +46,12 @@ lemma dim_field_eq_zero : krullDim K = 0 := by
     obtain ⟨J, JlP : J < P⟩ := spec
     have P0 : IsPrime P.asIdeal := P.IsPrime
     have J0 : IsPrime J.asIdeal := J.IsPrime
-    rw [prime_bot] at P0 J0
+    rw [field_prime_bot] at P0 J0
     have : J.asIdeal = P.asIdeal := Eq.trans J0 (Eq.symm P0)
     have JeqP : J = P := PrimeSpectrum.ext J P this
     have JneqP : J ≠ P := ne_of_lt JlP
     contradiction
-  simp [height_zero]
+
+lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by
+  unfold krullDim
+  simp [field_prime_height_zero]

From 6bbeb7e36d15abf34012208ff301eda1d461efea Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Mon, 12 Jun 2023 21:55:06 -0700
Subject: [PATCH 2/2] new: Made some progress on the other side of
 dim_eq_zero_iff_field

---
 CommAlg/sayantan.lean | 28 +++++++++++++++++++++-------
 1 file changed, 21 insertions(+), 7 deletions(-)

diff --git a/CommAlg/sayantan.lean b/CommAlg/sayantan.lean
index 90bf5d5..b2fc79a 100644
--- a/CommAlg/sayantan.lean
+++ b/CommAlg/sayantan.lean
@@ -6,9 +6,7 @@ import Mathlib.RingTheory.Ideal.Quotient
 import Mathlib.RingTheory.Localization.AtPrime
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
--- import Mathlib.Data.ENat.Lattice
--- import Mathlib.Order.OrderIsoNat
--- import Mathlib.Tactic.TFAE
+
 namespace Ideal
 
 example (x : Nat) : List.Chain' (· < ·)  [x] := by
@@ -17,9 +15,7 @@ example (x : Nat) : List.Chain' (· < ·)  [x] := by
 
   
 variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
-
 noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I}
-
 noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I
 
 lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl
@@ -48,10 +44,28 @@ lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : heig
     have J0 : IsPrime J.asIdeal := J.IsPrime
     rw [field_prime_bot] at P0 J0
     have : J.asIdeal = P.asIdeal := Eq.trans J0 (Eq.symm P0)
-    have JeqP : J = P := PrimeSpectrum.ext J P this
-    have JneqP : J ≠ P := ne_of_lt JlP
+    have : J = P := PrimeSpectrum.ext J P this
+    have : J ≠ P := ne_of_lt JlP
     contradiction
 
 lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by
   unfold krullDim
   simp [field_prime_height_zero]
+
+lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by
+  unfold krullDim at h
+  simp [height] at h
+  by_contra x
+  rw [Ring.not_isField_iff_exists_prime] at x
+  obtain ⟨P, ⟨h, primeP⟩⟩ := x
+  have PgtBot : P > ⊥ := Ne.bot_lt h
+  sorry
+
+lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
+  constructor
+  · exact isField.dim_zero
+  · intro fieldD
+    have : Field D := IsField.toField fieldD
+    -- Not exactly sure why this is failing
+    -- apply @dim_field_eq_zero D _
+    sorry