Issue ImperialCollegeLondon#259: Proof that A_K/K is compact, assumin…

…g that A_Q/Q is compact

FLT/ForMathlib/LinearAlgebra/TensorProduct/Pi.lean

@@ -0,0 +1,10 @@
+import Mathlib.LinearAlgebra.TensorProduct.Pi
+
+theorem TensorProduct.piScalarRight_symm_apply (R S N ι : Type*) [CommSemiring R]
+    [CommSemiring S] [Algebra R S] [AddCommMonoid N] [Module R N] [Module S N]
+    [IsScalarTower R S N] [Fintype ι] [DecidableEq ι] (x : ι → N) :
+    (TensorProduct.piScalarRight R S N ι).symm x = (LinearMap.lsum S (fun _ => N) S (fun i => {
+      toFun := fun n => n ⊗ₜ[R] Pi.single i (1 : R)
+      map_add' := fun _ _ => by simp [add_tmul]
+      map_smul' := fun _ _ => rfl
+    }) x) := rfl

FLT/ForMathlib/RingTheory/TensorProduct/Pi.lean

@@ -0,0 +1,12 @@
+import Mathlib.RingTheory.TensorProduct.Pi
+import FLT.ForMathlib.LinearAlgebra.TensorProduct.Pi
+
+theorem Algebra.TensorProduct.piScalarRight_symm_apply_of_algebraMap (R S N ι : Type*)
+    [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring N] [Algebra R N] [Algebra S N]
+    [IsScalarTower R S N] [Fintype ι] [DecidableEq ι] (x : ι → R) :
+    (TensorProduct.piScalarRight R S N ι).symm (fun i => algebraMap _ _ (x i)) =
+      1 ⊗ₜ[R] (∑ i, Pi.single i (x i)) := by
+  simp only [_root_.TensorProduct.piScalarRight_symm_apply, LinearMap.lsum_apply,
+    LinearMap.coeFn_sum, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.coe_proj,
+    Finset.sum_apply, Function.comp_apply, Function.eval, Algebra.algebraMap_eq_smul_one,
+    TensorProduct.smul_tmul, ← TensorProduct.tmul_sum, ← Pi.single_smul, smul_eq_mul, mul_one]

FLT/ForMathlib/Topology/Algebra/Algebra.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Salvatore Mercuri
 -/
 import Mathlib.Topology.Algebra.Algebra
+import Mathlib.Topology.Algebra.Module.Equiv
 
 /-!
 # Topological (sub)algebras
@@ -39,6 +40,11 @@ def toContinuousAlgHom (e : A ≃A[R] B) : A →A[R] B where
   __ := e.toAlgHom
   cont := e.continuous_toFun
 
+def toContinuousLinearEquiv (e : A ≃A[R] B) : A ≃L[R] B where
+  __ := e.toLinearEquiv
+  continuous_toFun := e.continuous_toFun
+  continuous_invFun := e.continuous_invFun
+
 instance coe : Coe (A ≃A[R] B) (A →A[R] B) := ⟨toContinuousAlgHom⟩
 
 instance equivLike : EquivLike (A ≃A[R] B) A B where

FLT/ForMathlib/Topology/Algebra/ContinuousMonoidHom.lean

