feat: the finite adele ring is an algebra over the finite integral ad…

…eles. (#13705)

Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

@@ -197,6 +197,10 @@ def IsFiniteAdele (x : K_hat R K) :=
   ∀ᶠ v : HeightOneSpectrum R in Filter.cofinite, x v ∈ v.adicCompletionIntegers K
 #align dedekind_domain.prod_adic_completions.is_finite_adele DedekindDomain.ProdAdicCompletions.IsFiniteAdele
 
+@[simp]
+lemma isFiniteAdele_iff (x : K_hat R K) :
+    x.IsFiniteAdele ↔ {v | x v ∉ adicCompletionIntegers K v}.Finite := Iff.rfl
+
 namespace IsFiniteAdele
 
 /-- The sum of two finite adèles is a finite adèle. -/
@@ -312,22 +316,32 @@ end ProdAdicCompletions
 open ProdAdicCompletions.IsFiniteAdele
 
 /-- The finite adèle ring of `R` is the restricted product over all maximal ideals `v` of `R`
-of `adicCompletion` with respect to `adicCompletionIntegers`. -/
-def FiniteAdeleRing : Type _ := (
-  { carrier := {x : K_hat R K | x.IsFiniteAdele}
-    mul_mem' := mul
-    one_mem' := one
-    add_mem' := add
-    zero_mem' := zero
-    algebraMap_mem' := algebraMap'
-  } : Subalgebra K (K_hat R K))
+of `adicCompletion`, with respect to `adicCompletionIntegers`. -/
+def FiniteAdeleRing : Type _ := {x : K_hat R K // x.IsFiniteAdele}
 #align dedekind_domain.finite_adele_ring DedekindDomain.FiniteAdeleRing
 
 namespace FiniteAdeleRing
 
-instance : CommRing (FiniteAdeleRing R K) := Subalgebra.toCommRing _
+/-- The finite adèle ring of `R`, regarded as a `K`-subalgebra of the
+product of the local completions of `K`.
+
+Note that this definition exists to streamline the proof that the finite adèles are an algebra
+over `K`, rather than to express their relationship to `K_hat R K` which is essentially a
+detail of their construction.
+-/
+def subalgebra : Subalgebra K (K_hat R K) where
+  carrier := {x : K_hat R K | x.IsFiniteAdele}
+  mul_mem' := mul
+  one_mem' := one
+  add_mem' := add
+  zero_mem' := zero
+  algebraMap_mem' := algebraMap'
+
+instance : CommRing (FiniteAdeleRing R K) :=
+  Subalgebra.toCommRing (subalgebra R K)
 
-instance : Algebra K (FiniteAdeleRing R K) := Subalgebra.algebra _
+instance : Algebra K (FiniteAdeleRing R K) :=
+  Subalgebra.algebra (subalgebra R K)
 
 instance : Coe (FiniteAdeleRing R K) (K_hat R K) where
   coe := fun x ↦ x.1
@@ -336,6 +350,20 @@ instance : Coe (FiniteAdeleRing R K) (K_hat R K) where
 lemma ext {a₁ a₂ : FiniteAdeleRing R K} (h : (a₁ : K_hat R K) = a₂) : a₁ = a₂ :=
   Subtype.ext h
 
+/-- The finite adele ring is an algebra over the finite integral adeles. -/
+instance : Algebra (R_hat R K) (FiniteAdeleRing R K) where
+  smul rhat fadele := ⟨fun v ↦ rhat v * fadele.1 v, Finite.subset fadele.2 <| fun v hv ↦ by
+    simp only [mem_adicCompletionIntegers, mem_compl_iff, mem_setOf_eq, map_mul] at hv ⊢
+    exact mt (mul_le_one₀ (rhat v).2) hv
+    ⟩
+  toFun r := ⟨r, by simp_all⟩
+  map_one' := by ext; rfl
+  map_mul' _ _ := by ext; rfl
+  map_zero' := by ext; rfl
+  map_add' _ _ := by ext; rfl
+  commutes' _ _ := mul_comm _ _
+  smul_def' r x := rfl
+
 end FiniteAdeleRing
 
 end DedekindDomain