Source: ProCGroups.Generation.Convergence

1import Mathlib.Topology.Compactification.OnePoint.Basic

2import ProCGroups.Generation.Basic

3import ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne

4import ProCGroups.Profinite.Basic

6/-!

7# Convergence of generating sets in profinite groups

9The open-subgroup convergence predicate is shown to be stable under pointed continuous maps,

10subsets, and finite modifications. For a generating set containing one, the module identifies

11its closure with a compact one-point extension and proves that the convergent set is closed.

12-/

14open Set

15open scoped Topology Pointwise

17namespace ProCGroups.Generation

19universe u v

21open ProCGroups.ProC

23variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

25/--

26A continuous map between topological groups that sends \(1\) to \(1\) carries convergent sets to

27convergent sets, provided the source is profinite.

28-/

29theorem ConvergesToOneAlongOpenSubgroups.image_of_continuous_pointed

30 {H : Type v} [Group H] [TopologicalSpace H]

31 [CompactSpace G] [TotallyDisconnectedSpace G]

32 {f : G → H} (hf : Continuous f) (hf1 : f 1 = 1)

33 {X : Set G} (hX : ConvergesToOneAlongOpenSubgroups (G := G) X) :

34 ConvergesToOneAlongOpenSubgroups (G := H) (f '' X) := by

35 intro U

36 have hpre : IsOpen (f ⁻¹' (U : Set H)) :=

37 (openSubgroup_isOpen (G := H) U).preimage hf

38 have h1pre : (1 : G) ∈ f ⁻¹' (U : Set H) := by

39 simp only [mem_preimage, hf1, SetLike.mem_coe, one_mem]

40 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hpre h1pre with ⟨V, hVU⟩

41 have hsubset : (f '' X) \ (U : Set H) ⊆ f '' (X \ (V : Set G)) := by

42 intro y hy

43 rcases hy with ⟨hyX, hyU⟩

44 rcases hyX with ⟨x, hxX, rfl⟩

45 refine ⟨x, ⟨hxX, ?_⟩, rfl⟩

46 intro hxV

47 exact hyU (hVU hxV)

48 exact (hX V.toOpenSubgroup).image f |>.subset hsubset

50omit [IsTopologicalGroup G] in

51/-- Passing to a subset preserves convergence to \(1\). -/

52theorem ConvergesToOneAlongOpenSubgroups.mono {X Y : Set G}

53 (hX : ConvergesToOneAlongOpenSubgroups (G := G) X) (hYX : Y ⊆ X) :

54 ConvergesToOneAlongOpenSubgroups (G := G) Y := by

55 intro U

56 exact (hX U).subset (by

57 intro y hy

58 exact ⟨hYX hy.1, hy.2⟩)

60omit [IsTopologicalGroup G] in

61/-- Finite enlargements preserve convergence to \(1\). -/

62theorem ConvergesToOneAlongOpenSubgroups.union_finite {X F : Set G}

63 (hX : ConvergesToOneAlongOpenSubgroups (G := G) X) (hF : F.Finite) :

64 ConvergesToOneAlongOpenSubgroups (G := G) (X ∪ F) := by

65 intro U

66 have h1 : (X \ (U : Set G)).Finite := hX U

67 have h2 : (F \ (U : Set G)).Finite := hF.subset (by

68 intro y hy

69 exact hy.1)

70 have hsubset : (X ∪ F) \ (U : Set G) ⊆ (X \ (U : Set G)) ∪ (F \ (U : Set G)) := by

71 intro y hy

72 rcases hy with ⟨hyXF, hyU⟩

73 rcases hyXF with hyX | hyF

74 · exact Or.inl ⟨hyX, hyU⟩

75 · exact Or.inr ⟨hyF, hyU⟩

76 exact (h1.union h2).subset hsubset

78omit [IsTopologicalGroup G] in

79/--

80Convergence to \(1\) is preserved and reflected by the indicated finite union, insertion, or

81continuous equivalence operation.

82-/

83theorem ConvergesToOneAlongOpenSubgroups.union_finite_iff {X F : Set G}

84 (hF : F.Finite) :

85 ConvergesToOneAlongOpenSubgroups (G := G) (X ∪ F) ↔ ConvergesToOneAlongOpenSubgroups (G :=

86 G) X := by

87 constructor

88 · intro h

89 exact ConvergesToOneAlongOpenSubgroups.mono (G := G) h (by

90 intro x hx

91 exact Or.inl hx)

92 · intro h

93 exact ConvergesToOneAlongOpenSubgroups.union_finite (G := G) h hF

95omit [IsTopologicalGroup G] in

96/--

97Convergence to \(1\) is preserved and reflected by the indicated finite union, insertion, or

98continuous equivalence operation.

99-/

100theorem ConvergesToOneAlongOpenSubgroups.insert_iff {X : Set G} {x : G} :

101 ConvergesToOneAlongOpenSubgroups (G := G) (Set.insert x X) ↔

102 ConvergesToOneAlongOpenSubgroups (G := G) X := by

103 have hEq : Set.insert x X = X ∪ ({x} : Set G) := by

104 ext y

105 constructor

106 · intro hy

107 rcases Set.mem_insert_iff.mp hy with rfl | hyX

108 · exact Or.inr (by simp only [mem_singleton_iff])

109 · exact Or.inl hyX

110 · intro hy

111 rcases hy with hyX | hyx

112 · exact Set.mem_insert_iff.mpr (Or.inr hyX)

113 · exact Set.mem_insert_iff.mpr (Or.inl (by simpa using hyx))

114 rw [hEq]

115 exact ConvergesToOneAlongOpenSubgroups.union_finite_iff (G := G) (X := X) (F := ({x} : Set G))

116 (Set.finite_singleton x)

117

118omit [IsTopologicalGroup G] in

119/--

120Convergence to \(1\) is preserved and reflected by the indicated finite union, insertion, or

121continuous equivalence operation.

122-/

123theorem ConvergesToOneAlongOpenSubgroups.union_one_iff {X : Set G} :

124 ConvergesToOneAlongOpenSubgroups (G := G) (X ∪ ({1} : Set G)) ↔

125 ConvergesToOneAlongOpenSubgroups (G := G) X := by

126 exact ConvergesToOneAlongOpenSubgroups.union_finite_iff (G := G) (X := X) (F := ({1} : Set G))

127 (Set.finite_singleton 1)

128

129/--

130A set converging to \(1\) is discrete away from \(1\), and if it is infinite its closure is

131obtained by adjoining the unique possible limit point \(1\).

132-/

133theorem closure_generatorsConvergingToOne

134 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] {X : Set G}

