ProCGroups/ProC/Quotients/ClosedNormal.lean

1import ProCGroups.Generation.Basic

2import ProCGroups.ProC.Quotients.LeftQuotientProjectionSections

4/-

5PUBLIC_PAGE_SNAPSHOT

6generated_at: 2026-05-27T09:47:29+09:00

7lean_source: lean4/ProCGroups/ProC/Quotients/ClosedNormal.lean

8translation_root: data/translation

9purpose: identifies the local data snapshot used to build pages/

10placement: after imports, never before imports

11-/

12/-!

13# Pro-C groups and open normal quotients

15Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.

16-/

18open Set

19open scoped Topology Pointwise

21namespace ProCGroups

23universe u v

25namespace IsProfiniteGroup

27open ProCGroups.ProC

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

31/-- A quotient of a profinite group by a closed normal subgroup is profinite. -/

32theorem quotient_closedNormalSubgroup

33 (hG : IsProfiniteGroup G) {N : Subgroup G} [N.Normal]

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

35 IsProfiniteGroup (G ⧸ N) := by

36 exact (isProC_allFinite_iff_isProfiniteGroup (G := G ⧸ N)).1 <|

37 ProCGroups.ProC.quotient_closedNormalSubgroup

38 (C := FiniteGroupClass.allFinite)

39 FiniteGroupClass.allFinite_isomClosed

40 FiniteGroupClass.allFinite_formation.quotientClosed

41 ((isProC_allFinite_iff_isProfiniteGroup (G := G)).2 hG)

42 N hNclosed

44/-- The range of a continuous homomorphism from a profinite group to a Hausdorff topological group is

45profinite, with the induced subtype topology. -/

46theorem range

47 (hG : IsProfiniteGroup G)

48 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]

49 (f : G →ₜ* H) :

50 IsProfiniteGroup f.toMonoidHom.range := by

51 letI : CompactSpace G := hG.compactSpace

52 let K : Subgroup G := f.toMonoidHom.ker

53 have hKclosed : IsClosed (K : Set G) := by

54 dsimp [K]

55 exact f.isClosed_ker

56 letI : K.Normal := by

57 dsimp [K]

58 infer_instance

59 have hQuot : IsProfiniteGroup (G ⧸ K) :=

60 quotient_closedNormalSubgroup hG hKclosed

61 have e : (G ⧸ K) ≃ₜ* f.toMonoidHom.range := by

62 simpa [K] using ContinuousMonoidHom.quotientKerContinuousMulEquivRange f

63 letI : IsTopologicalGroup (G ⧸ K) := hQuot.isTopologicalGroup

64 letI : CompactSpace (G ⧸ K) := hQuot.compactSpace

65 letI : T2Space (G ⧸ K) := hQuot.t2Space

66 letI : TotallyDisconnectedSpace (G ⧸ K) := hQuot.totallyDisconnectedSpace

67 letI : CompactSpace f.toMonoidHom.range := e.toHomeomorph.compactSpace

68 letI : T2Space f.toMonoidHom.range := e.toHomeomorph.t2Space

69 letI : TotallyDisconnectedSpace f.toMonoidHom.range := e.toHomeomorph.totallyDisconnectedSpace

70 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩

72end IsProfiniteGroup

74end ProCGroups

76namespace ProCGroups.Generation

78universe u v

80open ProCGroups.ProC

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

84/-- A chosen continuous section of the quotient map by a closed normal subgroup of a profinite

85group. -/

86noncomputable def closedNormalQuotientSection

87 (hG : IsProfiniteGroup G) {N : Subgroup G}

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

89 G ⧸ N → G :=

90 Classical.choose (exists_continuousSection_quotientMk_of_isClosed (G := G) N hG hNclosed)

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

93theorem closedNormalQuotientSection_continuous

94 (hG : IsProfiniteGroup G) {N : Subgroup G}

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

96 Continuous (closedNormalQuotientSection (G := G) hG (N := N) hNclosed) := by

97 exact (Classical.choose_spec

98 (exists_continuousSection_quotientMk_of_isClosed (G := G) N hG hNclosed)).1

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

101theorem closedNormalQuotientSection_rightInverse

102 (hG : IsProfiniteGroup G) {N : Subgroup G}

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

104 Function.RightInverse

105 (closedNormalQuotientSection (G := G) hG (N := N) hNclosed)

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

107 simpa using (Classical.choose_spec

108 (exists_continuousSection_quotientMk_of_isClosed (G := G) N hG hNclosed)).2.1

109

110/-- The chosen closed-normal quotient section sends the identity coset to `1`. -/

111theorem closedNormalQuotientSection_one

112 (hG : IsProfiniteGroup G) {N : Subgroup G}

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

