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

* Add ContinuousAlgEquiv

* Issue #259: Proof that A_K/K is compact, assuming that A_Q/Q is compact

* Issue #259: Proof that A_K/K is compact, assuming that A_Q/Q is compact

* Add TODOs

* Remove use of basis and try module topology

* Some work on module topology

* close goals

* Remove unncessary defs

* Refactor

* Remove unnecessary result

* Tidy

* Remove unnecessary results

FLT/Mathlib/Algebra/Algebra/Tower.lean

@@ -0,0 +1,11 @@
+import Mathlib.Algebra.Algebra.Tower
+import Mathlib.RingTheory.AlgebraTower
+
+def AlgEquiv.extendScalars {A C D : Type*} (B : Type*) [CommSemiring A] [CommSemiring C]
+    [CommSemiring D] [Algebra A C] [Algebra A D] [CommSemiring B] [Algebra A B] [Algebra B C]
+    [IsScalarTower A B C] (f : C ≃ₐ[A] D) :
+    letI := (f.toAlgHom.restrictDomain B).toRingHom.toAlgebra
+    C ≃ₐ[B] D where
+  __ := (f.toAlgHom.restrictDomain B).toRingHom.toAlgebra
+  __ := f
+  commutes' := fun _ => rfl

FLT/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -0,0 +1,8 @@
+import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+import Mathlib.Algebra.BigOperators.Pi
+
+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 _ _

FLT/Mathlib/LinearAlgebra/Dimension/Constructions.lean

