Merge branch 'monalisa' of github.com:GTBarkley/comm_alg into monalisa

CommAlg/final_poly_type.lean

@@ -54,8 +54,6 @@ noncomputable section
 def PolyType (f : ℤ → ℤ) (d : ℕ) := ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly) ∧ d = Polynomial.degree Poly
 section
 
-#check PolyType
-
 example (f : ℤ → ℤ) (hf : ∀ x, f x = x ^ 2) : PolyType f 2 := by
   unfold PolyType
   sorry
@@ -139,8 +137,8 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
 
 -- Δ of 0 times preserves the function
 lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by rfl
-  --simp only [Δ]
--- Δ of 1 times decreaes the polynomial type by one
+
+-- Δ of 1 times decreaes the polynomial type by one --can be golfed
 lemma Δ_1 (f : ℤ → ℤ) (d : ℕ) : PolyType f (d + 1) → PolyType (Δ f 1) d := by
   intro h
   simp only [PolyType, Δ, Int.cast_sub, exists_and_right]
@@ -193,53 +191,21 @@ lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d
 
 -- The "reverse" of Δ of 1 times increases the polynomial type by one
 lemma Δ_1_ (f : ℤ → ℤ) (d : ℕ) : PolyType (Δ f 1) d → PolyType f (d + 1) := by
-  intro h
+  rintro ⟨P, N, ⟨h1, h2⟩⟩ 
   simp only [PolyType, Nat.cast_add, Nat.cast_one, exists_and_right]
-  rcases h with ⟨P, N, h⟩
-  rcases h with ⟨h1, h2⟩
   let G := fun (q : ℤ) => f (N)
   sorry
 
-
-lemma foo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d)  := by
+lemma foo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → 
+    (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d)  := by
   induction' d with d hd
-
-  -- Base case
-  · intro f
-    intro h
-    rcases h with ⟨c, N, hh⟩
-    rw [PolyType_0]
-    use c
-    use N
-    tauto
-
-  -- Induction step
-  · intro f
-    intro h
-    rcases h with ⟨c, N, h⟩
-    have this : PolyType f (d + 1) := by
-      rcases h with ⟨H,c0⟩
-      let g := (Δ f 1)
-      have this1 : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ g d) (n) = c) ∧ c ≠ 0) := by
-        use c; use N
-        constructor
-        · intro n
-          specialize H n
-          intro h
-          have this : Δ f (d + 1) n = c := by tauto
-          rw [←this]
-          rw [Δ_1_s_equiv_Δ_s_1] 
-        · tauto 
-      have this2 : PolyType g d := by
-        apply hd
-        tauto
-      exact Δ_1_ f d this2
-    exact this
+  · rintro f ⟨c, N, hh⟩; rw [PolyType_0 f]; exact ⟨c, N, hh⟩
+  · exact fun f ⟨c, N, ⟨H, c0⟩⟩ =>
+      Δ_1_ f d (hd (Δ f 1) ⟨c, N, fun n h => by rw [← H n h, Δ_1_s_equiv_Δ_s_1], c0⟩)
 
 -- [BH, 4.1.2] (a) => (b)
 -- Δ^d f (n) = c for some nonzero integer c for n >> 0 → f is of polynomial type d
-lemma a_to_b (f : ℤ → ℤ) (d : ℕ) : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → PolyType f d := by
-  sorry
+lemma a_to_b (f : ℤ → ℤ) (d : ℕ) : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → PolyType f d := fun h => (foo d f) h
 
 -- [BH, 4.1.2] (a) <= (b)
 -- f is of polynomial type d → Δ^d f (n) = c for some nonzero integer c for n >> 0

CommAlg/grant2.lean

@@ -54,9 +54,20 @@ def symbolicIdeal(Q : Ideal R) {hin : Q.IsPrime} (I : Ideal R) : Ideal R where
     rw [←mul_assoc, mul_comm s, mul_assoc]
     exact Ideal.mul_mem_left _ _ hs2
 