135 (hX : ConvergesToOneAlongOpenSubgroups (G := G) X) :

136 IsDiscrete (X \ {1}) ∧

137 (Set.Infinite X → closure X = X ∪ ({1} : Set G)) := by

138 refine ⟨?_, ?_⟩

139 · rw [isDiscrete_iff_forall_mem_exists_isOpen]

140 intro y hy

141 have hy1 : y ≠ 1 := by simpa using hy.2

142 let W : Set G := ({y} : Set G)ᶜ

143 have hWopen : IsOpen W := isClosed_singleton.isOpen_compl

144 have h1W : (1 : G) ∈ W := by simpa [W, eq_comm] using hy1

145 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hWopen h1W with ⟨U, hUW⟩

146 have hyU : y ∉ (U : Set G) := by

147 intro hyU

148 have hyW : y ∈ W := hUW hyU

149 simp only [mem_compl_iff, mem_singleton_iff, not_true_eq_false, W] at hyW

150 let V : Set G := (fun z : G => y⁻¹ * z) ⁻¹' (U : Set G)

151 have hVopen : IsOpen V := by

152 exact (openNormalSubgroup_isOpen (G := G) U).preimage

153 (continuous_const.mul continuous_id)

154 have hyV : y ∈ V := by

155 simp only [mem_preimage, inv_mul_cancel, SetLike.mem_coe, one_mem, V]

156 have hsubset : V ∩ (X \ ({1} : Set G)) ⊆ X \ (U : Set G) := by

157 intro z hz

158 rcases hz with ⟨hzV, hzX⟩

159 refine ⟨hzX.1, ?_⟩

160 intro hzU

161 have hmem : z * (y⁻¹ * z)⁻¹ ∈ (U : Subgroup G) := U.mul_mem hzU (U.inv_mem hzV)

162 have : y ∈ (U : Subgroup G) := by

163 simpa [mul_assoc] using hmem

164 exact hyU this

165 have hfinite : (V ∩ (X \ ({1} : Set G))).Finite := by

166 exact (hX U.toOpenSubgroup).subset hsubset

167 rcases (isDiscrete_iff_forall_mem_exists_isOpen.mp hfinite.isDiscrete) y ⟨hyV, hy⟩ with

