Source: ProCGroups.ProC.Quotients.LeftQuotientProjectionSections

1import ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne

2import ProCGroups.ProC.Quotients.DescendingClosedSubgroupQuotients

4/-!

5# Continuous sections of left-quotient projections

7Using normalized section data ordered by intermediate closed subgroups, this file applies a chain

8upper-bound argument to construct continuous sections of \(G/K \to G/H\). It concludes with a

9continuous section of the quotient map by any closed subgroup of a profinite group.

10-/

12open Set

13open scoped Topology Pointwise

15namespace ProCGroups.ProC

17universe u v

19open InverseSystems

21/--

22If an intermediate closed subgroup is not contained in the base subgroup, the set-theoretic

23difference contains an element.

24-/

25theorem exists_mem_of_not_le {G : Type u} [Group G] [TopologicalSpace G] {K L : ClosedSubgroup G}

26 (hnotle : ¬ (L : Subgroup G) ≤ (K : Subgroup G)) :

27 ∃ x : G, x ∈ (L : Subgroup G) ∧ x ∉ (K : Subgroup G) := by

28 by_contra hNo

29 apply hnotle

30 intro x hxL

31 by_cases hxK : x ∈ (K : Set G)

32 · exact hxK

33 · exact False.elim (hNo ⟨x, hxL, hxK⟩)

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

36 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

38omit [T2Space G] in

39/--

40For any nontrivial element of a profinite group, there is an open normal subgroup that does not

41contain it.

42-/

43theorem exists_openNormalSubgroup_not_mem

44 {x : G} (hx : x ≠ 1) :

45 ∃ U : OpenNormalSubgroup G, x ∉ (U : Subgroup G) := by

46 let W : Set G := ({x} : Set G)ᶜ

47 have hW : IsOpen W := by

48 simp only [isOpen_compl_iff, finite_singleton, Finite.isClosed, W]

49 have h1W : (1 : G) ∈ W := by

50 simpa [W] using hx.symm

51 obtain ⟨U, hUW⟩ :=

52 exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hW h1W

53 refine ⟨U, ?_⟩

54 intro hxU

55 exact hx <| by

56 have hxW : x ∈ W := hUW hxU

57 simp only [mem_compl_iff, mem_singleton_iff, not_true_eq_false, W] at hxW

59omit [T2Space G] in

60/--

61A point outside a closed subgroup of a profinite group is omitted by some open subgroup

62containing that closed subgroup.

63-/

64theorem exists_openSubgroup_ge_closedSubgroup_not_mem

65 (K : ClosedSubgroup G) {x : G} (hx : x ∉ (K : Set G)) :

66 ∃ U : OpenSubgroup G, (K : Subgroup G) ≤ (U : Subgroup G) ∧ x ∉ (U : Set G) := by

67 have hxInf :

68 x ∉ sInf {N : Subgroup G | IsOpen (N : Set G) ∧ (K : Subgroup G) ≤ N} := by

69 rw [← closedSubgroup_eq_sInf_open (G := G) K]

70 exact hx

71 rw [Subgroup.mem_sInf] at hxInf

72 push Not at hxInf

73 rcases hxInf with ⟨U, hU, hxU⟩

74 exact ⟨⟨U, hU.1⟩, hU.2, hxU⟩

76/--

77An open subgroup of a closed subgroup of a profinite group, viewed again as a closed subgroup of

78the ambient group.

79-/

80noncomputable def closedSubgroupOfOpenSubgroup

81 (T : ClosedSubgroup G) (N : OpenSubgroup T) :

82 ClosedSubgroup G where

83 toSubgroup := (N : Subgroup T).map ((T : Subgroup G).subtype)

84 isClosed' := by

85 letI : IsTopologicalGroup ↥(T : Subgroup G) := by infer_instance

86 have hNclosed : IsClosed ((N : Subgroup T) : Set T) :=

87 Subgroup.isClosed_of_isOpen (N : Subgroup T) N.isOpen'

