Skip to content

Commit 46d1f44

Browse files
kbuzzardkbuzzard
committed
feat(Topology/Algebra/Algebra/Equiv): continuous algebra equivs (#20609)
From FLT. Written by Salvatore Mercuri.
1 parent 1d24f3c commit 46d1f44

File tree

2 files changed

+297
-0
lines changed

2 files changed

+297
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5132,6 +5132,7 @@ import Mathlib.Testing.Plausible.Testable
51325132
import Mathlib.Topology.AlexandrovDiscrete
51335133
import Mathlib.Topology.Algebra.Affine
51345134
import Mathlib.Topology.Algebra.Algebra
5135+
import Mathlib.Topology.Algebra.Algebra.Equiv
51355136
import Mathlib.Topology.Algebra.Algebra.Rat
51365137
import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
51375138
import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

‎Mathlib/Topology/Algebra/Algebra/Equiv.lean‎

Lines changed: 296 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,296 @@
1+
/-
2+
Copyright (c) 2024 Salvatore Mercuri. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Salvatore Mercuri
5+
-/
6+
import Mathlib.Topology.Algebra.Algebra
7+
8+
/-!
9+
# Isomorphisms of topological algebras
10+
11+
This file contains an API for `ContinuousAlgEquiv R A B`, the type of
12+
continuous `R`-algebra isomorphisms with continuous inverses. Here `R` is a
13+
commutative (semi)ring, and `A` and `B` are `R`-algebras with topologies.
14+
15+
## Main definitions
16+
17+
Let `R` be a commutative semiring and let `A` and `B` be `R`-algebras which
18+
are also topological spaces.
19+
20+
* `ContinuousAlgEquiv R A B`: the type of continuous `R`-algebra isomorphisms
21+
from `A` to `B` with continuous inverses.
22+
23+
## Notations
24+
25+
`A ≃A[R] B` : notation for `ContinuousAlgEquiv R A B`.
26+
27+
## Tags
28+
29+
* continuous, isomorphism, algebra
30+
-/
31+
32+
open scoped Topology
33+
34+
35+
/--
36+
`ContinuousAlgEquiv R A B`, with notation `A ≃A[R] B`, is the type of bijections
37+
between the topological `R`-algebras `A` and `B` which are both homeomorphisms
38+
and `R`-algebra isomorphisms.
39+
-/
40+
structure ContinuousAlgEquiv (R A B : Type*) [CommSemiring R]
41+
[Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A]
42+
[Algebra R B] extends A ≃ₐ[R] B, A ≃ₜ B
43+
44+
@[inherit_doc]
45+
notation:50 A " ≃A[" R "]" B => ContinuousAlgEquiv R A B
46+
47+
attribute [nolint docBlame] ContinuousAlgEquiv.toHomeomorph
48+
49+
/--
50+
`ContinuousAlgEquivClass F R A B` states that `F` is a type of topological algebra
51+
structure-preserving equivalences. You should extend this class when you
52+
extend `ContinuousAlgEquiv`.
53+
-/
54+
class ContinuousAlgEquivClass (F : Type*) (R A B : outParam Type*) [CommSemiring R]
55+
[Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B]
56+
[Algebra R A] [Algebra R B] [EquivLike F A B]
57+
extends AlgEquivClass F R A B, HomeomorphClass F A B : Prop
58+
59+
namespace ContinuousAlgEquiv
60+
61+
variable {R A B C : Type*}
62+
[CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B]
63+
[TopologicalSpace B] [Semiring C] [TopologicalSpace C] [Algebra R A] [Algebra R B]
64+
[Algebra R C]
65+
66+
/-- The natural coercion from a continuous algebra isomorphism to a continuous
67+
algebra morphism. -/
68+
@[coe]
69+
def toContinuousAlgHom (e : A ≃A[R] B) : A →A[R] B where
70+
__ := e.toAlgHom
71+
cont := e.continuous_toFun
72+
73+
instance coe : Coe (A ≃A[R] B) (A →A[R] B) := ⟨toContinuousAlgHom⟩
74+
75+
instance equivLike : EquivLike (A ≃A[R] B) A B where
76+
coe f := f.toFun
77+
inv f := f.invFun
78+
coe_injective' f g h₁ h₂ := by
79+
cases' f with f' _
80+
cases' g with g' _
81+
rcases f' with ⟨⟨_, _⟩, _⟩
82+
rcases g' with ⟨⟨_, _⟩, _⟩
83+
congr
84+
left_inv f := f.left_inv
85+
right_inv f := f.right_inv
86+
87+
instance continuousAlgEquivClass : ContinuousAlgEquivClass (A ≃A[R] B) R A B where
88+
map_add f := f.map_add'
89+
map_mul f := f.map_mul'
90+
commutes f := f.commutes'
91+
map_continuous := continuous_toFun
92+
inv_continuous := continuous_invFun
93+
94+
theorem coe_apply (e : A ≃A[R] B) (a : A) : (e : A →A[R] B) a = e a := rfl
95+
96+
@[simp]
97+
theorem coe_coe (e : A ≃A[R] B) : ⇑(e : A →A[R] B) = e := rfl
98+
99+
theorem toAlgEquiv_injective : Function.Injective (toAlgEquiv : (A ≃A[R] B) → A ≃ₐ[R] B) := by
100+
rintro ⟨e, _, _⟩ ⟨e', _, _⟩ rfl
101+
rfl
102+
103+
@[ext]
104+
theorem ext {f g : A ≃A[R] B} (h : ⇑f = ⇑g) : f = g :=
105+
toAlgEquiv_injective <| AlgEquiv.ext <| congr_fun h
106+
107+
theorem coe_injective : Function.Injective ((↑) : (A ≃A[R] B) → A →A[R] B) :=
108+
fun _ _ h => ext <| funext <| ContinuousAlgHom.ext_iff.1 h
109+
110+
@[simp]
111+
theorem coe_inj {f g : A ≃A[R] B} : (f : A →A[R] B) = g ↔ f = g :=
112+
coe_injective.eq_iff
113+
114+
@[simp]
115+
theorem coe_toAlgEquiv (e : A ≃A[R] B) : ⇑e.toAlgEquiv = e := rfl
116+
117+
theorem isOpenMap (e : A ≃A[R] B) : IsOpenMap e :=
118+
e.toHomeomorph.isOpenMap
119+
120+
theorem image_closure (e : A ≃A[R] B) (S : Set A) : e '' closure S = closure (e '' S) :=
121+
e.toHomeomorph.image_closure S
122+
123+
theorem preimage_closure (e : A ≃A[R] B) (S : Set B) : e ⁻¹' closure S = closure (e ⁻¹' S) :=
124+
e.toHomeomorph.preimage_closure S
125+
126+
@[simp]
127+
theorem isClosed_image (e : A ≃A[R] B) {S : Set A} : IsClosed (e '' S) ↔ IsClosed S :=
128+
e.toHomeomorph.isClosed_image
129+
130+
theorem map_nhds_eq (e : A ≃A[R] B) (a : A) : Filter.map e (𝓝 a) = 𝓝 (e a) :=
131+
e.toHomeomorph.map_nhds_eq a
132+
133+
theorem map_eq_zero_iff (e : A ≃A[R] B) {a : A} : e a = 0 ↔ a = 0 :=
134+
e.toAlgEquiv.toLinearEquiv.map_eq_zero_iff
135+
136+
attribute [continuity]
137+
ContinuousAlgEquiv.continuous_invFun ContinuousAlgEquiv.continuous_toFun
138+
139+
@[fun_prop]
140+
theorem continuous (e : A ≃A[R] B) : Continuous e := e.continuous_toFun
141+
142+
theorem continuousOn (e : A ≃A[R] B) {S : Set A} : ContinuousOn e S :=
143+
e.continuous.continuousOn
144+
145+
theorem continuousAt (e : A ≃A[R] B) {a : A} : ContinuousAt e a :=
146+
e.continuous.continuousAt
147+
148+
theorem continuousWithinAt (e : A ≃A[R] B) {S : Set A} {a : A} :
149+
ContinuousWithinAt e S a :=
150+
e.continuous.continuousWithinAt
151+
152+
theorem comp_continuous_iff {α : Type*} [TopologicalSpace α] (e : A ≃A[R] B) {f : α → A} :
153+
Continuous (e ∘ f) ↔ Continuous f :=
154+
e.toHomeomorph.comp_continuous_iff
155+
156+
theorem comp_continuous_iff' {β : Type*} [TopologicalSpace β] (e : A ≃A[R] B) {g : B → β} :
157+
Continuous (g ∘ e) ↔ Continuous g :=
158+
e.toHomeomorph.comp_continuous_iff'
159+
160+
variable (R A)
161+
162+
/-- The identity isomorphism as a continuous `R`-algebra equivalence. -/
163+
@[refl]
164+
def refl : A ≃A[R] A where
165+
__ := AlgEquiv.refl
166+
continuous_toFun := continuous_id
167+
continuous_invFun := continuous_id
168+
169+
@[simp]
170+
theorem refl_apply (a : A) : refl R A a = a := rfl
171+
172+
@[simp]
173+
theorem coe_refl : refl R A = ContinuousAlgHom.id R A := rfl
174+
175+
@[simp]
176+
theorem coe_refl' : ⇑(refl R A) = id := rfl
177+
178+
variable {R A}
179+
180+
/-- The inverse of a continuous algebra equivalence. -/
181+
@[symm]
182+
def symm (e : A ≃A[R] B) : B ≃A[R] A where
183+
__ := e.toAlgEquiv.symm
184+
continuous_toFun := e.continuous_invFun
185+
continuous_invFun := e.continuous_toFun
186+
187+
@[simp]
188+
theorem apply_symm_apply (e : A ≃A[R] B) (b : B) : e (e.symm b) = b :=
189+
e.1.right_inv b
190+
191+
@[simp]
192+
theorem symm_apply_apply (e : A ≃A[R] B) (a : A) : e.symm (e a) = a :=
193+
e.1.left_inv a
194+
195+
@[simp]
196+
theorem symm_image_image (e : A ≃A[R] B) (S : Set A) : e.symm '' (e '' S) = S :=
197+
e.toEquiv.symm_image_image S
198+
199+
@[simp]
200+
theorem image_symm_image (e : A ≃A[R] B) (S : Set B) : e '' (e.symm '' S) = S :=
201+
e.symm.symm_image_image S
202+
203+
@[simp]
204+
theorem symm_toAlgEquiv (e : A ≃A[R] B) : e.symm.toAlgEquiv = e.toAlgEquiv.symm := rfl
205+
206+
@[simp]
207+
theorem symm_toHomeomorph (e : A ≃A[R] B) : e.symm.toHomeomorph = e.toHomeomorph.symm := rfl
208+
209+
theorem symm_map_nhds_eq (e : A ≃A[R] B) (a : A) : Filter.map e.symm (𝓝 (e a)) = 𝓝 a :=
210+
e.toHomeomorph.symm_map_nhds_eq a
211+
212+
/-- The composition of two continuous algebra equivalences. -/
213+
@[trans]
214+
def trans (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) : A ≃A[R] C where
215+
__ := e₁.toAlgEquiv.trans e₂.toAlgEquiv
216+
continuous_toFun := e₂.continuous_toFun.comp e₁.continuous_toFun
217+
continuous_invFun := e₁.continuous_invFun.comp e₂.continuous_invFun
218+
219+
@[simp]
220+
theorem trans_toAlgEquiv (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) :
221+
(e₁.trans e₂).toAlgEquiv = e₁.toAlgEquiv.trans e₂.toAlgEquiv :=
222+
rfl
223+
224+
@[simp]
225+
theorem trans_apply (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) (a : A) :
226+
(e₁.trans e₂) a = e₂ (e₁ a) :=
227+
rfl
228+
229+
@[simp]
230+
theorem symm_trans_apply (e₁ : B ≃A[R] A) (e₂ : C ≃A[R] B) (a : A) :
231+
(e₂.trans e₁).symm a = e₂.symm (e₁.symm a) :=
232+
rfl
233+
234+
theorem comp_coe (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) :
235+
e₂.toAlgHom.comp e₁.toAlgHom = e₁.trans e₂ := by
236+
rfl
237+
238+
@[simp high]
239+
theorem coe_comp_coe_symm (e : A ≃A[R] B) :
240+
e.toContinuousAlgHom.comp e.symm = ContinuousAlgHom.id R B :=
241+
ContinuousAlgHom.ext e.apply_symm_apply
242+
243+
@[simp high]
244+
theorem coe_symm_comp_coe (e : A ≃A[R] B) :
245+
e.symm.toContinuousAlgHom.comp e = ContinuousAlgHom.id R A :=
246+
ContinuousAlgHom.ext e.symm_apply_apply
247+
248+
@[simp]
249+
theorem symm_comp_self (e : A ≃A[R] B) : (e.symm : B → A) ∘ e = id := by
250+
exact funext <| e.symm_apply_apply
251+
252+
@[simp]
253+
theorem self_comp_symm (e : A ≃A[R] B) : (e : A → B) ∘ e.symm = id :=
254+
funext <| e.apply_symm_apply
255+
256+
@[simp]
257+
theorem symm_symm (e : A ≃A[R] B) : e.symm.symm = e := rfl
258+
259+
@[simp]
260+
theorem refl_symm : (refl R A).symm = refl R A := rfl
261+
262+
theorem symm_symm_apply (e : A ≃A[R] B) (a : A) : e.symm.symm a = e a := rfl
263+
264+
theorem symm_apply_eq (e : A ≃A[R] B) {a : A} {b : B} : e.symm b = a ↔ b = e a :=
265+
e.toEquiv.symm_apply_eq
266+
267+
theorem eq_symm_apply (e : A ≃A[R] B) {a : A} {b : B} : a = e.symm b ↔ e a = b :=
268+
e.toEquiv.eq_symm_apply
269+
270+
theorem image_eq_preimage (e : A ≃A[R] B) (S : Set A) : e '' S = e.symm ⁻¹' S :=
271+
e.toEquiv.image_eq_preimage S
272+
273+
theorem image_symm_eq_preimage (e : A ≃A[R] B) (S : Set B) : e.symm '' S = e ⁻¹' S := by
274+
rw [e.symm.image_eq_preimage, e.symm_symm]
275+
276+
@[simp]
277+
theorem symm_preimage_preimage (e : A ≃A[R] B) (S : Set B) : e.symm ⁻¹' (e ⁻¹' S) = S :=
278+
e.toEquiv.symm_preimage_preimage S
279+
280+
@[simp]
281+
theorem preimage_symm_preimage (e : A ≃A[R] B) (S : Set A) : e ⁻¹' (e.symm ⁻¹' S) = S :=
282+
e.symm.symm_preimage_preimage S
283+
284+
theorem isUniformEmbedding {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂] [Ring E₁]
285+
[UniformAddGroup E₁] [Algebra R E₁] [Ring E₂] [UniformAddGroup E₂] [Algebra R E₂]
286+
(e : E₁ ≃A[R] E₂) : IsUniformEmbedding e :=
287+
e.toAlgEquiv.isUniformEmbedding e.toContinuousAlgHom.uniformContinuous
288+
e.symm.toContinuousAlgHom.uniformContinuous
289+
290+
theorem _root_.AlgEquiv.isUniformEmbedding {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂]
291+
[Ring E₁] [UniformAddGroup E₁] [Algebra R E₁] [Ring E₂] [UniformAddGroup E₂] [Algebra R E₂]
292+
(e : E₁ ≃ₐ[R] E₂) (h₁ : Continuous e) (h₂ : Continuous e.symm) :
293+
IsUniformEmbedding e :=
294+
ContinuousAlgEquiv.isUniformEmbedding { e with continuous_toFun := h₁ }
295+
296+
end ContinuousAlgEquiv

0 commit comments

Comments
 (0)