Source: ProCGroups.Generation.WordProductsAndClosure
1import ProCGroups.Generation.Basic
2import ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne
3import ProCGroups.Profinite.Basic
5/-!
6# Finite word products and subgroup closure
8The word-product filtration is related to multiplication, inversion, and the abstract subgroup
9generated by a set. Under compactness hypotheses its finite levels are compact or closed, which
10supports separation of a finite level by an open normal subgroup and later finite-quotient
11generation arguments.
12-/
14open Set
15open scoped Topology Pointwise
17namespace ProCGroups.Generation
19universe u
21open ProCGroups.ProC
23variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
25section WordProducts
27omit [TopologicalSpace G] [IsTopologicalGroup G] in
28/-- The identity element belongs to the word-product set. -/
29@[simp] theorem wordProducts_one (X : Set G) :
30 wordProducts X 1 = X := by
31 simp only [wordProducts, singleton_mul, one_mul, image_id']
33omit [TopologicalSpace G] [IsTopologicalGroup G] in
34/--
35Multiplying elements from two word-product sets lands in the word-product set with summed
36length.
37-/
38theorem wordProducts_mul_wordProducts (X : Set G) :
39 ∀ m n, wordProducts X m * wordProducts X n = wordProducts X (m + n)
40 | m, 0 => by
41 simp only [wordProducts, mul_singleton, mul_one, image_id', add_zero]
42 | m, n + 1 => by
43 calc
44 wordProducts X m * wordProducts X (n + 1)
45 = wordProducts X m * (wordProducts X n * X) := by
46 rfl
47 _ = (wordProducts X m * wordProducts X n) * X := by
48 rw [mul_assoc]
49 _ = wordProducts X (m + n) * X := by
50 rw [wordProducts_mul_wordProducts X m n]
51 _ = wordProducts X (m + n + 1) := by
52 rfl
54omit [TopologicalSpace G] [IsTopologicalGroup G] in
55/-- The identity element belongs to the corresponding word-product set. -/
56theorem one_mem_wordProducts {X : Set G} (h1 : (1 : G) ∈ X) :
57 ∀ n, (1 : G) ∈ wordProducts X n
58 | 0 => by
59 simp only [wordProducts, mem_singleton_iff]
60 | n + 1 => by
61 exact ⟨1, one_mem_wordProducts h1 n, 1, h1, by simp only [mul_one]⟩
63omit [TopologicalSpace G] [IsTopologicalGroup G] in
64/-- Every word product of elements of \(X\) lies in the subgroup generated by \(X\). -/
65theorem wordProducts_subset_closure (X : Set G) :
66 ∀ n, wordProducts X n ⊆ ((Subgroup.closure X : Subgroup G) : Set G)
67 | 0 => by
68 intro x hx
69 simp only [wordProducts, mem_singleton_iff] at hx
70 simp only [hx, SetLike.mem_coe, one_mem]
71 | n + 1 => by
72 intro x hx
73 rcases hx with ⟨a, ha, b, hb, rfl⟩
74 exact (Subgroup.closure X).mul_mem
75 (wordProducts_subset_closure X n ha)
76 (Subgroup.subset_closure hb)
78omit [TopologicalSpace G] [IsTopologicalGroup G] in
79/-- The word-product set is closed under taking inverses. -/
80theorem wordProducts_inv_mem {X : Set G} (hXinv : X = Inv.inv '' X) :
81 ∀ {n : ℕ} {x : G}, x ∈ wordProducts X n → x⁻¹ ∈ wordProducts X n
82 | 0, x, hx => by
83 simpa [wordProducts] using hx
84 | n + 1, x, hx => by
85 rcases hx with ⟨a, ha, b, hb, rfl⟩
86 have hb' : b⁻¹ ∈ X := by
87 rw [hXinv]
88 exact ⟨b, hb, by simp only⟩
89 have ha' : a⁻¹ ∈ wordProducts X n := wordProducts_inv_mem hXinv ha
90 have hmem : b⁻¹ * a⁻¹ ∈ wordProducts X 1 * wordProducts X n := by
91 exact ⟨b⁻¹, by
92 show b⁻¹ ∈ wordProducts X 1
93 simpa [wordProducts_one] using hb', a⁻¹, ha', rfl⟩
94 have hEq : wordProducts X 1 * wordProducts X n = wordProducts X (1 + n) := by
95 simpa using (wordProducts_mul_wordProducts X 1 n)
96 have hmem' : b⁻¹ * a⁻¹ ∈ wordProducts X (1 + n) := by
97 exact hEq ▸ hmem
98 simpa [Nat.succ_eq_add_one, Nat.add_comm] using hmem'
100omit [TopologicalSpace G] [IsTopologicalGroup G] in
101/-- Word-product sets are monotone in the allowed word length. -/
102theorem wordProducts_mono_len {X : Set G} (h1 : (1 : G) ∈ X) {m n : ℕ} (hmn : m ≤ n) :
103 wordProducts X m ⊆ wordProducts X n := by
104 rcases Nat.exists_eq_add_of_le hmn with ⟨k, rfl⟩
105 intro x hx
106 have hk : (1 : G) ∈ wordProducts X k := one_mem_wordProducts h1 k
107 have hmem : x * 1 ∈ wordProducts X m * wordProducts X k := by
108 exact ⟨x, hx, 1, hk, by simp only [mul_one]⟩
109 simpa [wordProducts_mul_wordProducts, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] using hmem
111omit [TopologicalSpace G] [IsTopologicalGroup G] in
112/-- The subgroup generated by word products has the stated closure property. -/
113theorem subgroupClosure_eq_iUnion_wordProducts {X : Set G}
114 (hXinv : X = Inv.inv '' X) :
115 (((Subgroup.closure X : Subgroup G) : Set G)) = ⋃ n, wordProducts X n := by
116 let S : Subgroup G := {
117 carrier := {g : G | ∃ n : ℕ, g ∈ wordProducts X n}
118 one_mem' := ⟨0, by simp only [wordProducts, mem_singleton_iff]⟩
119 mul_mem' := by
120 intro a b ha hb
121 rcases ha with ⟨m, hm⟩
122 rcases hb with ⟨n, hn⟩
123 refine ⟨m + n, ?_⟩
124 have hmem : a * b ∈ wordProducts X m * wordProducts X n := by
125 exact ⟨a, hm, b, hn, rfl⟩
126 simpa [wordProducts_mul_wordProducts] using hmem
127 inv_mem' := by
128 intro a ha
129 rcases ha with ⟨n, hn⟩
130 exact ⟨n, wordProducts_inv_mem hXinv hn⟩
131 }
132 have hXsubset : X ⊆ (S : Set G) := by
133 intro x hx
134 exact ⟨1, by simpa using hx⟩
135 have hle : Subgroup.closure X ≤ S := (Subgroup.closure_le (K := S)).mpr hXsubset
136 ext g
137 constructor
138 · intro hg
139 rcases hle hg with ⟨n, hn⟩
140 exact mem_iUnion.mpr ⟨n, hn⟩
141 · intro hg
142 rcases mem_iUnion.mp hg with ⟨n, hn⟩
143 exact wordProducts_subset_closure X n hn
145/-- Every bounded word-product set of a closed subset of a compact group is compact. -/
146theorem wordProducts_isCompact [CompactSpace G] {X : Set G}
147 (hXclosed : IsClosed X) :
148 ∀ n, IsCompact (wordProducts X n)
149 | 0 => by
150 simp only [wordProducts, finite_singleton, Finite.isCompact]
151 | n + 1 => by
152 have hprev : IsCompact (wordProducts X n) := wordProducts_isCompact hXclosed n
153 have hEq :
154 wordProducts X (n + 1) =
155 (fun p : G × G => p.1 * p.2) '' ((wordProducts X n) ×ˢ X) := by
156 ext x
157 constructor
158 · intro hx
159 rcases hx with ⟨a, ha, b, hb, rfl⟩
160 exact ⟨(a, b), ⟨ha, hb⟩, rfl⟩
161 · intro hx
162 rcases hx with ⟨⟨a, b⟩, hab, rfl⟩
163 exact ⟨a, hab.1, b, hab.2, rfl⟩
164 rw [hEq]
165 exact (hprev.prod hXclosed.isCompact).image (continuous_fst.mul continuous_snd)
167/-- The word-product set is closed in the profinite topology. -/
168theorem wordProducts_isClosed [CompactSpace G] [T2Space G] {X : Set G}
169 (hXclosed : IsClosed X) (n : ℕ) :
170 IsClosed (wordProducts X n) :=
171 (wordProducts_isCompact (G := G) hXclosed n).isClosed
173/-- A finite subgroup of a profinite group can be separated from 1 by an open normal subgroup. -/
174theorem exists_openNormalSubgroup_inf_eq_bot_of_finite
175 [CompactSpace G] [TotallyDisconnectedSpace G]
176 (K : Subgroup G) [Finite K] :
177 ∃ U : OpenNormalSubgroup G, ((U : Subgroup G) ⊓ K) = ⊥ := by
178 classical
179 letI : Fintype K := Fintype.ofFinite K
180 let topU : OpenNormalSubgroup G :=
181 { toSubgroup := ⊤
182 isOpen' := isOpen_univ
183 isNormal' := inferInstance }
184 have hsep :
185 ∀ k : K, k ≠ 1 → ∃ U : OpenNormalSubgroup G, (k : G) ∉ (U : Subgroup G) := by
186 intro k hk
187 have hnotall : ¬ ∀ U : OpenNormalSubgroup G, (k : G) ∈ (U : Subgroup G) := by
188 intro hkall
189 have hkone : (k : G) = 1 :=
190 ProfiniteGrp.eq_one_of_mem_all_openNormalSubgroups (G := G) hkall
191 apply hk
192 apply Subtype.ext
193 simpa using hkone
194 rcases not_forall.mp hnotall with ⟨U, hkU⟩
195 exact ⟨U, hkU⟩
196 choose U hU using hsep
197 let s : Finset K := Finset.univ.filter fun k : K => k ≠ 1
198 by_cases hs : s.Nonempty
199 · let t : Finset s := s.attach
200 have ht : t.Nonempty := by simpa [t] using hs
201 let V : OpenNormalSubgroup G := t.inf' ht fun k => U k.1 ((Finset.mem_filter.mp k.2).2)
202 refine ⟨V, ?_⟩
203 rw [Subgroup.eq_bot_iff_forall]
204 intro x hx
205 let k : K := ⟨x, hx.2⟩
206 by_cases hk : k = 1
207 · exact congrArg Subtype.val hk
208 · have hk_mem : k ∈ s := by
209 simp only [ne_eq, Finset.mem_filter, Finset.mem_univ, hk, not_false_eq_true, and_self, s]
210 have hxV :
211 x ∈ ((U k hk : OpenNormalSubgroup G) : Subgroup G) := by
212 exact (show (V : OpenNormalSubgroup G) ≤ U k hk from by
213 dsimp [V]
214 exact Finset.inf'_le (s := t)
215 (f := fun k => U k.1 ((Finset.mem_filter.mp k.2).2))
216 (h := by
217 change ⟨k, hk_mem⟩ ∈ s.attach
218 simp only [Finset.mem_attach])) hx.1
219 have hkV : (k : G) ∈ ((U k hk : OpenNormalSubgroup G) : Subgroup G) := by
220 simpa [k] using hxV
221 exact False.elim (hU k hk hkV)
222 · refine ⟨topU, ?_⟩
223 rw [Subgroup.eq_bot_iff_forall]
224 intro x hx
225 let k : K := ⟨x, hx.2⟩
226 have hk_eq : k = 1 := by
227 by_contra hk
228 exact hs ⟨k, by simp only [ne_eq, Finset.mem_filter, Finset.mem_univ, hk,
229 not_false_eq_true, and_self, s]⟩
230 exact congrArg Subtype.val hk_eq
232end WordProducts
234end ProCGroups.Generation