+
+theorem WF_interval_le_prime (I : Ideal R) (P : Ideal R) [P.IsPrime] 
+  (h : ∀ J ∈ (Set.Icc I P), J.IsPrime → J = P ):
+  WellFounded ((· < ·) : (Set.Icc I P) → (Set.Icc I P) → Prop ) := sorry 
+
 protected lemma LocalRing.height_le_one_of_minimal_over_principle
-  [LocalRing R] (q : PrimeSpectrum R) {x : R} 
+  [LocalRing R] {x : R} 
   (h : (closedPoint R).asIdeal ∈ (Ideal.span {x}).minimalPrimes) :
-  q = closedPoint R ∨ Ideal.height q = 0 := by
-  
+  Ideal.height (closedPoint R) ≤ 1 := by
+  -- by_contra hcont
+  -- push_neg at hcont
+  -- rw [Ideal.lt_height_iff'] at hcont
+  -- rcases hcont with ⟨c, hc1, hc2, hc3⟩
+  apply height_le_of_gt_height_lt
+  intro p hp
+
   sorry

CommAlg/krull.lean

@@ -19,6 +19,7 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic
   developed.
 -/
 
+/-- If something is smaller that Bot of a PartialOrder after attaching another Bot, it must be Bot. -/
 lemma lt_bot_eq_WithBot_bot [PartialOrder α] [OrderBot α] {a : WithBot α} (h : a < (⊥ : α)) : a = ⊥ := by
   cases a
   . rfl
@@ -29,18 +30,19 @@ open LocalRing
 
 variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
 
+/-- Definitions -/
 noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I}
-
 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
 
+/-- A lattice structure on WithBot ℕ∞. -/
 noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice
 
+/-- Height of ideals is monotonic. -/
 lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := by
   apply Set.chainHeight_mono
   intro J' hJ'
@@ -57,6 +59,38 @@ lemma krullDim_le_iff' (R : Type _) [CommRing R] (n : ℕ∞) :
 lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R := 
   le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I
 
+/-- In a domain, the height of a prime ideal is Bot (0 in this case) iff it's the Bot ideal. -/
+@[simp]
+lemma height_bot_iff_bot {D: Type _} [CommRing D] [IsDomain D] {P : PrimeSpectrum D} : height P = ⊥ ↔ P = ⊥ := by
+  constructor
+  · intro h
+    unfold height at h
+    rw [bot_eq_zero] at h
+    simp only [Set.chainHeight_eq_zero_iff] at h
+    apply eq_bot_of_minimal
+    intro I
+    by_contra x
+    have : I ∈ {J | J < P} := x
+    rw [h] at this
+    contradiction
+  · intro h
+    unfold height
+    simp only [bot_eq_zero', Set.chainHeight_eq_zero_iff]
+    by_contra spec
+    change _ ≠ _ at spec
+    rw [← Set.nonempty_iff_ne_empty] at spec
+    obtain ⟨J, JlP : J < P⟩ := spec
+    have JneP : J ≠ P := ne_of_lt JlP
+    rw [h, ←bot_lt_iff_ne_bot, ←h] at JneP
+    have := not_lt_of_lt JneP
+    contradiction
+
+@[simp]
+lemma height_bot_eq {D: Type _} [CommRing D] [IsDomain D] : height (⊥ : PrimeSpectrum D) = ⊥ := by
+  rw [height_bot_iff_bot]
+
+/-- The Krull dimension of a ring being ≥ n is equivalent to there being an
+    ideal of height ≥ n. -/
 lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) :
   n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by
   constructor
@@ -95,8 +129,32 @@ lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) :
     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