@@ -0,0 +1,19 @@
+import Mathlib.Topology.Algebra.ContinuousMonoidHom
+import Mathlib.Topology.Algebra.Module.Equiv
+import FLT.ForMathlib.Topology.Algebra.Module.Equiv
+import FLT.ForMathlib.Topology.Algebra.Module.Quotient
+
+def ContinuousAddEquiv.toIntContinuousLinearEquiv {M M₂ : Type*} [AddCommGroup M]
+    [TopologicalSpace M] [AddCommGroup M₂] [TopologicalSpace M₂] (e : M ≃ₜ+ M₂) :
+    M ≃L[ℤ] M₂ where
+  __ := e.toIntLinearEquiv
+  continuous_toFun := e.continuous
+  continuous_invFun := e.continuous_invFun
+
+def ContinuousAddEquiv.quotientPi {ι : Type*} {G : ι → Type*} [(i : ι) → AddCommGroup (G i)]
+    [(i : ι) → TopologicalSpace (G i)]
+    [(i : ι) → TopologicalAddGroup (G i)]
+    [Fintype ι] (p : (i : ι) → AddSubgroup (G i)) [DecidableEq ι] :
+    ((i : ι) → G i) ⧸ AddSubgroup.pi (_root_.Set.univ) p ≃ₜ+ ((i : ι) → G i ⧸ p i) :=
+  (Submodule.quotientPiContinuousLinearEquiv
+    (fun (i : ι) => AddSubgroup.toIntSubmodule (p i))).toContinuousAddEquiv

FLT/ForMathlib/Topology/Algebra/Group/Quotient.lean

