Source: ProCGroups.Topologies.OpenSubgroup
1import Mathlib.Topology.Algebra.OpenSubgroup
2import Mathlib.Topology.Algebra.ContinuousMonoidHom
4/-!
5# The whole group as an open subgroup
7This file records the canonical continuous multiplicative equivalence between a topological group
8and the subtype of its top open subgroup, together with its forward and inverse formulas.
9-/
11open scoped Topology
13namespace ProCGroups
15namespace OpenSubgroup
17universe u
19/-- The \(\top\) open subgroup is canonically equivalent to the ambient topological group. -/
20noncomputable def topContinuousMulEquiv
21 (G : Type u) [TopologicalSpace G] [Group G] :
22 ↥((⊤ : OpenSubgroup G) : Subgroup G) ≃ₜ* G :=
23 { toMulEquiv :=
24 { toFun := fun x => x.1
25 invFun := fun x => ⟨x, by simp only [_root_.OpenSubgroup.toSubgroup_top, Subgroup.mem_top]⟩
26 left_inv := by
27 intro x
28 ext
29 rfl
30 right_inv := by
31 intro x
32 rfl
33 map_mul' := by
34 intro x y
35 rfl }
36 continuous_toFun := continuous_subtype_val
37 continuous_invFun := by
38 exact Continuous.subtype_mk continuous_id (by intro x; simp only
39 [_root_.OpenSubgroup.toSubgroup_top, id_eq, Subgroup.mem_top]) }
41/-- The open-subgroup comparison equivalence evaluates on representatives. -/
42@[simp] theorem topContinuousMulEquiv_apply
43 (G : Type u) [TopologicalSpace G] [Group G]
44 (x : ↥((⊤ : OpenSubgroup G) : Subgroup G)) :
45 topContinuousMulEquiv G x = x.1 :=
46 rfl
48/--
49The inverse comparison equivalence is evaluated by the same coordinate data, read in the
50opposite direction.
51-/
52@[simp] theorem topContinuousMulEquiv_symm_apply
53 (G : Type u) [TopologicalSpace G] [Group G] (x : G) :
54 (topContinuousMulEquiv G).symm x = ⟨x, by simp only [_root_.OpenSubgroup.toSubgroup_top,
55 Subgroup.mem_top]⟩ :=
56 rfl
58end OpenSubgroup
60end ProCGroups