ProCGroups/Profinite/OpenSubgroups.lean
1import Mathlib.GroupTheory.OrderOfElement
2import Mathlib.Topology.Algebra.ClopenNhdofOne
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/Profinite/OpenSubgroups.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Profinite group basics
15Basic profinite group predicates, finite quotient facts, and standard closure properties used throughout the pro-C library.
16-/
18open Set
19open scoped Topology Pointwise
21namespace ProCGroups
23universe u v
25section OpenSubgroups
27variable {G : Type u} [Group G] [TopologicalSpace G]
29/-- An open subgroup is open as a subset. -/
30theorem openSubgroup_isOpen (U : OpenSubgroup G) :
31 IsOpen ((U : Subgroup G) : Set G) := by
32 simpa using U.isOpen'
34/-- An open subgroup is closed as a subset. -/
35theorem openSubgroup_isClosed [ContinuousMul G] (U : OpenSubgroup G) :
36 IsClosed ((U : Subgroup G) : Set G) := by
37 simpa using OpenSubgroup.isClosed U
39/-- An open normal subgroup is open as a subset. -/
40theorem openNormalSubgroup_isOpen (U : OpenNormalSubgroup G) :
41 IsOpen ((U : Subgroup G) : Set G) := by
42 simpa using U.toOpenSubgroup.isOpen'
44/-- An open normal subgroup is closed as a subset. -/
45theorem openNormalSubgroup_isClosed [ContinuousMul G] (U : OpenNormalSubgroup G) :
46 IsClosed ((U : Subgroup G) : Set G) := by
47 simpa using OpenSubgroup.isClosed U.toOpenSubgroup
49namespace OpenNormalSubgroup
51/-- Pull back an open normal subgroup along a continuous homomorphism. -/
52def comap {H : Type v} [Group H] [TopologicalSpace H]
53 (f : G →* H) (hf : Continuous f) (U : OpenNormalSubgroup H) : OpenNormalSubgroup G :=
54 { toOpenSubgroup := U.toOpenSubgroup.comap f hf
55 isNormal' := by
56 change ((U : Subgroup H).comap f).Normal
57 infer_instance }
59/-- The subgroup underlying the comap of an open subgroup is the subgroup comap. -/
60@[simp, norm_cast]
61theorem toSubgroup_comap {H : Type v} [Group H] [TopologicalSpace H]
62 (f : G →* H) (hf : Continuous f) (U : OpenNormalSubgroup H) :
63 ((OpenNormalSubgroup.comap f hf U : OpenNormalSubgroup G) : Subgroup G) =
64 (U : Subgroup H).comap f :=
65 rfl
67/-- Membership in the comap of an open subgroup is membership after applying the homomorphism. -/
68@[simp]
70 {f : G →* H} {hf : Continuous f} {U : OpenNormalSubgroup H} {x : G} :
71 x ∈ OpenNormalSubgroup.comap f hf U ↔ f x ∈ U :=
72 Iff.rfl
74end OpenNormalSubgroup
76/-- Any open subgroup of a compact topological group has finite quotient. -/
77theorem openSubgroup_finiteQuotient [ContinuousMul G] [CompactSpace G]
78 (U : OpenSubgroup G) :
79 Finite (G ⧸ (U : Subgroup G)) := by
80 exact Subgroup.quotient_finite_of_isOpen (U : Subgroup G) (openSubgroup_isOpen (G := G) U)
82/-- Any open normal subgroup of a compact topological group has finite quotient. -/
83theorem openNormalSubgroup_finiteQuotient [ContinuousMul G] [CompactSpace G]
84 (U : OpenNormalSubgroup G) :
85 Finite (G ⧸ (U : Subgroup G)) := by
86 exact Subgroup.quotient_finite_of_isOpen (U : Subgroup G)
87 (openNormalSubgroup_isOpen (G := G) U)
89/-- In a compact topological group, every element has a positive power in any open subgroup. -/
90theorem exists_pos_pow_mem_openSubgroup [ContinuousMul G] [CompactSpace G]
91 (U : OpenSubgroup G) (g : G) :
92 ∃ n : ℕ, 0 < n ∧ g ^ n ∈ (U : Subgroup G) := by
93 let K : Subgroup G := (U : Subgroup G).normalCore
94 letI : Finite (G ⧸ (U : Subgroup G)) :=
95 openSubgroup_finiteQuotient (G := G) U
96 letI : (U : Subgroup G).FiniteIndex := Subgroup.finiteIndex_of_finite_quotient
97 letI : K.FiniteIndex := Subgroup.finiteIndex_normalCore (H := (U : Subgroup G))
98 have hidx : K.index ≠ 0 := (Subgroup.finiteIndex_iff (H := K)).mp ‹K.FiniteIndex›
99 refine ⟨K.index, Nat.pos_iff_ne_zero.mpr hidx, ?_⟩
100 exact (Subgroup.normalCore_le (U : Subgroup G)) (K.pow_index_mem g)
102/-- In a compact topological group, a subgroup is open iff it is closed and the quotient is finite.
106-/
107theorem subgroup_isOpen_iff_isClosed_finite_quotient [ContinuousMul G] [CompactSpace G]
108 {U : Subgroup G} :
109 IsOpen (U : Set G) ↔ IsClosed (U : Set G) ∧ Finite (G ⧸ U) := by
110 constructor
111 · intro hU
112 exact ⟨Subgroup.isClosed_of_isOpen U hU, Subgroup.quotient_finite_of_isOpen U hU⟩
113 · rintro ⟨hUclosed, hUfinite⟩
114 letI : IsClosed (U : Set G) := hUclosed
115 letI : T1Space (G ⧸ U) := inferInstance
116 letI : Finite (G ⧸ U) := hUfinite
117 letI : DiscreteTopology (G ⧸ U) := inferInstance
118 exact (QuotientGroup.discreteTopology_iff (N := U)).1 inferInstance
120end OpenSubgroups
122end ProCGroups