feat: topology on ring of finite adeles. (#14176)

Use `SubmodulesRingBasis` to put a topology on the finite adeles.

Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

@@ -83,6 +83,10 @@ def intValuationDef (r : R) : ℤₘ₀ :=
 theorem intValuationDef_if_pos {r : R} (hr : r = 0) : v.intValuationDef r = 0 :=
   if_pos hr
 
+@[simp]
+theorem intValuationDef_zero : v.intValuationDef 0 = 0 :=
+  if_pos rfl
+
 theorem intValuationDef_if_neg {r : R} (hr : r ≠ 0) :
     v.intValuationDef r =
       Multiplicative.ofAdd
@@ -312,6 +316,10 @@ theorem valuation_of_mk' {r : R} {s : nonZeroDivisors R} :
 theorem valuation_of_algebraMap (r : R) : v.valuation (algebraMap R K r) = v.intValuation r := by
   rw [valuation_def, Valuation.extendToLocalization_apply_map_apply]
 
+open scoped algebraMap in
+lemma valuation_eq_intValuationDef (r : R) : v.valuation (r : K) = v.intValuationDef r :=
+  Valuation.extendToLocalization_apply_map_apply ..
+
 /-- The `v`-adic valuation on `R` is bounded above by 1. -/
 theorem valuation_le_one (r : R) : v.valuation (algebraMap R K r) ≤ 1 := by
   rw [valuation_of_algebraMap]; exact v.intValuation_le_one r
@@ -394,6 +402,11 @@ theorem mem_adicCompletionIntegers {x : v.adicCompletion K} :
     x ∈ v.adicCompletionIntegers K ↔ (Valued.v x : ℤₘ₀) ≤ 1 :=
   Iff.rfl
 
+theorem not_mem_adicCompletionIntegers {x : v.adicCompletion K} :
+    x ∉ v.adicCompletionIntegers K ↔ 1 < (Valued.v x : ℤₘ₀) := by
+  rw [not_congr <| mem_adicCompletionIntegers R K v]
+  exact not_le
+
 section AlgebraInstances
 
 instance (priority := 100) adicValued.has_uniform_continuous_const_smul' :
@@ -457,6 +470,28 @@ instance : Algebra R (v.adicCompletionIntegers K) where
     simp only [Subring.coe_mul, Algebra.smul_def]
     rfl
 
+variable {R K} in
+open scoped algebraMap in -- to make the coercions from `R` fire
+/-- The valuation on the completion agrees with the global valuation on elements of the
+integer ring. -/
+theorem valuedAdicCompletion_eq_valuation (r : R) :
+    Valued.v (r : v.adicCompletion K) = v.valuation (r : K) := by
+  convert Valued.valuedCompletion_apply (r : K)
+
+variable {R K} in
+/-- The valuation on the completion agrees with the global valuation on elements of the field. -/
+theorem valuedAdicCompletion_eq_valuation' (k : K) :
+    Valued.v (k : v.adicCompletion K) = v.valuation k := by
+  convert Valued.valuedCompletion_apply k
+
+variable {R K} in
+open scoped algebraMap in -- to make the coercion from `R` fire
+/-- A global integer is in the local integers. -/
+lemma coe_mem_adicCompletionIntegers (r : R) :
+    (r : adicCompletion K v) ∈ adicCompletionIntegers K v := by
+  rw [mem_adicCompletionIntegers, valuedAdicCompletion_eq_valuation, valuation_eq_intValuationDef]
+  exact intValuation_le_one v r
+
 @[simp]
 theorem coe_smul_adicCompletionIntegers (r : R) (x : v.adicCompletionIntegers K) :
     (↑(r • x) : v.adicCompletion K) = r • (x : v.adicCompletion K) :=
@@ -477,4 +512,32 @@ instance adicCompletion.instIsScalarTower' :
 
 end AlgebraInstances
 
+open nonZeroDivisors algebraMap in
+variable {R K} in
+lemma adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers (v : HeightOneSpectrum R)
+    (a : v.adicCompletion K) : ∃ b ∈ R⁰, a * b ∈ v.adicCompletionIntegers K := by
+  by_cases ha : a ∈ v.adicCompletionIntegers K
+  · use 1
+    simp [ha, Submonoid.one_mem]
+  · rw [not_mem_adicCompletionIntegers] at ha
+    -- Let the additive valuation of a be -d with d>0
+    obtain ⟨d, hd⟩ : ∃ d : ℤ, Valued.v a = ofAdd d :=
+      Option.ne_none_iff_exists'.mp <| (lt_trans zero_lt_one ha).ne'
+    rw [hd, WithZero.one_lt_coe, ← ofAdd_zero, ofAdd_lt] at ha
+    -- let ϖ be a uniformiser
+    obtain ⟨ϖ, hϖ⟩ := intValuation_exists_uniformizer v
+    have hϖ0 : ϖ ≠ 0 := by rintro rfl; simp at hϖ
+    -- use ϖ^d
+    refine ⟨ϖ^d.natAbs, pow_mem (mem_nonZeroDivisors_of_ne_zero hϖ0) _, ?_⟩
+    -- now manually translate the goal (an inequality in ℤₘ₀) to an inequality in ℤ
+    rw [mem_adicCompletionIntegers, algebraMap.coe_pow, map_mul, hd, map_pow,
+      valuedAdicCompletion_eq_valuation, valuation_eq_intValuationDef, hϖ, ← WithZero.coe_pow,
+      ← WithZero.coe_mul, WithZero.coe_le_one, ← toAdd_le, toAdd_mul, toAdd_ofAdd, toAdd_pow,
+      toAdd_ofAdd, toAdd_one,
+      show d.natAbs • (-1) = (d.natAbs : ℤ) • (-1) by simp only [nsmul_eq_mul,
+        Int.natCast_natAbs, smul_eq_mul],
+      ← Int.eq_natAbs_of_zero_le ha.le, smul_eq_mul]
+    -- and now it's easy
+    linarith
+
 end IsDedekindDomain.HeightOneSpectrum

Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

@@ -327,6 +327,12 @@ instance : CommRing (FiniteAdeleRing R K) :=
 instance : Algebra K (FiniteAdeleRing R K) :=
   Subalgebra.algebra (subalgebra R K)
 
+instance : Algebra R (FiniteAdeleRing R K) :=
+  ((algebraMap K (FiniteAdeleRing R K)).comp (algebraMap R K)).toAlgebra
+
+instance : IsScalarTower R K (FiniteAdeleRing R K) :=
+  IsScalarTower.of_algebraMap_eq' rfl
+
 instance : Coe (FiniteAdeleRing R K) (K_hat R K) where
   coe := fun x ↦ x.1
 
@@ -348,6 +354,86 @@ instance : Algebra (R_hat R K) (FiniteAdeleRing R K) where
   commutes' _ _ := mul_comm _ _
   smul_def' r x := rfl
 
+instance : CoeFun (FiniteAdeleRing R K)
+    (fun _ ↦ ∀ (v : HeightOneSpectrum R), adicCompletion K v) where
+  coe a v := a.1 v
+
+open scoped algebraMap in
+variable {R K} in
+lemma exists_finiteIntegralAdele_iff (a : FiniteAdeleRing R K) : (∃ c : R_hat R K,
+    a = c) ↔ ∀ (v : HeightOneSpectrum R), a v ∈ adicCompletionIntegers K v :=
+  ⟨by rintro ⟨c, rfl⟩ v; exact (c v).2, fun h ↦ ⟨fun v ↦ ⟨a v, h v⟩, rfl⟩⟩
+
+section Topology
+
+open Classical nonZeroDivisors Multiplicative Additive IsDedekindDomain.HeightOneSpectrum
+
+open scoped algebraMap -- coercion from R to FiniteAdeleRing R K
+open scoped DiscreteValuation
+
+variable {R K} in
+lemma mul_nonZeroDivisor_mem_finiteIntegralAdeles (a : FiniteAdeleRing R K) :
+    ∃ (b : R⁰) (c : R_hat R K), a * ((b : R) : FiniteAdeleRing R K) = c := by
+  let S := {v | a v ∉ adicCompletionIntegers K v}
+  choose b hb h using adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers (R := R) (K := K)
+  let p := ∏ᶠ v ∈ S, b v (a v)
+  have hp : p ∈ R⁰ := finprod_mem_induction (· ∈ R⁰) (one_mem _) (fun _ _ => mul_mem) <|
+    fun _ _ ↦ hb _ _
+  use ⟨p, hp⟩
+  rw [exists_finiteIntegralAdele_iff]
+  intro v
+  by_cases hv : a v ∈ adicCompletionIntegers K v
+  · exact mul_mem hv <| coe_mem_adicCompletionIntegers _ _
+  · dsimp only
+    have pprod : p = b v (a v) * ∏ᶠ w ∈ S \ {v}, b w (a w) := by
+      rw [← finprod_mem_singleton (a := v) (f := fun v ↦ b v (a v)),
+        finprod_mem_mul_diff (singleton_subset_iff.2 ‹v ∈ S›) a.2]
+    rw [pprod]
+    push_cast
+    rw [← mul_assoc]
+    exact mul_mem (h v (a v)) <| coe_mem_adicCompletionIntegers _ _
+
+open scoped Pointwise
+
+theorem submodulesRingBasis : SubmodulesRingBasis
+    (fun (r : R⁰) ↦ Submodule.span (R_hat R K) {((r : R) : FiniteAdeleRing R K)}) where
+  inter i j := ⟨i * j, by
+    push_cast
+    simp only [le_inf_iff, Submodule.span_singleton_le_iff_mem, Submodule.mem_span_singleton]
+    exact ⟨⟨((j : R) : R_hat R K), by rw [mul_comm]; rfl⟩, ⟨((i : R) : R_hat R K), rfl⟩⟩⟩
+  leftMul a r := by
+    rcases mul_nonZeroDivisor_mem_finiteIntegralAdeles a with ⟨b, c, h⟩
+    use r * b
+    rintro x ⟨m, hm, rfl⟩
+    simp only [Submonoid.coe_mul, SetLike.mem_coe] at hm
+    rw [Submodule.mem_span_singleton] at hm ⊢
+    rcases hm with ⟨n, rfl⟩
+    simp only [LinearMapClass.map_smul, DistribMulAction.toLinearMap_apply, smul_eq_mul]
+    use n * c
+    push_cast
+    rw [mul_left_comm, h, mul_comm _ (c : FiniteAdeleRing R K),
+      Algebra.smul_def', Algebra.smul_def', ← mul_assoc]
+    rfl
+  mul r := ⟨r, by
+    intro x hx
+    rw [mem_mul] at hx
+    rcases hx with ⟨a, ha, b, hb, rfl⟩
+    simp only [SetLike.mem_coe, Submodule.mem_span_singleton] at ha hb ⊢
+    rcases ha with ⟨m, rfl⟩
+    rcases hb with ⟨n, rfl⟩
+    use m * n * (r : R)
+    simp only [Algebra.smul_def', map_mul]
+    rw [mul_mul_mul_comm, mul_assoc]
+    rfl⟩
+
+instance : TopologicalSpace (FiniteAdeleRing R K) :=
+  SubmodulesRingBasis.topology (submodulesRingBasis R K)
+
+-- the point of the above: this now works
+example : TopologicalRing (FiniteAdeleRing R K) := inferInstance
+
+end Topology
+
 end FiniteAdeleRing
 
 end DedekindDomain