Merge branch 'main' of https://github.com/SinTan1729/comm_alg

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

@@ -129,9 +129,19 @@ lemma le_krullDim_iff {R : Type _} [CommRing R] {n : ℕ} :
 
 #check ENat.recTopCoe
 
-/- terrible place for this lemma. Also this probably exists somewhere
+/- terrible place for these two lemmas. Also this probably exists somewhere
   Also this is a terrible proof
 -/
+lemma eq_top_iff' (n : ℕ∞) : n = ⊤ ↔ ∀ m : ℕ, m ≤ n := by
+  refine' ⟨fun a b => _, fun h => _⟩
+  . rw [a]; exact le_top
+  . induction' n using ENat.recTopCoe with n
+    . rfl
+    . exfalso
+      apply not_lt_of_ge (h (n + 1))
+      norm_cast
+      norm_num
+
 lemma eq_top_iff (n : WithBot ℕ∞) : n = ⊤ ↔ ∀ m : ℕ, m ≤ n := by
   aesop
   induction' n using WithBot.recBotCoe with n
@@ -149,47 +159,30 @@ lemma eq_top_iff (n : WithBot ℕ∞) : n = ⊤ ↔ ∀ m : ℕ, m ≤ n := by
 
 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]
+  simp_rw [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
   apply le_antisymm
   . rw [krullDim_le_iff']
     intro I
-    apply WithBot.coe_mono
+    exact WithBot.coe_mono <| height_le_of_le <| le_maximalIdeal I.2.1
-    apply height_le_of_le
-    apply le_maximalIdeal
-    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
+  induction' n using ENat.recTopCoe with n
-  | ⊤ =>  
+  . simp
-    constructor <;> intro h <;> exfalso
+  . rw [←(ENat.add_one_le_iff <| ENat.coe_ne_top _)]
-    . 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]
+    rw [Ideal.height, Set.le_chainHeight_iff]
     show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
-    constructor <;> rintro ⟨c, hc⟩ <;> use c
+    norm_cast
-    . tauto
+    simp_rw [and_assoc]
-    . 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 : ℕ∞} : 
@@ -201,30 +194,24 @@ lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
 --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 :=
+lemma primeSpectrum_empty_of_subsingleton [Subsingleton R] : IsEmpty <| PrimeSpectrum R where
-  x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : R)) x.1.zero_mem
+  false x := 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
+  constructor <;> contrapose
-  . contrapose
+  . rw [not_isEmpty_iff, ←not_nontrivial_iff_subsingleton, not_not]
-    rw [not_isEmpty_iff, ←not_nontrivial_iff_subsingleton, not_not]
     apply PrimeSpectrum.instNonemptyPrimeSpectrum
-  . intro h
+  . intro hneg h
-    by_contra hneg
+    exact hneg primeSpectrum_empty_of_subsingleton
-    rw [not_isEmpty_iff] at hneg
-    rcases hneg with ⟨a, ha⟩
-    exact primeSpectrum_empty_of_subsingleton ⟨a, ha⟩
 
 /-- A ring has Krull dimension -∞ if and only if it is the zero ring -/
 lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
-  unfold Ideal.krullDim
+  rw [Ideal.krullDim, ←primeSpectrum_empty_iff, iSup_eq_bot]
-  rw [←primeSpectrum_empty_iff, iSup_eq_bot]
   constructor <;> intro h
   . rw [←not_nonempty_iff]
     rintro ⟨a, ha⟩
-    specialize h ⟨a, ha⟩
+    cases h ⟨a, ha⟩
-    tauto
   . rw [h.forall_iff]
     trivial
 
@@ -292,13 +279,10 @@ 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
-      constructor
+      refine' ⟨fun primeP => Or.elim (eq_bot_or_top P) _ _, fun botP => _⟩
-      · intro primeP
+      · intro P_top; exact P_top
-        obtain T := eq_bot_or_top P
+      . intro P_bot; exact False.elim (primeP.ne_top P_bot)
-        have : ¬P = ⊤ := IsPrime.ne_top primeP
+      · rw [botP]
-        tauto
-      · intro botP
-        rw [botP]
         exact bot_prime
 
 /-- In a field, all primes have height 0. -/

CommAlg/polynomial.lean

@@ -1,13 +1,3 @@
-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
@@ -132,7 +122,6 @@ lemma ht_adjoin_x_eq_ht_add_one [Nontrivial R] (I : PrimeSpectrum R) : height I
       apply hl.2
       exact hb
 
-#check (⊤ : ℕ∞)
 /-
 dim R + 1 ≤ dim R[X]
 -/