168 ⟨V', hV'open, hV'⟩

169 refine ⟨V' ∩ V, hV'open.inter hVopen, ?_⟩

170 simpa [Set.inter_assoc, Set.inter_left_comm, Set.inter_comm] using hV'

171 · intro hXinfinite

172 apply subset_antisymm

173 · intro y hycl

174 by_cases hy1 : y = 1

175 · simp only [union_singleton, hy1, mem_insert_iff, true_or]

176 · by_cases hyX : y ∈ X

177 · simp only [union_singleton, mem_insert_iff, hy1, hyX, or_true]

178 · let W : Set G := ({y} : Set G)ᶜ

179 have hWopen : IsOpen W := isClosed_singleton.isOpen_compl

180 have h1W : (1 : G) ∈ W := by simpa [W, eq_comm] using hy1

181 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hWopen h1W with

182 ⟨U, hUW⟩

183 have hyU : y ∉ (U : Set G) := by

184 intro hyU

185 have hyW : y ∈ W := hUW hyU

186 simp only [mem_compl_iff, mem_singleton_iff, not_true_eq_false, W] at hyW

187 let V : Set G := (fun z : G => y⁻¹ * z) ⁻¹' (U : Set G)

188 have hVopen : IsOpen V := by

189 exact (openNormalSubgroup_isOpen (G := G) U).preimage

190 (continuous_const.mul continuous_id)

191 have hyV : y ∈ V := by

192 simp only [mem_preimage, inv_mul_cancel, SetLike.mem_coe, one_mem, V]

193 have hsubset : V ∩ X ⊆ X \ (U : Set G) := by

194 intro z hz

195 rcases hz with ⟨hzV, hzX⟩

196 refine ⟨hzX, ?_⟩

197 intro hzU

198 have hmem : z * (y⁻¹ * z)⁻¹ ∈ (U : Subgroup G) := U.mul_mem hzU (U.inv_mem hzV)

199 have : y ∈ (U : Subgroup G) := by

200 simpa [mul_assoc] using hmem

201 exact hyU this

202 have hfinite : (V ∩ X).Finite := by

203 exact (hX U.toOpenSubgroup).subset hsubset

204 have hclosed : IsClosed (V ∩ X) := hfinite.isClosed

205 have hyVX : y ∉ V ∩ X := by

206 simp only [mem_inter_iff, hyV, hyX, and_false, not_false_eq_true]

207 have hne :=

208 (mem_closure_iff.1 hycl) (V \ (V ∩ X)) (hVopen.sdiff hclosed) ⟨hyV, hyVX⟩

209 rcases hne with ⟨z, hz⟩

210 exact False.elim (hz.1.2 ⟨hz.1.1, hz.2⟩)

211 · intro y hy

212 rcases hy with hyX | hy1

213 · exact subset_closure hyX

214 · subst hy1

215 refine mem_closure_iff.2 ?_

216 intro W hWopen h1W

217 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hWopen h1W with

218 ⟨U, hUW⟩

219 have hproper : ¬ X ⊆ X \ (U : Set G) := by

220 intro hsub

221 have hXfinite : X.Finite := (hX U.toOpenSubgroup).subset hsub

222 exact hXinfinite hXfinite

223 rcases Set.not_subset.1 hproper with ⟨x, hxX, hxnot⟩

224 have hxU : x ∈ (U : Set G) := by

225 by_contra hxU

226 exact hxnot ⟨hxX, hxU⟩

227 exact ⟨x, hUW hxU, hxX⟩

228

229/-- A convergent set containing its only possible limit point \(1\) is closed. -/

230theorem ConvergesToOneAlongOpenSubgroups.isClosed_of_one_mem

231 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] {X : Set G}

232 (hX : ConvergesToOneAlongOpenSubgroups (G := G) X) (h1 : (1 : G) ∈ X) :

233 IsClosed X := by

234 rcases closure_generatorsConvergingToOne (G := G) hX with ⟨_, hclosure⟩

235 by_cases hfinite : X.Finite

236 · exact hfinite.isClosed

237 · have hEq : closure X = X := by

238 calc

239 closure X = X ∪ ({1} : Set G) := by

240 exact hclosure hfinite

241 _ = X := by simp only [union_singleton, h1, insert_eq_of_mem]

242 exact closure_eq_iff_isClosed.mp hEq

243

244/--

245If \(X\) is infinite, converges to \(1\), and does not contain \(1\), then \(closure X\) is