@@ -0,0 +1,26 @@
+import Mathlib.LinearAlgebra.Dimension.Constructions
+import Mathlib.LinearAlgebra.TensorProduct.Pi
+import FLT.Mathlib.Algebra.BigOperators.Group.Finset.Basic
+import FLT.Mathlib.RingTheory.TensorProduct.Pi
+
+open scoped TensorProduct
+
+noncomputable def Module.Finite.equivPi (R M : Type*) [Ring R] [StrongRankCondition R]
+    [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] :
+    M ≃ₗ[R] Fin (Module.finrank R M) → R :=
+  LinearEquiv.ofFinrankEq _ _ <| by rw [Module.finrank_pi, Fintype.card_fin]
+
+noncomputable abbrev TensorProduct.AlgebraTensorModule.finiteEquivPi (R M N : Type*) [CommRing R]
+    [CommSemiring N] [CommRing M] [Algebra R N] [Module R M] [Module.Free R M] [Module.Finite R M]
+    [StrongRankCondition R] :
+    N ⊗[R] M ≃ₗ[N] Fin (Module.finrank R M) → N :=
+  (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.refl N N) (Module.Finite.equivPi _ _)).trans
+    (TensorProduct.piScalarRight _ _ _ _)
+
+theorem TensorProduct.AlgebraTensorModule.finiteEquivPi_symm_apply (R M N : Type*) [Field R]
+    [CommSemiring N] [CommRing M] [Algebra R N] [Module R M] [Module.Free R M] [Module.Finite R M]
+    [StrongRankCondition R]
+    (x : Fin (Module.finrank R M) → R) :
+    (finiteEquivPi R M N).symm (fun i => algebraMap R N (x i)) =
+      1 ⊗ₜ[R] (Module.Finite.equivPi R M).symm x := by
+  simp [Algebra.TensorProduct.piScalarRight_symm_apply_of_algebraMap, Fintype.sum_pi_single_pi]

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

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2024 Salvatore Mercuri. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Salvatore Mercuri
+-/
+import Mathlib.Topology.Algebra.Algebra.Equiv
+import Mathlib.Topology.Algebra.Algebra
+import Mathlib.Topology.Algebra.Module.Equiv
+
+/-!
+# Topological (sub)algebras
+
+This file contains an API for `ContinuousAlgEquiv`.
+-/
+
+open scoped Topology
+
+
+namespace ContinuousAlgEquiv
+
+variable {R A B C : Type*}
+  [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B]
+  [TopologicalSpace B] [Semiring C] [TopologicalSpace C] [Algebra R A] [Algebra R B]
+  [Algebra R C]
+
+@[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
+
+theorem toContinuousLinearEquiv_apply (e : A ≃A[R] B) (a : A) :
+  e.toContinuousLinearEquiv a = e a := rfl
+
+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,21 @@
+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
+
+@[simps!]
+def ContinuousLinearEquiv.restrictScalars (R : Type*) {S M M₂ : Type*}
+    [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂]
+    [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] [TopologicalSpace M]
+    [TopologicalSpace M₂] (f : M ≃L[S] M₂) :
+    M ≃L[R] M₂ where
+  __ := f.toLinearEquiv.restrictScalars R
+  continuous_toFun := f.continuous_toFun
+  continuous_invFun := f.continuous_invFun

FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean

@@ -240,3 +240,16 @@ topology is the ℤhat topology and this should be fine, it's finite and free
 over a complete thing so I don't think there can be any other possibility
 (the argument is weak here)
 -/
+
+def continuousLinearEquiv {A B R : Type*} [TopologicalSpace A]
+    [TopologicalSpace B] [TopologicalSpace R] [Semiring R] [AddCommMonoid A] [AddCommMonoid B]
+    [Module R A] [Module R B] [IsModuleTopology R A] [IsModuleTopology R B]
+    (e : A ≃ₗ[R] B) :
+    A ≃L[R] B where
+  __ := e
+  continuous_toFun :=
+    letI := IsModuleTopology.toContinuousAdd
+    IsModuleTopology.continuous_of_linearMap e.toLinearMap
+  continuous_invFun :=
+    letI := IsModuleTopology.toContinuousAdd
+    IsModuleTopology.continuous_of_linearMap e.symm.toLinearMap

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

@@ -0,0 +1,32 @@
+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 [quotientPi, piQuotientLift]
+    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,15 @@
 import Mathlib
+import FLT.DedekindDomain.FiniteAdeleRing.BaseChange
+import FLT.Mathlib.Algebra.Algebra.Tower
+import FLT.Mathlib.LinearAlgebra.Dimension.Constructions
 import FLT.Mathlib.NumberTheory.NumberField.Basic
+import FLT.Mathlib.RingTheory.TensorProduct.Pi
+import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
+import FLT.Mathlib.Topology.Algebra.Group.Quotient
+import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
+import FLT.NumberField.InfiniteAdeleRing
+
+open scoped TensorProduct
 
 universe u
 
@@ -98,54 +108,142 @@ 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),
     IsOpen U ∧ (algebraMap K (AdeleRing (𝓞 K) K)) ⁻¹' U = {k} := sorry -- issue #257
 
 end Discrete
 
-section Compact
-
-open NumberField
-
-theorem Rat.AdeleRing.cocompact :
-    CompactSpace (AdeleRing (𝓞 ℚ) ℚ ⧸ AddMonoidHom.range (algebraMap ℚ (AdeleRing (𝓞 ℚ) ℚ)).toAddMonoidHom) :=
-  sorry -- issue #258
-
-variable (K : Type*) [Field K] [NumberField K]
-
-theorem NumberField.AdeleRing.cocompact :
-    CompactSpace (AdeleRing (𝓞 K) K ⧸ AddMonoidHom.range (algebraMap K (AdeleRing (𝓞 K) K)).toAddMonoidHom) :=
-  sorry -- issue #259
-
-end Compact
-
 section BaseChange
 
+namespace NumberField.AdeleRing
+
 variable (K L : Type*) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L]
 
-open NumberField
+scoped notation:100 "𝔸" K => AdeleRing (𝓞 K) K
+
+noncomputable instance : Algebra K (𝔸 L) :=
+  Algebra.compHom _ (algebraMap K L)
 
