Source: ProCGroups.Profinite.OpenSubgroups
1import Mathlib.GroupTheory.OrderOfElement
2import Mathlib.Topology.Algebra.ClopenNhdofOne
4/-!
5# Open subgroups of compact groups
7This module records openness and closedness properties of open (normal) subgroups, constructs
8their pullbacks, and proves that they have finite index in compact topological groups.
9-/
11open Set
12open scoped Topology Pointwise
14namespace ProCGroups
16universe u v
18section OpenSubgroups
20variable {G : Type u} [Group G] [TopologicalSpace G]
22/-- An open subgroup is open as a subset. -/
23theorem openSubgroup_isOpen (U : OpenSubgroup G) :
24 IsOpen ((U : Subgroup G) : Set G) := by
25 exact U.isOpen
27/-- An open subgroup is closed as a subset. -/
28theorem openSubgroup_isClosed [ContinuousMul G] (U : OpenSubgroup G) :
29 IsClosed ((U : Subgroup G) : Set G) := by
30 simpa using OpenSubgroup.isClosed U
32/-- An open normal subgroup is open as a subset. -/
33theorem openNormalSubgroup_isOpen (U : OpenNormalSubgroup G) :
34 IsOpen ((U : Subgroup G) : Set G) := by
35 exact U.toOpenSubgroup.isOpen
37/-- An open normal subgroup is closed as a subset. -/
38theorem openNormalSubgroup_isClosed [ContinuousMul G] (U : OpenNormalSubgroup G) :
39 IsClosed ((U : Subgroup G) : Set G) := by
40 simpa using OpenSubgroup.isClosed U.toOpenSubgroup
42namespace OpenNormalSubgroup
44/-- Pull back an open normal subgroup along a continuous homomorphism. -/
45def comap {H : Type v} [Group H] [TopologicalSpace H]
46 (f : G →* H) (hf : Continuous f) (U : OpenNormalSubgroup H) : OpenNormalSubgroup G :=
47 { toOpenSubgroup := U.toOpenSubgroup.comap f hf
48 isNormal' := by
49 change ((U : Subgroup H).comap f).Normal
50 infer_instance }
52/-- The subgroup underlying the comap of an open subgroup is the subgroup comap. -/
53@[simp, norm_cast]
54theorem toSubgroup_comap {H : Type v} [Group H] [TopologicalSpace H]
55 (f : G →* H) (hf : Continuous f) (U : OpenNormalSubgroup H) :
56 ((OpenNormalSubgroup.comap f hf U : OpenNormalSubgroup G) : Subgroup G) =
57 (U : Subgroup H).comap f :=
58 rfl
60/-- Membership in the comap of an open subgroup is membership after applying the homomorphism. -/
61@[simp]
62theorem mem_comap {H : Type v} [Group H] [TopologicalSpace H]
63 {f : G →* H} {hf : Continuous f} {U : OpenNormalSubgroup H} {x : G} :
64 x ∈ OpenNormalSubgroup.comap f hf U ↔ f x ∈ U :=
65 Iff.rfl
67end OpenNormalSubgroup
69/--
70An open subgroup of a compact topological group has finite coset space, equivalently finite
71index.
72-/
73theorem openSubgroup_finiteQuotient [ContinuousMul G] [CompactSpace G]
74 (U : OpenSubgroup G) :
75 Finite (G ⧸ (U : Subgroup G)) := by
76 exact Subgroup.quotient_finite_of_isOpen (U : Subgroup G) (openSubgroup_isOpen (G := G) U)
78/-- Any open normal subgroup of a compact topological group has finite quotient. -/
79theorem openNormalSubgroup_finiteQuotient [ContinuousMul G] [CompactSpace G]
80 (U : OpenNormalSubgroup G) :
81 Finite (G ⧸ (U : Subgroup G)) := by
82 exact Subgroup.quotient_finite_of_isOpen (U : Subgroup G)
83 (openNormalSubgroup_isOpen (G := G) U)
85/-- In a compact topological group, every element has a positive power in any open subgroup. -/
86theorem exists_pos_pow_mem_openSubgroup [ContinuousMul G] [CompactSpace G]
87 (U : OpenSubgroup G) (g : G) :
88 ∃ n : ℕ, 0 < n ∧ g ^ n ∈ (U : Subgroup G) := by
89 let K : Subgroup G := (U : Subgroup G).normalCore
90 letI : Finite (G ⧸ (U : Subgroup G)) :=
91 openSubgroup_finiteQuotient (G := G) U
92 letI : (U : Subgroup G).FiniteIndex := Subgroup.finiteIndex_of_finite_quotient
93 letI : K.FiniteIndex := Subgroup.finiteIndex_normalCore (H := (U : Subgroup G))
94 have hidx : K.index ≠ 0 := (Subgroup.finiteIndex_iff (H := K)).mp ‹K.FiniteIndex›
95 refine ⟨K.index, Nat.pos_iff_ne_zero.mpr hidx, ?_⟩
96 exact (Subgroup.normalCore_le (U : Subgroup G)) (K.pow_index_mem g)
98/--
99In a compact topological group, a subgroup is open if and only if it is closed and the quotient
100is finite. Equivalently, the subgroup is closed of finite index; in this version, Finite
101(\(G/U\)) is the most direct encoding of finite index.
102-/
103theorem subgroup_isOpen_iff_isClosed_finite_quotient [ContinuousMul G] [CompactSpace G]
104 {U : Subgroup G} :
105 IsOpen (U : Set G) ↔ IsClosed (U : Set G) ∧ Finite (G ⧸ U) := by
106 constructor
107 · intro hU
108 exact ⟨Subgroup.isClosed_of_isOpen U hU, Subgroup.quotient_finite_of_isOpen U hU⟩
109 · rintro ⟨hUclosed, hUfinite⟩
110 letI : IsClosed (U : Set G) := hUclosed
111 letI : T1Space (G ⧸ U) := inferInstance
112 letI : Finite (G ⧸ U) := hUfinite
113 letI : DiscreteTopology (G ⧸ U) := inferInstance
114 exact (QuotientGroup.discreteTopology_iff (N := U)).1 inferInstance
116end OpenSubgroups
118end ProCGroups