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

…g that A_Q/Q is compact
smmercuri · Jan 11, 2025 · d3327d5 · d3327d5
1 parent 32818b3
commit d3327d5
Show file tree

Hide file tree

Showing 9 changed files with 18 additions and 286 deletions.
diff --git a/FLT/ForMathlib/Topology/Algebra/Algebra.lean b/FLT/ForMathlib/Topology/Algebra/Algebra.lean
diff --git a/...thlib/LinearAlgebra/TensorProduct/Pi.lean → ...thlib/LinearAlgebra/TensorProduct/Pi.lean b/...thlib/LinearAlgebra/TensorProduct/Pi.lean → ...thlib/LinearAlgebra/TensorProduct/Pi.lean
diff --git a/...rMathlib/RingTheory/TensorProduct/Pi.lean → FLT/Mathlib/RingTheory/TensorProduct/Pi.lean b/...rMathlib/RingTheory/TensorProduct/Pi.lean → FLT/Mathlib/RingTheory/TensorProduct/Pi.lean
@@ -1,5 +1,5 @@
 import Mathlib.RingTheory.TensorProduct.Pi
-import FLT.ForMathlib.LinearAlgebra.TensorProduct.Pi
+import FLT.Mathlib.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]

diff --git a/FLT/Mathlib/Topology/Algebra/ContinuousAlgEquiv.lean b/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

diff --git a/...Topology/Algebra/ContinuousMonoidHom.lean → ...Topology/Algebra/ContinuousMonoidHom.lean b/...Topology/Algebra/ContinuousMonoidHom.lean → ...Topology/Algebra/ContinuousMonoidHom.lean
@@ -1,7 +1,7 @@
 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
+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₂) :

diff --git a/...hlib/Topology/Algebra/Group/Quotient.lean → ...hlib/Topology/Algebra/Group/Quotient.lean b/...hlib/Topology/Algebra/Group/Quotient.lean → ...hlib/Topology/Algebra/Group/Quotient.lean
@@ -1,8 +1,8 @@
 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
+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]

diff --git a/...athlib/Topology/Algebra/Module/Equiv.lean → ...athlib/Topology/Algebra/Module/Equiv.lean b/...athlib/Topology/Algebra/Module/Equiv.lean → ...athlib/Topology/Algebra/Module/Equiv.lean
diff --git a/...lib/Topology/Algebra/Module/Quotient.lean → ...lib/Topology/Algebra/Module/Quotient.lean b/...lib/Topology/Algebra/Module/Quotient.lean → ...lib/Topology/Algebra/Module/Quotient.lean
diff --git a/FLT/NumberField/AdeleRing.lean b/FLT/NumberField/AdeleRing.lean
@@ -1,7 +1,7 @@
 import Mathlib
-import FLT.ForMathlib.RingTheory.TensorProduct.Pi
-import FLT.ForMathlib.Topology.Algebra.Group.Quotient
-import FLT.ForMathlib.Topology.Algebra.Algebra
+import FLT.Mathlib.RingTheory.TensorProduct.Pi
+import FLT.Mathlib.Topology.Algebra.Group.Quotient
+import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
 
 open scoped TensorProduct
 
@@ -148,7 +148,8 @@ theorem baseChangePi_map_principalSubgroup :
   rfl
 
 noncomputable def baseChangeQuotientPi :
-    (Fin (Module.finrank K L) → AdeleRing K ⧸ principalSubgroup K) ≃ₜ+ AdeleRing L ⧸ principalSubgroup L :=
+    (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)