From 79a4c47a94219be12ee4481da941f980f807def7 Mon Sep 17 00:00:00 2001 From: Salvatore Mercuri Date: Mon, 2 Dec 2024 16:15:50 +0000 Subject: [PATCH 1/3] Add ContinuousAlgEquiv --- FLT/ForMathlib/Topology/Algebra/Algebra.lean | 270 +++++++++++++++++++ 1 file changed, 270 insertions(+) create mode 100644 FLT/ForMathlib/Topology/Algebra/Algebra.lean diff --git a/FLT/ForMathlib/Topology/Algebra/Algebra.lean b/FLT/ForMathlib/Topology/Algebra/Algebra.lean new file mode 100644 index 00000000..26f61d8f --- /dev/null +++ b/FLT/ForMathlib/Topology/Algebra/Algebra.lean @@ -0,0 +1,270 @@ +/- +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 + +/-! +# Topological (sub)algebras + +This file contains an API for `ContinuousAlgEquiv`. +-/ + +open scoped Topology + +structure ContinuousAlgEquiv (R A B : Type*) [CommSemiring R] + [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] + [Algebra R B] extends A ≃ₐ[R] B where + continuous_toFun : Continuous toFun := by continuity + continuous_invFun : Continuous invFun := by continuity + +notation:50 A " ≃A[" R "]" B => ContinuousAlgEquiv R A B + +class ContinuousAlgEquivClass (F : Type*) (R A B : outParam Type*) [CommSemiring R] + [Semiring A][TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] + [Algebra R B] [EquivLike F A B] extends AlgEquivClass F R A B : Prop where + map_continuous : ∀ (f : F), Continuous f + inv_continuous : ∀ (f : F), Continuous (EquivLike.inv f) + +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 toContinuousAlgHom (e : A ≃A[R] B) : A →A[R] B where + __ := e.toAlgHom + cont := e.continuous_toFun + +instance coe : Coe (A ≃A[R] B) (A →A[R] B) := ⟨toContinuousAlgHom⟩ + +instance equivLike : EquivLike (A ≃A[R] B) A B where + coe f := f.toFun + inv f := f.invFun + coe_injective' f g h₁ h₂ := by + cases' f with f' _ + cases' g with g' _ + rcases f' with ⟨⟨_, _⟩, _⟩ + rcases g' with ⟨⟨_, _⟩, _⟩ + congr + left_inv f := f.left_inv + right_inv f := f.right_inv + +instance continuousAlgEquivClass : ContinuousAlgEquivClass (A ≃A[R] B) R A B where + map_add f := f.map_add' + map_mul f := f.map_mul' + commutes f := f.commutes' + map_continuous := continuous_toFun + inv_continuous := continuous_invFun + +theorem coe_apply (e : A ≃A[R] B) (a : A) : (e : A →A[R] B) a = e a := rfl + +@[simp] +theorem coe_coe (e : A ≃A[R] B) : ⇑(e : A →A[R] B) = e := rfl + +theorem toAlgEquiv_injective : Function.Injective (toAlgEquiv : (A ≃A[R] B) → A ≃ₐ[R] B) := by + rintro ⟨e, _, _⟩ ⟨e', _, _⟩ rfl + rfl + +@[ext] +theorem ext {f g : A ≃A[R] B} (h : ⇑f = ⇑g) : f = g := + toAlgEquiv_injective <| AlgEquiv.ext <| congr_fun h + +theorem coe_injective : Function.Injective ((↑) : (A ≃A[R] B) → A →A[R] B) := + fun _ _ h => ext <| funext <| ContinuousAlgHom.ext_iff.1 h + +@[simp] +theorem coe_inj {f g : A ≃A[R] B} : (f : A →A[R] B) = g ↔ f = g := + coe_injective.eq_iff + +def toHomeomorph (e : A ≃A[R] B) : A ≃ₜ B where + __ := e + toEquiv := e.toAlgEquiv.toEquiv + +@[simp] +theorem coe_toHomeomorph (e : A ≃A[R] B) : ⇑e.toHomeomorph = e := rfl + +theorem isOpenMap (e : A ≃A[R] B) : IsOpenMap e := + e.toHomeomorph.isOpenMap + +theorem image_closure (e : A ≃A[R] B) (S : Set A) : e '' closure S = closure (e '' S) := + e.toHomeomorph.image_closure S + +theorem preimage_closure (e : A ≃A[R] B) (S : Set B) : e ⁻¹' closure S = closure (e ⁻¹' S) := + e.toHomeomorph.preimage_closure S + +@[simp] +theorem isClosed_image (e : A ≃A[R] B) {S : Set A} : IsClosed (e '' S) ↔ IsClosed S := + e.toHomeomorph.isClosed_image + +theorem map_nhds_eq (e : A ≃A[R] B) (a : A) : Filter.map e (𝓝 a) = 𝓝 (e a) := + e.toHomeomorph.map_nhds_eq a + +theorem map_zero (e : A ≃A[R] B) : e (0 : A) = 0 := + e.toAlgHom.map_zero' + +theorem map_add (e : A ≃A[R] B) (a₁ a₂ : A) : e (a₁ + a₂) = e a₁ + e a₂ := + e.toAlgHom.map_add' a₁ a₂ + +theorem map_smul (e : A ≃A[R] B) (r : R) (a : A) : e (r • a) = r • e a := + _root_.map_smul e r a + +theorem map_eq_zero_iff (e : A ≃A[R] B) {a : A} : e a = 0 ↔ a = 0 := + e.toAlgEquiv.toLinearEquiv.map_eq_zero_iff + +attribute [continuity] + ContinuousAlgEquiv.continuous_invFun ContinuousAlgEquiv.continuous_toFun + +theorem continuous (e : A ≃A[R] B) : Continuous e := e.continuous_toFun + +theorem continuousOn (e : A ≃A[R] B) {S : Set A} : ContinuousOn e S := + e.continuous.continuousOn + +theorem continuousAt (e : A ≃A[R] B) {a : A} : ContinuousAt e a := + e.continuous.continuousAt + +theorem continuousWithinAt (e : A ≃A[R] B) {S : Set A} {a : A} : + ContinuousWithinAt e S a := + e.continuous.continuousWithinAt + +theorem comp_continuous_iff {α : Type*} [TopologicalSpace α] (e : A ≃A[R] B) {f : α → A} : + Continuous (e ∘ f) ↔ Continuous f := + e.toHomeomorph.comp_continuous_iff + +variable (R A) + +@[refl] +def refl : A ≃A[R] A where + __ := AlgEquiv.refl + continuous_toFun := continuous_id + continuous_invFun := continuous_id + +@[simp] +theorem refl_apply (a : A) : refl R A a = a := rfl + +@[simp] +theorem coe_refl : refl R A = ContinuousAlgHom.id R A := rfl + +@[simp] +theorem coe_refl' : ⇑(refl R A) = id := rfl + +variable {R A} +@[symm] +def symm (e : A ≃A[R] B) : B ≃A[R] A where + __ := e.toAlgEquiv.symm + continuous_toFun := e.continuous_invFun + continuous_invFun := e.continuous_toFun + +@[simp] +theorem apply_symm_apply (e : A ≃A[R] B) (b : B) : e (e.symm b) = b := + e.1.right_inv b + +@[simp] +theorem symm_apply_apply (e : A ≃A[R] B) (a : A) : e.symm (e a) = a := + e.1.left_inv a + +@[simp] +theorem symm_image_image (e : A ≃A[R] B) (S : Set A) : e.symm '' (e '' S) = S := + e.toEquiv.symm_image_image S + +@[simp] +theorem image_symm_image (e : A ≃A[R] B) (S : Set B) : e '' (e.symm '' S) = S := + e.symm.symm_image_image S + +@[simp] +theorem symm_toAlgEquiv (e : A ≃A[R] B) : e.symm.toAlgEquiv = e.toAlgEquiv.symm := rfl + +@[simp] +theorem symm_toHomeomorph (e : A ≃A[R] B) : e.symm.toHomeomorph = e.toHomeomorph.symm := rfl + +theorem symm_map_nhds_eq (e : A ≃A[R] B) (a : A) : Filter.map e.symm (𝓝 (e a)) = 𝓝 a := + e.toHomeomorph.symm_map_nhds_eq a + +@[trans] +def trans (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) : A ≃A[R] C where + __ := e₁.toAlgEquiv.trans e₂.toAlgEquiv + continuous_toFun := e₂.continuous_toFun.comp e₁.continuous_toFun + continuous_invFun := e₁.continuous_invFun.comp e₂.continuous_invFun + +@[simp] +theorem trans_toAlgEquiv (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) : + (e₁.trans e₂).toAlgEquiv = e₁.toAlgEquiv.trans e₂.toAlgEquiv := + rfl + +@[simp] +theorem trans_apply (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) (a : A) : + (e₁.trans e₂) a = e₂ (e₁ a) := + rfl + +@[simp] +theorem symm_trans_apply (e₁ : B ≃A[R] A) (e₂ : C ≃A[R] B) (a : A) : + (e₂.trans e₁).symm a = e₂.symm (e₁.symm a) := + rfl + +@[simp] +theorem comp_coe (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) : + e₂.toAlgHom.comp e₁.toAlgHom = e₁.trans e₂ := + rfl + +@[simp high] +theorem coe_comp_coe_symm (e : A ≃A[R] B) : + e.toContinuousAlgHom.comp e.symm = ContinuousAlgHom.id R B := + ContinuousAlgHom.ext e.apply_symm_apply + +@[simp high] +theorem coe_symm_comp_coe (e : A ≃A[R] B) : + e.symm.toContinuousAlgHom.comp e = ContinuousAlgHom.id R A := + ContinuousAlgHom.ext e.symm_apply_apply + +@[simp] +theorem symm_comp_self (e : A ≃A[R] B) : e.symm.toFun ∘ e.toFun = id := + funext <| e.symm_apply_apply + +@[simp] +theorem self_comp_symm (e : A ≃A[R] B) : e.toFun ∘ e.symm.toFun = id := + funext <| e.apply_symm_apply + +@[simp] +theorem symm_symm (e : A ≃A[R] B) : e.symm.symm = e := rfl + +@[simp] +theorem refl_symm : (refl R A).symm = refl R A := rfl + +theorem symm_symm_apply (e : A ≃A[R] B) (a : A) : e.symm.symm a = e a := rfl + +theorem symm_apply_eq (e : A ≃A[R] B) {a : A} {b : B} : e.symm b = a ↔ b = e a := + e.toEquiv.symm_apply_eq + +theorem eq_symm_apply (e : A ≃A[R] B) {a : A} {b : B} : a = e.symm b ↔ e a = b := + e.toEquiv.eq_symm_apply + +theorem image_eq_preimage (e : A ≃A[R] B) (S : Set A) : e '' S = e.symm ⁻¹' S := + e.toEquiv.image_eq_preimage S + +theorem image_symm_eq_preimage (e : A ≃A[R] B) (S : Set B) : e.symm '' S = e ⁻¹' S := by + rw [e.symm.image_eq_preimage, e.symm_symm] + +@[simp] +theorem symm_preimage_preimage (e : A ≃A[R] B) (S : Set B) : e.symm ⁻¹' (e ⁻¹' S) = S := + e.toEquiv.symm_preimage_preimage S + +@[simp] +theorem preimage_symm_preimage (e : A ≃A[R] B) (S : Set A) : e ⁻¹' (e.symm ⁻¹' S) = S := + e.symm.symm_preimage_preimage S + +theorem isUniformEmbedding {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂] [Ring E₁] + [UniformAddGroup E₁] [Algebra R E₁] [Ring E₂] [UniformAddGroup E₂] [Algebra R E₂] + (e : E₁ ≃A[R] E₂) : IsUniformEmbedding e := + e.toAlgEquiv.isUniformEmbedding e.toContinuousAlgHom.uniformContinuous + e.symm.toContinuousAlgHom.uniformContinuous + +theorem _root_.AlgEquiv.isUniformEmbedding {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂] + [Ring E₁] [UniformAddGroup E₁] [Algebra R E₁] [Ring E₂] [UniformAddGroup E₂] [Algebra R E₂] + (e : E₁ ≃ₐ[R] E₂) (h₁ : Continuous e) (h₂ : Continuous e.symm) : + IsUniformEmbedding e := + ContinuousAlgEquiv.isUniformEmbedding { e with continuous_toFun := h₁ } + +end ContinuousAlgEquiv From 32818b3dd92d035bb3b2e2eb3c02ea84ef214266 Mon Sep 17 00:00:00 2001 From: Salvatore Mercuri Date: Sat, 11 Jan 2025 15:01:26 +0000 Subject: [PATCH 2/3] Issue #259: Proof that A_K/K is compact, assuming that A_Q/Q is compact --- .../LinearAlgebra/TensorProduct/Pi.lean | 10 ++ .../RingTheory/TensorProduct/Pi.lean | 12 ++ FLT/ForMathlib/Topology/Algebra/Algebra.lean | 6 + .../Topology/Algebra/ContinuousMonoidHom.lean | 19 +++ .../Topology/Algebra/Group/Quotient.lean | 13 ++ .../Topology/Algebra/Module/Equiv.lean | 11 ++ .../Topology/Algebra/Module/Quotient.lean | 34 ++++ FLT/NumberField/AdeleRing.lean | 149 +++++++++++++++++- 8 files changed, 249 insertions(+), 5 deletions(-) create mode 100644 FLT/ForMathlib/LinearAlgebra/TensorProduct/Pi.lean create mode 100644 FLT/ForMathlib/RingTheory/TensorProduct/Pi.lean create mode 100644 FLT/ForMathlib/Topology/Algebra/ContinuousMonoidHom.lean create mode 100644 FLT/ForMathlib/Topology/Algebra/Group/Quotient.lean create mode 100644 FLT/ForMathlib/Topology/Algebra/Module/Equiv.lean create mode 100644 FLT/ForMathlib/Topology/Algebra/Module/Quotient.lean diff --git a/FLT/ForMathlib/LinearAlgebra/TensorProduct/Pi.lean b/FLT/ForMathlib/LinearAlgebra/TensorProduct/Pi.lean new file mode 100644 index 00000000..25b28d0e --- /dev/null +++ b/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 diff --git a/FLT/ForMathlib/RingTheory/TensorProduct/Pi.lean b/FLT/ForMathlib/RingTheory/TensorProduct/Pi.lean new file mode 100644 index 00000000..b7d04f9f --- /dev/null +++ b/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] diff --git a/FLT/ForMathlib/Topology/Algebra/Algebra.lean b/FLT/ForMathlib/Topology/Algebra/Algebra.lean index 26f61d8f..fc9efa70 100644 --- a/FLT/ForMathlib/Topology/Algebra/Algebra.lean +++ b/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 diff --git a/FLT/ForMathlib/Topology/Algebra/ContinuousMonoidHom.lean b/FLT/ForMathlib/Topology/Algebra/ContinuousMonoidHom.lean new file mode 100644 index 00000000..17c1453c --- /dev/null +++ b/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 diff --git a/FLT/ForMathlib/Topology/Algebra/Group/Quotient.lean b/FLT/ForMathlib/Topology/Algebra/Group/Quotient.lean new file mode 100644 index 00000000..3b7bd3aa --- /dev/null +++ b/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 diff --git a/FLT/ForMathlib/Topology/Algebra/Module/Equiv.lean b/FLT/ForMathlib/Topology/Algebra/Module/Equiv.lean new file mode 100644 index 00000000..b408de37 --- /dev/null +++ b/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 diff --git a/FLT/ForMathlib/Topology/Algebra/Module/Quotient.lean b/FLT/ForMathlib/Topology/Algebra/Module/Quotient.lean new file mode 100644 index 00000000..d063a5cc --- /dev/null +++ b/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 _) diff --git a/FLT/NumberField/AdeleRing.lean b/FLT/NumberField/AdeleRing.lean index 92993466..19e4d73d 100644 --- a/FLT/NumberField/AdeleRing.lean +++ b/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 From d3327d5873d8466867f1f1c6dfd2d2dc7aefb625 Mon Sep 17 00:00:00 2001 From: Salvatore Mercuri Date: Sat, 11 Jan 2025 15:20:58 +0000 Subject: [PATCH 3/3] Issue #259: Proof that A_K/K is compact, assuming that A_Q/Q is compact --- FLT/ForMathlib/Topology/Algebra/Algebra.lean | 276 ------------------ .../LinearAlgebra/TensorProduct/Pi.lean | 0 .../RingTheory/TensorProduct/Pi.lean | 2 +- .../Topology/Algebra/ContinuousAlgEquiv.lean | 7 + .../Topology/Algebra/ContinuousMonoidHom.lean | 4 +- .../Topology/Algebra/Group/Quotient.lean | 6 +- .../Topology/Algebra/Module/Equiv.lean | 0 .../Topology/Algebra/Module/Quotient.lean | 0 FLT/NumberField/AdeleRing.lean | 9 +- 9 files changed, 18 insertions(+), 286 deletions(-) delete mode 100644 FLT/ForMathlib/Topology/Algebra/Algebra.lean rename FLT/{ForMathlib => Mathlib}/LinearAlgebra/TensorProduct/Pi.lean (100%) rename FLT/{ForMathlib => Mathlib}/RingTheory/TensorProduct/Pi.lean (93%) rename FLT/{ForMathlib => Mathlib}/Topology/Algebra/ContinuousMonoidHom.lean (89%) rename FLT/{ForMathlib => Mathlib}/Topology/Algebra/Group/Quotient.lean (78%) rename FLT/{ForMathlib => Mathlib}/Topology/Algebra/Module/Equiv.lean (100%) rename FLT/{ForMathlib => Mathlib}/Topology/Algebra/Module/Quotient.lean (100%) diff --git a/FLT/ForMathlib/Topology/Algebra/Algebra.lean b/FLT/ForMathlib/Topology/Algebra/Algebra.lean deleted file mode 100644 index fc9efa70..00000000 --- a/FLT/ForMathlib/Topology/Algebra/Algebra.lean +++ /dev/null @@ -1,276 +0,0 @@ -/- -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 -import Mathlib.Topology.Algebra.Module.Equiv - -/-! -# Topological (sub)algebras - -This file contains an API for `ContinuousAlgEquiv`. --/ - -open scoped Topology - -structure ContinuousAlgEquiv (R A B : Type*) [CommSemiring R] - [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] - [Algebra R B] extends A ≃ₐ[R] B where - continuous_toFun : Continuous toFun := by continuity - continuous_invFun : Continuous invFun := by continuity - -notation:50 A " ≃A[" R "]" B => ContinuousAlgEquiv R A B - -class ContinuousAlgEquivClass (F : Type*) (R A B : outParam Type*) [CommSemiring R] - [Semiring A][TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] - [Algebra R B] [EquivLike F A B] extends AlgEquivClass F R A B : Prop where - map_continuous : ∀ (f : F), Continuous f - inv_continuous : ∀ (f : F), Continuous (EquivLike.inv f) - -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 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 - coe f := f.toFun - inv f := f.invFun - coe_injective' f g h₁ h₂ := by - cases' f with f' _ - cases' g with g' _ - rcases f' with ⟨⟨_, _⟩, _⟩ - rcases g' with ⟨⟨_, _⟩, _⟩ - congr - left_inv f := f.left_inv - right_inv f := f.right_inv - -instance continuousAlgEquivClass : ContinuousAlgEquivClass (A ≃A[R] B) R A B where - map_add f := f.map_add' - map_mul f := f.map_mul' - commutes f := f.commutes' - map_continuous := continuous_toFun - inv_continuous := continuous_invFun - -theorem coe_apply (e : A ≃A[R] B) (a : A) : (e : A →A[R] B) a = e a := rfl - -@[simp] -theorem coe_coe (e : A ≃A[R] B) : ⇑(e : A →A[R] B) = e := rfl - -theorem toAlgEquiv_injective : Function.Injective (toAlgEquiv : (A ≃A[R] B) → A ≃ₐ[R] B) := by - rintro ⟨e, _, _⟩ ⟨e', _, _⟩ rfl - rfl - -@[ext] -theorem ext {f g : A ≃A[R] B} (h : ⇑f = ⇑g) : f = g := - toAlgEquiv_injective <| AlgEquiv.ext <| congr_fun h - -theorem coe_injective : Function.Injective ((↑) : (A ≃A[R] B) → A →A[R] B) := - fun _ _ h => ext <| funext <| ContinuousAlgHom.ext_iff.1 h - -@[simp] -theorem coe_inj {f g : A ≃A[R] B} : (f : A →A[R] B) = g ↔ f = g := - coe_injective.eq_iff - -def toHomeomorph (e : A ≃A[R] B) : A ≃ₜ B where - __ := e - toEquiv := e.toAlgEquiv.toEquiv - -@[simp] -theorem coe_toHomeomorph (e : A ≃A[R] B) : ⇑e.toHomeomorph = e := rfl - -theorem isOpenMap (e : A ≃A[R] B) : IsOpenMap e := - e.toHomeomorph.isOpenMap - -theorem image_closure (e : A ≃A[R] B) (S : Set A) : e '' closure S = closure (e '' S) := - e.toHomeomorph.image_closure S - -theorem preimage_closure (e : A ≃A[R] B) (S : Set B) : e ⁻¹' closure S = closure (e ⁻¹' S) := - e.toHomeomorph.preimage_closure S - -@[simp] -theorem isClosed_image (e : A ≃A[R] B) {S : Set A} : IsClosed (e '' S) ↔ IsClosed S := - e.toHomeomorph.isClosed_image - -theorem map_nhds_eq (e : A ≃A[R] B) (a : A) : Filter.map e (𝓝 a) = 𝓝 (e a) := - e.toHomeomorph.map_nhds_eq a - -theorem map_zero (e : A ≃A[R] B) : e (0 : A) = 0 := - e.toAlgHom.map_zero' - -theorem map_add (e : A ≃A[R] B) (a₁ a₂ : A) : e (a₁ + a₂) = e a₁ + e a₂ := - e.toAlgHom.map_add' a₁ a₂ - -theorem map_smul (e : A ≃A[R] B) (r : R) (a : A) : e (r • a) = r • e a := - _root_.map_smul e r a - -theorem map_eq_zero_iff (e : A ≃A[R] B) {a : A} : e a = 0 ↔ a = 0 := - e.toAlgEquiv.toLinearEquiv.map_eq_zero_iff - -attribute [continuity] - ContinuousAlgEquiv.continuous_invFun ContinuousAlgEquiv.continuous_toFun - -theorem continuous (e : A ≃A[R] B) : Continuous e := e.continuous_toFun - -theorem continuousOn (e : A ≃A[R] B) {S : Set A} : ContinuousOn e S := - e.continuous.continuousOn - -theorem continuousAt (e : A ≃A[R] B) {a : A} : ContinuousAt e a := - e.continuous.continuousAt - -theorem continuousWithinAt (e : A ≃A[R] B) {S : Set A} {a : A} : - ContinuousWithinAt e S a := - e.continuous.continuousWithinAt - -theorem comp_continuous_iff {α : Type*} [TopologicalSpace α] (e : A ≃A[R] B) {f : α → A} : - Continuous (e ∘ f) ↔ Continuous f := - e.toHomeomorph.comp_continuous_iff - -variable (R A) - -@[refl] -def refl : A ≃A[R] A where - __ := AlgEquiv.refl - continuous_toFun := continuous_id - continuous_invFun := continuous_id - -@[simp] -theorem refl_apply (a : A) : refl R A a = a := rfl - -@[simp] -theorem coe_refl : refl R A = ContinuousAlgHom.id R A := rfl - -@[simp] -theorem coe_refl' : ⇑(refl R A) = id := rfl - -variable {R A} -@[symm] -def symm (e : A ≃A[R] B) : B ≃A[R] A where - __ := e.toAlgEquiv.symm - continuous_toFun := e.continuous_invFun - continuous_invFun := e.continuous_toFun - -@[simp] -theorem apply_symm_apply (e : A ≃A[R] B) (b : B) : e (e.symm b) = b := - e.1.right_inv b - -@[simp] -theorem symm_apply_apply (e : A ≃A[R] B) (a : A) : e.symm (e a) = a := - e.1.left_inv a - -@[simp] -theorem symm_image_image (e : A ≃A[R] B) (S : Set A) : e.symm '' (e '' S) = S := - e.toEquiv.symm_image_image S - -@[simp] -theorem image_symm_image (e : A ≃A[R] B) (S : Set B) : e '' (e.symm '' S) = S := - e.symm.symm_image_image S - -@[simp] -theorem symm_toAlgEquiv (e : A ≃A[R] B) : e.symm.toAlgEquiv = e.toAlgEquiv.symm := rfl - -@[simp] -theorem symm_toHomeomorph (e : A ≃A[R] B) : e.symm.toHomeomorph = e.toHomeomorph.symm := rfl - -theorem symm_map_nhds_eq (e : A ≃A[R] B) (a : A) : Filter.map e.symm (𝓝 (e a)) = 𝓝 a := - e.toHomeomorph.symm_map_nhds_eq a - -@[trans] -def trans (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) : A ≃A[R] C where - __ := e₁.toAlgEquiv.trans e₂.toAlgEquiv - continuous_toFun := e₂.continuous_toFun.comp e₁.continuous_toFun - continuous_invFun := e₁.continuous_invFun.comp e₂.continuous_invFun - -@[simp] -theorem trans_toAlgEquiv (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) : - (e₁.trans e₂).toAlgEquiv = e₁.toAlgEquiv.trans e₂.toAlgEquiv := - rfl - -@[simp] -theorem trans_apply (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) (a : A) : - (e₁.trans e₂) a = e₂ (e₁ a) := - rfl - -@[simp] -theorem symm_trans_apply (e₁ : B ≃A[R] A) (e₂ : C ≃A[R] B) (a : A) : - (e₂.trans e₁).symm a = e₂.symm (e₁.symm a) := - rfl - -@[simp] -theorem comp_coe (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) : - e₂.toAlgHom.comp e₁.toAlgHom = e₁.trans e₂ := - rfl - -@[simp high] -theorem coe_comp_coe_symm (e : A ≃A[R] B) : - e.toContinuousAlgHom.comp e.symm = ContinuousAlgHom.id R B := - ContinuousAlgHom.ext e.apply_symm_apply - -@[simp high] -theorem coe_symm_comp_coe (e : A ≃A[R] B) : - e.symm.toContinuousAlgHom.comp e = ContinuousAlgHom.id R A := - ContinuousAlgHom.ext e.symm_apply_apply - -@[simp] -theorem symm_comp_self (e : A ≃A[R] B) : e.symm.toFun ∘ e.toFun = id := - funext <| e.symm_apply_apply - -@[simp] -theorem self_comp_symm (e : A ≃A[R] B) : e.toFun ∘ e.symm.toFun = id := - funext <| e.apply_symm_apply - -@[simp] -theorem symm_symm (e : A ≃A[R] B) : e.symm.symm = e := rfl - -@[simp] -theorem refl_symm : (refl R A).symm = refl R A := rfl - -theorem symm_symm_apply (e : A ≃A[R] B) (a : A) : e.symm.symm a = e a := rfl - -theorem symm_apply_eq (e : A ≃A[R] B) {a : A} {b : B} : e.symm b = a ↔ b = e a := - e.toEquiv.symm_apply_eq - -theorem eq_symm_apply (e : A ≃A[R] B) {a : A} {b : B} : a = e.symm b ↔ e a = b := - e.toEquiv.eq_symm_apply - -theorem image_eq_preimage (e : A ≃A[R] B) (S : Set A) : e '' S = e.symm ⁻¹' S := - e.toEquiv.image_eq_preimage S - -theorem image_symm_eq_preimage (e : A ≃A[R] B) (S : Set B) : e.symm '' S = e ⁻¹' S := by - rw [e.symm.image_eq_preimage, e.symm_symm] - -@[simp] -theorem symm_preimage_preimage (e : A ≃A[R] B) (S : Set B) : e.symm ⁻¹' (e ⁻¹' S) = S := - e.toEquiv.symm_preimage_preimage S - -@[simp] -theorem preimage_symm_preimage (e : A ≃A[R] B) (S : Set A) : e ⁻¹' (e.symm ⁻¹' S) = S := - e.symm.symm_preimage_preimage S - -theorem isUniformEmbedding {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂] [Ring E₁] - [UniformAddGroup E₁] [Algebra R E₁] [Ring E₂] [UniformAddGroup E₂] [Algebra R E₂] - (e : E₁ ≃A[R] E₂) : IsUniformEmbedding e := - e.toAlgEquiv.isUniformEmbedding e.toContinuousAlgHom.uniformContinuous - e.symm.toContinuousAlgHom.uniformContinuous - -theorem _root_.AlgEquiv.isUniformEmbedding {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂] - [Ring E₁] [UniformAddGroup E₁] [Algebra R E₁] [Ring E₂] [UniformAddGroup E₂] [Algebra R E₂] - (e : E₁ ≃ₐ[R] E₂) (h₁ : Continuous e) (h₂ : Continuous e.symm) : - IsUniformEmbedding e := - ContinuousAlgEquiv.isUniformEmbedding { e with continuous_toFun := h₁ } - -end ContinuousAlgEquiv diff --git a/FLT/ForMathlib/LinearAlgebra/TensorProduct/Pi.lean b/FLT/Mathlib/LinearAlgebra/TensorProduct/Pi.lean similarity index 100% rename from FLT/ForMathlib/LinearAlgebra/TensorProduct/Pi.lean rename to FLT/Mathlib/LinearAlgebra/TensorProduct/Pi.lean diff --git a/FLT/ForMathlib/RingTheory/TensorProduct/Pi.lean b/FLT/Mathlib/RingTheory/TensorProduct/Pi.lean similarity index 93% rename from FLT/ForMathlib/RingTheory/TensorProduct/Pi.lean rename to FLT/Mathlib/RingTheory/TensorProduct/Pi.lean index b7d04f9f..8b981058 100644 --- a/FLT/ForMathlib/RingTheory/TensorProduct/Pi.lean +++ b/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 index 26f61d8f..46aad9c6 100644 --- 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/FLT/ForMathlib/Topology/Algebra/ContinuousMonoidHom.lean b/FLT/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean similarity index 89% rename from FLT/ForMathlib/Topology/Algebra/ContinuousMonoidHom.lean rename to FLT/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean index 17c1453c..15288c2d 100644 --- a/FLT/ForMathlib/Topology/Algebra/ContinuousMonoidHom.lean +++ b/FLT/Mathlib/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/FLT/ForMathlib/Topology/Algebra/Group/Quotient.lean b/FLT/Mathlib/Topology/Algebra/Group/Quotient.lean similarity index 78% rename from FLT/ForMathlib/Topology/Algebra/Group/Quotient.lean rename to FLT/Mathlib/Topology/Algebra/Group/Quotient.lean index 3b7bd3aa..eb9dd583 100644 --- a/FLT/ForMathlib/Topology/Algebra/Group/Quotient.lean +++ b/FLT/Mathlib/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/FLT/ForMathlib/Topology/Algebra/Module/Equiv.lean b/FLT/Mathlib/Topology/Algebra/Module/Equiv.lean similarity index 100% rename from FLT/ForMathlib/Topology/Algebra/Module/Equiv.lean rename to FLT/Mathlib/Topology/Algebra/Module/Equiv.lean diff --git a/FLT/ForMathlib/Topology/Algebra/Module/Quotient.lean b/FLT/Mathlib/Topology/Algebra/Module/Quotient.lean similarity index 100% rename from FLT/ForMathlib/Topology/Algebra/Module/Quotient.lean rename to FLT/Mathlib/Topology/Algebra/Module/Quotient.lean diff --git a/FLT/NumberField/AdeleRing.lean b/FLT/NumberField/AdeleRing.lean index 19e4d73d..8cc940c7 100644 --- 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)