From 5b38350326598c4d105baad4579b3418ffdd6d40 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 6 Feb 2024 01:19:20 -0600 Subject: [PATCH] new: Added the more advanced examples --- LeanTalkSP24.lean | 2 + LeanTalkSP24/infinitely_many_primes.lean | 238 ++++++++++++++++++ .../polynomial_over_field_dim_one.lean | 144 +++++++++++ 3 files changed, 384 insertions(+) create mode 100644 LeanTalkSP24/infinitely_many_primes.lean create mode 100644 LeanTalkSP24/polynomial_over_field_dim_one.lean diff --git a/LeanTalkSP24.lean b/LeanTalkSP24.lean index baa4c31..870a651 100644 --- a/LeanTalkSP24.lean +++ b/LeanTalkSP24.lean @@ -1,3 +1,5 @@ -- This module serves as the root of the `«LeanTalkSP24»` library. -- Import modules here that should be built as part of the library. import «LeanTalkSP24».basics +import «LeanTalkSP24».infinitely_many_primes +import «LeanTalkSP24».polynomial_over_field_dim_one diff --git a/LeanTalkSP24/infinitely_many_primes.lean b/LeanTalkSP24/infinitely_many_primes.lean new file mode 100644 index 0000000..e6df1df --- /dev/null +++ b/LeanTalkSP24/infinitely_many_primes.lean @@ -0,0 +1,238 @@ +import Mathlib.Data.Nat.Prime +import Mathlib.Algebra.BigOperators.Order +import Mathlib.Tactic +import Mathlib.Tactic.IntervalCases + +open BigOperators + +theorem two_le {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m := by + have : m > 0 := Nat.pos_of_ne_zero h0 + have : m >= 1 := this + have h1 : 1 ≠ m := Ne.symm h1 + change ¬_ = _ at h1 + have : m > 1 := Nat.lt_of_le_of_ne this h1 + exact this + +theorem exists_prime_factor {n : Nat} (h : 2 ≤ n) : ∃ p : Nat, p.Prime ∧ p ∣ n := by + by_cases np : n.Prime + · use n, np + induction' n using Nat.strong_induction_on with n ih + rw [Nat.prime_def_lt] at np + push_neg at np + rcases np h with ⟨m, mltn, mdvdn, mne1⟩ + have : m ≠ 0 := by + intro mz + rw [mz, zero_dvd_iff] at mdvdn + linarith + have mgt2 : 2 ≤ m := two_le this mne1 + by_cases mp : m.Prime + · use m, mp + . rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩ + use p, pp + apply pdvd.trans mdvdn + +theorem primes_infinite : ∀ n, ∃ p > n, Nat.Prime p := by + intro n + have : 2 ≤ Nat.factorial (n + 1) + 1 := by + apply Nat.succ_le_succ + apply Nat.succ_le_of_lt + apply Nat.factorial_pos + rcases exists_prime_factor this with ⟨p, pp, pdvd⟩ + refine' ⟨p, _, pp⟩ + show p > n + by_contra ple + push_neg at ple + have : p ∣ Nat.factorial (n + 1) := by + apply Nat.dvd_factorial + apply pp.pos + linarith + have : p ∣ 1 := by + convert Nat.dvd_sub' pdvd this + simp + show False + have ple1 : p ≤ 1 := Nat.le_of_dvd (Nat.lt_succ_self 0) this + have plt1 : p > 1 := pp.one_lt + linarith + +open Finset + +section +variable {α : Type _} [DecidableEq α] (r s t : Finset α) + +example : r ∩ (s ∪ t) ⊆ r ∩ s ∪ r ∩ t := by + rw [subset_iff] + intro x + rw [mem_inter, mem_union, mem_union, mem_inter, mem_inter] + tauto + +example : r ∩ (s ∪ t) ⊆ r ∩ s ∪ r ∩ t := by + simp [subset_iff] + intro x + tauto + +example : r ∩ s ∪ r ∩ t ⊆ r ∩ (s ∪ t) := by + simp [subset_iff] + intro x + tauto + +example : r ∩ s ∪ r ∩ t = r ∩ (s ∪ t) := by + ext x + simp + tauto + +end + +theorem _root_.Nat.Prime.eq_of_dvd_of_prime {p q : ℕ} + (prime_p : Nat.Prime p) (prime_q : Nat.Prime q) (h : p ∣ q) : + p = q := by + cases prime_q.eq_one_or_self_of_dvd _ h + · linarith [prime_p.two_le] + assumption + +theorem mem_of_dvd_prod_primes {s : Finset ℕ} {p : ℕ} (prime_p : p.Prime) : + (∀ n ∈ s, Nat.Prime n) → (p ∣ ∏ n in s, n) → p ∈ s := by + intro h₀ h₁ + induction' s using Finset.induction_on with a s ans ih + · simp at h₁ + linarith [prime_p.two_le] + simp [Finset.prod_insert ans, prime_p.dvd_mul] at h₀ h₁ + rw [mem_insert] + cases' h₁ with h₁ h₁ + · left + exact prime_p.eq_of_dvd_of_prime h₀.1 h₁ + right + exact ih h₀.2 h₁ + +theorem primes_infinite' : ∀ s : Finset Nat, ∃ p, Nat.Prime p ∧ p ∉ s := by + intro s + by_contra h + push_neg at h + set s' := s.filter Nat.Prime with s'_def + have mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime := by + intro n + simp [s'_def] + apply h + have : 2 ≤ (∏ i in s', i) + 1 := by + apply Nat.succ_le_succ + apply Nat.succ_le_of_lt + apply Finset.prod_pos + intro n ns' + apply (mem_s'.mp ns').pos + rcases exists_prime_factor this with ⟨p, pp, pdvd⟩ + have : p ∣ ∏ i in s', i := by + apply dvd_prod_of_mem + rw [mem_s'] + apply pp + have : p ∣ 1 := by + convert Nat.dvd_sub' pdvd this + simp + show False + have := Nat.le_of_dvd zero_lt_one this + linarith [pp.two_le] + +theorem bounded_of_ex_finset (Q : ℕ → Prop) : + (∃ s : Finset ℕ, ∀ k, Q k → k ∈ s) → ∃ n, ∀ k, Q k → k < n := by + rintro ⟨s, hs⟩ + use s.sup id + 1 + intro k Qk + apply Nat.lt_succ_of_le + show id k ≤ s.sup id + apply le_sup (hs k Qk) + +theorem ex_finset_of_bounded (Q : ℕ → Prop) [DecidablePred Q] : + (∃ n, ∀ k, Q k → k ≤ n) → ∃ s : Finset ℕ, ∀ k, Q k ↔ k ∈ s := by + rintro ⟨n, hn⟩ + use (range (n + 1)).filter Q + intro k + simp [Nat.lt_succ_iff] + exact hn k + +theorem mod_4_eq_3_or_mod_4_eq_3 {m n : ℕ} (h : m * n % 4 = 3) : m % 4 = 3 ∨ n % 4 = 3 := by + revert h + rw [Nat.mul_mod] + have : m % 4 < 4 := Nat.mod_lt m (by norm_num) + interval_cases hm : m % 4 <;> simp [hm] + have : n % 4 < 4 := Nat.mod_lt n (by norm_num) + interval_cases hn : n % 4 <;> simp [hn] + +theorem two_le_of_mod_4_eq_3 {n : ℕ} (h : n % 4 = 3) : 2 ≤ n := by + apply two_le <;> + · intro neq + rw [neq] at h + norm_num at h + +theorem aux {m n : ℕ} (h₀ : m ∣ n) (h₁ : 2 ≤ m) (h₂ : m < n) : n / m ∣ n ∧ n / m < n := by + constructor + · exact Nat.div_dvd_of_dvd h₀ + exact Nat.div_lt_self (lt_of_le_of_lt (zero_le _) h₂) h₁ + +theorem exists_prime_factor_mod_4_eq_3 {n : Nat} (h : n % 4 = 3) : + ∃ p : Nat, p.Prime ∧ p ∣ n ∧ p % 4 = 3 := by + by_cases np : n.Prime + · use n + induction' n using Nat.strong_induction_on with n ih + rw [Nat.prime_def_lt] at np + push_neg at np + rcases np (two_le_of_mod_4_eq_3 h) with ⟨m, mltn, mdvdn, mne1⟩ + have mge2 : 2 ≤ m := by + apply two_le _ mne1 + intro mz + rw [mz, zero_dvd_iff] at mdvdn + linarith + have neq : m * (n / m) = n := Nat.mul_div_cancel' mdvdn + have : m % 4 = 3 ∨ n / m % 4 = 3 := by + apply mod_4_eq_3_or_mod_4_eq_3 + rw [neq, h] + cases' this with h1 h1 + · by_cases mp : m.Prime + · use m + rcases ih m mltn h1 mp with ⟨p, pp, pdvd, p4eq⟩ + use p + exact ⟨pp, pdvd.trans mdvdn, p4eq⟩ + obtain ⟨nmdvdn, nmltn⟩ := aux mdvdn mge2 mltn + by_cases nmp : (n / m).Prime + · use n / m + rcases ih (n / m) nmltn h1 nmp with ⟨p, pp, pdvd, p4eq⟩ + use p + exact ⟨pp, pdvd.trans nmdvdn, p4eq⟩ + +theorem primes_mod_4_eq_3_infinite : ∀ n, ∃ p > n, Nat.Prime p ∧ p % 4 = 3 := by + by_contra h + push_neg at h + cases' h with n hn + have : ∃ s : Finset Nat, ∀ p : ℕ, p.Prime ∧ p % 4 = 3 ↔ p ∈ s := by + apply ex_finset_of_bounded + use n + contrapose! hn + rcases hn with ⟨p, ⟨pp, p4⟩, pltn⟩ + exact ⟨p, pltn, pp, p4⟩ + cases' this with s hs + have h₁ : ((4 * ∏ i in erase s 3, i) + 3) % 4 = 3 := by + rw [add_comm, Nat.add_mul_mod_self_left] + norm_num + rcases exists_prime_factor_mod_4_eq_3 h₁ with ⟨p, pp, pdvd, p4eq⟩ + have ps : p ∈ s := by + rw [← hs p] + exact ⟨pp, p4eq⟩ + have pne3 : p ≠ 3 := by + intro peq + rw [peq, ← Nat.dvd_add_iff_left (dvd_refl 3)] at pdvd + rw [Nat.prime_three.dvd_mul] at pdvd + norm_num at pdvd + have : 3 ∈ s.erase 3 := by + apply mem_of_dvd_prod_primes Nat.prime_three _ pdvd + intro n + simp [← hs n] + tauto + simp at this + have : p ∣ 4 * ∏ i in erase s 3, i := by + apply dvd_trans _ (dvd_mul_left _ _) + apply dvd_prod_of_mem + simp + constructor <;> assumption + have : p ∣ 3 := by + convert Nat.dvd_sub' pdvd this + simp + have : p = 3 := by + apply pp.eq_of_dvd_of_prime Nat.prime_three this + contradiction diff --git a/LeanTalkSP24/polynomial_over_field_dim_one.lean b/LeanTalkSP24/polynomial_over_field_dim_one.lean new file mode 100644 index 0000000..26e5e81 --- /dev/null +++ b/LeanTalkSP24/polynomial_over_field_dim_one.lean @@ -0,0 +1,144 @@ +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.Order.Height +import Mathlib.RingTheory.PrincipalIdealDomain +import Mathlib.RingTheory.DedekindDomain.Basic +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic + +namespace Ideal + +namespace Ideal +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 + +/-- Singleton sets have chainHeight 1 -/ +lemma singleton_chainHeight_one {α : Type _} {x : α} [Preorder α] : Set.chainHeight {x} = 1 := by + have le : Set.chainHeight {x} ≤ 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 _) + suffices : Set.chainHeight {x} > 0 + · change _ < _ at this + rw [←ENat.one_le_iff_pos] at this + apply le_antisymm <;> trivial + by_contra x + simp only [gt_iff_lt, not_lt, nonpos_iff_eq_zero, Set.chainHeight_eq_zero_iff, Set.singleton_ne_empty] at x + +/-- In a domain, the height of a prime ideal is Bot (0 in this case) iff it's the Bot ideal. -/ +@[simp] +lemma height_zero_iff_bot {D: Type _} [CommRing D] [IsDomain D] {P : PrimeSpectrum D} : height P = 0 ↔ P = ⊥ := by + constructor + · intro h + unfold height 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 + +/-- The ring of polynomials over a field has dimension one. -/ +-- It's the exact same lemma as in krull.lean, added ' to avoid conflict +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 + · unfold krullDim + apply @iSup_le (WithBot ℕ∞) _ _ _ _ + intro I + have PIR : IsPrincipalIdealRing (Polynomial K) := by infer_instance + by_cases h: I = ⊥ + · rw [← height_zero_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 le_of_eq 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 + 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