+#check ENat.recTopCoe
+
+/- terrible place for this lemma. Also this probably exists somewhere
+  Also this is a terrible proof
+-/
+lemma eq_top_iff (n : WithBot ℕ∞) : n = ⊤ ↔ ∀ m : ℕ, m ≤ n := by
+  aesop
+  induction' n using WithBot.recBotCoe with n
+  . exfalso
+    have := (a 0)
+    simp [not_lt_of_ge] at this
+  induction' n using ENat.recTopCoe with n
+  . rfl
+  . have := a (n + 1)
+    exfalso
+    change (((n + 1) : ℕ∞) : WithBot ℕ∞) ≤ _ at this
+    simp [WithBot.coe_le_coe] at this
+    change ((n + 1) : ℕ∞) ≤ (n : ℕ∞) at this
+    simp [ENat.add_one_le_iff] at this
+
+lemma krullDim_eq_top_iff (R : Type _) [CommRing R] :
+  krullDim R = ⊤ ↔ ∀ (n : ℕ), ∃ I : PrimeSpectrum R, n ≤ height I := by
+  simp [eq_top_iff, le_krullDim_iff]
+  change (∀ (m : ℕ), ∃ I, ((m : ℕ∞) : WithBot ℕ∞) ≤ height I) ↔ _
+  simp [WithBot.coe_le_coe]
+  
 
 /-- 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
@@ -206,9 +264,9 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal
     . exact List.chain'_singleton _
     . constructor
       . intro I' hI'
-        simp at hI'
+        simp only [List.mem_singleton] at hI' 
         rwa [hI']
-      . simp
+      . simp only [List.length_singleton, Nat.cast_one, zero_add]
   . contrapose! h
     change (0 : ℕ∞) < (_ : WithBot ℕ∞) at h
     rw [lt_height_iff''] at h
@@ -235,7 +293,7 @@ lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum
 
 /-- 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
+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
@@ -246,25 +304,16 @@ lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P =
         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
-    by_contra spec
-    change _ ≠ _ at spec
-    rw [← Set.nonempty_iff_ne_empty] at spec
-    obtain ⟨J, JlP : J < P⟩ := spec
-    have P0 : IsPrime P.asIdeal := P.IsPrime
-    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 : J = P := PrimeSpectrum.ext J P this
-    have : J ≠ P := ne_of_lt JlP
-    contradiction
+lemma field_prime_height_bot {K: Type _} [Nontrivial K] [Field K] (P : PrimeSpectrum K) : height P = ⊥ := by
+    have : IsPrime P.asIdeal := P.IsPrime
+    rw [field_prime_bot] at this
+    have : P = ⊥ := PrimeSpectrum.ext P ⊥ this
+    rwa [height_bot_iff_bot]
 
 /-- 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]
+  simp only [field_prime_height_bot, ciSup_unique]
 
 /-- 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
