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)