Issue #259: A_K/K is compact if A_Q/Q is compact

FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean

@@ -525,4 +525,9 @@ noncomputable def bar {K L AK AL : Type*} [CommRing K] [CommRing L]
 noncomputable def FiniteAdeleRing.baseChangeEquiv : L ⊗[K] FiniteAdeleRing A K ≃ₐ[L] FiniteAdeleRing B L :=
   AlgEquiv.ofBijective (bar <| FiniteAdeleRing.baseChange A K L B) sorry -- #243
 
+instance : TopologicalSpace (L ⊗[K] FiniteAdeleRing A K) := sorry
+
+instance : letI := TopologicalSpace.induced (algebraMap K (FiniteAdeleRing A K)) inferInstance
+    IsModuleTopology K (FiniteAdeleRing A K) := sorry
+
 end DedekindDomain

FLT/Mathlib/RingTheory/TensorProduct/Pi.lean

@@ -0,0 +1,8 @@
+import Mathlib.RingTheory.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 [LinearEquiv.symm_apply_eq, algebraMap_eq_smul_one]

FLT/Mathlib/Topology/Algebra/ContinuousAlgEquiv.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,12 @@ def toContinuousAlgHom (e : A ≃A[R] B) : A →A[R] B where
   __ := e.toAlgHom
   cont := e.continuous_toFun
 
