ProCGroups/Topologies/ContinuousMulEquiv.lean
1import Mathlib.GroupTheory.QuotientGroup.Basic
2import Mathlib.Topology.Algebra.ContinuousMonoidHom
3import ProCGroups.Topologies.ContinuousMonoidHom
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/Topologies/ContinuousMulEquiv.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Topological group constructions
16Topological subgroup, quotient, continuous homomorphism, continuous equivalence, conjugation, and full-subgroup-topology lemmas.
17-/
19namespace ContinuousMulEquiv
21universe u v
23section
25variable {G : Type u} {H : Type v}
26variable [Group G] [Group H]
27variable [TopologicalSpace G] [TopologicalSpace H]
29/-- The continuous monoid homomorphism induced by a continuous multiplicative equivalence. -/
30def toContinuousMonoidHom (e : G ≃ₜ* H) : G →ₜ* H :=
31 { toMonoidHom := e.toMulEquiv.toMonoidHom
32 continuous_toFun := e.continuous_toFun }
34/-- The continuous monoid homomorphism underlying a continuous multiplicative equivalence evaluates as the equivalence. -/
35@[simp] theorem toContinuousMonoidHom_apply (e : G ≃ₜ* H) (g : G) :
36 e.toContinuousMonoidHom g = e g :=
37 rfl
39/-- Build a continuous multiplicative equivalence from inverse continuous homomorphisms. -/
41 (f : G →ₜ* H) (g : H →ₜ* G)
42 (hleft : Function.LeftInverse g f)
43 (hright : Function.RightInverse g f) :
44 G ≃ₜ* H :=
45 { toMulEquiv :=
46 { toFun := f
47 invFun := g
48 left_inv := hleft
49 right_inv := hright
50 map_mul' := f.map_mul }
51 continuous_toFun := f.continuous_toFun
52 continuous_invFun := g.continuous_toFun }
54@[simp] theorem ofHomInv_apply
55 (f : G →ₜ* H) (g : H →ₜ* G)
56 (hleft : Function.LeftInverse g f)
57 (hright : Function.RightInverse g f) (x : G) :
59 rfl
61end
63/-- Upgrade a bijective continuous homomorphism from a compact topological group to a Hausdorff
64topological group to a continuous multiplicative equivalence. -/
65noncomputable def ofBijectiveCompactToT2
66 {G : Type u} {H : Type v}
67 [Group G] [TopologicalSpace G]
68 [Group H] [TopologicalSpace H]
69 [CompactSpace G] [T2Space H]
70 (φ : G →* H) (hφcont : Continuous φ)
71 (hφ : Function.Bijective φ) :
72 G ≃ₜ* H := by
73 let e : G ≃ H := Equiv.ofBijective φ hφ
74 let eh : G ≃ₜ H :=
75 e.toHomeomorphOfContinuousClosed hφcont (Continuous.isClosedMap hφcont)
76 exact ContinuousMulEquiv.mk' eh (by
77 intro x y
78 exact φ.map_mul x y)
80@[simp 900] theorem ofBijectiveCompactToT2_apply
81 {G : Type u} {H : Type v}
82 [Group G] [TopologicalSpace G]
83 [Group H] [TopologicalSpace H]
84 [CompactSpace G] [T2Space H]
85 (φ : G →* H) (hφcont : Continuous φ)
86 (hφ : Function.Bijective φ) (x : G) :
87 ofBijectiveCompactToT2 φ hφcont hφ x = φ x := by
88 unfold ofBijectiveCompactToT2
89 rfl
91end ContinuousMulEquiv
93namespace ContinuousMonoidHom
95universe u v
97/-- The first isomorphism theorem for continuous monoid homomorphisms from a compact group to a
98Hausdorff group, with the quotient and range carrying their induced topologies. -/
99noncomputable def quotientKerContinuousMulEquivRange
100 {G : Type u} {H : Type v}
101 [Group G] [TopologicalSpace G] [CompactSpace G]
102 [Group H] [TopologicalSpace H] [T2Space H]
103 (f : G →ₜ* H) :
104 (G ⧸ (f.toMonoidHom.ker : Subgroup G)) ≃ₜ* f.toMonoidHom.range := by
105 let φ : (G ⧸ (f.toMonoidHom.ker : Subgroup G)) →* f.toMonoidHom.range :=
106 (QuotientGroup.quotientKerEquivRange f.toMonoidHom).toMonoidHom
107 have hφcont : Continuous φ := by
108 refine (QuotientGroup.isQuotientMap_mk f.toMonoidHom.ker).continuous_iff.2 ?_
109 simpa [φ, ContinuousMonoidHom.rangeRestrict] using f.rangeRestrict.continuous_toFun
110 exact ContinuousMulEquiv.ofBijectiveCompactToT2 φ hφcont
111 (QuotientGroup.quotientKerEquivRange f.toMonoidHom).bijective
113/-- The quotient-by-kernel equivalence to the range sends a representative to its image. -/
114@[simp] theorem quotientKerContinuousMulEquivRange_mk
115 {G : Type u} {H : Type v}
116 [Group G] [TopologicalSpace G] [CompactSpace G]
117 [Group H] [TopologicalSpace H] [T2Space H]
118 (f : G →ₜ* H) (g : G) :
120 (QuotientGroup.mk' (f.toMonoidHom.ker : Subgroup G) g) =
121 f.toMonoidHom.rangeRestrict g :=
122 rfl
124/-- Coercing the quotient-by-kernel equivalence to the codomain gives the original homomorphism value. -/
125@[simp] theorem coe_quotientKerContinuousMulEquivRange_mk
126 {G : Type u} {H : Type v}
127 [Group G] [TopologicalSpace G] [CompactSpace G]
128 [Group H] [TopologicalSpace H] [T2Space H]
129 (f : G →ₜ* H) (g : G) :
131 (QuotientGroup.mk' (f.toMonoidHom.ker : Subgroup G) g) : H) = f g :=
132 rfl
134end ContinuousMonoidHom