Source: ProCGroups.ProC.Quotients.ClosedNormal

1import ProCGroups.Generation.Basic

2import ProCGroups.ProC.Quotients.LeftQuotientProjectionSections

4/-!

5# Quotients by closed normal subgroups

7This file supplies the profinite topology and normalized continuous sections for closed-normal

8quotients, identifies iterated quotients, proves closedness of quotient images, and transfers

9topological generation between a group, its kernel, and its quotient.

10-/

12open Set

13open scoped Topology Pointwise

15namespace ProCGroups

17universe u v

19/-- A quotient by a closed normal subgroup of a compact Hausdorff totally disconnected

20topological group is totally disconnected. -/

21theorem totallyDisconnectedSpace_quotient_closedNormal

22 {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

23 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

24 (N : Subgroup G) [N.Normal] (hN : IsClosed (N : Set G)) :

25 TotallyDisconnectedSpace (G ⧸ N) := by

26 letI : IsClosed (N : Set G) := hN

27 let q : G →* G ⧸ N := QuotientGroup.mk' N

28 have hsep : Pairwise (fun a b : G ⧸ N =>

29 ∃ U : Set (G ⧸ N), IsClopen U ∧ a ∈ U ∧ b ∈ Uᶜ) := by

30 intro a b hab

31 obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective N a

32 obtain ⟨y, rfl⟩ := QuotientGroup.mk'_surjective N b

33 let g : G := x⁻¹ * y

34 have hgN : g ∉ N := by

35 intro hgN

36 apply hab

37 apply inv_mul_eq_one.mp

38 change q g = 1

39 exact (QuotientGroup.eq_one_iff g).2 hgN

40 let W : Set G := {u | g * u⁻¹ ∉ N}

41 have hWopen : IsOpen W := by

42 change IsOpen ((fun u : G => g * u⁻¹) ⁻¹' ((N : Set G)ᶜ))

43 exact hN.isOpen_compl.preimage (continuous_const.mul continuous_inv)

44 have hWone : (1 : G) ∈ W := by

45 simpa [W] using hgN

46 obtain ⟨V, hVW⟩ :=

47 ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one

48 (G := G) hWopen hWone

49 let K : Subgroup G := N ⊔ (V : Subgroup G)

50 have hKopen : IsOpen (K : Set G) :=

51 Subgroup.isOpen_of_openSubgroup K

52 (show (V : Subgroup G) ≤ K from le_sup_right)

53 have hNK : N ≤ K := le_sup_left

54 have hgK : g ∉ K := by

55 intro hgK

56 rcases (Subgroup.mem_sup_of_normal_right

57 (s := N) (t := (V : Subgroup G))).1 hgK with

58 ⟨n, hnN, v, hvV, hnv⟩

59 have hvW : v ∈ W := hVW hvV

60 have hgn : g * v⁻¹ = n := by

61 calc

62 g * v⁻¹ = (n * v) * v⁻¹ := by rw [hnv]

63 _ = n := by simp

64 apply hvW

65 simpa [hgn] using hnN

66 let Kbar : Subgroup (G ⧸ N) := K.map q

67 have hKbarOpen : IsOpen (Kbar : Set (G ⧸ N)) := by

68 change IsOpen (((↑) : G → G ⧸ N) '' (K : Set G))

69 exact QuotientGroup.isOpenMap_coe (K : Set G) hKopen

70 have hqgKbar : q g ∉ Kbar := by

71 intro hqgKbar

72 have hgComap : g ∈ Kbar.comap q := hqgKbar

73 have hker : q.ker ≤ K := by

74 simpa [q] using hNK

75 have hcomap : Kbar.comap q = K := by

76 simpa [Kbar] using Subgroup.comap_map_eq_self hker

77 rw [hcomap] at hgComap

78 exact hgK hgComap

79 let U : Set (G ⧸ N) := {z | (q x)⁻¹ * z ∈ Kbar}

80 have hUclopen : IsClopen U := by

81 have hcont : Continuous (fun z : G ⧸ N => (q x)⁻¹ * z) :=

82 (continuous_const : Continuous (fun _ : G ⧸ N => (q x)⁻¹)).mul continuous_id'

83 exact

84 ⟨(Subgroup.isClosed_of_isOpen Kbar hKbarOpen).preimage hcont,

85 hKbarOpen.preimage hcont⟩

86 refine ⟨U, hUclopen, ?_, ?_⟩

87 · simp [U, q]

88 · change (q x)⁻¹ * q y ∉ Kbar

89 simpa [g, q] using hqgKbar

90 letI : TotallySeparatedSpace (G ⧸ N) :=

91 totallySeparatedSpace_iff_exists_isClopen.2 hsep

92 infer_instance

94end ProCGroups

96namespace ProCGroups.Generation

98universe u v

100open ProCGroups.ProC

101

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

103 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

104

105/--

106A chosen continuous section of the quotient map by a closed normal subgroup of a profinite

107group.

108-/

109noncomputable def closedNormalQuotientSection

110 {N : Subgroup G} (hNclosed : IsClosed (N : Set G)) :

111 G ⧸ N → G :=

112 Classical.choose (exists_continuousSection_quotientMk_of_isClosed (G := G) N hNclosed)

113

114/-- The chosen closed-normal quotient section is continuous. -/

115theorem closedNormalQuotientSection_continuous

116 {N : Subgroup G} (hNclosed : IsClosed (N : Set G)) :

117 Continuous (closedNormalQuotientSection (G := G) (N := N) hNclosed) := by

118 exact (Classical.choose_spec

119 (exists_continuousSection_quotientMk_of_isClosed (G := G) N hNclosed)).1

120

121/-- The chosen closed-normal quotient section is a right inverse to the quotient map. -/

122theorem closedNormalQuotientSection_rightInverse

123 {N : Subgroup G} (hNclosed : IsClosed (N : Set G)) :

124 Function.RightInverse

125 (closedNormalQuotientSection (G := G) (N := N) hNclosed)

126 (QuotientGroup.mk (s := N)) := by

127 simpa [closedNormalQuotientSection] using (Classical.choose_spec

128 (exists_continuousSection_quotientMk_of_isClosed (G := G) N hNclosed)).2.1

129

130/-- The chosen closed-normal quotient section sends the identity coset to \(1\). -/

131theorem closedNormalQuotientSection_one

132 {N : Subgroup G} (hNclosed : IsClosed (N : Set G)) :

133 closedNormalQuotientSection (G := G) (N := N) hNclosed

134 (QuotientGroup.mk (s := N) (1 : G)) = 1 := by

135 simpa [closedNormalQuotientSection] using (Classical.choose_spec

136 (exists_continuousSection_quotientMk_of_isClosed (G := G) N hNclosed)).2.2

137

138/--

139The quotient by the bottom subgroup is continuously multiplicatively equivalent to the original

140profinite group.

141-/

142noncomputable def quotientBotContinuousMulEquiv :

143 G ≃ₜ* G ⧸ (⊥ : Subgroup G) :=

144 ContinuousMulEquiv.mk' (quotientBotHomeomorph (G := G)) (by

145 intro x y

146 simp only [quotientBotHomeomorph_apply, QuotientGroup.mk_mul])

147

148omit [T2Space G] [TotallyDisconnectedSpace G] in

149/--

150Adding a closed normal subgroup to a generating set is equivalent to generating the quotient

151from the image of the set.

152-/

153theorem topologicallyGenerates_union_closedNormal_iff_quotient

154 {N : Subgroup G} [N.Normal]

155 (hNclosed : IsClosed (N : Set G)) {X : Set G} :

156 TopologicallyGenerates (G := G) (X ∪ (N : Set G)) ↔

157 TopologicallyGenerates (G := G ⧸ N) ((QuotientGroup.mk' N) '' X) := by

158 letI : IsClosed (N : Set G) := hNclosed

159 constructor

160 · intro hX

161 have himg :

162 (QuotientGroup.mk' N) '' (X ∪ (N : Set G)) =

163 ((QuotientGroup.mk' N) '' X) ∪ ({1} : Set (G ⧸ N)) := by

164 ext q

165 constructor

166 · intro hq

167 rcases hq with ⟨x, hx, rfl⟩

168 rcases hx with hxX | hxN

169 · exact Or.inl ⟨x, hxX, rfl⟩

170 · exact Or.inr ((QuotientGroup.eq_one_iff (N := N) x).2 hxN)

171 · intro hq

172 rcases hq with hqX | hq1

173 · rcases hqX with ⟨x, hxX, rfl⟩

174 exact ⟨x, Or.inl hxX, rfl⟩

175 · exact ⟨1, Or.inr N.one_mem, by simpa using hq1.symm⟩

176 have hquot :

177 TopologicallyGenerates (G := G ⧸ N)

178 ((QuotientGroup.mk' N) '' (X ∪ (N : Set G))) := by

179 exact topologicallyGenerates_image_of_continuousSurjective

180 (G := G)

181 (H := G ⧸ N)

182 (QuotientGroup.mk' N)

183 continuous_quotient_mk'

184 (QuotientGroup.mk'_surjective N)

185 hX

186 have hquot' :

187 TopologicallyGenerates (G := G ⧸ N)

188 ((((QuotientGroup.mk' N) '' X) ∪ ({1} : Set (G ⧸ N)))) := by

189 rwa [himg] at hquot

190 exact (topologicallyGenerates_union_one_iff (G := G ⧸ N)

191 (X := (QuotientGroup.mk' N) '' X)).1

192 hquot'

193 · intro hX

194 let H : Subgroup G := (Subgroup.closure (X ∪ (N : Set G))).topologicalClosure

195 have hXleH : X ⊆ (H : Set G) := by

196 intro x hx

197 exact Subgroup.le_topologicalClosure _

198 (Subgroup.subset_closure (Or.inl hx))

199 have hNleH : N ≤ H := by

200 intro n hn

201 exact Subgroup.le_topologicalClosure _

202 (Subgroup.subset_closure (Or.inr hn))

203 let qH : Subgroup (G ⧸ N) := H.map (QuotientGroup.mk' N)

204 have hqHclosed : IsClosed (qH : Set (G ⧸ N)) := by

205 have hHcompact : IsCompact (H : Set G) := (Subgroup.isClosed_topologicalClosure _).isCompact

206 have himage : IsCompact ((QuotientGroup.mk' N) '' (H : Set G)) :=

207 hHcompact.image continuous_quotient_mk'

208 have hEq : (QuotientGroup.mk' N) '' (H : Set G) = (qH : Set (G ⧸ N)) := by

209 ext q

210 constructor

211 · rintro ⟨x, hx, rfl⟩

212 exact ⟨x, hx, rfl⟩

213 · rintro ⟨x, hx, rfl⟩

214 exact ⟨x, hx, rfl⟩

215 rw [← hEq]

216 exact himage.isClosed

217 have himage_le_qH :

218 ((QuotientGroup.mk' N) '' X) ⊆ (qH : Set (G ⧸ N)) := by

219 intro q hq

220 rcases hq with ⟨x, hx, rfl⟩

221 exact ⟨x, hXleH hx, rfl⟩

222 have hcl_le_qH :

223 Subgroup.closure ((QuotientGroup.mk' N) '' X) ≤ qH := by

224 exact (Subgroup.closure_le (K := qH)).2 himage_le_qH

225 have hclosure_le_qH :

226 (Subgroup.closure ((QuotientGroup.mk' N) '' X)).topologicalClosure ≤ qH := by

227 exact Subgroup.topologicalClosure_minimal _ hcl_le_qH hqHclosed

228 have htop :

229 (⊤ : Subgroup (G ⧸ N)) ≤

230 (Subgroup.closure ((QuotientGroup.mk' N) '' X)).topologicalClosure := by

231 simpa [TopologicallyGenerates] using hX

232 have hqHtop :

233 qH = ⊤ := by

234 apply top_unique

235 intro q hq

236 exact hclosure_le_qH (htop hq)

237 rw [TopologicallyGenerates]

238 apply top_unique

239 intro g hg

240 have hgq : QuotientGroup.mk' N g ∈ qH := by

241 rw [hqHtop]

242 simp only [QuotientGroup.mk'_apply, Subgroup.mem_top]

243 rcases hgq with ⟨h, hhH, hhEq⟩

244 have hdivN : h⁻¹ * g ∈ N := by

245 exact (QuotientGroup.eq).1 hhEq

246 have hdivH : h⁻¹ * g ∈ H := hNleH hdivN

247 have hhH' : h ∈ H := hhH

248 have hgH : g = h * (h⁻¹ * g) := by simp only [mul_inv_cancel_left]

249 rw [hgH]

250 exact H.mul_mem hhH' hdivH

251

252omit [T2Space G] [TotallyDisconnectedSpace G] in

253/-- The image of a closed subgroup in a quotient by a closed normal subgroup is closed. -/

254theorem isClosed_image_closedNormal_quotient

255 {N N' : Subgroup G} [N'.Normal]

256 (hNclosed : IsClosed (N : Set G)) (hN'closed : IsClosed (N' : Set G)) :

257 IsClosed ((N.map (QuotientGroup.mk' N') : Subgroup (G ⧸ N')) : Set (G ⧸ N')) := by

258 letI : IsClosed (N' : Set G) := hN'closed

259 have hNcompact : IsCompact (N : Set G) := hNclosed.isCompact

260 have himage : IsCompact ((QuotientGroup.mk' N') '' (N : Set G)) :=

261 hNcompact.image continuous_quotient_mk'

262 have hEq :

263 (QuotientGroup.mk' N') '' (N : Set G) =

264 ((N.map (QuotientGroup.mk' N') : Subgroup (G ⧸ N')) : Set (G ⧸ N')) := by

265 ext q

266 constructor

267 · rintro ⟨x, hx, rfl⟩

268 exact ⟨x, hx, rfl⟩

269 · rintro ⟨x, hx, rfl⟩

270 exact ⟨x, hx, rfl⟩

271 rw [← hEq]

272 exact himage.isClosed

273

274/--

275The quotient-of-quotient isomorphism for closed normal subgroups as a continuous multiplicative

276equivalence.

277-/

278noncomputable def quotientQuotientContinuousMulEquiv

279 {N N' : Subgroup G} [N.Normal] [N'.Normal]

280 (hNclosed : IsClosed (N : Set G))

281 (hN'N : N' ≤ N) :

282 ((G ⧸ N') ⧸ N.map (QuotientGroup.mk' N')) ≃ₜ* G ⧸ N := by

283 let K : Subgroup (G ⧸ N') := N.map (QuotientGroup.mk' N')

284 letI : IsClosed (N : Set G) := hNclosed

285 let f : ((G ⧸ N') ⧸ K) →* G ⧸ N :=

286 QuotientGroup.quotientQuotientEquivQuotientAux N' N hN'N

287 have hfcont : Continuous f := by

288 refine (QuotientGroup.isQuotientMap_mk K).continuous_iff.2 ?_

289 change Continuous (leftQuotientProjection N' N hN'N)

290 exact continuous_leftQuotientProjection (G := G) (K := N') (H := N) hN'N

291 have hfbij : Function.Bijective f := by

292 exact (QuotientGroup.quotientQuotientEquivQuotient N' N hN'N).bijective

293 exact ContinuousMulEquiv.ofBijectiveCompactToT2 f hfcont hfbij

294

295omit [T2Space G] [TotallyDisconnectedSpace G] in

296/--

297A quotient section together with generators for the kernel generates the intermediate quotient.

298-/

299theorem topologicallyGenerates_of_quotient_section_union_kernel

300 {N N' : Subgroup G} [N.Normal] [N'.Normal]

301 (hNclosed : IsClosed (N : Set G)) (hN'closed : IsClosed (N' : Set G))

302 (hN'N : N' ≤ N)

303 {Y : Set (G ⧸ N)}

304 (hYgen : TopologicallyGenerates (G := G ⧸ N) Y)

305 {σ : (G ⧸ N) → (G ⧸ N')}

306 (hσright : Function.RightInverse σ (leftQuotientProjection N' N hN'N))

307 {T : Set G}

308 (hTgen : N ≤ Subgroup.closure (T ∪ (N' : Set G))) :

309 TopologicallyGenerates (G := G ⧸ N')

310 (σ '' Y ∪ ((QuotientGroup.mk' N') '' T)) := by

311 classical

312 letI : IsClosed (N' : Set G) := hN'closed

313 let K : Subgroup (G ⧸ N') := N.map (QuotientGroup.mk' N')

314 letI : K.Normal := by infer_instance

315 let X : Set (G ⧸ N') := σ '' Y ∪ ((QuotientGroup.mk' N') '' T)

316 have hKclosed : IsClosed (K : Set (G ⧸ N')) := by

317 simpa [K] using

318 isClosed_image_closedNormal_quotient (G := G) hNclosed hN'closed

319 let e : ((G ⧸ N') ⧸ K) ≃ₜ* G ⧸ N :=

320 quotientQuotientContinuousMulEquiv

321 (G := G) hNclosed hN'N

322 have hsright :

323 Function.RightInverse

324 (fun y : G ⧸ N => QuotientGroup.mk' K (σ y))

325 e := by

326 intro y

327 change leftQuotientProjection N' N hN'N (σ y) = y

328 exact hσright y

329 have hsleft :

330 Function.LeftInverse

331 (fun y : G ⧸ N => QuotientGroup.mk' K (σ y))

332 e := by

333 intro z

334 apply e.injective

335 simpa using hsright (e z)

336 have hs_eq :

337 e.symm = (fun y : G ⧸ N => QuotientGroup.mk' K (σ y)) := by

338 funext y

339 simpa using (hsleft (e.symm y)).symm

340 have hgenInv :

341 TopologicallyGenerates (G := ((G ⧸ N') ⧸ K)) (e.symm '' Y) := by

342 exact topologicallyGenerates_continuousMulEquiv_image

343 (G := G ⧸ N) e.symm hYgen

344 have hEq :

345 e.symm '' Y = (QuotientGroup.mk' K) '' (σ '' Y) := by

346 ext q

347 constructor

348 · rintro ⟨y, hy, rfl⟩

349 exact ⟨σ y, ⟨y, hy, rfl⟩, by simp only [QuotientGroup.mk'_apply, hs_eq]⟩

350 · rintro ⟨x, ⟨y, hy, rfl⟩, rfl⟩

351 exact ⟨y, hy, by simp only [hs_eq, QuotientGroup.mk'_apply]⟩

352 have hgenQuotY : TopologicallyGenerates (G := ((G ⧸ N') ⧸ K))

353 ((QuotientGroup.mk' K) '' (σ '' Y)) := by

354 simpa [hEq] using hgenInv

355 have hgenQuotX :

356 TopologicallyGenerates (G := ((G ⧸ N') ⧸ K))

357 ((QuotientGroup.mk' K) '' X) := by

358 exact topologicallyGenerates_mono hgenQuotY (by

359 intro q hq

360 rcases hq with ⟨x, hx, rfl⟩

361 exact ⟨x, Or.inl hx, rfl⟩)

362 have hgenUnionK :

363 TopologicallyGenerates (G := G ⧸ N') (X ∪ (K : Set (G ⧸ N'))) := by

364 exact

365 (topologicallyGenerates_union_closedNormal_iff_quotient

366 (G := G ⧸ N') (N := K) hKclosed (X := X)).2 hgenQuotX

367 have hKsubset :

368 (K : Set (G ⧸ N')) ⊆ ((Subgroup.closure X : Subgroup (G ⧸ N')) : Set (G ⧸ N')) := by

369 have himgSubset :

370 (QuotientGroup.mk' N' '' (T ∪ (N' : Set G))) ⊆

371 ((Subgroup.closure X : Subgroup (G ⧸ N')) : Set (G ⧸ N')) := by

372 intro q hq

373 rcases hq with ⟨g, hg, rfl⟩

374 rcases hg with hgT | hgN'

375 · exact Subgroup.subset_closure (Or.inr ⟨g, hgT, rfl⟩)

376 · have hg1 : QuotientGroup.mk' N' g = (1 : G ⧸ N') := by

377 exact (QuotientGroup.eq_one_iff (N := N') g).2 hgN'

378 rw [hg1]

379 exact (Subgroup.closure X).one_mem

380 have hclosureSubset :

381 Subgroup.closure ((QuotientGroup.mk' N') '' (T ∪ (N' : Set G))) ≤

382 Subgroup.closure X := by

383 exact (Subgroup.closure_le (K := Subgroup.closure X)).2 himgSubset

384 intro q hq

385 have hq' :

386 q ∈ Subgroup.closure ((QuotientGroup.mk' N') '' (T ∪ (N' : Set G))) := by

387 rcases hq with ⟨n, hnN, rfl⟩

388 have hncl : n ∈ Subgroup.closure (T ∪ (N' : Set G)) := hTgen hnN

389 have hmap :

390 QuotientGroup.mk' N' n ∈

391 (Subgroup.closure (T ∪ (N' : Set G))).map (QuotientGroup.mk' N') := by

392 exact ⟨n, hncl, rfl⟩

393 have hmapEq :

394 (Subgroup.closure (T ∪ (N' : Set G))).map (QuotientGroup.mk' N') =

395 Subgroup.closure ((QuotientGroup.mk' N') '' (T ∪ (N' : Set G))) := by

396 simpa using

397 (MonoidHom.map_closure (QuotientGroup.mk' N') (T ∪ (N' : Set G)))

398 exact hmapEq ▸ hmap

399 exact hclosureSubset hq'

400 exact topologicallyGenerates_of_subset_closure hgenUnionK (by

401 intro q hq

402 rcases hq with hqX | hqK

403 · exact Subgroup.subset_closure hqX

404 · exact hKsubset hqK)

405

406end ProCGroups.Generation