114 closedNormalQuotientSection (G := G) hG (N := N) hNclosed

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

116 simpa using (Classical.choose_spec

117 (exists_continuousSection_quotientMk_of_isClosed (G := G) N hG hNclosed)).2.2

118

119/-- The quotient of a profinite group by a closed normal subgroup is profinite. -/

120theorem isProfinite_quotient_closedNormal

121 (hG : IsProfiniteGroup G) {N : Subgroup G} [N.Normal]

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

123 IsProfiniteGroup (G ⧸ N) :=

124 ProCGroups.IsProfiniteGroup.quotient_closedNormalSubgroup hG hNclosed

125

126/-- The quotient by the bottom subgroup is continuously multiplicatively equivalent to the

127original profinite group. -/

128noncomputable def quotientBotContinuousMulEquiv (hG : IsProfiniteGroup G) :

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

130 ContinuousMulEquiv.mk' (quotientBotHomeomorph (G := G) hG) (by

131 intro x y

132 simp only [quotientBotHomeomorph_apply, QuotientGroup.mk_mul])

133

134/-- Adding a closed normal subgroup to a generating set is equivalent to generating the quotient

135from the image of the set. -/

136theorem topologicallyGenerates_union_closedNormal_iff_quotient

137 (hG : IsProfiniteGroup G) {N : Subgroup G} [N.Normal]

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

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

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

141 let hGquot : IsProfiniteGroup (G ⧸ N) :=

142 isProfinite_quotient_closedNormal (G := G) hG hNclosed

143 constructor

144 · intro hX

145 have himg :

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

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

148 ext q

149 constructor

150 · intro hq

151 rcases hq with ⟨x, hx, rfl⟩

152 rcases hx with hxX | hxN

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

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

155 · intro hq

156 rcases hq with hqX | hq1

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

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

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

160 have hquot :

161 TopologicallyGenerates (G := G ⧸ N)

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

163 exact topologicallyGenerates_image_of_continuousSurjective

164 (G := G)

165 (H := G ⧸ N)

