From e735a5254f16e44464b501e5b9979c1325b8c322 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Fri, 16 Jun 2023 10:42:02 -0700 Subject: [PATCH 1/5] Completed polynomial_over_field_dim_one --- CommAlg/sayantan(poly_over_field).lean | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) diff --git a/CommAlg/sayantan(poly_over_field).lean b/CommAlg/sayantan(poly_over_field).lean index 367e30f..fc5f967 100644 --- a/CommAlg/sayantan(poly_over_field).lean +++ b/CommAlg/sayantan(poly_over_field).lean @@ -7,6 +7,20 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic namespace Ideal +private lemma singleton_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_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 From efbeadc4cefb2ddf6a1d18e40ffa37087457b00d Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Fri, 16 Jun 2023 11:11:13 -0700 Subject: [PATCH 2/5] Completed polynomial_over_field_dim_one --- CommAlg/sayantan(poly_over_field).lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CommAlg/sayantan(poly_over_field).lean b/CommAlg/sayantan(poly_over_field).lean index fc5f967..48aa955 100644 --- a/CommAlg/sayantan(poly_over_field).lean +++ b/CommAlg/sayantan(poly_over_field).lean @@ -7,7 +7,7 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic namespace Ideal -private lemma singleton_chainHeight_one {α : Type} [Preorder α] [Bot α] : Set.chainHeight {(⊥ : α)} ≤ 1 := by +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 @@ -67,7 +67,7 @@ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullD unfold height rw [sngletn] simp only [WithBot.coe_le_one, ge_iff_le] - exact singleton_chainHeight_one + 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 From 56fc9aefb2a17ffb5c2eef01de5a166bdd95444d Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Fri, 16 Jun 2023 11:12:41 -0700 Subject: [PATCH 3/5] Added polynomial_over_field_dim_one to the main file --- CommAlg/krull.lean | 63 ++++++++++++++++++++++++++++++---------------- 1 file changed, 41 insertions(+), 22 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index e24aa0f..7d4a31c 100644 --- a/CommAlg/krull.lean +++ b/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 : ℕ) : @@ -300,27 +304,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 - -- This should be doable by - -- have : IsPrime P.asIdeal := P.IsPrime - -- rw [field_prime_bot] at this - -- have : P = ⊥ := PrimeSpectrum.ext P ⊥ this - -- 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 +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 @@ -386,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 From 642127709227a19370a7bd05b953518e92757c57 Mon Sep 17 00:00:00 2001 From: Andre Date: Fri, 16 Jun 2023 14:22:13 -0400 Subject: [PATCH 4/5] proved foo, added polynomial_shifting --- CommAlg/final_poly_type.lean | 51 +++++++++++++++++++++++++++++++++--- 1 file changed, 47 insertions(+), 4 deletions(-) diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean index 1cc5c48..1a7eb77 100644 --- a/CommAlg/final_poly_type.lean +++ b/CommAlg/final_poly_type.lean @@ -86,12 +86,29 @@ 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⟩ - sorry + 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 : ℤ), @@ -143,7 +160,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,7 +187,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) + -- let g := fun (x : ℤ) => (f (x + 1) - f (x)) + 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 tauto -- [BH, 4.1.2] (a) => (b) From 5f0bf3b0663600901fb8ed44a09289106bdac92e Mon Sep 17 00:00:00 2001 From: Andre Date: Fri, 16 Jun 2023 14:36:28 -0400 Subject: [PATCH 5/5] Filled in proofs for Delta_1_ --- CommAlg/final_poly_type.lean | 49 ++++++++++++++++++++++++++---------- 1 file changed, 36 insertions(+), 13 deletions(-) diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean index 1a7eb77..85b01a2 100644 --- a/CommAlg/final_poly_type.lean +++ b/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 : ℚ) : @@ -109,7 +102,6 @@ lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s : sorry · rw [h2, s2] - -- PolyType 0 = constant function lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), (N ≤ n → f n = c)) ∧ c ≠ 0) := by @@ -142,12 +134,44 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : 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 - sorry +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 @@ -189,7 +213,6 @@ lemma foo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ have this : PolyType f (d + 1) := by rcases h with ⟨H,c0⟩ let g := (Δ f 1) - -- let g := fun (x : ℤ) => (f (x + 1) - f (x)) have this1 : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ g d) (n) = c) ∧ c ≠ 0) := by use c; use N constructor @@ -204,7 +227,7 @@ lemma foo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ apply hd tauto exact Δ_1_ f d this2 - tauto + 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