88 have hNcompact : IsCompact ((N : Subgroup T) : Set T) := hNclosed.isCompact

89 have hEq :

90 ((T : Subgroup G).subtype '' ((N : Subgroup T) : Set T)) =

91 (((N : Subgroup T).map ((T : Subgroup G).subtype) : Subgroup G) : Set G) := by

92 ext x

93 constructor <;> rintro ⟨y, hy, rfl⟩ <;> exact ⟨y, hy, rfl⟩

94 change IsClosed ((((N : Subgroup T).map ((T : Subgroup G).subtype) : Subgroup G) : Set G))

95 rw [← hEq]

96 exact hNcompact.image continuous_subtype_val |>.isClosed

98omit [TotallyDisconnectedSpace G] in

99/--

100Membership in the ambient closed subgroup induced by an open subgroup is tested inside the

101original subgroup.

102-/

103@[simp] theorem mem_closedSubgroupOfOpenSubgroup

104 {T : ClosedSubgroup G} {N : OpenSubgroup T} {x : T} :

105 (x : G) ∈ (closedSubgroupOfOpenSubgroup (G := G) T N : Subgroup G) ↔

106 x ∈ (N : Subgroup T) := by

107 constructor

108 · intro hx

109 rcases hx with ⟨y, hy, hyx⟩

110 have : y = x := Subtype.ext hyx

111 simpa [this] using hy

112 · intro hx

113 exact ⟨x, hx, rfl⟩

114

115omit [TotallyDisconnectedSpace G] in

116/-- The ambient closed subgroup attached to an open subgroup of T still lies inside T. -/

117theorem closedSubgroupOfOpenSubgroup_le

118 (T : ClosedSubgroup G) (N : OpenSubgroup T) :

119 (closedSubgroupOfOpenSubgroup (G := G) T N : Subgroup G) ≤ (T : Subgroup G) := by

120 intro x hx

121 rcases hx with ⟨y, hy, rfl⟩

122 exact y.2

123

124omit [TotallyDisconnectedSpace G] in

125/--

126The closed subgroup obtained inside an open subgroup agrees with the corresponding subgroup of

127the ambient group.

128-/

129@[simp 900] theorem closedSubgroupOfOpenSubgroup_subgroupOf_eq

130 (T : ClosedSubgroup G) (N : OpenSubgroup T) :

131 (((closedSubgroupOfOpenSubgroup (G := G) T N : ClosedSubgroup G) : Subgroup G).subgroupOf

132 (T : Subgroup G)) = (N : Subgroup T) := by

133 ext x

134 simp only [Subgroup.mem_subgroupOf, mem_closedSubgroupOfOpenSubgroup, OpenSubgroup.mem_toSubgroup]

135

136/-- The canonical quotient map \(G \to G/\bot\) is a homeomorphism for profinite groups. -/

137noncomputable def quotientBotHomeomorph :

138 G ≃ₜ G ⧸ (⊥ : Subgroup G) := by

139 letI : IsClosed (((⊥ : Subgroup G) : Set G)) := by

140 change IsClosed ({(1 : G)} : Set G)

141 simp only [finite_singleton, Finite.isClosed]

142 exact Continuous.homeoOfEquivCompactToT2

143 (f := Equiv.ofBijective

144 (QuotientGroup.mk (s := (⊥ : Subgroup G)))

145 (by

146 constructor

147 · intro x y hxy

148 have hmem : x⁻¹ * y ∈ (⊥ : Subgroup G) := QuotientGroup.eq.1 hxy

149 exact inv_mul_eq_one.mp <| by simpa using hmem

150 · intro q

151 rcases Quotient.exists_rep q with ⟨g, rfl⟩

152 exact ⟨g, rfl⟩))

153 (by

154 simpa using

155 (QuotientGroup.continuous_mk : Continuous

156 (QuotientGroup.mk (s := (⊥ : Subgroup G)) : G → G ⧸ (⊥ : Subgroup G))))

157

158omit [T2Space G] in

