From 670828723572c1d4925037f8c40fb286d3c750d6 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Mon, 6 Jan 2025 18:14:02 +0000 Subject: [PATCH 1/3] mem_integers_of_valuation_le_one --- .../DedekindDomain/AdicValuation.lean | 36 +++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean diff --git a/FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean b/FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean new file mode 100644 index 00000000..3537de7e --- /dev/null +++ b/FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean @@ -0,0 +1,36 @@ +import Mathlib.RingTheory.DedekindDomain.AdicValuation + +open IsDedekindDomain + +namespace IsDedekindDomain.HeightOneSpectrum + +variable (R K : Type*) [CommRing R] [Field K] [IsDedekindDomain R] [Algebra R K] + [IsFractionRing R K] in +theorem mem_integers_of_valuation_le_one (x : K) + (h : ∀ v : HeightOneSpectrum R, v.valuation x ≤ 1) : x ∈ (algebraMap R K).range := by + obtain ⟨⟨n, d, hd⟩, hx⟩ := IsLocalization.surj (nonZeroDivisors R) x + obtain rfl : x = IsLocalization.mk' K n ⟨d, hd⟩ := IsLocalization.eq_mk'_iff_mul_eq.mpr hx + have hd0 := nonZeroDivisors.ne_zero hd + obtain rfl | hn0 := eq_or_ne n 0 + · simp + suffices Ideal.span {d} ∣ (Ideal.span {n} : Ideal R) by + obtain ⟨z, rfl⟩ := Ideal.span_singleton_le_span_singleton.1 (Ideal.le_of_dvd this) + use z + rw [map_mul, mul_comm,mul_eq_mul_left_iff] at hx + cases' hx with h h + · exact h.symm + · simp [hd0] at h + classical + have ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥ := fun {r} ↦ mt Ideal.span_singleton_eq_bot.mp + rw [← Associates.mk_le_mk_iff_dvd, ← Associates.factors_le, Associates.factors_mk _ (ine hn0), + Associates.factors_mk _ (ine hd0), WithTop.coe_le_coe, Multiset.le_iff_count] + rintro ⟨v, hv⟩ + obtain ⟨v, rfl⟩ := Associates.mk_surjective v + have hv' := hv + rw [Associates.irreducible_mk, irreducible_iff_prime] at hv + specialize h ⟨v, Ideal.isPrime_of_prime hv, hv.ne_zero⟩ + simp_rw [valuation_of_mk', intValuation, ← Valuation.toFun_eq_coe, + intValuationDef_if_neg _ hn0, intValuationDef_if_neg _ hd0, ← WithZero.coe_div, + ← WithZero.coe_one, WithZero.coe_le_coe, Associates.factors_mk _ (ine hn0), + Associates.factors_mk _ (ine hd0), Associates.count_some hv'] at h + simpa using h From 07144405e92c805daa035d9c2b25a5665a943036 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Mon, 6 Jan 2025 18:15:33 +0000 Subject: [PATCH 2/3] Rat.ringOfIntegersEquiv_eq_algebraMap --- FLT/Mathlib/NumberTheory/NumberField/Basic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/FLT/Mathlib/NumberTheory/NumberField/Basic.lean b/FLT/Mathlib/NumberTheory/NumberField/Basic.lean index 118b8ff8..caf51d16 100644 --- a/FLT/Mathlib/NumberTheory/NumberField/Basic.lean +++ b/FLT/Mathlib/NumberTheory/NumberField/Basic.lean @@ -4,4 +4,5 @@ open scoped NumberField theorem Rat.ringOfIntegersEquiv_eq_algebraMap (z : 𝓞 ℚ) : (Rat.ringOfIntegersEquiv z : ℚ) = algebraMap (𝓞 ℚ) ℚ z := by - sorry -- #307 + obtain ⟨z, rfl⟩ := Rat.ringOfIntegersEquiv.symm.surjective z + simp From d1ae46f0f7c760284f5954dbb3e27a8eb3838900 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Mon, 6 Jan 2025 18:42:45 +0000 Subject: [PATCH 3/3] finish proof --- .../DedekindDomain/AdicValuation.lean | 1 + FLT/NumberField/AdeleRing.lean | 22 +++++++++---------- 2 files changed, 12 insertions(+), 11 deletions(-) diff --git a/FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean b/FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean index 3537de7e..07bca0f3 100644 --- a/FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean +++ b/FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean @@ -2,6 +2,7 @@ import Mathlib.RingTheory.DedekindDomain.AdicValuation open IsDedekindDomain +-- mathlib PR #20523 namespace IsDedekindDomain.HeightOneSpectrum variable (R K : Type*) [CommRing R] [Field K] [IsDedekindDomain R] [Algebra R K] diff --git a/FLT/NumberField/AdeleRing.lean b/FLT/NumberField/AdeleRing.lean index 92993466..6dc3b3b2 100644 --- a/FLT/NumberField/AdeleRing.lean +++ b/FLT/NumberField/AdeleRing.lean @@ -1,4 +1,6 @@ import Mathlib +import FLT.Mathlib.NumberTheory.NumberField.Basic +import FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation universe u @@ -49,17 +51,15 @@ theorem Rat.AdeleRing.zero_discrete : ∃ U : Set (AdeleRing ℚ), change ‖(x : ℂ)‖ < 1 at h1 simp at h1 have intx: ∃ (y:ℤ), y = x - · clear h1 -- not needed - -- mathematically this is trivial: - -- h2 says that no prime divides the denominator of x - -- so x is an integer - -- and the goal is that there exists an integer `y` such that `y = x`. - suffices ∀ p : ℕ, p.Prime → ¬(p ∣ x.den) by - use x.num - rw [← den_eq_one_iff] - contrapose! this - exact ⟨x.den.minFac, Nat.minFac_prime this, Nat.minFac_dvd _⟩ - sorry -- issue #254 + · obtain ⟨z, hz⟩ := IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one + (𝓞 ℚ) ℚ x <| fun v ↦ by + specialize h2 v + letI : UniformSpace ℚ := v.adicValued.toUniformSpace + rw [IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers] at h2 + rwa [← IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation'] + use Rat.ringOfIntegersEquiv z + rw [← hz] + apply Rat.ringOfIntegersEquiv_eq_algebraMap obtain ⟨y, rfl⟩ := intx simp only [abs_lt] at h1 norm_cast at h1 ⊢