Tried to avoid the finiteness condition on height P

CommAlg/krull.lean

@@ -4,6 +4,7 @@ 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
@@ -270,8 +271,12 @@ lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1
 lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
   krullDim R + 1 ≤ krullDim (Polynomial R) := sorry
 
-lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
-  krullDim R + 1 = krullDim (Polynomial R) := sorry
+-- lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
+--   krullDim R + 1 = krullDim (Polynomial R) := sorry
+
+lemma krull_height_theorem [Nontrivial R] [IsNoetherianRing R] (P: PrimeSpectrum R) (S: Finset R)
+  (h: P.asIdeal ∈ Ideal.minimalPrimes (Ideal.span S)) : height P ≤ S.card := by
+  sorry
 
 lemma dim_mvPolynomial [Field K] (n : ℕ) : krullDim (MvPolynomial (Fin n) K) = n := sorry
 

CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean

@@ -8,38 +8,54 @@ import Mathlib.RingTheory.Localization.AtPrime
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Data.Set.Ncard
+import CommAlg.krull
 
 namespace Ideal
 
 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
-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
+/--
+-- 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
+-- 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
 
 noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice
 
-lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
-  krullDim R + 1 ≤ krullDim (Polynomial R) := sorry -- Others are working on it
+-- lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
+--   krullDim R + 1 ≤ krullDim (Polynomial R) := sorry -- Others are working on it
 
-lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := sorry -- Already done in main file
+-- lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := sorry -- Already done in main file
 
-lemma primeIdeal_finite_height_of_noetherianRing [Nontrivial R] [IsNoetherianRing R] (P: PrimeSpectrum R) : height P ≠ ⊤ := by
-  sorry
+-- lemma primeIdeal_finite_height_of_noetherianRing [Nontrivial R] [IsNoetherianRing R]
+--   (P: PrimeSpectrum R) : height P ≠ ⊤ := by
+--   sorry
+--/
 
-lemma exist_elts_MinimalOver_of_primeIdeal_of_noetherianRing [Nontrivial R] [IsNoetherianRing R] (P: PrimeSpectrum R) :
+lemma exist_elts_MinimalOver_of_primeIdeal_of_noetherianRing [Nontrivial R] [IsNoetherianRing R]
+  (P: PrimeSpectrum R) (h : height P < ⊤) :
   ∃S : Set R, Set.ncard s = height P ∧ P.asIdeal ∈ Ideal.minimalPrimes (Ideal.span S) := by
   sorry
 
-lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
+lemma dim_eq_dim_polynomial_add_one [h1: Nontrivial R] [IsNoetherianRing R] :
   krullDim R + 1 = krullDim (Polynomial R) := by
   rw [le_antisymm_iff]
   constructor
   · exact dim_le_dim_polynomial_add_one
-  · unfold krullDim
-    have htPBdd : ∀ (P : PrimeSpectrum (Polynomial R)), (height P : WithBot ℕ∞) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by
+  · by_cases krullDim R = ⊤
+    calc
+      krullDim (Polynomial R) ≤ ⊤ := le_top
+      _ ≤ krullDim R := top_le_iff.mpr h 
+      _ ≤ krullDim R + 1 := by
+        apply le_of_eq
+        rw [h]
+        rfl
+    have h:= Ne.lt_top h
+    unfold krullDim
+    have htPBdd : ∀ (P : PrimeSpectrum (Polynomial R)), (height P : WithBot ℕ∞)
+          ≤ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by
       intro P
       have : ∃ (I : PrimeSpectrum R), (height P : WithBot ℕ∞) ≤ ↑(height I + 1) := by
         have : ∃ M, Ideal.IsMaximal M ∧ P.asIdeal ≤ M := by
@@ -53,7 +69,6 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
         simp only [WithBot.coe_le_coe]
         have : ∃ (I : PrimeSpectrum R), height P' ≤ height I + 1 := by
           -- Prime avoidance is called subset_union_prime
-
           sorry
         obtain ⟨I, h⟩ := this
         use I
@@ -62,7 +77,8 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
       have : (↑(height I + 1) : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum R), ↑(height I + 1) := by
         apply @le_iSup (WithBot ℕ∞) _ _ _ I
       exact ge_trans this IP
-    have oneOut : (⨆ (I : PrimeSpectrum R), (height I : WithBot ℕ∞) + 1) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by
+    have oneOut : (⨆ (I : PrimeSpectrum R), (height I : WithBot ℕ∞) + 1)
+          ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by
       have : ∀ P : PrimeSpectrum R, (height P : WithBot ℕ∞) + 1 ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 :=
         fun P ↦ (by apply add_le_add_right (@le_iSup (WithBot ℕ∞) _ _ _ P) 1)
       apply iSup_le