246homeomorphic to the one-point compactification of the discrete space \(X\).

247-/

248noncomputable def closure_generatorsConvergingToOne_homeomorph_onePoint

249 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] {X : Set G}

250 (hX : ConvergesToOneAlongOpenSubgroups (G := G) X) (hXinfinite : X.Infinite) (h1X : (1 : G)

251 ∉ X) :

252 OnePoint X ≃ₜ closure X := by

253 classical

254 rcases closure_generatorsConvergingToOne (G := G) hX with ⟨hdisc, hclosure⟩

255 have hdiff : X \ ({1} : Set G) = X := by

256 ext x

257 by_cases hx : x = 1

258 · simp only [h1X, not_false_eq_true, sdiff_singleton_eq_self, hx]

259 · simp only [mem_sdiff, mem_singleton_iff, hx, not_false_eq_true, and_true]

260 have hdiscX : IsDiscrete X := by

261 simpa [hdiff] using hdisc

262 letI : DiscreteTopology X := (isDiscrete_iff_discreteTopology).1 hdiscX

263 have h1closure : (1 : G) ∈ closure X := by

264 have : (1 : G) ∈ X ∪ ({1} : Set G) := by simp only [union_singleton, mem_insert_iff, true_or]

265 rw [hclosure hXinfinite]

266 simp only [union_singleton, mem_insert_iff, true_or]

267 let toClosure : OnePoint X → closure X

268 | OnePoint.infty => ⟨1, h1closure⟩

269 | (x : X) => ⟨x.1, subset_closure x.2⟩

270 let fromClosure : closure X → OnePoint X := fun y =>

271 if hy : (y : G) = 1 then

272 OnePoint.infty

273 else

274 OnePoint.some ⟨(y : G), by

275 have hy' : (y : G) ∈ X ∪ ({1} : Set G) := by

276 simpa [hclosure hXinfinite] using y.2

277 rcases hy' with hyX | hy1

278 · exact hyX

279 · exact False.elim (hy hy1)⟩

280 have hleft : Function.LeftInverse fromClosure toClosure := by

281 intro z

282 refine OnePoint.rec ?_ ?_ z

283 · simp only [↓reduceDIte, fromClosure, toClosure]

284 · intro x

285 have hx1 : (x : G) ≠ 1 := by

286 intro hx1

287 exact h1X (hx1 ▸ x.2)

288 simp only [hx1, ↓reduceDIte, Subtype.coe_eta, fromClosure, toClosure]

289 have hright : Function.RightInverse fromClosure toClosure := by

290 intro y

291 by_cases hy : (y : G) = 1

292 · apply Subtype.ext

293 simp only [hy, ↓reduceDIte, toClosure, fromClosure]

294 · apply Subtype.ext

295 simp only [hy, ↓reduceDIte, Subtype.coe_eta, toClosure, fromClosure]

296 let e : OnePoint X ≃ closure X :=

297 { toFun := toClosure

298 invFun := fromClosure

299 left_inv := hleft

300 right_inv := hright }

301 have hcont : Continuous e := by

302 rw [OnePoint.continuous_iff_from_discrete]

303 rw [tendsto_subtype_rng]

304 change Filter.Tendsto (fun x : X => ((toClosure (x : OnePoint X) : closure X) : G))

305 Filter.cofinite

306 (𝓝 (((toClosure OnePoint.infty : closure X) : G)))

307 change Filter.Tendsto (fun x : X => (x : G)) Filter.cofinite (𝓝 (1 : G))

308 rw [Filter.tendsto_def]

309 intro s hs

310 rcases mem_nhds_iff.mp hs with ⟨W, hWs, hWopen, h1W⟩

311 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hWopen h1W with ⟨U, hUW⟩

312 have hfinite : (X \ (U : Set G)).Finite := hX U.toOpenSubgroup

313 have hcof : ∀ᶠ x : X in Filter.cofinite, (x : G) ∈ (U : Set G) := by

314 let f : X ↪ G := ⟨Subtype.val, Subtype.val_injective⟩

315 have hpre : {x : X | (x : G) ∉ (U : Set G)}.Finite := by

316 simpa [f, Set.preimage] using hfinite.preimage_embedding f

317 exact Filter.eventually_cofinite.2 hpre

318 exact hcof.mono fun x hx => hWs (hUW hx)

319 exact Continuous.homeoOfEquivCompactToT2 (f := e) hcont

320

321end ProCGroups.Generation