159/-- The continuous equivalence is evaluated by the corresponding comparison formula. -/

160@[simp 900] theorem quotientBotHomeomorph_apply (g : G) :

161 quotientBotHomeomorph (G := G) g = QuotientGroup.mk (s := (⊥ : Subgroup G)) g :=

162 rfl

163

164/--

165Data of a normalized continuous section of a left quotient projection \(G/L \to G/H\), ordered

166so that smaller intermediate subgroups correspond to larger elements. This is the Zorn package

167used for the closed-subgroup section theorem.

168-/

169structure LeftQuotientSectionData (K H : ClosedSubgroup G) where

170 /-- The intermediate closed subgroup through which the section is constructed. -/

171 L : ClosedSubgroup G

172 /-- The lower endpoint \(K\) is contained in the intermediate subgroup \(L\). -/

173 hKL : (K : Subgroup G) ≤ (L : Subgroup G)

174 /-- The intermediate subgroup \(L\) is contained in the upper endpoint \(H\). -/

175 hLH : (L : Subgroup G) ≤ (H : Subgroup G)

176 /-- A section from the left quotient by \(H\) to the left quotient by \(L\). -/

177 σ : G ⧸ (H : Subgroup G) → G ⧸ (L : Subgroup G)

178 /-- The section \(\sigma\) is continuous. -/

179 continuous_σ : Continuous σ

180 /-- The map \(\sigma\) is a right inverse of the quotient projection from \(G/L\) to \(G/H\). -/

181 rightInv : Function.RightInverse σ

182 (leftQuotientProjection (L : Subgroup G) (H : Subgroup G) hLH)

183 /-- The section sends the identity coset modulo \(H\) to the identity coset modulo \(L\). -/

184 one_eq :

185 σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =

186 QuotientGroup.mk (s := (L : Subgroup G)) (1 : G)

187

188namespace LeftQuotientSectionData

189

190variable {K H : ClosedSubgroup G}

191

192/-- The order relation is the refinement relation on the corresponding data. -/

193instance instLELeftQuotientSectionData : LE (LeftQuotientSectionData (G := G) K H) where

194 le a b :=

195 ∃ hba : (b.L : Subgroup G) ≤ (a.L : Subgroup G),

196 leftQuotientProjection (b.L : Subgroup G) (a.L : Subgroup G) hba ∘ b.σ = a.σ

197

198/-- The preorder is induced by refinement of the corresponding data. -/

199instance instPreorderLeftQuotientSectionData : Preorder (LeftQuotientSectionData (G := G) K H) where

200 le_refl a := by

201 refine ⟨le_rfl, ?_⟩

202 funext x

203 simp only [leftQuotientProjection_id, Function.comp_apply, id_eq]

204 le_trans a b c hab hbc := by

205 rcases hab with ⟨hba, hbaσ⟩

206 rcases hbc with ⟨hcb, hcbσ⟩

207 refine ⟨hcb.trans hba, ?_⟩

208 funext x

209 calc

210 leftQuotientProjection (c.L : Subgroup G) (a.L : Subgroup G) (hcb.trans hba) (c.σ x)

211 = leftQuotientProjection (b.L : Subgroup G) (a.L : Subgroup G) hba

212 (leftQuotientProjection (c.L : Subgroup G) (b.L : Subgroup G) hcb (c.σ x)) := by

213 convert

214 (leftQuotientProjection_comp_apply

215 (K := (c.L : Subgroup G)) (H := (b.L : Subgroup G))

216 (L := (a.L : Subgroup G)) hcb hba (c.σ x)).symm

217 _ = leftQuotientProjection (b.L : Subgroup G) (a.L : Subgroup G) hba (b.σ x) := by

218 exact congrArg (leftQuotientProjection (b.L : Subgroup G) (a.L : Subgroup G) hba)

219 (congrFun hcbσ x)

220 _ = a.σ x := congrFun hbaσ x

221

222/-- The maximal element of the Zorn poset, given by the identity section over H itself. -/

