chore(NumberTheory/NumberField/AdeleRing): refactor adele rings

Mathlib/NumberTheory/NumberField/AdeleRing.lean

@@ -41,8 +41,6 @@ open InfinitePlace AbsoluteValue.Completion InfinitePlace.Completion DedekindDom
 
 open scoped Classical
 
-variable (K : Type*) [Field K]
-
 /-! ## The infinite adele ring
 
 The infinite adele ring is the finite product of completions of a number field over its
@@ -51,10 +49,12 @@ infinite places. See `NumberField.InfinitePlace` for the definition of an infini
 -/
 
 /-- The infinite adele ring of a number field. -/
-def InfiniteAdeleRing := (v : InfinitePlace K) → v.Completion
+def InfiniteAdeleRing (K : Type*) [Field K] := (v : InfinitePlace K) → v.Completion
 
 namespace InfiniteAdeleRing
 
+variable (K : Type*) [Field K]
+
 instance : CommRing (InfiniteAdeleRing K) := Pi.commRing
 
 instance : Inhabited (InfiniteAdeleRing K) := ⟨0⟩
@@ -115,38 +115,47 @@ theorem mixedEmbedding_eq_algebraMap_comp {x : K} :
 
 end InfiniteAdeleRing
 
-variable [NumberField K]
-
 /-! ## The adele ring  -/
 
-/-- The adele ring of a number field. -/
-def AdeleRing := InfiniteAdeleRing K × FiniteAdeleRing (𝓞 K) K
+/-- `AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.
+
+More generally `AdeleRing R K` can be used if `K` is the field of fractions
+of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
+in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.
+
+Note that this definition does not give the correct answer in the function field case.
+-/
+def AdeleRing (R K : Type*) [CommRing R] [IsDedekindDomain R] [Field K]
+  [Algebra R K] [IsFractionRing R K] := InfiniteAdeleRing K × FiniteAdeleRing R K
 
 namespace AdeleRing
 
-instance : CommRing (AdeleRing K) := Prod.instCommRing
+variable (R K : Type*) [CommRing R] [IsDedekindDomain R] [Field K]
+  [Algebra R K] [IsFractionRing R K]
+
+instance : CommRing (AdeleRing R K) := Prod.instCommRing
 
-instance : Inhabited (AdeleRing K) := ⟨0⟩
+instance : Inhabited (AdeleRing R K) := ⟨0⟩
 
-instance : TopologicalSpace (AdeleRing K) := instTopologicalSpaceProd
+instance : TopologicalSpace (AdeleRing R K) := instTopologicalSpaceProd
 
-instance : TopologicalRing (AdeleRing K) := instTopologicalRingProd
+instance : TopologicalRing (AdeleRing R K) := instTopologicalRingProd
 
-instance : Algebra K (AdeleRing K) := Prod.algebra _ _ _
+instance : Algebra K (AdeleRing R K) := Prod.algebra _ _ _
 
 @[simp]
 theorem algebraMap_fst_apply (x : K) (v : InfinitePlace K) :
-    (algebraMap K (AdeleRing K) x).1 v = x := rfl
+    (algebraMap K (AdeleRing R K) x).1 v = x := rfl
 
 @[simp]
-theorem algebraMap_snd_apply (x : K) (v : HeightOneSpectrum (𝓞 K)) :
-    (algebraMap K (AdeleRing K) x).2 v = x := rfl
+theorem algebraMap_snd_apply (x : K) (v : HeightOneSpectrum R) :
+    (algebraMap K (AdeleRing R K) x).2 v = x := rfl
 
-theorem algebraMap_injective : Function.Injective (algebraMap K (AdeleRing K)) :=
+theorem algebraMap_injective [NumberField K] : Function.Injective (algebraMap K (AdeleRing R K)) :=
   fun _ _ hxy => (algebraMap K _).injective (Prod.ext_iff.1 hxy).1
 
 /-- The subgroup of principal adeles `(x)ᵥ` where `x ∈ K`. -/
-abbrev principalSubgroup : AddSubgroup (AdeleRing K) := (algebraMap K _).range.toAddSubgroup
+abbrev principalSubgroup : AddSubgroup (AdeleRing R K) := (algebraMap K _).range.toAddSubgroup
 
 end AdeleRing