Yamaguchi Lean 4 Library
ProCGroups/Generation/WordProductsAndClosure.lean
ProCGroups/Generation/WordProductsAndClosure/Source

ProCGroups/Generation/WordProductsAndClosure.lean

1import ProCGroups.Generation.Basic
2import ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne
3import ProCGroups.Profinite.Basic
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/Generation/WordProductsAndClosure.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Topological generation
16Develops topological generation, generating families, convergence-to-one criteria, quotient generation, and profinite generation lemmas.
17-/
19open Set
20open scoped Topology Pointwise
22namespace ProCGroups.Generation
24universe u
26open ProCGroups.ProC
28variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
30section WordProducts
32omit [TopologicalSpace G] [IsTopologicalGroup G] in
33@[simp] theorem wordProducts_one (X : Set G) :
34 wordProducts X 1 = X := by
35 simp only [wordProducts, singleton_mul, one_mul, image_id']
37omit [TopologicalSpace G] [IsTopologicalGroup G] in
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
51 _ = wordProducts X (m + n + 1) := by
52 rfl
54omit [TopologicalSpace G] [IsTopologicalGroup G] in
55theorem one_mem_wordProducts {X : Set G} (h1 : (1 : G) ∈ X) :
56 ∀ n, (1 : G) ∈ wordProducts X n
57 | 0 => by
58 simp only [wordProducts, mem_singleton_iff]
59 | n + 1 => by
60 exact ⟨1, one_mem_wordProducts h1 n, 1, h1, by simp only [mul_one]⟩
62omit [TopologicalSpace G] [IsTopologicalGroup G] in
63theorem wordProducts_subset_closure (X : Set G) :
64 ∀ n, wordProducts X n ⊆ ((Subgroup.closure X : Subgroup G) : Set G)
65 | 0 => by
66 intro x hx
67 simp only [wordProducts, mem_singleton_iff] at hx
68 simp only [hx, SetLike.mem_coe, one_mem]
69 | n + 1 => by
70 intro x hx
71 rcases hx with ⟨a, ha, b, hb, rfl⟩
72 exact (Subgroup.closure X).mul_mem
74 (Subgroup.subset_closure hb)
76omit [TopologicalSpace G] [IsTopologicalGroup G] in
77theorem wordProducts_inv_mem {X : Set G} (hXinv : X = Inv.inv '' X) :
78 ∀ {n : ℕ} {x : G}, x ∈ wordProducts X n → x⁻¹ ∈ wordProducts X n
79 | 0, x, hx => by
80 simpa [wordProducts] using hx
81 | n + 1, x, hx => by
82 rcases hx with ⟨a, ha, b, hb, rfl⟩
83 have hb' : b⁻¹ ∈ X := by
84 rw [hXinv]
85 exact ⟨b, hb, by simp only⟩
86 have ha' : a⁻¹ ∈ wordProducts X n := wordProducts_inv_mem hXinv ha
87 have hmem : b⁻¹ * a⁻¹ ∈ wordProducts X 1 * wordProducts X n := by
88 exact ⟨b⁻¹, by
89 show b⁻¹ ∈ wordProducts X 1
90 simpa [wordProducts_one] using hb', a⁻¹, ha', rfl⟩
91 have hEq : wordProducts X 1 * wordProducts X n = wordProducts X (1 + n) := by
92 simpa using (wordProducts_mul_wordProducts X 1 n)
93 have hmem' : b⁻¹ * a⁻¹ ∈ wordProducts X (1 + n) := by
94 exact hEq ▸ hmem
95 simpa [Nat.succ_eq_add_one, Nat.add_comm] using hmem'
97omit [TopologicalSpace G] [IsTopologicalGroup G] in
98theorem wordProducts_mono_len {X : Set G} (h1 : (1 : G) ∈ X) {m n : ℕ} (hmn : m ≤ n) :
99 wordProducts X m ⊆ wordProducts X n := by
100 rcases Nat.exists_eq_add_of_le hmn with ⟨k, rfl⟩
101 intro x hx
102 have hk : (1 : G) ∈ wordProducts X k := one_mem_wordProducts h1 k
103 have hmem : x * 1 ∈ wordProducts X m * wordProducts X k := by
104 exact ⟨x, hx, 1, hk, by simp only [mul_one]⟩
105 simpa [wordProducts_mul_wordProducts, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] using hmem
107omit [TopologicalSpace G] [IsTopologicalGroup G] in
109 (hXinv : X = Inv.inv '' X) :
110 (((Subgroup.closure X : Subgroup G) : Set G)) = ⋃ n, wordProducts X n := by
111 let S : Subgroup G := {
112 carrier := {g : G | ∃ n : ℕ, g ∈ wordProducts X n}
113 one_mem' := ⟨0, by simp only [wordProducts, mem_singleton_iff]⟩
114 mul_mem' := by
115 intro a b ha hb
116 rcases ha with ⟨m, hm⟩
117 rcases hb with ⟨n, hn⟩
118 refine ⟨m + n, ?_⟩
119 have hmem : a * b ∈ wordProducts X m * wordProducts X n := by
120 exact ⟨a, hm, b, hn, rfl⟩
122 inv_mem' := by
123 intro a ha
124 rcases ha with ⟨n, hn⟩
125 exact ⟨n, wordProducts_inv_mem hXinv hn⟩
126 }
127 have hXsubset : X ⊆ (S : Set G) := by
128 intro x hx
129 exact ⟨1, by simpa using hx⟩
130 have hle : Subgroup.closure X ≤ S := (Subgroup.closure_le (K := S)).mpr hXsubset
131 ext g
132 constructor
133 · intro hg
134 rcases hle hg with ⟨n, hn⟩
135 exact mem_iUnion.mpr ⟨n, hn⟩
136 · intro hg
137 rcases mem_iUnion.mp hg with ⟨n, hn⟩
140theorem wordProducts_isCompact [CompactSpace G] {X : Set G}
141 (hXclosed : IsClosed X) :
143 | 0 => by
144 simp only [wordProducts, finite_singleton, Finite.isCompact]
145 | n + 1 => by
146 have hprev : IsCompact (wordProducts X n) := wordProducts_isCompact hXclosed n
147 have hEq :
148 wordProducts X (n + 1) =
149 (fun p : G × G => p.1 * p.2) '' ((wordProducts X n) ×ˢ X) := by
150 ext x
151 constructor
152 · intro hx
153 rcases hx with ⟨a, ha, b, hb, rfl⟩
154 exact ⟨(a, b), ⟨ha, hb⟩, rfl⟩
155 · intro hx
156 rcases hx with ⟨⟨a, b⟩, hab, rfl⟩
157 exact ⟨a, hab.1, b, hab.2, rfl⟩
158 rw [hEq]
159 exact (hprev.prod hXclosed.isCompact).image (continuous_fst.mul continuous_snd)
161theorem wordProducts_isClosed [CompactSpace G] [T2Space G] {X : Set G}
162 (hXclosed : IsClosed X) (n : ℕ) :
163 IsClosed (wordProducts X n) :=
164 (wordProducts_isCompact (G := G) hXclosed n).isClosed
166/-- A finite subgroup of a profinite group can be separated from `1` by an open normal subgroup. -/
168 (hG : IsProfiniteGroup G) (K : Subgroup G) [Finite K] :
169 ∃ U : OpenNormalSubgroup G, ((U : Subgroup G) ⊓ K) = ⊥ := by
170 classical
171 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
172 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
173 letI : Fintype K := Fintype.ofFinite K
174 let topU : OpenNormalSubgroup G :=
175 { toSubgroup := ⊤
176 isOpen' := isOpen_univ
177 isNormal' := inferInstance }
178 have hsep :
179 ∀ k : K, k ≠ 1 → ∃ U : OpenNormalSubgroup G, (k : G) ∉ (U : Subgroup G) := by
180 intro k hk
181 have hnotall : ¬ ∀ U : OpenNormalSubgroup G, (k : G) ∈ (U : Subgroup G) := by
182 intro hkall
183 have hkone : (k : G) = 1 :=
185 apply hk
186 apply Subtype.ext
187 simpa using hkone
188 rcases not_forall.mp hnotall with ⟨U, hkU⟩
189 exact ⟨U, hkU⟩
190 choose U hU using hsep
191 let s : Finset K := Finset.univ.filter fun k : K => k ≠ 1
192 by_cases hs : s.Nonempty
193 · let t : Finset s := s.attach
194 have ht : t.Nonempty := by simpa [t] using hs
195 let V : OpenNormalSubgroup G := t.inf' ht fun k => U k.1 ((Finset.mem_filter.mp k.2).2)
196 refine ⟨V, ?_⟩
197 rw [Subgroup.eq_bot_iff_forall]
198 intro x hx
199 let k : K := ⟨x, hx.2⟩
200 by_cases hk : k = 1
201 · exact congrArg Subtype.val hk
202 · have hk_mem : k ∈ s := by
203 simp only [ne_eq, Finset.mem_filter, Finset.mem_univ, hk, not_false_eq_true, and_self, s]
204 have hxV :
205 x ∈ ((U k hk : OpenNormalSubgroup G) : Subgroup G) := by
206 exact (show (V : OpenNormalSubgroup G) ≤ U k hk from by
207 dsimp [V]
208 exact Finset.inf'_le (s := t)
209 (f := fun k => U k.1 ((Finset.mem_filter.mp k.2).2))
210 (h := by
211 change ⟨k, hk_mem⟩ ∈ s.attach
212 simp only [Finset.mem_attach])) hx.1
213 have hkV : (k : G) ∈ ((U k hk : OpenNormalSubgroup G) : Subgroup G) := by
214 simpa [k] using hxV
215 exact False.elim (hU k hk hkV)
216 · refine ⟨topU, ?_⟩
217 rw [Subgroup.eq_bot_iff_forall]
218 intro x hx
219 let k : K := ⟨x, hx.2⟩
220 have hk_eq : k = 1 := by
221 by_contra hk
222 exact hs ⟨k, by simp only [ne_eq, Finset.mem_filter, Finset.mem_univ, hk, not_false_eq_true, and_self, s]⟩
223 exact congrArg Subtype.val hk_eq
225end WordProducts
227end ProCGroups.Generation