@@ -311,7 +360,7 @@ lemma dim_le_one_of_dimLEOne :  Ring.DimensionLEOne R → krullDim R ≤ 1 := by
   rcases (lt_height_iff''.mp h) with ⟨c, ⟨hc1, hc2, hc3⟩⟩
   norm_cast at hc3
   rw [List.chain'_iff_get] at hc1
-  specialize hc1 0 (by rw [hc3]; simp)
+  specialize hc1 0 (by rw [hc3]; simp only)
   set q0 : PrimeSpectrum R := List.get c { val := 0, isLt := _ }
   set q1 : PrimeSpectrum R := List.get c { val := 1, isLt := _ } 
   specialize hc2 q1 (List.get_mem _ _ _)
@@ -325,6 +374,37 @@ lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1
   rw [dim_le_one_iff]
   exact Ring.DimensionLEOne.principal_ideal_ring R
 
+/-- The ring of polynomials over a field has dimension one. -/
+lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullDim (Polynomial K) = 1 := by
+  rw [le_antisymm_iff]
+  let X := @Polynomial.X K _
+  constructor
+  · exact dim_le_one_of_pid
+  · 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 _ _
+    have : IsPrime (span {X}) := by
+      refine (span_singleton_prime ?hp).mpr 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, 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
+
 lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
   krullDim R + 1 ≤ krullDim (Polynomial R) := sorry
 

CommAlg/polynomial.lean

@@ -0,0 +1,167 @@
+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 ChainLemma
+variable {α β : Type _}
+variable [LT α] [LT β] (s t : Set α)
+
+namespace Set
+open List
+
+/-
+Sorry for using aesop, but it doesn't take that long
+-/
+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
+end ChainLemma
+
+variable {R : Type _} [CommRing R]
+open Ideal Polynomial
+
+namespace Polynomial
+/-
+The composition R → R[X] → R is the identity
+-/
+theorem coeff_C_eq : RingHom.comp constantCoeff C = RingHom.id R := by ext; simp
+
+end Polynomial
+
+/-
+Given an ideal I in R, we define the ideal adjoin_x' I to be the kernel
+of R[X] → R → R/I
+-/
+def adj_x_map (I : Ideal R) : R[X] →+* R ⧸ I := (Ideal.Quotient.mk I).comp constantCoeff
+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 _
+
+@[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]
+
+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]
+
+/-
+If I is prime in R, the pushforward I*R[X] is prime in R[X]
+-/
+def map_prime (I : PrimeSpectrum R) : PrimeSpectrum R[X] :=
+  ⟨I.asIdeal.map C, isPrime_map_C_of_isPrime I.IsPrime⟩
+
+/-
+The pushforward map (Ideal R) → (Ideal R[X]) is injective
+-/
+lemma map_inj {I J : Ideal R} (h : I.map C = J.map C) : I = J := by
+  have H : map constantCoeff (I.map C) = map constantCoeff (J.map C) := by rw [h]
+  simp [Ideal.map_map, coeff_C_eq] at H
+  exact H
+
+/-
+The pushforward map (Ideal R) → (Ideal R[X]) is strictly monotone
+-/
+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 ⊢
+  exact ⟨map_mono h.1, fun H => h.2 (map_inj H)⟩
+
+lemma map_lt_adjoin_x (I : PrimeSpectrum R) : map_prime I < adjoin_x I := by
+  simp [adjoin_x, adjoin_x_eq]
+  show I.asIdeal.map C  < I.asIdeal.map C ⊔ span {X}
+  simp [Ideal.span_le, mem_map_C_iff]
+  use 1
+  simp
+  rw [←Ideal.eq_top_iff_one]
+  exact I.IsPrime.ne_top'
+
+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])
+  refine' ⟨_, by simp⟩
+  . simp [Set.append_mem_subchain_iff]
+    refine' ⟨_, map_lt_adjoin_x I, fun a ha => _⟩
+    . refine' ⟨_, fun i hi => _⟩
+      . apply List.chain'_map_of_chain' map_prime (fun a b hab => map_strictmono hab) hl.1
+      . rw [List.mem_map] at hi
+        obtain ⟨a, ha, rfl⟩ := hi
+        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
+    . 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
+
+#check (⊤ : ℕ∞)
+/-
+dim R + 1 ≤ dim R[X]
+-/
+lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
+  krullDim R + (1 : ℕ∞) ≤ krullDim R[X] := by
+  obtain ⟨n, hn⟩ := krullDim_nonneg_of_nontrivial R
+  rw [hn]
+  change ↑(n + 1) ≤ krullDim R[X]
+  have := le_of_eq hn.symm
+  induction' n using ENat.recTopCoe with n
+  . change krullDim R = ⊤ at hn
+    change ⊤ ≤ krullDim R[X] 
+    rw [krullDim_eq_top_iff] at hn
+    rw [top_le_iff, krullDim_eq_top_iff]
+    intro n
+    obtain ⟨I, hI⟩ := hn n
+    use adjoin_x I
+    calc n ≤ height I := hI
+      _ ≤ height I + 1 := le_self_add
+      _ ≤ height (adjoin_x I) := ht_adjoin_x_eq_ht_add_one I
+  change n ≤ krullDim R at this
+  change (n + 1 : ℕ) ≤ krullDim R[X]
+  rw [le_krullDim_iff] at this ⊢
+  obtain ⟨I, hI⟩ := this
+  use adjoin_x I
+  apply WithBot.coe_mono
+  calc n + 1 ≤ height I + 1 := by
+        apply add_le_add_right
+        change ((n : ℕ∞) : WithBot ℕ∞) ≤ (height I) at hI
+        rw [WithBot.coe_le_coe] at hI
+        exact hI
+    _ ≤ height (adjoin_x I) := ht_adjoin_x_eq_ht_add_one I