+@[coe]
+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
@@ -267,4 +274,14 @@ theorem _root_.AlgEquiv.isUniformEmbedding {E₁ E₂ : Type*} [UniformSpace E
     IsUniformEmbedding e :=
   ContinuousAlgEquiv.isUniformEmbedding { e with continuous_toFun := h₁ }
 
+@[simps!]
+def restrictScalars (A : Type*) {B : Type*} {C D : Type*}
+    [CommSemiring A] [CommSemiring C] [CommSemiring D] [TopologicalSpace C]
+    [TopologicalSpace D] [CommSemiring B]  [Algebra B C] [Algebra B D] [Algebra A B]
+    [Algebra A C] [Algebra A D] [IsScalarTower A B C] [IsScalarTower A B D] (f : C ≃A[B] D) :
+    C ≃A[A] D where
+  __ := f.toAlgEquiv.restrictScalars A
+  continuous_toFun := f.continuous_toFun
+  continuous_invFun := f.continuous_invFun
+
 end ContinuousAlgEquiv

FLT/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

@@ -0,0 +1,19 @@
+import Mathlib.Topology.Algebra.ContinuousMonoidHom
+import Mathlib.Topology.Algebra.Module.Equiv
+import FLT.Mathlib.Topology.Algebra.Module.Equiv
+import FLT.Mathlib.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/Mathlib/Topology/Algebra/Group/Quotient.lean

@@ -0,0 +1,13 @@
+import Mathlib.Topology.Algebra.Group.Quotient
+import Mathlib.Topology.Algebra.ContinuousMonoidHom
+import FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom
+import FLT.Mathlib.Topology.Algebra.Module.Quotient
+import FLT.Mathlib.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/Mathlib/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/Mathlib/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,5 +1,12 @@
 import Mathlib
+import FLT.DedekindDomain.FiniteAdeleRing.BaseChange
 import FLT.Mathlib.NumberTheory.NumberField.Basic
+import FLT.Mathlib.RingTheory.TensorProduct.Pi
+import FLT.Mathlib.Topology.Algebra.Group.Quotient
+import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
+import FLT.NumberField.InfiniteAdeleRing
+
+open scoped TensorProduct
 
 universe u
 
@@ -19,6 +26,159 @@ end LocallyCompact
 
 section BaseChange
 
+-- TODO: Move this stuff
+noncomputable def FiniteDimensional.pi (R M : Type*) [Field R] [AddCommGroup M] [Module R M]
+    [FiniteDimensional R M] :
+    M ≃ₗ[R] Fin (Module.finrank R M) → R :=
+  LinearEquiv.ofFinrankEq _ _ <| by rw [Module.finrank_pi, Fintype.card_fin]
+
+noncomputable def TensorProduct.finiteDimensionalPi (R M N : Type*) [Field R] [AddCommMonoid N]
+    [AddCommGroup M] [Module R N] [Module R M] [FiniteDimensional R M] :
+    M ⊗[R] N ≃ₗ[R] Π (_ : Fin (Module.finrank R M)), N :=
+  (TensorProduct.comm _ _ _).trans <|
+    (TensorProduct.congr (LinearEquiv.refl R N)
+      (FiniteDimensional.pi _ _)).trans
+    (TensorProduct.piScalarRight _ _ _ _)
+
+theorem TensorProduct.finiteDimensionalPi_tsum_left (R M N : Type*) [Field R] [CommSemiring N]
+    [AddCommGroup M] [Algebra R N] [Module R M] [FiniteDimensional R M] (m : M) :
+    finiteDimensionalPi R M N (m ⊗ₜ[R] 1) = fun i => algebraMap _ _ (FiniteDimensional.pi R M m i) := by
+  simp [finiteDimensionalPi, FiniteDimensional.pi, Algebra.algebraMap_eq_smul_one]
+
+theorem Fintype.sum_pi_single_pi {α : Type*} {β : α → Type*} [DecidableEq α] [Fintype α]
+    [(a : α) → AddCommMonoid (β a)] (f : (a : α) → β a) :
+    ∑ (a : α), Pi.single a (f a) = f := by
+  simp_rw [funext_iff, Fintype.sum_apply]
+  exact fun _ => Fintype.sum_pi_single _ _
+
+theorem TensorProduct.finiteDimensionalPi_symm_apply (R M N : Type*) [Field R] [CommSemiring N]
+    [AddCommGroup M] [Algebra R N] [Module R M] [FiniteDimensional R M]
+    (x : Fin (Module.finrank R M) → R) :
+    (finiteDimensionalPi R M N).symm (fun i => algebraMap _ _ (x i)) =
+      (FiniteDimensional.pi R M).symm x ⊗ₜ[R] 1 := by
+  simp only [finiteDimensionalPi, LinearEquiv.trans_symm, LinearEquiv.trans_apply,
+    Algebra.TensorProduct.piScalarRight_symm_apply_of_algebraMap, TensorProduct.congr_symm_tmul,
+    LinearEquiv.refl_symm, LinearEquiv.refl_apply, TensorProduct.comm_symm_tmul,
+    Fintype.sum_pi_single_pi]
+
+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) L) :=
+  Algebra.compHom _ (algebraMap K L)
+
+def instPrincipalTopology : TopologicalSpace K :=
+  TopologicalSpace.induced (algebraMap K (AdeleRing (𝓞 K) K)) inferInstance
+
+attribute [local instance] instPrincipalTopology in
+instance : TopologicalSpace (L ⊗[K] AdeleRing (𝓞 K) K) :=
+  moduleTopology K _
+
+attribute [local instance] instPrincipalTopology in
+instance : IsModuleTopology K (L ⊗[K] AdeleRing (𝓞 K) K) :=
+  ⟨rfl⟩
+
+-- TODO : Is this true?
+attribute [local instance] instPrincipalTopology in
+instance {v : InfinitePlace K} : IsModuleTopology K (v.Completion) := sorry
+
+attribute [local instance] instPrincipalTopology in
+instance : IsModuleTopology K (InfiniteAdeleRing K) := IsModuleTopology.instPi
+
+attribute [local instance] instPrincipalTopology in
+instance : IsModuleTopology K (DedekindDomain.FiniteAdeleRing (𝓞 K) K) := sorry
+
+attribute [local instance] instPrincipalTopology in
+instance : IsModuleTopology K (AdeleRing (𝓞 K) K) :=
+  IsModuleTopology.instProd
+
+attribute [local instance] instPrincipalTopology in
+instance : IsModuleTopology K (Fin (Module.finrank K L) → AdeleRing (𝓞 K) K) :=
+  IsModuleTopology.instPi
+
+attribute [local instance] instPrincipalTopology in
+noncomputable def tensorProductContinuousLinearEquivPi :
+    L ⊗[K] AdeleRing (𝓞 K) K ≃L[K] (Fin (Module.finrank K L) → AdeleRing (𝓞 K) K) where
+  toLinearEquiv := TensorProduct.finiteDimensionalPi K L (AdeleRing (𝓞 K) K)
+  continuous_toFun := IsModuleTopology.continuous_of_linearMap _
+  continuous_invFun := by
+    convert ModuleTopology.eq_coinduced_of_surjective
+      (TensorProduct.finiteDimensionalPi K L (AdeleRing (𝓞 K) K)).symm.surjective ▸
+        continuous_coinduced_rng
+
+variable {K L}
+
+-- Probably can remove this
+theorem tensorProductContinuousLinearEquivPi_symm_apply_of_algebraMap
+    (x : Fin (Module.finrank K L) → K) :
+    (tensorProductContinuousLinearEquivPi K L).symm (fun i => algebraMap _ _ (x i)) =
+      ((FiniteDimensional.pi _ _).symm x) ⊗ₜ[K] 1 := by
+  exact TensorProduct.finiteDimensionalPi_symm_apply K L _ x
+
+variable (K L)
+
+def baseChange : L ⊗[K] AdeleRing (𝓞 K) K ≃A[L] AdeleRing (𝓞 L) L := sorry
+
+variable {L}
+
+theorem baseChange_tsum_apply_right (l : L) :
+  baseChange K L (l ⊗ₜ[K] 1) = algebraMap L (AdeleRing (𝓞 L) L) l := sorry
+
+variable (L)
+
+instance : IsScalarTower K L (AdeleRing (𝓞 L) L) :=
+  IsScalarTower.of_algebraMap_eq' rfl
+
+noncomputable def baseChangePi :
+    (Fin (Module.finrank K L) → AdeleRing (𝓞 K) K) ≃L[K] AdeleRing (𝓞 L) L :=
+  (tensorProductContinuousLinearEquivPi K L).symm.trans
+    ((baseChange K L).restrictScalars K).toContinuousLinearEquiv
+
+variable {K L}
+
+theorem baseChangePi_apply (x : Fin (Module.finrank K L) → AdeleRing (𝓞 K) 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) K}
+    {y : Fin (Module.finrank K L) → K}
+    (h : ∀ i, algebraMap K (AdeleRing (𝓞 K) K) (y i) = x i) :
+    baseChangePi K L x = algebraMap L _ ((FiniteDimensional.pi _ _).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) K}
+    (h : x ∈ AddSubgroup.pi Set.univ (fun _ => principalSubgroup (𝓞 K) K)) :
+    baseChangePi K L x ∈ principalSubgroup (𝓞 L) 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 ▸ ⟨(FiniteDimensional.pi _ _).symm y, rfl⟩
+
+variable (K L)
+
+theorem baseChangePi_map_principalSubgroup :
+    (AddSubgroup.pi Set.univ (fun (_ : Fin (Module.finrank K L)) => principalSubgroup (𝓞 K) K)).map
+      (baseChangePi K L).toAddMonoidHom = principalSubgroup (𝓞 L) 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) K) (FiniteDimensional.pi _ _ a i)
+  refine ⟨fun i _ => ⟨FiniteDimensional.pi _ _ a i, rfl⟩, ?_⟩
+  rw [baseChangePi_apply_eq_algebraMap_comp (fun i => rfl), LinearEquiv.symm_apply_apply]
+
+noncomputable def baseChangeQuotientPi :
+    (Fin (Module.finrank K L) → AdeleRing (𝓞 K) K ⧸ principalSubgroup (𝓞 K) K) ≃ₜ+
+      AdeleRing (𝓞 L) L ⧸ principalSubgroup (𝓞 L) L :=
+  (ContinuousAddEquiv.quotientPi _).symm.trans <|
+    QuotientAddGroup.continuousAddEquiv _ _ _ _ (baseChangePi K L).toContinuousAddEquiv
+      (baseChangePi_map_principalSubgroup K L)
+
+end NumberField.AdeleRing
+
 end BaseChange
 
 section Discrete