223def top (hKH : (K : Subgroup G) ≤ (H : Subgroup G)) :

224 LeftQuotientSectionData (G := G) K H where

225 L := H

226 hKL := hKH

227 hLH := le_rfl

228 σ := id

229 continuous_σ := continuous_id

230 rightInv := by

231 intro x

232 simp only [id_eq, leftQuotientProjection_id]

233 one_eq := rfl

234

235omit [T2Space G] [TotallyDisconnectedSpace G] in

236/-- Any nonempty chain of partial sections admits an upper bound over the infimum subgroup. -/

237theorem exists_upperBound_of_chain

238 (c : Set (LeftQuotientSectionData (G := G) K H))

239 (hc : IsChain (· ≤ ·) c) (hcn : c.Nonempty) :

240 ∃ ub : LeftQuotientSectionData (G := G) K H, ∀ a ∈ c, a ≤ ub := by

241 classical

242 let I : Type u := {a : LeftQuotientSectionData (G := G) K H // a ∈ c}

243 have hI_nonempty : Nonempty I := by

244 rcases hcn with ⟨a, ha⟩

245 exact ⟨⟨a, ha⟩⟩

246 letI : Nonempty I := hI_nonempty

247 let L : I → ClosedSubgroup G := fun i => i.1.L

248 have hL : ∀ {i j : I}, i ≤ j → (L j : Subgroup G) ≤ (L i : Subgroup G) := by

249 intro i j hij

250 rcases hij with ⟨hji, -⟩

251 exact hji

252 have hdir : Directed (· ≤ ·) (id : I → I) := by

253 intro i j

254 by_cases hij : i = j

255 · subst hij

256 exact ⟨i, le_rfl, le_rfl⟩

257 · have hcmp := hc i.2 j.2 (by

258 intro hij'

259 apply hij

260 exact Subtype.ext hij')

261 rcases hcmp with hij' | hji'

262 · exact ⟨j, hij', le_rfl⟩

263 · exact ⟨i, le_rfl, hji'⟩

264 obtain ⟨ηinf, hηinf_continuous, hηinf_fac, hηinf_one⟩ :=

265 exists_continuous_leftQuotient_lift_of_directed (G := G) L hL hdir

266 (η := fun i => i.1.σ) (hηcont := fun i => i.1.continuous_σ)

267 (hηcompat := by

268 intro i j hij

269 rcases hij with ⟨hji, hσ⟩

270 exact hσ)

271 (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))

272 (by

273 intro i

274 exact i.1.one_eq)

275 let Linf : ClosedSubgroup G := closedSubgroup_sInf L

276 have hKinf : (K : Subgroup G) ≤ (Linf : Subgroup G) := by

277 intro x hx

278 change x ∈ iInf fun i => (L i : Subgroup G)

279 rw [Subgroup.mem_iInf]

280 intro i

281 exact i.1.hKL hx

282 let i0 : I := Classical.choice hI_nonempty

283 have hInfH : (Linf : Subgroup G) ≤ (H : Subgroup G) := by

284 exact (closedSubgroup_sInf_le (L := L) i0).trans i0.1.hLH

285 refine ⟨{ L := Linf

286 hKL := hKinf

287 hLH := hInfH

288 σ := ηinf

289 continuous_σ := hηinf_continuous

290 rightInv := by

291 intro y

292 calc

293 leftQuotientProjection (Linf : Subgroup G) (H : Subgroup G) hInfH (ηinf y)

294 = leftQuotientProjection (i0.1.L : Subgroup G) (H : Subgroup G) i0.1.hLH

295 (leftQuotientProjection (Linf : Subgroup G) (i0.1.L : Subgroup G)

296 (closedSubgroup_sInf_le (L := L) i0) (ηinf y)) := by

297 convert

298 (leftQuotientProjection_comp_apply

299 (K := (Linf : Subgroup G)) (H := (i0.1.L : Subgroup G))

300 (L := (H : Subgroup G)) (closedSubgroup_sInf_le (L := L) i0)

301 i0.1.hLH (ηinf y)).symm

302 _ = leftQuotientProjection (i0.1.L : Subgroup G) (H : Subgroup G) i0.1.hLH

303 (i0.1.σ y) := by

304 exact congrArg

305 (leftQuotientProjection (i0.1.L : Subgroup G) (H : Subgroup G) i0.1.hLH)

306 (congrFun (hηinf_fac i0) y)

307 _ = y := i0.1.rightInv y

308 one_eq := hηinf_one }, ?_⟩

309 intro a ha

310 refine ⟨closedSubgroup_sInf_le (L := L) ⟨a, ha⟩, ?_⟩

311 exact hηinf_fac ⟨a, ha⟩

312

313end LeftQuotientSectionData

314

315/--

316General section theorem for left quotient projections between closed subgroups of a profinite

317group.

318-/

319theorem leftQuotientProjection_hasContinuousSection

320 (K H : ClosedSubgroup G)

321 (hKH : (K : Subgroup G) ≤ (H : Subgroup G)) :

322 ∃ σ : G ⧸ (H : Subgroup G) → G ⧸ (K : Subgroup G),

323 Continuous σ ∧

324 Function.RightInverse σ

325 (leftQuotientProjection (K : Subgroup G) (H : Subgroup G) hKH) ∧

326 σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =

327 QuotientGroup.mk (s := (K : Subgroup G)) (1 : G) := by

328 classical

329 let P := LeftQuotientSectionData (G := G) K H

330 letI : Nonempty P := ⟨LeftQuotientSectionData.top (G := G) hKH⟩

331 obtain ⟨m, hmmax⟩ := zorn_le_nonempty (α := P) <| by

332 intro c hc hcn

333 rcases LeftQuotientSectionData.exists_upperBound_of_chain (G := G) (K := K) (H := H)

334 c hc hcn with ⟨ub, hub⟩

335 exact ⟨ub, hub⟩

336 have hmLK : m.L = K := by

337 by_contra hne

338 have hnotle : ¬ (m.L : Subgroup G) ≤ (K : Subgroup G) := by

339 intro hmK

340 apply hne

341 ext x

342 change x ∈ (m.L : Subgroup G) ↔ x ∈ (K : Subgroup G)

343 exact ⟨fun hx => hmK hx, fun hx => m.hKL hx⟩

344 letI : CompactSpace ↥(m.L : Subgroup G) :=

345 m.L.isClosed'.isClosedEmbedding_subtypeVal.compactSpace

346 rcases exists_mem_of_not_le (G := G) (K := K) (L := m.L) hnotle with ⟨x, hxL, hxK⟩

347 let KT : ClosedSubgroup ↥(m.L : Subgroup G) := {

348 toSubgroup := (K : Subgroup G).subgroupOf (m.L : Subgroup G)

349 isClosed' := by

350 change IsClosed (((↑) : ↥(m.L : Subgroup G) → G) ⁻¹'

351 (K : Subgroup G).carrier)

352 exact K.isClosed'.preimage continuous_subtype_val }

353 let xT : ↥(m.L : Subgroup G) := ⟨x, hxL⟩

354 have hxTK : xT ∉ (KT : Set ↥(m.L : Subgroup G)) := by

355 change x ∉ (K : Subgroup G)

356 exact hxK

357 obtain ⟨N, hKTN, hxN⟩ :=

358 exists_openSubgroup_ge_closedSubgroup_not_mem (G := ↥(m.L : Subgroup G)) KT hxTK

359 let L' : ClosedSubgroup G := closedSubgroupOfOpenSubgroup (G := G) m.L N

360 have hL'm : (L' : Subgroup G) ≤ (m.L : Subgroup G) :=

361 closedSubgroupOfOpenSubgroup_le (G := G) m.L N

362 have hKL' : (K : Subgroup G) ≤ (L' : Subgroup G) := by

