From a5d9c8216452ef8dfb411b733dd58b300e173b3b Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Sun, 1 Dec 2024 16:25:40 +0000
Subject: [PATCH] Add Samuel Yin's work on discreteness of Q in A_Q

---
 FLT/NumberField/AdeleRing.lean | 123 ++++++++++++++++-----------------
 1 file changed, 59 insertions(+), 64 deletions(-)

diff --git a/FLT/NumberField/AdeleRing.lean b/FLT/NumberField/AdeleRing.lean
index b5795941..4cf2fdf0 100644
--- a/FLT/NumberField/AdeleRing.lean
+++ b/FLT/NumberField/AdeleRing.lean
@@ -1,4 +1,4 @@
-import FLT.NumberField.InfiniteAdeleRing
+import Mathlib
 
 universe u
 
@@ -18,86 +18,81 @@ section BaseChange
 
 end BaseChange
 
--- Maybe this discreteness isn't even stated in the best way?
--- I'm ambivalent about how it's stated
 
 section Discrete
 
 open NumberField DedekindDomain
 
--- Should surely be in mathlib
-abbrev Rat.infinitePlace : InfinitePlace ℚ where
-  val := {
-    toFun := fun q ↦ |(q : ℝ)|
-    map_mul' := fun x y ↦ by
-      simp only [cast_mul]
-      exact abs_mul (x : ℝ) y
-    nonneg' := by
-      intro x
-      simp only [abs_nonneg]
-    eq_zero' := by
-      intro x
-      simp
-    add_le' := by
-      intro x y
-      simp only [cast_add]
-      exact abs_add_le (x : ℝ) y
-  }
-  property := ⟨Rat.castHom ℂ, by
-    ext x
-    simp
-    ⟩
+-- mathlib PR #19644
+lemma Rat.norm_infinitePlace_completion (v : InfinitePlace ℚ) (x : ℚ) :
+    ‖(x : v.completion)‖ = |x| := sorry
+
+-- mathlib PR #19644
+noncomputable def Rat.infinitePlace : InfinitePlace ℚ := .mk (Rat.castHom _)
 
 theorem Rat.AdeleRing.zero_discrete : ∃ U : Set (AdeleRing ℚ),
     IsOpen U ∧ (algebraMap ℚ (AdeleRing ℚ)) ⁻¹' U = {0} := by
   use {f | ∀ v, f v ∈ (Metric.ball 0 1)} ×ˢ
     {f | ∀ v , f v ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v}
-  refine ⟨sorry, ?_⟩
-  apply subset_antisymm
-  · intro x hx
-    rw [Set.mem_preimage] at hx
-    simp only [Set.mem_singleton_iff]
-    have : (algebraMap ℚ (AdeleRing ℚ)) x = (algebraMap ℚ (InfiniteAdeleRing ℚ) x, algebraMap ℚ (FiniteAdeleRing (𝓞 ℚ) ℚ) x)
-    · rfl
-    rw [this] at hx
-    clear this
-    rw [Set.mem_prod] at hx
-    obtain ⟨h1, h2⟩ := hx
-    dsimp only at h1 h2
-    simp only [Metric.mem_ball, dist_zero_right, Set.mem_setOf_eq, InfiniteAdeleRing.algebraMap_apply, UniformSpace.Completion.norm_coe] at h1
-    simp only [Set.mem_setOf_eq] at h2
-    specialize h1 Rat.infinitePlace
-    simp at h1
-    change (|(x:ℝ)|) < 1 at h1
-    norm_cast at h1
-    have := padicNorm.not_int_of_not_padic_int
-    have intx: ∃ (y:ℤ), y = x
-    · by_contra h
-      push_neg at h
+  refine ⟨?_, ?_⟩
+  · sorry -- should be easy (product of opens is open, product of integers is surely
+          -- known to be open)
+  · apply subset_antisymm
+    · intro x hx
+      rw [Set.mem_preimage] at hx
+      simp only [Set.mem_singleton_iff]
+      have : (algebraMap ℚ (AdeleRing ℚ)) x =
+        (algebraMap ℚ (InfiniteAdeleRing ℚ) x, algebraMap ℚ (FiniteAdeleRing (𝓞 ℚ) ℚ) x)
+      · rfl
+      rw [this] at hx
+      clear this
+      rw [Set.mem_prod] at hx
+      obtain ⟨h1, h2⟩ := hx
+      dsimp only at h1 h2
+      simp only [Metric.mem_ball, dist_zero_right, Set.mem_setOf_eq,
+        InfiniteAdeleRing.algebraMap_apply, UniformSpace.Completion.norm_coe] at h1
+      simp only [Set.mem_setOf_eq] at h2
+      specialize h1 Rat.infinitePlace
+      change ‖(x : ℂ)‖ < 1 at h1
+      simp at h1
+      have intx: ∃ (y:ℤ), y = x
+      · by_contra h
+        push_neg at h
+        -- mathematically this is trivial:
+        -- h2 says that no prime divides the denominator of x
+        -- so x is an integer
+        -- and then h says it's not an integer
+        sorry
+      obtain ⟨y, rfl⟩ := intx
+      simp at h1
+      -- mathematically this is trivial:
+      -- h1 says that the integer y satisfies |y| < 1
+      -- and the goal is that y = 0
       sorry
-    sorry
-  · intro x
-    simp only [Set.mem_singleton_iff, Set.mem_preimage]
-    rintro rfl
-    simp only [map_zero]
-    change (0, 0) ∈ _
-    simp only [Prod.mk_zero_zero, Set.mem_prod, Prod.fst_zero, Prod.snd_zero]
-    constructor
-    · simp only [Metric.mem_ball, dist_zero_right, Set.mem_setOf_eq]
-      intro v
-      have : ‖(0:InfiniteAdeleRing ℚ) v‖ = 0
-      · simp only [norm_eq_zero]
-        rfl
-      simp [this, zero_lt_one]
-    · simp only [Set.mem_setOf_eq]
-      intro v
-      apply zero_mem
+    · intro x
+      simp only [Set.mem_singleton_iff, Set.mem_preimage]
+      rintro rfl
+      simp only [map_zero]
+      change (0, 0) ∈ _
+      simp only [Prod.mk_zero_zero, Set.mem_prod, Prod.fst_zero, Prod.snd_zero]
+      constructor
+      · simp only [Metric.mem_ball, dist_zero_right, Set.mem_setOf_eq]
+        intro v
+        have : ‖(0:InfiniteAdeleRing ℚ) v‖ = 0
+        · simp only [norm_eq_zero]
+          rfl
+        simp [this, zero_lt_one]
+      · simp only [Set.mem_setOf_eq]
+        intro v
+        apply zero_mem
 
 theorem Rat.AdeleRing.discrete : ∀ q : ℚ, ∃ U : Set (AdeleRing ℚ),
     IsOpen U ∧ (algebraMap ℚ (AdeleRing ℚ)) ⁻¹' U = {q} := sorry
 
 variable (K : Type*) [Field K] [NumberField K]
 
+-- Maybe this discreteness isn't even stated in the best way?
+-- I'm ambivalent about how it's stated
 theorem NumberField.AdeleRing.discrete : ∀ k : K, ∃ U : Set (AdeleRing K),
     IsOpen U ∧ (algebraMap K (AdeleRing K)) ⁻¹' U = {k} := sorry