@@ -0,0 +1,13 @@
+import Mathlib.Topology.Algebra.Group.Quotient
+import Mathlib.Topology.Algebra.ContinuousMonoidHom
+import FLT.ForMathlib.Topology.Algebra.ContinuousMonoidHom
+import FLT.ForMathlib.Topology.Algebra.Module.Quotient
+import FLT.ForMathlib.Topology.Algebra.Module.Equiv
+
+def QuotientAddGroup.continuousAddEquiv (G H : Type*) [AddCommGroup G] [AddCommGroup H] [TopologicalSpace G]
+    [TopologicalSpace H] (G' : AddSubgroup G) (H' : AddSubgroup H) [G'.Normal] [H'.Normal]
+    (e : G ≃ₜ+ H) (h : AddSubgroup.map e G' = H') :
+    G ⧸ G' ≃ₜ+ H ⧸ H' :=
+  (Submodule.Quotient.continuousLinearEquiv _ _ (AddSubgroup.toIntSubmodule G')
+    (AddSubgroup.toIntSubmodule H') e.toIntContinuousLinearEquiv
+      (congrArg AddSubgroup.toIntSubmodule h)).toContinuousAddEquiv

FLT/ForMathlib/Topology/Algebra/Module/Equiv.lean

@@ -0,0 +1,11 @@
+import Mathlib.Topology.Algebra.Module.Equiv
+import Mathlib.Topology.Algebra.ContinuousMonoidHom
+
+def ContinuousLinearEquiv.toContinuousAddEquiv
+    {R₁ R₂ : Type*} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂}  {σ₂₁ : R₂ →+* R₁}
+    [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ M₂ : Type*} [TopologicalSpace M₁]
+    [AddCommMonoid M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂]
+    (e : M₁ ≃SL[σ₁₂] M₂) :
+    M₁ ≃ₜ+ M₂ where
+  __ := e.toLinearEquiv.toAddEquiv
+  continuous_invFun := e.symm.continuous

FLT/ForMathlib/Topology/Algebra/Module/Quotient.lean

@@ -0,0 +1,34 @@
+import Mathlib.LinearAlgebra.Quotient.Pi
+import Mathlib.Topology.Algebra.Module.Equiv
+
+def Submodule.Quotient.continuousLinearEquiv {R : Type*} [Ring R] (G H : Type*) [AddCommGroup G]
+    [Module R G] [AddCommGroup H] [Module R H] [TopologicalSpace G] [TopologicalSpace H]
+    (G' : Submodule R G) (H' : Submodule R H) (e : G ≃L[R] H) (h : Submodule.map e G' = H') :
+    (G ⧸ G') ≃L[R] (H ⧸ H') where
+  toLinearEquiv := Submodule.Quotient.equiv G' H' e h
+  continuous_toFun := by
+    apply continuous_quot_lift
+    simp only [LinearMap.toAddMonoidHom_coe, LinearMap.coe_comp]
+    exact Continuous.comp continuous_quot_mk e.continuous
+  continuous_invFun := by
+    apply continuous_quot_lift
+    simp only [LinearMap.toAddMonoidHom_coe, LinearMap.coe_comp]
+    exact Continuous.comp continuous_quot_mk e.continuous_invFun
+
+def Submodule.quotientPiContinuousLinearEquiv {R ι : Type*} [CommRing R] {G : ι → Type*}
+    [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] [(i : ι) → TopologicalSpace (G i)]
+    [(i : ι) → TopologicalAddGroup (G i)] [Fintype ι] [DecidableEq ι]
+    (p : (i : ι) → Submodule R (G i)) :
+    (((i : ι) → G i) ⧸ Submodule.pi Set.univ p) ≃L[R] ((i : ι) → G i ⧸ p i) where
+  toLinearEquiv := Submodule.quotientPi p
+  continuous_toFun := by
+    apply Continuous.quotient_lift
+    exact continuous_pi (fun i => Continuous.comp continuous_quot_mk (continuous_apply _))
+  continuous_invFun := by
+    rw [show (quotientPi p).invFun = fun a => (quotientPi p).invFun a from rfl]
+    simp only [LinearEquiv.invFun_eq_symm, quotientPi_symm_apply, Submodule.piQuotientLift,
+      LinearMap.lsum_apply, LinearMap.coeFn_sum, LinearMap.coe_comp, LinearMap.coe_proj,
+      Finset.sum_apply, Function.comp_apply, Function.eval]
+    refine continuous_finset_sum _ (fun i _ => ?_)
+    apply Continuous.comp ?_ (continuous_apply _)
+    apply Continuous.quotient_lift <| Continuous.comp (continuous_quot_mk) (continuous_single _)

FLT/NumberField/AdeleRing.lean

@@ -1,4 +1,9 @@
 import Mathlib
+import FLT.ForMathlib.RingTheory.TensorProduct.Pi
+import FLT.ForMathlib.Topology.Algebra.Group.Quotient
+import FLT.ForMathlib.Topology.Algebra.Algebra
+
+open scoped TensorProduct
 
 universe u
 
@@ -16,6 +21,140 @@ end LocallyCompact
 
 section BaseChange
 
+namespace NumberField.AdeleRing
+
+variable (K L : Type*) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
+
+noncomputable instance : Algebra K (NumberField.AdeleRing L) :=
+  RingHom.toAlgebra <| (algebraMap L (NumberField.AdeleRing L)).comp <| algebraMap K L
+
+noncomputable abbrev tensorProductLinearEquivPi : AdeleRing K ⊗[K] L ≃ₗ[K]
+    (Fin (Module.finrank K L) → AdeleRing K) :=
+  LinearEquiv.trans (TensorProduct.congr (LinearEquiv.refl K (AdeleRing K))
+      (Basis.equivFun (Module.finBasis K L)))
+    (TensorProduct.piScalarRight _ _ _ _)
+
+variable {L}
+
+theorem tensorProductLinearEquivPi_tsum_apply (l : L) :
+    tensorProductLinearEquivPi K L (1 ⊗ₜ[K] l) =
+      fun i => algebraMap _ _ (Module.finBasis K L |>.equivFun l i) := by
+  simp [tensorProductLinearEquivPi, Algebra.algebraMap_eq_smul_one]
+
+variable {K}
+
+theorem tensorProductLinearEquivPi_symm_apply_of_algebraMap
+    (x : Fin (Module.finrank K L) → K) :
+    (tensorProductLinearEquivPi K L).symm (fun i => algebraMap _ _ (x i)) =
+      1 ⊗ₜ[K] ((Module.finBasis K L).equivFun.symm x) := by
+  simp only [LinearEquiv.trans_symm, LinearEquiv.trans_apply,
+    Algebra.TensorProduct.piScalarRight_symm_apply_of_algebraMap, TensorProduct.congr_symm_tmul,
+    LinearEquiv.refl_symm, LinearEquiv.refl_apply, map_sum, Basis.equivFun_symm_apply]
+  rw [Finset.sum_comm]
+  simp only [← Finset.sum_smul, Fintype.sum_pi_single]
+
+/-
+smmercuri: A possible alternative using `moduleTopology` is
+```
+instance :
+    TopologicalSpace (NumberField.AdeleRing K ⊗[K] L) :=
+  letI := TopologicalSpace.induced (algebraMap K (AdeleRing K)) inferInstance
+  moduleTopology K _
+```
+However it is not clear to me how the inverse function is of `tensorProductLinearEquivPi`
+is continuous in that case. Additionally,
+https://math.mit.edu/classes/18.785/2017fa/LectureNotes25.pdf (just above Prop 25.10)
+for an informal source where the tensor product is given the product topology. Maybe they
+coincide!
+-/
+instance : TopologicalSpace (NumberField.AdeleRing K ⊗[K] L) :=
+  TopologicalSpace.induced (NumberField.AdeleRing.tensorProductLinearEquivPi K L) inferInstance
+
+variable (K L)
+
+noncomputable def tensorProductContinuousLinearEquivPi :
+    AdeleRing K ⊗[K] L ≃L[K] (Fin (Module.finrank K L) → AdeleRing K) where
+  toLinearEquiv := tensorProductLinearEquivPi K L
+  continuous_toFun := continuous_induced_dom
+  continuous_invFun := by
+    convert (tensorProductLinearEquivPi K L).toEquiv.coinduced_symm ▸ continuous_coinduced_rng
+
+variable {K L}
+
+theorem tensorProductContinuousLinearEquivPi_symm_apply_of_algebraMap
+    (x : Fin (Module.finrank K L) → K) :
+    (tensorProductContinuousLinearEquivPi K L).symm (fun i => algebraMap _ _ (x i)) =
+      1 ⊗ₜ[K] ((Module.finBasis K L).equivFun.symm x) := by
+  exact tensorProductLinearEquivPi_symm_apply_of_algebraMap _
+
+variable (K L)
+
+/-
+smmercuri : The tensor product here is in a different order to the one
+appearing in the finite adele ring base change, where `L ⊗[K] FiniteAdeleRing A K`
+is used. Is there a preference between these orderings? One benefit
+to using `AdeleRing K ⊗[K] L` is that it automatically gets
+a `K` algebra instance via the instance `Algebra.TensorProduct.leftAlgebra`
+(while `rightAlgebra` is a def), but maybe there are other reasons to
+prefer the `rightAlgebra` set up.
+-/
+def baseChange : (AdeleRing K ⊗[K] L) ≃A[K] AdeleRing L := sorry
+
+variable {L}
+
+theorem baseChange_tsum_apply_right (l : L) :
+  baseChange K L (1 ⊗ₜ[K] l) = algebraMap L (AdeleRing L) l := sorry
+
+variable (L)
+
+noncomputable def baseChangePi :
+    (Fin (Module.finrank K L) → AdeleRing K) ≃L[K] AdeleRing L :=
+  (tensorProductContinuousLinearEquivPi K L).symm.trans (baseChange K L).toContinuousLinearEquiv
+
+variable {K L}
+
+theorem baseChangePi_apply (x : Fin (Module.finrank K L) → AdeleRing K) :
+    baseChangePi K L x = baseChange K L ((tensorProductContinuousLinearEquivPi K L).symm x) := rfl
+
+theorem baseChangePi_apply_eq_algebraMap_comp
+    {x : Fin (Module.finrank K L) → AdeleRing K}
+    {y : Fin (Module.finrank K L) → K}
+    (h : ∀ i, algebraMap K (AdeleRing K) (y i) = x i) :
+    baseChangePi K L x = algebraMap L (AdeleRing L) ((Module.finBasis K L).equivFun.symm y) := by
+  rw [← funext h, baseChangePi_apply, tensorProductContinuousLinearEquivPi_symm_apply_of_algebraMap,
+    baseChange_tsum_apply_right]
+
+theorem baseChangePi_mem_principalSubgroup
+    {x : Fin (Module.finrank K L) → AdeleRing K}
+    (h : x ∈ AddSubgroup.pi Set.univ (fun _ => principalSubgroup K)) :
+    baseChangePi K L x ∈ principalSubgroup L := by
+  simp only [AddSubgroup.mem_pi, Set.mem_univ, forall_const] at h
+  choose y hy using h
+  exact baseChangePi_apply_eq_algebraMap_comp hy ▸ ⟨(Module.finBasis K L).equivFun.symm y, rfl⟩
+
+variable (K L)
+
+theorem baseChangePi_map_principalSubgroup :
+    (AddSubgroup.pi Set.univ (fun (_ : Fin (Module.finrank K L)) => principalSubgroup K)).map
+      (baseChangePi K L).toAddMonoidHom = principalSubgroup L := by
+  ext x
+  simp only [AddSubgroup.mem_map, LinearMap.toAddMonoidHom_coe, LinearEquiv.coe_coe,
+    ContinuousLinearEquiv.coe_toLinearEquiv]
+  refine ⟨fun ⟨a, h, ha⟩ => ha ▸ baseChangePi_mem_principalSubgroup h, ?_⟩
+  rintro ⟨a, rfl⟩
+  use fun i => algebraMap K (AdeleRing K) ((Module.finBasis K L).equivFun a i)
+  refine ⟨fun i _ => ⟨(Module.finBasis K L).equivFun a i, rfl⟩, ?_⟩
+  rw [baseChangePi_apply_eq_algebraMap_comp (fun i => rfl), LinearEquiv.symm_apply_apply]
+  rfl
+
+noncomputable def baseChangeQuotientPi :
+    (Fin (Module.finrank K L) → AdeleRing K ⧸ principalSubgroup K) ≃ₜ+ AdeleRing L ⧸ principalSubgroup L :=
+  (ContinuousAddEquiv.quotientPi _).symm.trans <|
+    QuotientAddGroup.continuousAddEquiv _ _ _ _ (baseChangePi K L).toContinuousAddEquiv
+      (baseChangePi_map_principalSubgroup K L)
+
+end NumberField.AdeleRing
+
 end BaseChange
 
 section Discrete
@@ -101,7 +240,6 @@ theorem Rat.AdeleRing.discrete : ∀ q : ℚ, ∃ U : Set (AdeleRing ℚ),
   ext
   simp only [Set.mem_preimage, Homeomorph.subLeft_apply, Set.mem_singleton_iff, sub_eq_zero, eq_comm]
 
-
 variable (K : Type*) [Field K] [NumberField K]
 
 theorem NumberField.AdeleRing.discrete : ∀ k : K, ∃ U : Set (AdeleRing K),
@@ -114,13 +252,14 @@ section Compact
 open NumberField
 
 theorem Rat.AdeleRing.cocompact :
-    CompactSpace (AdeleRing ℚ ⧸ AddMonoidHom.range (algebraMap ℚ (AdeleRing ℚ)).toAddMonoidHom) :=
+    CompactSpace (AdeleRing ℚ ⧸ AdeleRing.principalSubgroup ℚ) :=
   sorry -- issue #258
 
-variable (K : Type*) [Field K] [NumberField K]
+variable (K L : Type*) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
 
 theorem NumberField.AdeleRing.cocompact :
-    CompactSpace (AdeleRing K ⧸ AddMonoidHom.range (algebraMap K (AdeleRing K)).toAddMonoidHom) :=
-  sorry -- issue #259
+    CompactSpace (AdeleRing K ⧸ principalSubgroup K) :=
+  letI := Rat.AdeleRing.cocompact
+  (baseChangeQuotientPi ℚ K).compactSpace
 
 end Compact