ProCGroups/Topologies/OpenSubgroup.lean

1import Mathlib.Topology.Algebra.OpenSubgroup

2import Mathlib.Topology.Algebra.ContinuousMonoidHom

4/-

5PUBLIC_PAGE_SNAPSHOT

6generated_at: 2026-05-27T09:47:29+09:00

7lean_source: lean4/ProCGroups/Topologies/OpenSubgroup.lean

8translation_root: data/translation

9purpose: identifies the local data snapshot used to build pages/

10placement: after imports, never before imports

12/-!

13# Topological group constructions

15Topological subgroup, quotient, continuous homomorphism, continuous equivalence, conjugation, and full-subgroup-topology lemmas.

18open scoped Topology

20namespace OpenSubgroup

22universe u

24/-- The top open subgroup is canonically equivalent to the ambient topological group. -/

26 (G : Type u) [TopologicalSpace G] [Group G] :

27 ↥((⊤ : OpenSubgroup G) : Subgroup G) ≃ₜ* G :=

28 { toMulEquiv :=

29 { toFun := fun x => x.1

30 invFun := fun x => ⟨x, by simp only [toSubgroup_top, Subgroup.mem_top]⟩

31 left_inv := by

32 intro x

33 ext

34 rfl

35 right_inv := by

36 intro x

37 rfl

38 map_mul' := by

39 intro x y

40 rfl }

41 continuous_toFun := continuous_subtype_val

42 continuous_invFun := by

43 exact Continuous.subtype_mk continuous_id (by intro x; simp only [toSubgroup_top, id_eq, Subgroup.mem_top]) }

46 (G : Type u) [TopologicalSpace G] [Group G]

47 (x : ↥((⊤ : OpenSubgroup G) : Subgroup G)) :

49 rfl

52 (G : Type u) [TopologicalSpace G] [Group G] (x : G) :

53 (topContinuousMulEquiv G).symm x = ⟨x, by simp only [toSubgroup_top, Subgroup.mem_top]⟩ :=

54 rfl

56end OpenSubgroup