Prove prodAdicCompletionComap_isModuleTopology (#353)

* Prove prodAdicCompletionComap_isModuleTopology

Fixes #327.

* Finite

Co-authored-by: Yakov Pechersky <[email protected]>

* Update blueprint

---------

Co-authored-by: Yakov Pechersky <[email protected]>

Author: Ruben-VandeVelde

FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean

@@ -246,23 +246,54 @@ lemma v_adicCompletionComapSemialgHom
   subst hvw
   rw [← valuation_comap A K L B w a]
 
+def noZeroSMulDivisors : NoZeroSMulDivisors A B := by
+  constructor
+  intro r x h
+  suffices (algebraMap A K r) • (algebraMap B L x) = 0 by
+    rw [smul_eq_zero] at this
+    simpa using this
+  have ht : Algebra.linearMap B L (r • x) = r • algebraMap B L x := by
+    simp [LinearMap.map_smul_of_tower]
+  rw [IsScalarTower.algebraMap_smul, ← ht, h, map_zero]
+
+def finite (v : HeightOneSpectrum A) : Finite {w : HeightOneSpectrum B // v = comap A w} := by
+  have := noZeroSMulDivisors A K L B
+  rw [← Set.coe_setOf]
+  rw [@Set.finite_coe_iff]
+  have := primesOver_finite v.asIdeal B
+  refine Set.Finite.of_finite_image (f := HeightOneSpectrum.asIdeal) ?_ ?_
+  · refine Set.Finite.subset this ?_
+    simp only [Set.subset_def, Set.mem_image, Set.mem_setOf_eq, forall_exists_index, and_imp,
+      forall_apply_eq_imp_iff₂]
+    rintro w rfl
+    simp only [Ideal.primesOver, Set.mem_setOf_eq, isPrime, true_and]
+    constructor
+    simp [Ideal.under_def, comap]
+  · intro x hx y hy hxy
+    rwa [← @HeightOneSpectrum.ext_iff] at hxy
+
 /-- The canonical map `K_v → ∏_{w|v} L_w` extending K → L. -/
 noncomputable def adicCompletionComapSemialgHom' (v : HeightOneSpectrum A) :
   (HeightOneSpectrum.adicCompletion K v) →ₛₐ[algebraMap K L]
     (∀ w : {w : HeightOneSpectrum B // v = comap A w}, HeightOneSpectrum.adicCompletion L w.1) :=
   Pi.semialgHom _ _ fun i ↦ adicCompletionComapSemialgHom A K L B v i.1 i.2
 
-lemma prodAdicCompletionComap_isModuleTopology
-    (v : HeightOneSpectrum A) (w : HeightOneSpectrum B) (hvw : v = comap A w) :
+lemma prodAdicCompletionComap_isModuleTopology (v : HeightOneSpectrum A) :
     -- temporarily make ∏_w L_w a K_v-algebra
-    let inst_alg : Algebra (HeightOneSpectrum.adicCompletion K v)
+    letI inst_alg : Algebra (HeightOneSpectrum.adicCompletion K v)
       (∀ w : {w : HeightOneSpectrum B // v = comap A w}, HeightOneSpectrum.adicCompletion L w.1) :=
-      RingHom.toAlgebra <|
-        Pi.ringHom (fun w : {w : HeightOneSpectrum B // v = comap A w} ↦ adicCompletionComapSemialgHom A K L B v w.1 w.2)
+      RingHom.toAlgebra <| adicCompletionComapSemialgHom' A K L B v
     -- the claim that L_w has the module topology.
     IsModuleTopology (HeightOneSpectrum.adicCompletion K v)
       (∀ w : {w : HeightOneSpectrum B // v = comap A w}, HeightOneSpectrum.adicCompletion L w.1) := by
-  sorry -- FLT#327
+  let _ (w : { w : HeightOneSpectrum B // v = comap A w }) :
+      Module (adicCompletion K v) (adicCompletion L w.1) :=
+    @Algebra.toModule _ _ _ _ <| RingHom.toAlgebra <| adicCompletionComapSemialgHom A K L B v w.1 w.2
+  let _ (w : { w : HeightOneSpectrum B // v = comap A w }) :
+      IsModuleTopology (adicCompletion K v) (adicCompletion L w.1) :=
+    adicCompletionComap_isModuleTopology A K L B v w.1 w.2
+  let _ := finite A K L B v
+  infer_instance
 
 open scoped TensorProduct -- ⊗ notation for tensor product
 

blueprint/src/chapter/AdeleMiniproject.tex

@@ -225,6 +225,7 @@ \subsection{Base change for finite adeles}
   topology.
 \end{theorem}
 \begin{proof}
+  \leanok
   This is a finite product of $K_v$-modules each of which has the $K_v$-module topology
   by~\ref{IsDedekindDomain.HeightOneSpectrum.adicCompletionComap_isModuleTopology},
   and the product topology is the module topology for a finite product of modules each of which