Merge branch 'main' of github.com:ImperialCollegeLondon/FLT

FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean

@@ -277,11 +277,22 @@ attribute [local instance] Algebra.TensorProduct.rightAlgebra in
 variable (v : HeightOneSpectrum A) in
 instance : TopologicalSpace (L ⊗[K] adicCompletion K v) := moduleTopology (adicCompletion K v) _
 
+attribute [local instance] Algebra.TensorProduct.rightAlgebra in
+variable (v : HeightOneSpectrum A) in
+instance : IsModuleTopology (adicCompletion K v) (L ⊗[K] adicCompletion K v) :=
+  ⟨rfl⟩
+
+attribute [local instance] Algebra.TensorProduct.rightAlgebra in
 noncomputable def adicCompletionTensorComapContinuousAlgHom (v : HeightOneSpectrum A) :
     L ⊗[K] adicCompletion K v →A[L]
       Π w : {w : HeightOneSpectrum B // v = comap A w}, adicCompletion L w.1 where
   __ := adicCompletionTensorComapAlgHom A K L B v
-  cont := sorry -- #237
+  cont := by
+    apply IsModuleTopology.continuous_of_ringHom (R := adicCompletion K v)
+    show Continuous (RingHom.comp _ (Algebra.TensorProduct.includeRight.toRingHom))
+    convert (adicCompletionContinuousComapAlgHom A K L B v).cont using 1
+    ext
+    simp [adicCompletionTensorComapAlgHom, adicCompletionContinuousComapAlgHom]
 
 noncomputable def adicCompletionComapAlgEquiv (v : HeightOneSpectrum A) :
   (L ⊗[K] (HeightOneSpectrum.adicCompletion K v)) ≃ₐ[L]

FLT/NumberField/AdeleRing.lean

@@ -18,7 +18,6 @@ section BaseChange
 
 end BaseChange
 
-
 section Discrete
 
 open NumberField DedekindDomain
@@ -64,14 +63,13 @@ theorem Rat.AdeleRing.zero_discrete : ∃ U : Set (AdeleRing ℚ),
         -- and the goal is that there exists an integer `y` such that `y = x`.
         sorry -- issue #254
       obtain ⟨y, rfl⟩ := intx
-      simp at h1
-      clear h2 -- not needed
-      norm_cast
-      norm_cast at h1
-      -- mathematically this is trivial:
-      -- h1 says that the integer y satisfies |y| < 1
-      -- and the goal is that y = 0
-      sorry -- issue #255
+      simp only [abs_lt] at h1
+      norm_cast at h1 ⊢
+      -- We need the next line because `norm_cast` is for some reason producing a `negSucc 0`.
+      -- I haven't been able to isolate this behaviour even in a standalone lemma.
+      -- We could also make `omega` more robust against accidental appearances of `negSucc`.
+      rw [Int.negSucc_eq] at h1
+      omega
     · intro x
       simp only [Set.mem_singleton_iff, Set.mem_preimage]
       rintro rfl