@@ -102,7 +262,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) K),
@@ -115,13 +274,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) K ⧸ AddMonoidHom.range (algebraMap K (AdeleRing (𝓞 K) K)).toAddMonoidHom) :=
-  sorry -- issue #259
+    CompactSpace (AdeleRing (𝓞 K) K ⧸ AdeleRing.principalSubgroup (𝓞 K) K) :=
+  letI := Rat.AdeleRing.cocompact
+  (baseChangeQuotientPi ℚ K).compactSpace
 
 end Compact

FLT/NumberField/InfiniteAdeleRing.lean

@@ -1,9 +1,12 @@
 import Mathlib
+import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
 
 variable (K L : Type*) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L]
 
 open NumberField
 
+open scoped Classical
+
 variable [Algebra K (InfiniteAdeleRing L)] [IsScalarTower K L (InfiniteAdeleRing L)]
 
 -- https://leanprover.zulipchat.com/#narrow/channel/416277-FLT/topic/Functoriality.20of.20infinite.20completion.20for.20number.20fields/near/492313867
@@ -14,9 +17,19 @@ noncomputable def NumberField.InfiniteAdeleRing.baseChange :
 
 open scoped TensorProduct
 
+attribute [local instance] Algebra.TensorProduct.rightAlgebra in
+instance {v : InfinitePlace K} : TopologicalSpace (L ⊗[K] v.Completion) :=
+  moduleTopology v.Completion _
+
+attribute [local instance] Algebra.TensorProduct.rightAlgebra in
+instance {v : InfinitePlace K} : IsModuleTopology v.Completion (L ⊗[K] v.Completion) := ⟨rfl⟩
+
+instance : TopologicalSpace (L ⊗[K] InfiniteAdeleRing K) :=
+  TopologicalSpace.induced (TensorProduct.piRight _ L _ _) inferInstance
+
 -- TODO should be ≃A[L]
 /-- The canonical `L`-algebra isomorphism from `L ⊗_K K_∞` to `L_∞` induced by the
 `K`-algebra base change map `K_∞ → L_∞`. -/
 def NumberField.InfiniteAdeleRing.baseChangeIso :
-    (L ⊗[K] (InfiniteAdeleRing K)) ≃ₐ[L] InfiniteAdeleRing L :=
+    L ⊗[K] InfiniteAdeleRing K ≃A[L] InfiniteAdeleRing L :=
   sorry