-variable [Algebra K (AdeleRing (𝓞 L) L)] [IsScalarTower K L (AdeleRing (𝓞 L) L)]
+instance : IsScalarTower K L (𝔸 L) :=
+  IsScalarTower.of_algebraMap_eq' rfl
 
 /-- The canonical map from the adeles of K to the adeles of L -/
-noncomputable def NumberField.AdeleRing.baseChange :
-    AdeleRing (𝓞 K) K →A[K] AdeleRing (𝓞 L) L :=
+noncomputable def baseChange :
+    (𝔸 K) →A[K] 𝔸 L :=
   sorry -- product of finite and infinite adele maps
 
 open scoped TensorProduct
 
-noncomputable instance : Algebra (AdeleRing (𝓞 K) K) (L ⊗[K] AdeleRing (𝓞 K) K) :=
+noncomputable instance : Algebra (𝔸  K) (L ⊗[K] 𝔸 K) :=
   Algebra.TensorProduct.rightAlgebra
 
-instance : TopologicalSpace (L ⊗[K] AdeleRing (𝓞 K) K) :=
-  moduleTopology (AdeleRing (𝓞 K) K) (L ⊗[K] AdeleRing (𝓞 K) K)
-/-- The canonical `L`-algebra isomorphism from `L ⊗_K K_∞` to `L_∞` induced by the
-`K`-algebra base change map `K_∞ → L_∞`. -/
-def NumberField.AdeleRing.baseChangeEquiv :
-    (L ⊗[K] (AdeleRing (𝓞 K) K)) ≃A[L] AdeleRing (𝓞 L) L :=
+instance : TopologicalSpace (L ⊗[K] 𝔸 K) :=
+  moduleTopology (𝔸 K) (L ⊗[K] 𝔸 K)
+
+instance : IsModuleTopology (𝔸 K) (L ⊗[K] 𝔸 K) := ⟨rfl⟩
+
+instance instPiIsModuleTopology : IsModuleTopology (𝔸 K) (Fin (Module.finrank K L) → 𝔸 K) :=
+  IsModuleTopology.instPi
+
+open DedekindDomain in
+/-- The canonical `L`-algebra isomorphism from `L ⊗_K 𝔸_K` to `𝔸_L` induced by the
+`K`-algebra base change map `𝔸_K → 𝔸_L`. -/
+def baseChangeEquiv :
+    (L ⊗[K] 𝔸 K) ≃A[L] 𝔸 L :=
+  sorry
+
+variable {L}
+
+theorem baseChangeEquiv_tsum_apply_right (l : L) :
+    baseChangeEquiv K L (l ⊗ₜ[K] 1) = algebraMap L (𝔸 L) l :=
   sorry
 