166 (QuotientGroup.mk' N)

167 continuous_quotient_mk'

168 (QuotientGroup.mk'_surjective N)

169 hX

170 have hquot' :

171 TopologicallyGenerates (G := G ⧸ N)

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

173 rwa [himg] at hquot

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

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

176 hquot'

177 · intro hX

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

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

180 intro x hx

181 exact Subgroup.le_topologicalClosure _

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

183 have hNleH : N ≤ H := by

184 intro n hn

185 exact Subgroup.le_topologicalClosure _

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

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

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

189 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG

190 letI : T2Space (G ⧸ N) := IsProfiniteGroup.t2Space hGquot

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

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

193 hHcompact.image continuous_quotient_mk'

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

195 ext q

196 constructor

197 · rintro ⟨x, hx, rfl⟩

198 exact ⟨x, hx, rfl⟩

199 · rintro ⟨x, hx, rfl⟩

200 exact ⟨x, hx, rfl⟩

201 rw [← hEq]

202 exact himage.isClosed

203 have himage_le_qH :

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

205 intro q hq

206 rcases hq with ⟨x, hx, rfl⟩

207 exact ⟨x, hXleH hx, rfl⟩

208 have hcl_le_qH :

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

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

211 have hclosure_le_qH :

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

213 exact Subgroup.topologicalClosure_minimal _ hcl_le_qH hqHclosed

214 have htop :

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

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

217 simpa [TopologicallyGenerates] using hX

218 have hqHtop :

219 qH = ⊤ := by

220 apply top_unique

221 intro q hq

222 exact hclosure_le_qH (htop hq)

223 rw [TopologicallyGenerates]

224 apply top_unique

225 intro g hg

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

227 rw [hqHtop]

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

229 rcases hgq with ⟨h, hhH, hhEq⟩

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

231 exact (QuotientGroup.eq).1 hhEq

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

233 have hhH' : h ∈ H := hhH

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

235 rw [hgH]

236 exact H.mul_mem hhH' hdivH

237

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

239theorem isClosed_image_closedNormal_quotient

240 (hG : IsProfiniteGroup G) {N N' : Subgroup G} [N'.Normal]

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

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

243 let hGquot : IsProfiniteGroup (G ⧸ N') :=

244 isProfinite_quotient_closedNormal (G := G) hG hN'closed

245 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG

246 letI : T2Space (G ⧸ N') := IsProfiniteGroup.t2Space hGquot

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

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

249 hNcompact.image continuous_quotient_mk'

250 have hEq :

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

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

253 ext q

254 constructor

255 · rintro ⟨x, hx, rfl⟩

256 exact ⟨x, hx, rfl⟩

257 · rintro ⟨x, hx, rfl⟩

258 exact ⟨x, hx, rfl⟩

259 rw [← hEq]

260 exact himage.isClosed

261

262/-- The quotient-of-quotient isomorphism for closed normal subgroups as a continuous

263multiplicative equivalence. -/

264noncomputable def quotientQuotientContinuousMulEquiv

265 (hG : IsProfiniteGroup G) {N N' : Subgroup G} [N.Normal] [N'.Normal]

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

267 (hN'N : N' ≤ N) :

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

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

270 let hGquotN' : IsProfiniteGroup (G ⧸ N') :=

271 isProfinite_quotient_closedNormal (G := G) hG hN'closed

272 let hGdom : IsProfiniteGroup ((G ⧸ N') ⧸ K) :=

273 isProfinite_quotient_closedNormal

274 (G := G ⧸ N') hGquotN'

275 (isClosed_image_closedNormal_quotient (G := G) hG hNclosed hN'closed)

276 letI : CompactSpace ((G ⧸ N') ⧸ K) := IsProfiniteGroup.compactSpace hGdom

277 letI : T2Space (G ⧸ N) :=

278 IsProfiniteGroup.t2Space (isProfinite_quotient_closedNormal (G := G) hG hNclosed)

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

280 QuotientGroup.quotientQuotientEquivQuotientAux N' N hN'N

281 have hfcont : Continuous f := by

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

283 simpa [Function.comp, K, leftQuotientProjection] using

284 (continuous_leftQuotientProjection (G := G) (K := N') (H := N) hN'N)

285 have hfbij : Function.Bijective f := by

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

287 exact ContinuousMulEquiv.ofBijectiveCompactToT2 f hfcont hfbij

288

289/-- A quotient section together with generators for the kernel generates the intermediate

290quotient. -/

291theorem topologicallyGenerates_of_quotient_section_union_kernel

292 (hG : IsProfiniteGroup G)

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

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

295 (hN'N : N' ≤ N)

296 {Y : Set (G ⧸ N)}

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

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

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

300 {T : Set G}

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

302 TopologicallyGenerates (G := G ⧸ N')

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

304 classical

305 let hGquotN' : IsProfiniteGroup (G ⧸ N') :=

306 isProfinite_quotient_closedNormal (G := G) hG hN'closed

307 letI : T2Space (G ⧸ N') := IsProfiniteGroup.t2Space hGquotN'

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

309 letI : K.Normal := by infer_instance

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

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

312 simpa [K] using

313 isClosed_image_closedNormal_quotient (G := G) hG hNclosed hN'closed

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

315 quotientQuotientContinuousMulEquiv

316 (G := G) hG hNclosed hN'closed hN'N

317 have hsright :

318 Function.RightInverse

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

320 e := by

321 intro y

322 simpa [e, quotientQuotientContinuousMulEquiv, K, leftQuotientProjection] using hσright y

323 have hsleft :

324 Function.LeftInverse

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

326 e := by

327 intro z

328 apply e.injective

329 simpa using hsright (e z)

330 have hs_eq :

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

332 funext y

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

334 have hgenInv :

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

336 exact topologicallyGenerates_continuousMulEquiv_image

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

338 have hEq :

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

340 ext q

341 constructor

342 · rintro ⟨y, hy, rfl⟩

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

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

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

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

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

348 simpa [hEq] using hgenInv

349 have hgenQuotX :

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

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

352 exact topologicallyGenerates_mono hgenQuotY (by

353 intro q hq

354 rcases hq with ⟨x, hx, rfl⟩

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

356 have hgenUnionK :

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

358 exact

359 (topologicallyGenerates_union_closedNormal_iff_quotient

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

361 have hKsubset :

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

363 have himgSubset :

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

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

366 intro q hq

367 rcases hq with ⟨g, hg, rfl⟩

368 rcases hg with hgT | hgN'

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

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

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

372 rw [hg1]

373 exact (Subgroup.closure X).one_mem

374 have hclosureSubset :

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

376 Subgroup.closure X := by

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

378 intro q hq

379 have hq' :

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

381 rcases hq with ⟨n, hnN, rfl⟩

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

383 have hmap :

384 QuotientGroup.mk' N' n ∈

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

386 exact ⟨n, hncl, rfl⟩

387 have hmapEq :

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

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

390 simpa using

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

392 exact hmapEq ▸ hmap

393 exact hclosureSubset hq'

394 exact topologicallyGenerates_of_subset_closure hgenUnionK (by

395 intro q hq

396 rcases hq with hqX | hqK

397 · exact Subgroup.subset_closure hqX

398 · exact hKsubset hqK)

399

400end ProCGroups.Generation