363 intro g hg

364 have hgT : (⟨g, m.hKL hg⟩ : ↥(m.L : Subgroup G)) ∈ (KT : Subgroup ↥(m.L : Subgroup G)) := by

365 simpa [KT, Subgroup.mem_subgroupOf] using hg

366 have hgN : (⟨g, m.hKL hg⟩ : ↥(m.L : Subgroup G)) ∈ (N : Subgroup ↥(m.L : Subgroup G)) :=

367 hKTN hgT

368 exact (mem_closedSubgroupOfOpenSubgroup (G := G) (T := m.L) (N := N)

369 (x := ⟨g, m.hKL hg⟩)).2 hgN

370 have hL'H : (L' : Subgroup G) ≤ (H : Subgroup G) := hL'm.trans m.hLH

371 have hL'open :

372 IsOpen (((L' : Subgroup G).subgroupOf (m.L : Subgroup G)) : Set ↥(m.L : Subgroup G)) := by

373 rw [closedSubgroupOfOpenSubgroup_subgroupOf_eq (G := G) m.L N]

374 exact N.isOpen'

375 have hxL' : x ∉ (L' : Subgroup G) := by

376 intro hxL'

377 have : xT ∈ (N : Subgroup ↥(m.L : Subgroup G)) := by

378 exact (mem_closedSubgroupOfOpenSubgroup (G := G) (T := m.L) (N := N)

379 (x := xT)).1 (by simpa [xT] using hxL')

380 exact hxN this

381 obtain ⟨ξ, hξcont, hξright, hξone⟩ :=

382 leftQuotientProjection_hasContinuousSection_of_openSubgroup (G := G) L' m.L hL'm hL'open

383 let m' : P :=

384 { L := L'

385 hKL := hKL'

386 hLH := hL'H

387 σ := ξ ∘ m.σ

388 continuous_σ := hξcont.comp m.continuous_σ

389 rightInv := by

390 intro y

391 calc

392 leftQuotientProjection (L' : Subgroup G) (H : Subgroup G) hL'H ((ξ ∘ m.σ) y)

393 = leftQuotientProjection (m.L : Subgroup G) (H : Subgroup G) m.hLH

394 (leftQuotientProjection (L' : Subgroup G) (m.L : Subgroup G) hL'm

395 (ξ (m.σ y))) := by

396 change

397 leftQuotientProjection (L' : Subgroup G) (H : Subgroup G) hL'H

398 (ξ (m.σ y)) =

399 leftQuotientProjection (m.L : Subgroup G) (H : Subgroup G)

400 m.hLH

401 (leftQuotientProjection (L' : Subgroup G)

402 (m.L : Subgroup G) hL'm (ξ (m.σ y)))

403 exact

404 (leftQuotientProjection_comp_apply

405 (K := (L' : Subgroup G)) (H := (m.L : Subgroup G))

406 (L := (H : Subgroup G)) hL'm m.hLH (ξ (m.σ y))).symm

407 _ = leftQuotientProjection (m.L : Subgroup G) (H : Subgroup G) m.hLH (m.σ y) := by

408 rw [hξright (m.σ y)]

409 _ = y := m.rightInv y

410 one_eq := by

411 change ξ (m.σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))) =

412 QuotientGroup.mk (s := (L' : Subgroup G)) (1 : G)

413 rw [m.one_eq]

414 exact hξone }

415 have hmm' : m ≤ m' := by

416 refine ⟨hL'm, ?_⟩

417 funext y

418 exact hξright (m.σ y)

419 have hm'm : m' ≤ m := hmmax hmm'

420 rcases hm'm with ⟨hm'mL, -⟩

421 exact hxL' (hm'mL hxL)

422 have hLKsub : (m.L : Subgroup G) = (K : Subgroup G) := congrArg ClosedSubgroup.toSubgroup hmLK

423 have hmLleK : (m.L : Subgroup G) ≤ (K : Subgroup G) := by

424 intro x hx

425 simpa [hLKsub] using hx

426 let σ : G ⧸ (H : Subgroup G) → G ⧸ (K : Subgroup G) :=

427 leftQuotientProjection (m.L : Subgroup G) (K : Subgroup G) hmLleK ∘ m.σ

428 refine ⟨σ, (continuous_leftQuotientProjection

429 (K := (m.L : Subgroup G)) (H := (K : Subgroup G)) hmLleK).comp m.continuous_σ, ?_, ?_⟩

430 · intro y

431 have hproof : hmLleK.trans hKH = m.hLH := Subsingleton.elim _ _

432 calc

433 leftQuotientProjection (K : Subgroup G) (H : Subgroup G) hKH (σ y) =

434 leftQuotientProjection

435 (m.L : Subgroup G)

436 (H : Subgroup G)

437 (hmLleK.trans hKH)

438 (m.σ y) := by

439 simpa only [σ, Function.comp] using

440 (leftQuotientProjection_comp_apply

441 (K := (m.L : Subgroup G)) (H := (K : Subgroup G))

442 (L := (H : Subgroup G)) hmLleK hKH (m.σ y))

443 _ = leftQuotientProjection (m.L : Subgroup G) (H : Subgroup G) m.hLH (m.σ y) := by

444 rw [hproof]

445 _ = y := m.rightInv y

446 · calc

447 σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))

448 = leftQuotientProjection (m.L : Subgroup G) (K : Subgroup G) hmLleK

449 (m.σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))) := by

450 rfl

451 _ = leftQuotientProjection (m.L : Subgroup G) (K : Subgroup G) hmLleK

452 (QuotientGroup.mk (s := (m.L : Subgroup G)) (1 : G)) := by

453 rw [m.one_eq]

454 _ = QuotientGroup.mk (s := (K : Subgroup G)) (1 : G) := rfl

455

456/--

457A quotient by a closed normal subgroup of a profinite group admits a continuous section that

458sends the identity coset to the identity.

459-/

460theorem exists_continuousSection_quotientMk_of_isClosed

461 (H : Subgroup G) (hH : IsClosed (H : Set G)) :

462 ∃ σ : (G ⧸ H) → G,

463 Continuous σ ∧

464 Function.RightInverse σ (QuotientGroup.mk (s := H)) ∧

465 σ (QuotientGroup.mk (s := H) (1 : G)) = 1 := by

466 let K0 : ClosedSubgroup G := ⟨⊥, by

467 change IsClosed ({(1 : G)} : Set G)

468 simp only [finite_singleton, Finite.isClosed]⟩

469 let HC : ClosedSubgroup G := ⟨H, hH⟩

470 have hbotH : (⊥ : Subgroup G) ≤ H := by

471 intro x hx

472 have hx1 : x = 1 := by

473 simpa [Subgroup.mem_bot] using hx

474 simp only [hx1, one_mem]

475 obtain ⟨σ0, hσ0cont, hσ0right, hσ0one⟩ :=

476 leftQuotientProjection_hasContinuousSection (G := G) K0 HC hbotH

477 let e : G ≃ₜ G ⧸ (⊥ : Subgroup G) := quotientBotHomeomorph (G := G)

478 refine ⟨e.symm ∘ σ0, e.symm.continuous.comp hσ0cont, ?_, ?_⟩

479 · intro y

480 calc

481 QuotientGroup.mk (s := H) ((e.symm ∘ σ0) y)

482 = leftQuotientProjection (⊥ : Subgroup G) H hbotH

483 (e ((e.symm ∘ σ0) y)) := by

484 rfl

485 _ = leftQuotientProjection (⊥ : Subgroup G) H hbotH (σ0 y) := by

486 exact congrArg (leftQuotientProjection (⊥ : Subgroup G) H hbotH) (e.right_inv (σ0 y))

487 _ = y := hσ0right y

488 · change e.symm (σ0 (QuotientGroup.mk (s := H) (1 : G))) = 1

489 rw [hσ0one]

490 change e.symm (e (1 : G)) = 1

491 exact e.left_inv (1 : G)

492

493end ProCGroups.ProC