CommAlg/sayantan(poly_over_field).lean

@@ -1,39 +1,87 @@
 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
 
+private lemma singleton_bot_chainHeight_one {α : Type} [Preorder α] [Bot α] : Set.chainHeight {(⊥ : α)} ≤ 1 := by
+  unfold Set.chainHeight
+  simp only [iSup_le_iff, Nat.cast_le_one]
+  intro L h
+  unfold Set.subchain at h
+  simp only [Set.mem_singleton_iff, Set.mem_setOf_eq] at h
+  rcases L with (_ | ⟨a,L⟩)
+  . simp only [List.length_nil, zero_le]
+  rcases L with (_ | ⟨b,L⟩)
+  . simp only [List.length_singleton, le_refl]
+  simp only [List.chain'_cons, List.find?, List.mem_cons, forall_eq_or_imp] at h
+  rcases h with ⟨⟨h1, _⟩,  ⟨rfl, rfl, _⟩⟩
+  exact absurd h1 (lt_irrefl _)
+
+/-- The ring of polynomials over a field has dimension one. -/
 lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullDim (Polynomial K) = 1 := by
-  -- unfold krullDim
   rw [le_antisymm_iff]
+  let X := @Polynomial.X K _
   constructor
-  · 
-    sorry
+  · unfold krullDim
+    apply @iSup_le (WithBot ℕ∞) _ _ _ _
+    intro I
+    have PIR : IsPrincipalIdealRing (Polynomial K) := by infer_instance
+    by_cases I = ⊥
+    · rw [← height_bot_iff_bot] at h
+      simp only [WithBot.coe_le_one, ge_iff_le]
+      rw [h]
+      exact bot_le
+    · push_neg at h
+      have : I.asIdeal ≠ ⊥ := by
+        by_contra a
+        have : I = ⊥ := PrimeSpectrum.ext I ⊥ a
+        contradiction
+      have maxI := IsPrime.to_maximal_ideal this
+      have sngletn : ∀P, P ∈ {J | J < I} ↔ P = ⊥ := by
+          intro P
+          constructor
+          · intro H
+            simp only [Set.mem_setOf_eq] at H
+            by_contra x
+            push_neg at x
+            have : P.asIdeal ≠ ⊥ := by
+              by_contra a
+              have : P = ⊥ := PrimeSpectrum.ext P ⊥ a
+              contradiction 
+            have maxP := IsPrime.to_maximal_ideal this
+            have IneTop := IsMaximal.ne_top maxI
+            have : P ≤ I := le_of_lt H
+            rw [←PrimeSpectrum.asIdeal_le_asIdeal] at this
+            have : P.asIdeal = I.asIdeal := Ideal.IsMaximal.eq_of_le maxP IneTop this
+            have : P = I := PrimeSpectrum.ext P I this
+            replace H : P ≠ I := ne_of_lt H
+            contradiction
+          · intro pBot
+            simp only [Set.mem_setOf_eq, pBot]
+            exact lt_of_le_of_ne bot_le h.symm
+      replace sngletn : {J | J < I} = {⊥} := Set.ext sngletn
+      unfold height
+      rw [sngletn]
+      simp only [WithBot.coe_le_one, ge_iff_le]
+      exact singleton_bot_chainHeight_one
   · 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
+      refine (span_singleton_prime ?hp).mpr 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]
+      simp only [Set.mem_setOf_eq, bot_lt_iff_ne_bot]
       suffices : P.asIdeal ≠ ⊥
       · by_contra x
         rw [PrimeSpectrum.ext_iff] at x