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

CommAlg/final_poly_type.lean

@@ -66,13 +66,6 @@ end section
 def Δ : (ℤ → ℤ) → ℕ → (ℤ → ℤ)
   | f, 0 => f
   | f, d + 1 => fun (n : ℤ) ↦ (Δ f d) (n + 1) - (Δ f d) (n)  
-section
-
-#check Δ
-def f (n : ℤ) := n
-#eval (Δ f 1) 100
--- #check (by (show_term unfold Δ) : Δ f 0=0)
-end section
 
 -- (NO need to prove another direction) Constant polynomial function = constant function
 lemma Poly_constant (F : Polynomial ℚ) (c : ℚ) : 
@@ -86,12 +79,28 @@ lemma Poly_constant (F : Polynomial ℚ) (c : ℚ) :
     simp
   · sorry
 
+-- Get the polynomial G (X) = F (X + s) from the polynomial F(X)
+lemma Polynomial_shifting (F : Polynomial ℚ) (s : ℚ) : ∃ (G : Polynomial ℚ), (∀ (x : ℚ), Polynomial.eval x G = Polynomial.eval (x + s) F) ∧ (Polynomial.degree G = Polynomial.degree F) := by  
+  sorry
+
 -- Shifting doesn't change the polynomial type
 lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s : ℤ) (hfg : ∀ (n : ℤ), f (n + s) = g (n)) : PolyType g d := by
   simp only [PolyType]
   rcases hf with ⟨F, hh⟩
-  rcases hh with ⟨N,ss⟩
+  rcases hh with ⟨N,s1, s2⟩
+  have this : ∃ (G : Polynomial ℚ), (∀ (x : ℚ), Polynomial.eval x G = Polynomial.eval (x + s) F) ∧ (Polynomial.degree G = Polynomial.degree F) := by
+    exact Polynomial_shifting F s
+  rcases this with ⟨Poly, h1, h2⟩
+  use Poly
+  use N
+  constructor
+  · intro n
+    specialize s1 (n + s)
+    intro hN
+    have this1 : f (n + s) = Polynomial.eval (n + s : ℚ) F := by
       sorry
+    sorry
+  · rw [h2, s2]
 
 -- PolyType 0 = constant function
 lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), 
@@ -126,11 +135,43 @@ lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by rfl
   --simp only [Δ]
 -- Δ of 1 times decreaes the polynomial type by one
 lemma Δ_1 (f : ℤ → ℤ) (d : ℕ) : PolyType f (d + 1) → PolyType (Δ f 1) d := by
+  intro h
+  simp only [PolyType, Δ, Int.cast_sub, exists_and_right]
+  rcases h with ⟨F, N, h⟩
+  rcases h with ⟨h1, h2⟩
+  have this : ∃ (G : Polynomial ℚ), (∀ (x : ℚ), Polynomial.eval x G = Polynomial.eval (x + 1) F) ∧ (Polynomial.degree G = Polynomial.degree F) := by
+    exact Polynomial_shifting F 1
+  rcases this with ⟨G, hG, hGG⟩
+  let Poly := G - F
+  use Poly
+  constructor
+  · use N
+    intro n hn
+    specialize hG n
+    norm_num
+    rw [hG]
+    let h3 := h1
+    specialize h3 n
+    have this1 : f n = Polynomial.eval (n : ℚ) F := by tauto
+    have this2 : f (n + 1) = Polynomial.eval ((n + 1) : ℚ) F := by
+      specialize h1 (n + 1)
+      have this3 : N ≤ n + 1 := by linarith
+      aesop
+    rw [←this1, ←this2]
+  · have this1 : Polynomial.degree Poly = d := by
+      have this2 : Polynomial.degree Poly ≤ d := by
         sorry
+      have this3 : Polynomial.degree Poly ≥ d := by
+        sorry
+      sorry
+    tauto
 
 -- Δ of d times maps polynomial of degree d to polynomial of degree 0
 lemma Δ_1_s_equiv_Δ_s_1 (f : ℤ → ℤ) (s : ℕ) : Δ (Δ f 1) s = (Δ f (s + 1)) := by
-  sorry
+  induction' s with s hs
+  · norm_num
+  · aesop
+
 lemma foofoo (d : ℕ) : (f : ℤ → ℤ) → (PolyType f d) → (PolyType (Δ f d) 0):= by
   induction' d with d hd
   · intro f h
@@ -143,7 +184,17 @@ lemma foofoo (d : ℕ) : (f : ℤ → ℤ) → (PolyType f d) → (PolyType (Δ
 lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d → PolyType (Δ f d) 0 := 
   fun h => (foofoo d f) h
 
-lemma foofoofoo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d)  := by
+-- 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
+  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
   induction' d with d hd
 
   -- Base case
@@ -160,8 +211,23 @@ lemma foofoofoo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ),
     intro h
     rcases h with ⟨c, N, h⟩
     have this : PolyType f (d + 1) := by
-      sorry
+      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
 
 -- [BH, 4.1.2] (a) => (b)
 -- Δ^d f (n) = c for some nonzero integer c for n >> 0 → f is of polynomial type d

CommAlg/krull.lean

@@ -61,7 +61,7 @@ lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R :=
 
 /-- 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
+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
@@ -85,6 +85,10 @@ lemma height_bot_iff_bot {D: Type} [CommRing D] [IsDomain D] {P : PrimeSpectrum
     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 : ℕ) :
@@ -284,27 +288,11 @@ 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_bot {K: Type _} [Nontrivial K] [Field K] {P : PrimeSpectrum K} : height P = ⊥ := by
+lemma field_prime_height_bot {K: Type _} [Nontrivial K] [Field K] (P : PrimeSpectrum K) : height P = ⊥ := by
-    -- This should be doable by
+    have : IsPrime P.asIdeal := P.IsPrime
-    -- have : IsPrime P.asIdeal := P.IsPrime
+    rw [field_prime_bot] at this
-    -- rw [field_prime_bot] at this
+    have : P = ⊥ := PrimeSpectrum.ext P ⊥ this
-    -- have : P = ⊥ := PrimeSpectrum.ext P ⊥ this
+    rwa [height_bot_iff_bot]
-    -- rw [height_bot_iff_bot]
-    -- Need to check what's happening
-    rw [bot_eq_zero]
-    unfold height
-    simp only [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 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
 
 /-- The Krull dimension of a field is 0. -/
 lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by
@@ -370,6 +358,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/sayantan(poly_over_field).lean

@@ -7,6 +7,20 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.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
   rw [le_antisymm_iff]
@@ -27,7 +41,7 @@ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullD
         have : I = ⊥ := PrimeSpectrum.ext I ⊥ a
         contradiction
       have maxI := IsPrime.to_maximal_ideal this
-      have singleton : ∀P, P ∈ {J | J < I} ↔ P = ⊥ := by
+      have sngletn : ∀P, P ∈ {J | J < I} ↔ P = ⊥ := by
           intro P
           constructor
           · intro H
@@ -49,9 +63,11 @@ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullD
           · intro pBot
             simp only [Set.mem_setOf_eq, pBot]
             exact lt_of_le_of_ne bot_le h.symm
-      replace singleton : {J | J < I} = {⊥} := Set.ext singleton
+      replace sngletn : {J | J < I} = {⊥} := Set.ext sngletn
       unfold height
-      sorry
+      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