From d0a6d8605e8a8b38a7e6cc9ea2312a2641015d8a Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Fri, 16 Jun 2023 09:54:07 -0700 Subject: [PATCH 1/4] golfed imports --- CommAlg/polynomial.lean | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/CommAlg/polynomial.lean b/CommAlg/polynomial.lean index 8dd886a..e7380b0 100644 --- a/CommAlg/polynomial.lean +++ b/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] -/ From 642127709227a19370a7bd05b953518e92757c57 Mon Sep 17 00:00:00 2001 From: Andre Date: Fri, 16 Jun 2023 14:22:13 -0400 Subject: [PATCH 2/4] 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 3/4] 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 From 19b490ab9e3f64dc28f7f7f294ac13c7156540e7 Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Fri, 16 Jun 2023 11:43:00 -0700 Subject: [PATCH 4/4] some golfing, one new lemma --- CommAlg/krull.lean | 78 ++++++++++++++++++---------------------------- 1 file changed, 31 insertions(+), 47 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index e24aa0f..78c9a9b 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -127,9 +127,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 @@ -147,47 +157,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 - apply height_le_of_le - apply le_maximalIdeal - exact I.2.1 + exact WithBot.coe_mono <| height_le_of_le <| le_maximalIdeal 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 + induction' n using ENat.recTopCoe with n + . simp + . rw [←(ENat.add_one_le_iff <| ENat.coe_ne_top _)] 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 - . tauto - . change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc - norm_cast at hc - tauto + norm_cast + simp_rw [and_assoc] /-- Form of `lt_height_iff''` for rewriting with the height coerced to `WithBot ℕ∞`. -/ lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : @@ -199,30 +192,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 := - x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : R)) x.1.zero_mem +lemma primeSpectrum_empty_of_subsingleton [Subsingleton R] : IsEmpty <| PrimeSpectrum R where + 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 - . contrapose - rw [not_isEmpty_iff, ←not_nontrivial_iff_subsingleton, not_not] + constructor <;> contrapose + . rw [not_isEmpty_iff, ←not_nontrivial_iff_subsingleton, not_not] apply PrimeSpectrum.instNonemptyPrimeSpectrum - . intro h - by_contra hneg - rw [not_isEmpty_iff] at hneg - rcases hneg with ⟨a, ha⟩ - exact primeSpectrum_empty_of_subsingleton ⟨a, ha⟩ + . intro hneg h + exact hneg primeSpectrum_empty_of_subsingleton /-- 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 [←primeSpectrum_empty_iff, iSup_eq_bot] + rw [Ideal.krullDim, ←primeSpectrum_empty_iff, iSup_eq_bot] constructor <;> intro h . rw [←not_nonempty_iff] rintro ⟨a, ha⟩ - specialize h ⟨a, ha⟩ - tauto + cases h ⟨a, ha⟩ . rw [h.forall_iff] trivial @@ -290,13 +277,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 - · intro primeP - obtain T := eq_bot_or_top P - have : ¬P = ⊤ := IsPrime.ne_top primeP - tauto - · intro botP - rw [botP] + refine' ⟨fun primeP => Or.elim (eq_bot_or_top P) _ _, fun botP => _⟩ + · intro P_top; exact P_top + . intro P_bot; exact False.elim (primeP.ne_top P_bot) + · rw [botP] exact bot_prime /-- In a field, all primes have height 0. -/