Merge branch 'main' into main

FLT/Mathlib/NumberTheory/NumberField/Basic.lean

@@ -0,0 +1,9 @@
+import Mathlib.NumberTheory.NumberField.Basic
+
+open scoped NumberField
+
+-- Mathlib PR #20544
+theorem Rat.ringOfIntegersEquiv_eq_algebraMap (z : 𝓞 ℚ) :
+    (Rat.ringOfIntegersEquiv z : ℚ) = algebraMap (𝓞 ℚ) ℚ z := by
+  obtain ⟨z, rfl⟩ := Rat.ringOfIntegersEquiv.symm.surjective z
+  simp

FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

@@ -0,0 +1,37 @@
+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]
+    [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

FLT/NumberField/AdeleRing.lean

@@ -1,4 +1,6 @@
 import Mathlib
+import FLT.Mathlib.NumberTheory.NumberField.Basic
+import FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation
 import FLT.Mathlib.RingTheory.TensorProduct.Pi
 import FLT.Mathlib.Topology.Algebra.Group.Quotient
 import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
@@ -189,17 +191,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 ⊢

FLT/NumberField/InfiniteAdeleRing.lean

@@ -6,13 +6,15 @@ open NumberField
 
 variable [Algebra K (InfiniteAdeleRing L)] [IsScalarTower K L (InfiniteAdeleRing L)]
 
+-- TODO should be →A[K]
 /-- The canonical map from the infinite adeles of K to the infinite adeles of L -/
 def NumberField.InfiniteAdeleRing.baseChange :
     InfiniteAdeleRing K →ₐ[K] InfiniteAdeleRing L :=
   sorry
 
 open scoped TensorProduct
 
+-- TODO should be ≃A[L]
 /-- The canonical `L`-algebra isomorphism from `L ⊗_K K_∞` to `L_∞` induced by the
 `K`-algebra base change map `K_∞ → L_∞`. -/
 def NumberField.InfiniteAdeleRing.baseChangeIso :

FLT/NumberField/IsTotallyReal.lean

@@ -1,5 +1,11 @@
 import Mathlib.NumberTheory.NumberField.Basic
 import Mathlib.Data.Complex.Basic
 
-class NumberField.IsTotallyReal (F : Type*) [Field F] [NumberField F] : Prop where
+namespace NumberField
+
+-- #20542
+class IsTotallyReal (F : Type*) [Field F] [NumberField F] : Prop where
   isTotallyReal : ∀ τ : F →+* ℂ, ∀ f : F, ∃ r : ℝ, τ f = r
+
+instance : IsTotallyReal ℚ where
+  isTotallyReal τ q := ⟨q, by simp⟩

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e498801db5f148f633237b7cf9f4284f0fd197f8",
+   "rev": "0291556f04e89d46cd2999f0f4c1164c81778207",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/PatrickMassot/checkdecls.git",
@@ -25,10 +25,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e4220ebf1cdae020e7e79ba5a35d26e163bac828",
+   "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
+   "inputRev": "v4.15.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/mhuisi/lean4-cli",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d55279d2ff01759fa75752fcf1a93d1db8db18ff",
+   "rev": "470c41643209208d325a5a7315116f293c7443fb",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b",
+   "rev": "46376bc3c8f46ac1a1fd7712856b0f7bd6166098",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fe8e6e649ac8251f43c6f6f934f095ebebce7e7c",
+   "rev": "f8ed91f3a9d806648ae6a03ab98c8b87e8bedc7e",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,10 +75,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35",
+   "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377",
+   "rev": "9a0b533c2fbd6195df067630be18e11e4349051c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
@@ -115,30 +115,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a4a08d92be3de00def5298059bf707c72dfd3c66",
+   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac",
+   "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "v4.15.0",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f007bfe46ea8fb801ec907df9ab540054abcc5fd",
+   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "FLT",

lakefile.lean

@@ -8,14 +8,14 @@ package FLT where
     ⟨`relaxedAutoImplicit, false⟩ -- switch off relaxed auto-implicit
   ]
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4.git"
+require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0"
 
 require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"
 
 -- This is run only if we're in `dev` mode. This is so not everyone has to build doc-gen
 meta if get_config? env = some "dev" then
 require «doc-gen4» from git
-  "https://github.com/leanprover/doc-gen4" @ "main"
+  "https://github.com/leanprover/doc-gen4" @ "v4.15.0"
 
 @[default_target]
 lean_lib FLT where

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.15.0-rc1
+leanprover/lean4:v4.15.0