+variable (L)
+
+open TensorProduct.AlgebraTensorModule in
+noncomputable abbrev tensorProductEquivPi :
+    L ⊗[K] (𝔸 K) ≃L[K] (Fin (Module.finrank K L) → 𝔸 K) :=
+  letI := instPiIsModuleTopology K L
+  -- `𝔸 K ⊗[K] L ≃ₗ[𝔸 K] L ⊗[K] 𝔸 K`
+  -- Note: needs to be this order to avoid instance clash with inferred leftAlgebra
+  let comm := (Algebra.TensorProduct.comm K (𝔸 K) L).extendScalars (𝔸 K) |>.toLinearEquiv
+  -- `𝔸 K ⊗[K] L ≃ₗ[𝔸 K] ⊕ 𝔸 K`
+  let π := finiteEquivPi K L (𝔸 K)
+  -- Stitch together to get `L ⊗[K] 𝔸 K ≃ₗ[𝔸 K] ⊕ 𝔸 K`, which is automatically
+  -- continuous due to `𝔸 K` module topologies on both sides, then restrict scalars to `K`
+  IsModuleTopology.continuousLinearEquiv (comm.symm.trans π) |>.restrictScalars K
+
+noncomputable abbrev piEquiv :
+    (Fin (Module.finrank K L) → 𝔸 K) ≃L[K] 𝔸 L :=
+  -- `⊕ 𝔸 K ≃L[K] L ⊗[K] 𝔸 K` from previous def
+  let π := (tensorProductEquivPi K L).symm
+  -- `L ⊗[K] 𝔸 K ≃L[K] 𝔸 L` base change  restricted to `K` as a continuous linear equiv
+  let BC := baseChangeEquiv K L |>.toContinuousLinearEquiv |>.restrictScalars K
+  π.trans BC
+
+variable {K L}
+
+open TensorProduct.AlgebraTensorModule in
+theorem piEquiv_apply_of_algebraMap
+    {x : Fin (Module.finrank K L) → 𝔸 K}
+    {y : Fin (Module.finrank K L) → K}
+    (h : ∀ i, algebraMap K (𝔸 K) (y i) = x i) :
+    piEquiv K L x = algebraMap L _ (Module.Finite.equivPi _ _ |>.symm y) := by
+  simp [← funext h]
+  simp only [IsModuleTopology.continuousLinearEquiv]
+  rw [LinearEquiv.trans_symm, LinearEquiv.trans_apply, finiteEquivPi_symm_apply]
+  simp [AlgEquiv.extendScalars, ContinuousAlgEquiv.toContinuousLinearEquiv_apply,
+    baseChangeEquiv_tsum_apply_right]
+
+theorem piEquiv_mem_principalSubgroup
+    {x : Fin (Module.finrank K L) → 𝔸 K}
+    (h : x ∈ AddSubgroup.pi Set.univ (fun _ => principalSubgroup (𝓞 K) K)) :
+    piEquiv 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 piEquiv_apply_of_algebraMap hy ▸ ⟨Module.Finite.equivPi _ _ |>.symm y, rfl⟩
+
+variable (K L)
+
+theorem piEquiv_map_principalSubgroup :
+    (AddSubgroup.pi Set.univ (fun (_ : Fin (Module.finrank K L)) => principalSubgroup (𝓞 K) K)).map
+      (piEquiv 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 ▸ piEquiv_mem_principalSubgroup h, ?_⟩
+  rintro ⟨a, rfl⟩
+  use fun i => algebraMap K (𝔸 K) (Module.Finite.equivPi _ _ a i)
+  refine ⟨fun i _ => ⟨Module.Finite.equivPi _ _ a i, rfl⟩, ?_⟩
+  rw [piEquiv_apply_of_algebraMap (fun i => rfl), LinearEquiv.symm_apply_apply]
+
+noncomputable def piQuotientEquiv :
+    (Fin (Module.finrank K L) → (𝔸 K) ⧸ principalSubgroup (𝓞 K) K) ≃ₜ+
+      (𝔸 L) ⧸ principalSubgroup (𝓞 L) L :=
+  -- The map `⊕ 𝔸 K ≃L[K] 𝔸 L` reduces to quotients `⊕ 𝔸 K / K ≃ₜ+ 𝔸 L / L`
+  (ContinuousAddEquiv.quotientPi _).symm.trans <|
+    QuotientAddGroup.continuousAddEquiv _ _ _ _ (piEquiv K L).toContinuousAddEquiv
+      (piEquiv_map_principalSubgroup K L)
+
+end NumberField.AdeleRing
+
 end BaseChange
+
+section Compact
+
+open NumberField
+
+theorem Rat.AdeleRing.cocompact :
+    CompactSpace (AdeleRing (𝓞 ℚ) ℚ ⧸ AdeleRing.principalSubgroup (𝓞 ℚ) ℚ) :=
+  sorry -- issue #258
+
+variable (K L : Type*) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
+
+theorem NumberField.AdeleRing.cocompact :
+    CompactSpace (AdeleRing (𝓞 K) K ⧸ principalSubgroup (𝓞 K) K) :=
+  letI := Rat.AdeleRing.cocompact
+  (piQuotientEquiv ℚ K).compactSpace
+
+end Compact