Merge pull request #83 from GTBarkley/main

update with main

CommAlg/Leo.lean

@@ -0,0 +1,334 @@
+import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.RingTheory.FiniteType
+import Mathlib.Order.Height
+import Mathlib.RingTheory.Polynomial.Quotient
+import Mathlib.RingTheory.PrincipalIdealDomain
+import Mathlib.RingTheory.DedekindDomain.Basic
+import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Localization.AtPrime
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
+import CommAlg.krull
+
+section AddToOrder
+
+open List hiding le_antisymm
+open OrderDual
+
+universe u v
+
+variable {α β : Type _}
+variable [LT α] [LT β] (s t : Set α)
+
+namespace Set
+
+theorem append_mem_subchain_iff :
+l ++ l' ∈ s.subchain ↔ l ∈ s.subchain ∧ l' ∈ s.subchain ∧ ∀ a ∈ l.getLast?, ∀ b ∈ l'.head?, a < b := by
+  simp [subchain, chain'_append]
+  aesop
+
+end Set
+
+namespace List
+#check Option
+
+theorem getLast?_map (l : List α) (f : α → β) :
+  (l.map f).getLast? = Option.map f (l.getLast?) := by
+  cases' l with a l
+  . rfl
+  induction' l with b l ih
+  . rfl
+  . simp [List.getLast?_cons_cons, ih]
+  
+
+end List
+end AddToOrder
+
+--trying and failing to prove ht p = dim R_p
+section Localization
+
+variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
+variable {S : Type _} [CommRing S] [Algebra R S] [IsLocalization.AtPrime S I.asIdeal]
+
+open Ideal
+open LocalRing
+open PrimeSpectrum
+
+#check algebraMap R (Localization.AtPrime I.asIdeal)
+#check PrimeSpectrum.comap (algebraMap R (Localization.AtPrime I.asIdeal))
+
+#check krullDim
+#check dim_eq_bot_iff
+#check height_le_krullDim
+
+variable (J₁ J₂ : PrimeSpectrum (Localization.AtPrime I.asIdeal))
+example (h : J₁ ≤ J₂) : PrimeSpectrum.comap (algebraMap R (Localization.AtPrime I.asIdeal)) J₁ ≤
+  PrimeSpectrum.comap (algebraMap R (Localization.AtPrime I.asIdeal)) J₂ := by
+  intro x hx
+  exact h hx
+
+def gadslfasd' : Ideal S := (IsLocalization.AtPrime.localRing S I.asIdeal).maximalIdeal
+
+-- instance gadslfasd : LocalRing S := IsLocalization.AtPrime.localRing S I.asIdeal
+
+example (f : α → β) (hf : Function.Injective f) (h : a₁ ≠ a₂) : f a₁ ≠ f a₂ := by library_search
+
+instance map_prime (J : PrimeSpectrum R) (hJ : J ≤ I) :
+  (Ideal.map (algebraMap R S) J.asIdeal : Ideal S).IsPrime where
+    ne_top' := by
+      intro h
+      rw [eq_top_iff_one, map, mem_span] at h
+    mem_or_mem' := sorry
+
+lemma comap_lt_of_lt (J₁ J₂ : PrimeSpectrum S) (J_lt : J₁ < J₂) : 
+  PrimeSpectrum.comap (algebraMap R S) J₁ < PrimeSpectrum.comap (algebraMap R S) J₂ := by
+  apply lt_of_le_of_ne
+  apply comap_mono (le_of_lt J_lt)
+  sorry
+
+lemma lt_of_comap_lt (J₁ J₂ : PrimeSpectrum S)
+(hJ : PrimeSpectrum.comap (algebraMap R S) J₁ < PrimeSpectrum.comap (algebraMap R S) J₂) :
+J₁ < J₂ := by
+  apply lt_of_le_of_ne
+  sorry
+
+/- If S = R_p, then height p = dim S -/
+lemma height_eq_height_comap (J : PrimeSpectrum S) :
+  height (PrimeSpectrum.comap (algebraMap R S) J) = height J := by
+  simp [height]
+  have H : {J_1 | J_1 < (PrimeSpectrum.comap (algebraMap R S)) J} = 
+    (PrimeSpectrum.comap (algebraMap R S))'' {J_2 | J_2 < J}
+  . sorry
+  rw [H]
+  apply Set.chainHeight_image
+  intro x y
+  constructor
+  apply comap_lt_of_lt
+  apply lt_of_comap_lt
+  
+lemma disjoint_primeCompl (I : PrimeSpectrum R) :
+  { p | Disjoint (I.asIdeal.primeCompl : Set R) p.asIdeal} = {p | p ≤ I} := by
+  ext p; apply Set.disjoint_compl_left_iff_subset
+
+theorem localizationPrime_comap_range [Algebra R S] (I : PrimeSpectrum R) [IsLocalization.AtPrime S I.asIdeal] :
+    Set.range (PrimeSpectrum.comap (algebraMap R S)) = { p | p ≤ I} := by
+    rw [← disjoint_primeCompl]
+    apply localization_comap_range
+
+
+#check Set.chainHeight_image
+
+lemma height_eq_dim_localization : height I = krullDim S := by
+  --first show height I = height gadslfasd'
+  simp [@krullDim_eq_height _ _ (IsLocalization.AtPrime.localRing S I.asIdeal)]
+  simp [height]
+  let f := (PrimeSpectrum.comap (algebraMap R S))
+  have H : {J | J < I} = f '' {J | J < closedPoint S}
+  
+lemma height_eq_dim_localization' :
+  height I = krullDim (Localization.AtPrime I.asIdeal) := Ideal.height_eq_dim_localization I
+
+end Localization
+
+
+
+
+section Polynomial
+
+open Ideal Polynomial
+variables {R : Type _} [CommRing R]
+variable (J : Ideal R[X])
+#check Ideal.comap C J
+
+--given ideals I J, I ⊔ J is their sum
+--given a in R, span {a} is the ideal generated by a
+--the map R → R[X] is C →+*
+--to show p[x] is prime, show p[x] is the kernel of the map R[x] → R → R/p
+#check RingHom.ker_isPrime
+
+def adj_x_map (I : Ideal R) : R[X] →+* R ⧸ I := (Ideal.Quotient.mk I).comp constantCoeff
+--def adj_x_map' (I : Ideal R) : R[X] →+* R ⧸ I := (Ideal.Quotient.mk I).comp (evalRingHom 0)
+def adjoin_x (I : Ideal R) : Ideal (Polynomial R) := RingHom.ker (adj_x_map I)
+def adjoin_x' (I : PrimeSpectrum R) : PrimeSpectrum (Polynomial R) where
+  asIdeal := adjoin_x I.asIdeal
+  IsPrime := RingHom.ker_isPrime _
+
+/- This somehow isn't in Mathlib? -/
+@[simp]
+theorem span_singleton_one : span ({0} : Set R) = ⊥ := by simp only [span_singleton_eq_bot]
+
+theorem coeff_C_eq : RingHom.comp constantCoeff C = RingHom.id R := by ext; simp
+
+variable (I : PrimeSpectrum R)
+#check RingHom.ker (C.comp (Ideal.Quotient.mk I.asIdeal))
+--#check Ideal.Quotient.mk I.asIdeal
+
+def map_prime' (I : PrimeSpectrum R) : IsPrime (I.asIdeal.map C) := Ideal.isPrime_map_C_of_isPrime I.IsPrime
+
+def map_prime'' (I : PrimeSpectrum R) : PrimeSpectrum R[X] := ⟨I.asIdeal.map C, map_prime' I⟩
+
+@[simp]
+lemma adj_x_comp_C (I : Ideal R) : RingHom.comp (adj_x_map I) C = Ideal.Quotient.mk I := by
+  ext x; simp [adj_x_map]
+
+-- ideal.mem_quotient_iff_mem_sup
+lemma adjoin_x_eq (I : Ideal R) : adjoin_x I = I.map C ⊔ Ideal.span {X} := by
+  apply le_antisymm
+  . rintro p hp
+    have h : ∃ q r, p = C r + X * q := ⟨p.divX, p.coeff 0, p.divX_mul_X_add.symm.trans $ by ring⟩
+    obtain ⟨q, r, rfl⟩ := h
+    suffices : r ∈ I
+    . simp only [Submodule.mem_sup, Ideal.mem_span_singleton]
+      refine' ⟨C r, Ideal.mem_map_of_mem C this, X * q, ⟨q, rfl⟩, rfl⟩
+    rw [adjoin_x, adj_x_map, RingHom.mem_ker, RingHom.comp_apply] at hp
+    rw [constantCoeff_apply, coeff_add, coeff_C_zero, coeff_X_mul_zero, add_zero] at hp
+    rwa  [←RingHom.mem_ker, Ideal.mk_ker] at hp
+  . rw [sup_le_iff]
+    constructor
+    . simp [adjoin_x, RingHom.ker, ←map_le_iff_le_comap, Ideal.map_map]
+    . simp [span_le, adjoin_x, RingHom.mem_ker, adj_x_map]
+
+lemma adjoin_x_inj {I J : Ideal R} (h : adjoin_x I = adjoin_x J) : I = J := by
+  simp [adjoin_x_eq] at h
+  have H : Ideal.map constantCoeff (Ideal.map C I ⊔ span {X}) =
+          Ideal.map constantCoeff (Ideal.map C J ⊔ span {X}) := by rw [h]
+  simp [Ideal.map_sup, Ideal.map_span, Ideal.map_map, coeff_C_eq] at H
+  exact H
+
+
+lemma map_lt_adjoin_x (I : PrimeSpectrum R) : map_prime'' I < adjoin_x' I := by
+  simp [map_prime'', adjoin_x', adjoin_x_eq]
+  show Ideal.map C I.asIdeal < Ideal.map C I.asIdeal ⊔ span {X}
+  simp [Ideal.span_le, mem_map_C_iff]
+  use 1
+  simp
+  intro h
+  apply I.IsPrime.ne_top'
+  rw [Ideal.eq_top_iff_one]
+  exact h
+
+lemma map_inj {I J : Ideal R} (h : I.map C = J.map C) : I = J := by
+  have H : Ideal.map constantCoeff (Ideal.map C I) =
+          Ideal.map constantCoeff (Ideal.map C J) := by rw [h]
+  simp [Ideal.map_map, coeff_C_eq] at H
+  exact H
+
+lemma map_strictmono (I J : Ideal R) (h : I < J) : I.map C < J.map C := by
+  rw [lt_iff_le_and_ne] at h ⊢
+  constructor
+  . apply map_mono h.1
+  . intro H
+    exact h.2 (map_inj H)
+
+lemma adjoin_x_strictmono (I J : Ideal R) (h : I < J) : adjoin_x I < adjoin_x J := by
+  rw [lt_iff_le_and_ne] at h ⊢
+  constructor
+  . rw [adjoin_x_eq, adjoin_x_eq]
+    apply sup_le_sup_right
+    apply map_mono h.1
+  . intro H
+    exact h.2 (adjoin_x_inj H)
+
+example (n : ℕ∞) : n + 0 = n := by simp?
+
+#eval List.Chain' (· < ·) [2,3]
+example : [4,5] ++ [2] = [4,5,2] := rfl
+#eval [2,4,5].map (λ n => n + n)
+
+/- Given an ideal p in R, define the ideal p[x] in R[x] -/
+lemma ht_adjoin_x_eq_ht_add_one [Nontrivial R] (I : PrimeSpectrum R) : height I + 1 ≤ height (adjoin_x' I) := by
+  suffices H : height I + (1 : ℕ) ≤ height (adjoin_x' I) + (0 : ℕ)
+  . norm_cast at H; rw [add_zero] at H; exact H
+  rw [height, height, Set.chainHeight_add_le_chainHeight_add {J | J < I} _ 1 0]
+  intro l hl
+  use ((l.map map_prime'') ++ [map_prime'' I])
+  constructor
+  . simp [Set.append_mem_subchain_iff]
+    refine' ⟨_,_,_⟩
+    . show (List.map map_prime'' l).Chain' (· < ·) ∧ ∀ i ∈ _, i ∈ _
+      constructor
+      . apply List.chain'_map_of_chain' map_prime''
+        intro a b hab
+        apply map_strictmono a.asIdeal b.asIdeal
+        exact hab
+        exact hl.1
+      . intro i hi
+        rw [List.mem_map] at hi
+        obtain ⟨a, ha, rfl⟩ := hi
+        show map_prime'' a < adjoin_x' I
+        calc map_prime'' a < map_prime'' I := by apply map_strictmono; apply hl.2; apply ha
+          _ < adjoin_x' I := by apply map_lt_adjoin_x
+    . apply map_lt_adjoin_x
+    . intro a ha
+      have H : ∃ b : PrimeSpectrum R, b ∈ l ∧ map_prime'' b = a
+      . have H2 : l ≠ []
+        . intro h
+          rw [h] at ha
+          tauto
+        use l.getLast H2
+        refine' ⟨List.getLast_mem H2, _⟩
+        have H3 : l.map map_prime'' ≠ []
+        . intro hl
+          apply H2
+          apply List.eq_nil_of_map_eq_nil hl
+        rw [List.getLast?_eq_getLast _ H3, Option.some_inj] at ha
+        simp [←ha, List.getLast_map _ H2]
+      obtain ⟨b, hb, rfl⟩ := H
+      apply map_strictmono
+      apply hl.2
+      exact hb
+  . simp
+
+lemma ne_bot_iff_exists' (n : WithBot ℕ∞) : n ≠ ⊥ ↔ ∃ m : ℕ∞, n = m := by
+  convert WithBot.ne_bot_iff_exists using 3
+  exact comm
+
+
+lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
+  krullDim R + (1 : ℕ∞) ≤ krullDim (Polynomial R) := by
+  cases' krullDim_nonneg_of_nontrivial R with n hn
+  rw [hn]
+  change ↑(n + 1) ≤ krullDim R[X]
+  have hn' := le_of_eq hn.symm
+  rw [le_krullDim_iff'] at hn' ⊢
+  cases' hn' with I hI
+  use adjoin_x' I
+  apply WithBot.coe_mono
+  calc n + 1 ≤ height I + 1 := by
+        apply add_le_add_right
+        rw [WithBot.coe_le_coe] at hI
+        exact hI
+    _ ≤ height (adjoin_x' I) := ht_adjoin_x_eq_ht_add_one I
+  
+
+end Polynomial
+
+open Ideal
+
+variable {R : Type _} [CommRing R]
+
+lemma height_le_top_iff_exists {I : PrimeSpectrum R} (hI : height I ≤ ⊤) :
+  ∃ n : ℕ, true := by
+  sorry
+
+lemma eq_of_height_eq_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) (hJ : height J < ⊤)
+  (ht_eq : height I = height J) : I = J := by
+  by_cases h : I = J
+  . exact h
+  . have I_lt_J := lt_of_le_of_ne I_le_J h
+    exfalso
+    sorry
+
+section Quotient
+
+variables {R : Type _} [CommRing R] (I : Ideal R)
+
+#check List.map <| PrimeSpectrum.comap <| Ideal.Quotient.mk I
+
+lemma comap_chain {l : List (PrimeSpectrum (R ⧸ I))} (hl : l.Chain' (· < ·)) :
+  List.Chain' (. < .) ((List.map <| PrimeSpectrum.comap <| Ideal.Quotient.mk I) l) := by
+
+
+lemma dim_quotient_le_dim : krullDim (R ⧸ I) ≤ krullDim R := by
+
+end Quotient

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

CommAlg/grant2.lean

@@ -0,0 +1,62 @@
+import Mathlib.Order.KrullDimension
+import Mathlib.Order.JordanHolder
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.Order.Height
+import Mathlib.RingTheory.Noetherian
+import CommAlg.krull
+
+variable (R : Type _) [CommRing R] [IsNoetherianRing R]
+
+lemma height_le_of_gt_height_lt {n : ℕ∞} (q : PrimeSpectrum R)
+  (h : ∀(p : PrimeSpectrum R), p < q → Ideal.height p ≤ n - 1) : Ideal.height q ≤ n := by
+  sorry
+   
+
+theorem height_le_one_of_minimal_over_principle (p : PrimeSpectrum R) (x : R):
+  p ∈ minimals (· < ·) {p | x ∈ p.asIdeal} → Ideal.height p ≤ 1 := by
+  intro h
+  apply height_le_of_gt_height_lt _ p
+  intro q qlep
+  by_contra hcontr
+  push_neg at hcontr
+  simp only [le_refl, tsub_eq_zero_of_le] at hcontr 
+  
+  sorry
+
+#check (_ : Ideal R) ^ (_ : ℕ)
+#synth Pow (Ideal R) (ℕ)
+
+def symbolicIdeal(Q : Ideal R) {hin : Q.IsPrime} (I : Ideal R) : Ideal R where
+  carrier := {r : R | ∃ s : R, s ∉ Q ∧ s * r ∈ I}
+  zero_mem' := by
+    simp only [Set.mem_setOf_eq, mul_zero, Submodule.zero_mem, and_true]
+    use 1
+    rw [←Q.ne_top_iff_one]
+    exact hin.ne_top
+  add_mem' := by
+    rintro a b ⟨sa, hsa1, hsa2⟩ ⟨sb, hsb1, hsb2⟩
+    use sa * sb
+    constructor
+    . intro h
+      cases hin.mem_or_mem h <;> contradiction
+    ring_nf
+    apply I.add_mem --<;> simp only [I.mul_mem_left, hsa2, hsb2]
+    . rw [mul_comm sa, mul_assoc]
+      exact I.mul_mem_left sb hsa2 
+    . rw [mul_assoc]
+      exact I.mul_mem_left sa hsb2
+  smul_mem' := by
+    intro c x
+    dsimp
+    rintro ⟨s, hs1, hs2⟩
+    use s
+    constructor; exact hs1
+    rw [←mul_assoc, mul_comm s, mul_assoc]
+    exact Ideal.mul_mem_left _ _ hs2
+
+protected lemma LocalRing.height_le_one_of_minimal_over_principle
+  [LocalRing R] (q : PrimeSpectrum R) {x : R} 
+  (h : (closedPoint R).asIdeal ∈ (Ideal.span {x}).minimalPrimes) :
+  q = closedPoint R ∨ Ideal.height q = 0 := by
+  
+  sorry

CommAlg/jayden(krull-dim-zero).lean

@@ -16,18 +16,18 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Algebra.Ring.Pi
 import Mathlib.RingTheory.Finiteness
 import Mathlib.Util.PiNotation
+import CommAlg.krull
 
 open PiNotation
 
-
 namespace Ideal
 
 variable (R : Type _) [CommRing R] (P : PrimeSpectrum R)
 
-noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < P}
+-- noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < P}
 
-noncomputable def krullDim (R : Type) [CommRing R] :
+-- noncomputable def krullDim (R : Type) [CommRing R] :
-     WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height R I
+--      WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height R I
 
 --variable {R}
 
@@ -43,7 +43,6 @@ class IsLocallyNilpotent {R : Type _} [CommRing R] (I : Ideal R) : Prop :=
 #check Ideal.IsLocallyNilpotent
 end Ideal
 
-
 -- Repeats the definition of the length of a module by Monalisa
 variable (R : Type _) [CommRing R] (I J : Ideal R)
 variable (M : Type _) [AddCommMonoid M] [Module R M]
@@ -67,9 +66,11 @@ lemma ring_Noetherian_iff_spec_Noetherian : IsNoetherianRing R
     ↔ TopologicalSpace.NoetherianSpace (PrimeSpectrum R) := by
     constructor
     intro RisNoetherian
+    sorry
+    sorry
     -- how do I apply an instance to prove one direction?
 
-
+-- Stacks Lemma 5.9.2: 
 -- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible :
 -- Every closed subset of a noetherian space is a finite union 
 -- of irreducible closed subsets.
@@ -100,9 +101,9 @@ lemma containment_radical_power_containment :
 
 -- Stacks Lemma 10.52.6: I is a maximal ideal and IM = 0. Then length of M is
 -- the same as the dimension as a vector space over R/I,
-lemma length_eq_dim_if_maximal_annihilates {I : Ideal R} [Ideal.IsMaximal I] 
+-- lemma length_eq_dim_if_maximal_annihilates {I : Ideal R} [Ideal.IsMaximal I] 
-    : I • (⊤ : Submodule R M) = 0
+--     : I • (⊤ : Submodule R M) = 0
-     → Module.length R M = Module.rank R⧸I M⧸(I • (⊤ : Submodule R M)) := by sorry
+--      → Module.length R M = Module.rank R⧸I M⧸(I • (⊤ : Submodule R M)) := by sorry
 
 -- Does lean know that M/IM is a R/I module?
 -- Use 10.52.5
@@ -116,19 +117,44 @@ lemma power_zero_finite_length [Ideal.IsMaximal I] (h₁ : Ideal.FG I) [Module.F
     -- rcases power with ⟨n, npower⟩
     -- how do I get a generating set?
 
+open Finset
 
 -- Stacks Lemma 10.53.3: R is Artinian iff R has finitely many maximal ideals
 lemma Artinian_has_finite_max_ideal 
     [IsArtinianRing R] : Finite (MaximalSpectrum R) := by 
     by_contra infinite
     simp only [not_finite_iff_infinite] at infinite
-    
+    let m' : ℕ ↪ MaximalSpectrum R := Infinite.natEmbedding (MaximalSpectrum R)
+    have m'inj := m'.injective
+    let m'' : ℕ → Ideal R := fun n : ℕ ↦ ⨅ k ∈ range n, (m' k).asIdeal
+    -- let f : ℕ → MaximalSpectrum R := fun n : ℕ ↦ m' n
+    -- let F : (n : ℕ) → Fin n → MaximalSpectrum R := fun n k ↦ m' k
+    have DCC : ∃ n : ℕ, ∀ k : ℕ, n ≤ k → m'' n = m'' k := by
+      apply IsArtinian.monotone_stabilizes {
+        toFun := m''
+        monotone' := sorry
+      }
+    cases' DCC with n DCCn
+    specialize DCCn (n+1)
+    specialize DCCn (Nat.le_succ n)
+    have containment1 : m'' n < (m' (n + 1)).asIdeal := by sorry
+    have : ∀ (j : ℕ), (j ≠ n + 1) → ∃ x, x ∈ (m' j).asIdeal ∧ x ∉ (m' (n+1)).asIdeal := by
+      intro j jnotn
+      have notcontain : ¬ (m' j).asIdeal ≤ (m' (n+1)).asIdeal := by
+        -- apply Ideal.IsMaximal (m' j).asIdeal
+        sorry
+      sorry
+    sorry
+      -- have distinct : (m' j).asIdeal ≠ (m' (n+1)).asIdeal := by         
+      --   intro h
+      --   apply Function.Injective.ne m'inj jnotn
+      --   exact MaximalSpectrum.ext _ _ h      
+      -- simp
+      -- unfold 
+     
 
 -- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent
-lemma Jacobson_of_Artinian_is_nilpotent 
+-- This is in mathlib: IsArtinianRing.isNilpotent_jacobson_bot
-    [IsArtinianRing R] : IsNilpotent (Ideal.jacobson (⊥ : Ideal R)) := by 
-    have J := Ideal.jacobson (⊥ : Ideal R)
-    
 
 -- Stacks Lemma 10.53.5: If R has finitely many maximal ideals and 
 -- locally nilpotent Jacobson radical, then R is the product of its localizations at 
@@ -142,7 +168,7 @@ abbrev Prod_of_localization :=
      
 def foo : Prod_of_localization R →+* R where
   toFun := sorry
-  invFun := sorry
+  -- invFun := sorry
   left_inv := sorry
   right_inv := sorry
   map_mul' := sorry
@@ -167,23 +193,27 @@ lemma primes_of_Artinian_are_maximal
 
 -- Lemma: Krull dimension of a ring is the supremum of height of maximal ideals
 
-
 -- Stacks Lemma 10.60.5: R is Artinian iff R is Noetherian of dimension 0
-lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : 
+lemma dim_le_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : 
-    IsNoetherianRing R ∧ Ideal.krullDim R = 0 ↔ IsArtinianRing R := by 
+    IsNoetherianRing R ∧ Ideal.krullDim R ≤ 0 ↔ IsArtinianRing R := by 
     constructor
+    rintro ⟨RisNoetherian, dimzero⟩  
+    rw [ring_Noetherian_iff_spec_Noetherian] at RisNoetherian
+    let Z := irreducibleComponents (PrimeSpectrum R)
+    have Zfinite : Set.Finite Z := by
+      -- apply TopologicalSpace.NoetherianSpace.finite_irreducibleComponents ?_
+      sorry
+    
     sorry
     intro RisArtinian
     constructor
     apply finite_length_is_Noetherian
     rwa [IsArtinian_iff_finite_length] at RisArtinian
-    sorry
+    rw [Ideal.dim_le_zero_iff]
-
+    intro I
-
+    apply primes_of_Artinian_are_maximal
-
-
-    
 
+-- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible :
 
 
 

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
@@ -18,6 +19,11 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic
   developed.
 -/
 
+lemma lt_bot_eq_WithBot_bot [PartialOrder α] [OrderBot α] {a : WithBot α} (h : a < (⊥ : α)) : a = ⊥ := by
+  cases a
+  . rfl
+  . cases h.not_le (WithBot.coe_le_coe.2 bot_le)
+
 namespace Ideal
 open LocalRing
 
@@ -27,6 +33,8 @@ noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J <
 
 noncomputable def krullDim (R : Type _) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I
 
+noncomputable def codimension (J : Ideal R) : WithBot ℕ∞ := ⨅ I ∈ {I : PrimeSpectrum R | J ≤ I.asIdeal}, 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
@@ -45,16 +53,52 @@ lemma krullDim_le_iff (R : Type _) [CommRing R] (n : ℕ) :
 lemma krullDim_le_iff' (R : Type _) [CommRing R] (n : ℕ∞) :
   krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞)
 
-lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) :
-  n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry
-
-lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) :
-  n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry
-
 @[simp]
 lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R := 
   le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I
 
+lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) :
+  n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by
+  constructor
+  · unfold krullDim
+    intro H
+    by_contra H1
+    push_neg at H1
+    by_cases n ≤ 0
+    · rw [Nat.le_zero] at h
+      rw [h] at H H1
+      have : ∀ (I : PrimeSpectrum R), ↑(height I) = (⊥ : WithBot ℕ∞) := by
+        intro I
+        specialize H1 I
+        exact lt_bot_eq_WithBot_bot H1
+      rw [←iSup_eq_bot] at this
+      have := le_of_le_of_eq H this
+      rw [le_bot_iff] at this
+      exact WithBot.coe_ne_bot this
+    · push_neg at h
+      have : (n: ℕ∞) > 0 := Nat.cast_pos.mpr h
+      replace H1 : ∀ (I : PrimeSpectrum R), height I ≤ n - 1 := by
+        intro I
+        specialize H1 I
+        apply ENat.le_of_lt_add_one
+        rw [←ENat.coe_one, ←ENat.coe_sub, ←ENat.coe_add, tsub_add_cancel_of_le]
+        exact WithBot.coe_lt_coe.mp H1
+        exact h
+      replace H1 : ∀ (I : PrimeSpectrum R), (height I : WithBot ℕ∞) ≤ ↑(n - 1):=
+          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
+      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⟩
+    have : height I ≤ krullDim R := by apply height_le_krullDim
+    exact le_trans h this
+
+lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) :
+  n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry
+
+/-- The Krull dimension of a local ring is the height of its maximal ideal. -/
 lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := by
   apply le_antisymm
   . rw [krullDim_le_iff']
@@ -65,12 +109,46 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) :=
     exact I.2.1
   . simp only [height_le_krullDim]
 
+/-- The height of a prime `𝔭` is greater than `n` if and only if there is a chain of primes less than `𝔭`
+  with length `n + 1`. -/
+lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
+n < height 𝔭 ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
+  match n with
+  | ⊤ =>  
+    constructor <;> intro h <;> exfalso
+    . exact (not_le.mpr h) le_top
+    . tauto
+  | (n : ℕ) => 
+    have (m : ℕ∞) : n < m ↔ (n + 1 : ℕ∞) ≤ m := 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
+
+/-- Form of `lt_height_iff''` for rewriting with the height coerced to `WithBot ℕ∞`. -/
+lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
+(n : WithBot ℕ∞) < height 𝔭 ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
+  rw [WithBot.coe_lt_coe]
+  exact lt_height_iff'
+
 #check height_le_krullDim
 --some propositions that would be nice to be able to eventually
 
+/-- The prime spectrum of the zero ring is empty. -/
 lemma primeSpectrum_empty_of_subsingleton (x : PrimeSpectrum R) [Subsingleton R] : False :=
   x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : R)) x.1.zero_mem
 
+/-- A CommRing has empty prime spectrum if and only if it is the zero ring. -/
 lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by
   constructor
   . contrapose
@@ -94,17 +172,68 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
   . rw [h.forall_iff]
     trivial
 
+/-- Nonzero rings have Krull dimension in ℕ∞ -/
 lemma krullDim_nonneg_of_nontrivial (R : Type _) [CommRing R] [Nontrivial R] : ∃ n : ℕ∞, Ideal.krullDim R = n := by
   have h := dim_eq_bot_iff.not.mpr (not_subsingleton R)
   lift (Ideal.krullDim R) to ℕ∞ using h with k
   use k
 
+/-- An ideal which is less than a prime is not a maximal ideal. -/
+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
+
+/-- Krull dimension is ≤ 0 if and only if all primes are maximal. -/
+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 (0 : ℕ∞) < (_ : WithBot ℕ∞) 
+    rw [lt_height_iff'']
+    use [I]
+    constructor
+    . exact List.chain'_singleton _
+    . constructor
+      . intro I' hI'
+        simp at hI'
+        rwa [hI']
+      . simp
+  . contrapose! h
+    change (0 : ℕ∞) < (_ : WithBot ℕ∞) 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
+
+/-- For a nonzero ring, Krull dimension is 0 if and only if all primes are maximal. -/
 lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
-  constructor <;> intro h
+  rw [←dim_le_zero_iff]
-  . intro I
+  obtain ⟨n, hn⟩ := krullDim_nonneg_of_nontrivial R
-    sorry
+  have : n ≥ 0 := zero_le n
-  . sorry
+  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
+
+/-- In a field, the unique prime ideal is the zero ideal. -/
 @[simp]
 lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by
       constructor
@@ -116,6 +245,7 @@ lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P =
         rw [botP]
         exact bot_prime
 
+/-- In a field, all primes have height 0. -/
 lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : height P = 0 := by
     unfold height
     simp
@@ -131,10 +261,12 @@ lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : heig
     have : J ≠ P := ne_of_lt JlP
     contradiction
 
+/-- The Krull dimension of a field is 0. -/
 lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by
   unfold krullDim
   simp [field_prime_height_zero]
 
+/-- A domain with Krull dimension 0 is a field. -/
 lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by
   by_contra x
   rw [Ring.not_isField_iff_exists_prime] at x
@@ -149,55 +281,29 @@ 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
     aesop
   contradiction
 
+/-- A domain has Krull dimension 0 if and only if it is a field. -/
 lemma domain_dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
   constructor
   · exact domain_dim_zero.isField
   · intro fieldD
-    let h : Field D := IsField.toField fieldD
+    let h : Field D := fieldD.toField
     exact dim_field_eq_zero
 
 #check Ring.DimensionLEOne
 -- 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
+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
@@ -212,10 +318,9 @@ lemma dim_le_one_of_dimLEOne :  Ring.DimensionLEOne R → krullDim R ≤ (1 :
   change q0.asIdeal < q1.asIdeal at hc1
   have q1nbot := Trans.trans (bot_le : ⊥ ≤ q0.asIdeal) hc1
   specialize H q1.asIdeal (bot_lt_iff_ne_bot.mp q1nbot) q1.IsPrime
-  apply IsPrime.ne_top p.IsPrime
+  exact (not_maximal_of_lt_prime p.IsPrime hc2) H
-  apply (IsCoatom.lt_iff H.out).mp
-  exact hc2
 
+/-- The Krull dimension of a PID is at most 1. -/
 lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1 := by
   rw [dim_le_one_iff]
   exact Ring.DimensionLEOne.principal_ideal_ring R
@@ -223,8 +328,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] :
+-- lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
-  krullDim R + 1 = krullDim (Polynomial R) := sorry
+--   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/sameer(artinian-rings).lean

@@ -6,10 +6,20 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import Mathlib.RingTheory.DedekindDomain.DVR
 
 
-lemma FieldisArtinian (R : Type _) [CommRing R] (h: IsField R) : 
+lemma FieldisArtinian (R : Type _) [CommRing R] (h : IsField R) : 
-  IsArtinianRing R := by sorry
+    IsArtinianRing R := by
-
+  let inst := h.toField
-
+  rw [isArtinianRing_iff, isArtinian_iff_wellFounded]
+  apply WellFounded.intro
+  intro I
+  constructor
+  intro J hJI
+  constructor
+  intro K hKJ
+  exfalso
+  rcases Ideal.eq_bot_or_top J with rfl | rfl
+  . exact not_lt_bot hKJ
+  . exact not_top_lt hJI
 
 lemma ArtinianDomainIsField (R : Type _) [CommRing R] [IsDomain R]
 (IsArt : IsArtinianRing R) : IsField (R) := by 

CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean

@@ -3,34 +3,59 @@ 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
+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
+-- noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I}
-lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl
+-- 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] :
+-- lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
-  krullDim R + 1 ≤ krullDim (Polynomial R) := sorry -- Others are working on it
+--   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 dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
+-- 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) (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 [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
+  · by_cases krullDim R = ⊤
-    have htPBdd : ∀ (P : PrimeSpectrum (Polynomial R)), (height P : WithBot ℕ∞) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by
+    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
@@ -43,7 +68,7 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
         have : height P ≤ height P' := height_le_of_le PleP'
         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
@@ -52,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

CommAlg/sayantan(poly_over_field).lean

@@ -0,0 +1,46 @@
+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