ProCGroups/ProC/Quotients/LeftQuotientProjectionSections.lean
1import ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne
2import ProCGroups.ProC.Quotients.DescendingClosedSubgroupQuotients
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/ProC/Quotients/LeftQuotientProjectionSections.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.ProC
23universe u v
25open InverseSystems
27/-- If an intermediate closed subgroup is not contained in the base subgroup, one can choose an
28element in the set-theoretic difference. This is the witness extraction used in the Zorn
29maximality argument. -/
30theorem exists_mem_of_not_le {G : Type u} [Group G] [TopologicalSpace G] {K L : ClosedSubgroup G}
31 (hnotle : ¬ (L : Subgroup G) ≤ (K : Subgroup G)) :
32 ∃ x : G, x ∈ (L : Subgroup G) ∧ x ∉ (K : Subgroup G) := by
33 by_contra hNo
34 apply hnotle
35 intro x hxL
36 by_cases hxK : x ∈ (K : Set G)
37 · exact hxK
38 · exact False.elim (hNo ⟨x, hxL, hxK⟩)
40variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
42/-- Any open normal subgroup of a profinite group is also a closed subgroup. -/
44 (hG : IsProfiniteGroup G) {x : G} (hx : x ≠ 1) :
45 ∃ U : OpenNormalSubgroup G, x ∉ (U : Subgroup G) := by
46 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
47 letI : T2Space G := IsProfiniteGroup.t2Space hG
48 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
49 let W : Set G := ({x} : Set G)ᶜ
50 have hW : IsOpen W := by
51 simp only [isOpen_compl_iff, finite_singleton, Finite.isClosed, W]
52 have h1W : (1 : G) ∈ W := by
53 simpa [W] using hx.symm
54 obtain ⟨U, hUW⟩ :=
55 exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hW h1W
56 refine ⟨U, ?_⟩
57 intro hxU
58 exact hx <| by
59 have hxW : x ∈ W := hUW hxU
60 simp only [mem_compl_iff, mem_singleton_iff, not_true_eq_false, W] at hxW
62/-- A point outside a closed subgroup of a profinite group is omitted by some open subgroup
63containing that closed subgroup. -/
65 (hG : IsProfiniteGroup G) (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 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
68 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
69 have hxInf :
70 x ∉ sInf {N : Subgroup G | IsOpen (N : Set G) ∧ (K : Subgroup G) ≤ N} := by
71 rw [← closedSubgroup_eq_sInf_open (G := G) K]
72 exact hx
73 rw [Subgroup.mem_sInf] at hxInf
74 push_neg at hxInf
75 rcases hxInf with ⟨U, hU, hxU⟩
76 exact ⟨⟨U, hU.1⟩, hU.2, hxU⟩
78/-- An open subgroup of a closed subgroup of a profinite group, viewed again as a closed subgroup
79of the ambient group. -/
80noncomputable def closedSubgroupOfOpenSubgroup
81 (hG : IsProfiniteGroup G) (T : ClosedSubgroup G) (N : OpenSubgroup T) :
82 ClosedSubgroup G where
84 isClosed' := by
85 letI : IsTopologicalGroup ↥(T : Subgroup G) := by infer_instance
86 let hT : IsProfiniteGroup T := IsProfiniteGroup.of_closedSubgroup (G := G) hG T
87 letI : CompactSpace T := IsProfiniteGroup.compactSpace hT
88 letI : T2Space G := IsProfiniteGroup.t2Space hG
89 have hNclosed : IsClosed ((N : Subgroup T) : Set T) :=
90 Subgroup.isClosed_of_isOpen (N : Subgroup T) N.isOpen'
92 have hEq :
95 ext x
96 constructor <;> rintro ⟨y, hy, rfl⟩ <;> exact ⟨y, hy, rfl⟩
98 rw [← hEq]
99 exact hNcompact.image continuous_subtype_val |>.isClosed
101/-- Membership in the ambient closed subgroup induced by an open subgroup is tested inside the
102original subgroup. -/
103@[simp] theorem mem_closedSubgroupOfOpenSubgroup
104 (hG : IsProfiniteGroup G) {T : ClosedSubgroup G} {N : OpenSubgroup T} {x : T} :
105 (x : G) ∈ (closedSubgroupOfOpenSubgroup (G := G) hG 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⟩
115/-- The ambient closed subgroup attached to an open subgroup of `T` still lies inside `T`. -/
117 (hG : IsProfiniteGroup G) (T : ClosedSubgroup G) (N : OpenSubgroup T) :
118 (closedSubgroupOfOpenSubgroup (G := G) hG T N : Subgroup G) ≤ (T : Subgroup G) := by
119 intro x hx
120 rcases hx with ⟨y, hy, rfl⟩
121 exact y.2
123/-- Passing back to `T` recovers the original open subgroup exactly. -/
124@[simp 900] theorem closedSubgroupOfOpenSubgroup_subgroupOf_eq
125 (hG : IsProfiniteGroup G) (T : ClosedSubgroup G) (N : OpenSubgroup T) :
126 (((closedSubgroupOfOpenSubgroup (G := G) hG T N : ClosedSubgroup G) : Subgroup G).subgroupOf
127 (T : Subgroup G)) = (N : Subgroup T) := by
128 ext x
129 simp only [Subgroup.mem_subgroupOf, mem_closedSubgroupOfOpenSubgroup, OpenSubgroup.mem_toSubgroup]
131/-- The canonical quotient map `G → G/⊥` is a homeomorphism for profinite groups. -/
132noncomputable def quotientBotHomeomorph (hG : IsProfiniteGroup G) :
133 G ≃ₜ G ⧸ (⊥ : Subgroup G) := by
134 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
135 letI : T2Space G := IsProfiniteGroup.t2Space hG
136 letI : IsClosed (((⊥ : Subgroup G) : Set G)) := by
137 change IsClosed ({(1 : G)} : Set G)
138 simp only [finite_singleton, Finite.isClosed]
140 (f := QuotientGroup.mk (s := (⊥ : Subgroup G)))
141 (by
142 simpa using
143 (QuotientGroup.continuous_mk : Continuous
144 (QuotientGroup.mk (s := (⊥ : Subgroup G)) : G → G ⧸ (⊥ : 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⟩)
154/-- The homeomorphism `G ≃ₜ G / ⊥` sends an element to its quotient class. -/
155@[simp 900] theorem quotientBotHomeomorph_apply (hG : IsProfiniteGroup G) (g : G) :
156 quotientBotHomeomorph (G := G) hG g = QuotientGroup.mk (s := (⊥ : Subgroup G)) g :=
157 rfl
159/-- Data of a normalized continuous section of a left quotient projection `G/L → G/H`, ordered so
160that smaller intermediate subgroups correspond to larger elements. This is the Zorn package used
161for the closed-subgroup section theorem. -/
162structure LeftQuotientSectionData (K H : ClosedSubgroup G) where
163 L : ClosedSubgroup G
164 hKL : (K : Subgroup G) ≤ (L : Subgroup G)
165 hLH : (L : Subgroup G) ≤ (H : Subgroup G)
166 σ : G ⧸ (H : Subgroup G) → G ⧸ (L : Subgroup G)
167 continuous_σ : Continuous σ
168 rightInv : Function.RightInverse σ
169 (leftQuotientProjection (L : Subgroup G) (H : Subgroup G) hLH)
170 one_eq :
171 σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =
172 QuotientGroup.mk (s := (L : Subgroup G)) (1 : G)
174namespace LeftQuotientSectionData
176variable {K H : ClosedSubgroup G}
178/-- Order partial left-quotient section data by refinement of intermediate closed subgroups. -/
179instance instLELeftQuotientSectionData : LE (LeftQuotientSectionData (G := G) K H) where
180 le a b :=
181 ∃ hba : (b.L : Subgroup G) ≤ (a.L : Subgroup G),
182 leftQuotientProjection (b.L : Subgroup G) (a.L : Subgroup G) hba ∘ b.σ = a.σ
184/-- Partial left-quotient section data form a preorder under refinement. -/
185instance instPreorderLeftQuotientSectionData : Preorder (LeftQuotientSectionData (G := G) K H) where
186 le_refl a := by
187 refine ⟨le_rfl, ?_⟩
188 funext x
189 simp only [leftQuotientProjection_id, Function.comp_apply, id_eq]
190 le_trans a b c hab hbc := by
191 rcases hab with ⟨hba, hbaσ⟩
192 rcases hbc with ⟨hcb, hcbσ⟩
193 refine ⟨hcb.trans hba, ?_⟩
194 funext x
195 calc
196 leftQuotientProjection (c.L : Subgroup G) (a.L : Subgroup G) (hcb.trans hba) (c.σ x)
197 = leftQuotientProjection (b.L : Subgroup G) (a.L : Subgroup G) hba
198 (leftQuotientProjection (c.L : Subgroup G) (b.L : Subgroup G) hcb (c.σ x)) := by
199 convert
201 (K := (c.L : Subgroup G)) (H := (b.L : Subgroup G))
202 (L := (a.L : Subgroup G)) hcb hba (c.σ x)).symm
203 _ = leftQuotientProjection (b.L : Subgroup G) (a.L : Subgroup G) hba (b.σ x) := by
204 exact congrArg (leftQuotientProjection (b.L : Subgroup G) (a.L : Subgroup G) hba)
205 (congrFun hcbσ x)
206 _ = a.σ x := congrFun hbaσ x
208/-- The maximal element of the Zorn poset, given by the identity section over `H` itself. -/
209def top (hKH : (K : Subgroup G) ≤ (H : Subgroup G)) :
210 LeftQuotientSectionData (G := G) K H where
211 L := H
212 hKL := hKH
213 hLH := le_rfl
214 σ := id
215 continuous_σ := continuous_id
216 rightInv := by
217 intro x
218 simp only [id_eq, leftQuotientProjection_id]
219 one_eq := rfl
221/-- Any nonempty chain of partial sections admits an upper bound obtained by descending to the
222infimum subgroup. This is the Zorn step in the section argument. -/
223theorem exists_upperBound_of_chain
224 (hG : IsProfiniteGroup G) (c : Set (LeftQuotientSectionData (G := G) K H))
225 (hc : IsChain (· ≤ ·) c) (hcn : c.Nonempty) :
226 ∃ ub : LeftQuotientSectionData (G := G) K H, ∀ a ∈ c, a ≤ ub := by
227 classical
228 let I : Type u := {a : LeftQuotientSectionData (G := G) K H // a ∈ c}
229 have hI_nonempty : Nonempty I := by
230 rcases hcn with ⟨a, ha⟩
231 exact ⟨⟨a, ha⟩⟩
232 letI : Nonempty I := hI_nonempty
233 let L : I → ClosedSubgroup G := fun i => i.1.L
234 have hL : ∀ {i j : I}, i ≤ j → (L j : Subgroup G) ≤ (L i : Subgroup G) := by
235 intro i j hij
236 rcases hij with ⟨hji, -⟩
237 exact hji
238 have hdir : Directed (· ≤ ·) (id : I → I) := by
239 intro i j
240 by_cases hij : i = j
241 · subst hij
242 exact ⟨i, le_rfl, le_rfl⟩
243 · have hcmp := hc i.2 j.2 (by
244 intro hij'
245 apply hij
246 exact Subtype.ext hij')
247 rcases hcmp with hij' | hji'
248 · exact ⟨j, hij', le_rfl⟩
249 · exact ⟨i, le_rfl, hji'⟩
250 obtain ⟨ηinf, hηinf_continuous, hηinf_fac, hηinf_one⟩ :=
251 exists_continuous_leftQuotient_lift_of_directed (G := G) hG L hL hdir
252 (η := fun i => i.1.σ) (hηcont := fun i => i.1.continuous_σ)
253 (hηcompat := by
254 intro i j hij
255 rcases hij with ⟨hji, hσ⟩
256 exact hσ)
257 (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))
258 (by
259 intro i
260 exact i.1.one_eq)
261 let Linf : ClosedSubgroup G := closedSubgroup_sInf L
262 have hKinf : (K : Subgroup G) ≤ (Linf : Subgroup G) := by
263 intro x hx
264 change x ∈ iInf fun i => (L i : Subgroup G)
265 rw [Subgroup.mem_iInf]
266 intro i
267 exact i.1.hKL hx
268 let i0 : I := Classical.choice hI_nonempty
269 have hInfH : (Linf : Subgroup G) ≤ (H : Subgroup G) := by
270 exact (closedSubgroup_sInf_le (L := L) i0).trans i0.1.hLH
271 refine ⟨{ L := Linf
272 hKL := hKinf
273 hLH := hInfH
274 σ := ηinf
275 continuous_σ := hηinf_continuous
276 rightInv := by
277 intro y
278 calc
279 leftQuotientProjection (Linf : Subgroup G) (H : Subgroup G) hInfH (ηinf y)
280 = leftQuotientProjection (i0.1.L : Subgroup G) (H : Subgroup G) i0.1.hLH
281 (leftQuotientProjection (Linf : Subgroup G) (i0.1.L : Subgroup G)
282 (closedSubgroup_sInf_le (L := L) i0) (ηinf y)) := by
283 convert
285 (K := (Linf : Subgroup G)) (H := (i0.1.L : Subgroup G))
286 (L := (H : Subgroup G)) (closedSubgroup_sInf_le (L := L) i0)
287 i0.1.hLH (ηinf y)).symm
288 _ = leftQuotientProjection (i0.1.L : Subgroup G) (H : Subgroup G) i0.1.hLH
289 (i0.1.σ y) := by
290 exact congrArg
291 (leftQuotientProjection (i0.1.L : Subgroup G) (H : Subgroup G) i0.1.hLH)
292 (congrFun (hηinf_fac i0) y)
293 _ = y := i0.1.rightInv y
294 one_eq := hηinf_one }, ?_⟩
295 intro a ha
296 refine ⟨closedSubgroup_sInf_le (L := L) ⟨a, ha⟩, ?_⟩
297 exact hηinf_fac ⟨a, ha⟩
301/-- General section theorem for left quotient projections between closed subgroups of a profinite
302group. -/
304 (hG : IsProfiniteGroup G) (K H : ClosedSubgroup G)
305 (hKH : (K : Subgroup G) ≤ (H : Subgroup G)) :
306 ∃ σ : G ⧸ (H : Subgroup G) → G ⧸ (K : Subgroup G),
307 Continuous σ ∧
308 Function.RightInverse σ
309 (leftQuotientProjection (K : Subgroup G) (H : Subgroup G) hKH) ∧
310 σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =
311 QuotientGroup.mk (s := (K : Subgroup G)) (1 : G) := by
312 classical
313 let P := LeftQuotientSectionData (G := G) K H
314 letI : Nonempty P := ⟨LeftQuotientSectionData.top (G := G) hKH⟩
315 obtain ⟨m, hmmax⟩ := zorn_le_nonempty (α := P) <| by
316 intro c hc hcn
317 rcases LeftQuotientSectionData.exists_upperBound_of_chain (G := G) (K := K) (H := H)
318 hG c hc hcn with ⟨ub, hub⟩
319 exact ⟨ub, hub⟩
320 have hmLK : m.L = K := by
321 by_contra hne
322 have hnotle : ¬ (m.L : Subgroup G) ≤ (K : Subgroup G) := by
323 intro hmK
324 apply hne
325 ext x
326 change x ∈ (m.L : Subgroup G) ↔ x ∈ (K : Subgroup G)
327 exact ⟨fun hx => hmK hx, fun hx => m.hKL hx⟩
328 rcases exists_mem_of_not_le (G := G) (K := K) (L := m.L) hnotle with ⟨x, hxL, hxK⟩
329 let hT : IsProfiniteGroup ↥(m.L : Subgroup G) :=
330 IsProfiniteGroup.of_closedSubgroup (G := G) hG m.L
331 let KT : ClosedSubgroup ↥(m.L : Subgroup G) := {
332 toSubgroup := (K : Subgroup G).subgroupOf (m.L : Subgroup G)
333 isClosed' := by
334 change IsClosed (((↑) : ↥(m.L : Subgroup G) → G) ⁻¹' (K : Set G))
335 simpa [Subgroup.coe_subgroupOf] using K.isClosed'.preimage continuous_subtype_val }
336 let xT : ↥(m.L : Subgroup G) := ⟨x, hxL⟩
337 have hxTK : xT ∉ (KT : Set ↥(m.L : Subgroup G)) := by
338 simpa [KT, Subgroup.mem_subgroupOf] using hxK
339 obtain ⟨N, hKTN, hxN⟩ :=
340 exists_openSubgroup_ge_closedSubgroup_not_mem (G := ↥(m.L : Subgroup G)) hT KT hxTK
341 let L' : ClosedSubgroup G := closedSubgroupOfOpenSubgroup (G := G) hG m.L N
342 have hL'm : (L' : Subgroup G) ≤ (m.L : Subgroup G) :=
343 closedSubgroupOfOpenSubgroup_le (G := G) hG m.L N
344 have hKL' : (K : Subgroup G) ≤ (L' : Subgroup G) := by
345 intro g hg
346 have hgT : (⟨g, m.hKL hg⟩ : ↥(m.L : Subgroup G)) ∈ (KT : Subgroup ↥(m.L : Subgroup G)) := by
347 simpa [KT, Subgroup.mem_subgroupOf] using hg
348 have hgN : (⟨g, m.hKL hg⟩ : ↥(m.L : Subgroup G)) ∈ (N : Subgroup ↥(m.L : Subgroup G)) :=
349 hKTN hgT
350 exact (mem_closedSubgroupOfOpenSubgroup (G := G) hG (T := m.L) (N := N)
351 (x := ⟨g, m.hKL hg⟩)).2 hgN
352 have hL'H : (L' : Subgroup G) ≤ (H : Subgroup G) := hL'm.trans m.hLH
353 have hL'open :
354 IsOpen (((L' : Subgroup G).subgroupOf (m.L : Subgroup G)) : Set ↥(m.L : Subgroup G)) := by
355 rw [closedSubgroupOfOpenSubgroup_subgroupOf_eq (G := G) hG m.L N]
356 exact N.isOpen'
357 have hxL' : x ∉ (L' : Subgroup G) := by
358 intro hxL'
359 have : xT ∈ (N : Subgroup ↥(m.L : Subgroup G)) := by
360 exact (mem_closedSubgroupOfOpenSubgroup (G := G) hG (T := m.L) (N := N)
361 (x := xT)).1 (by simpa [xT] using hxL')
362 exact hxN this
363 obtain ⟨ξ, hξcont, hξright, hξone⟩ :=
364 leftQuotientProjection_hasContinuousSection_of_openSubgroup (G := G) hG L' m.L hL'm hL'open
365 let m' : P :=
366 { L := L'
367 hKL := hKL'
368 hLH := hL'H
369 σ := ξ ∘ m.σ
370 continuous_σ := hξcont.comp m.continuous_σ
371 rightInv := by
372 intro y
373 calc
374 leftQuotientProjection (L' : Subgroup G) (H : Subgroup G) hL'H ((ξ ∘ m.σ) y)
375 = leftQuotientProjection (m.L : Subgroup G) (H : Subgroup G) m.hLH
376 (leftQuotientProjection (L' : Subgroup G) (m.L : Subgroup G) hL'm
377 (ξ (m.σ y))) := by
378 convert
380 (K := (L' : Subgroup G)) (H := (m.L : Subgroup G))
381 (L := (H : Subgroup G)) hL'm m.hLH (ξ (m.σ y))).symm
382 _ = leftQuotientProjection (m.L : Subgroup G) (H : Subgroup G) m.hLH (m.σ y) := by
383 rw [hξright (m.σ y)]
384 _ = y := m.rightInv y
385 one_eq := by
386 change ξ (m.σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))) =
387 QuotientGroup.mk (s := (L' : Subgroup G)) (1 : G)
388 rw [m.one_eq]
389 exact hξone }
390 have hmm' : m ≤ m' := by
391 refine ⟨hL'm, ?_⟩
392 funext y
393 exact hξright (m.σ y)
394 have hm'm : m' ≤ m := hmmax hmm'
395 rcases hm'm with ⟨hm'mL, -⟩
396 exact hxL' (hm'mL hxL)
397 have hLKsub : (m.L : Subgroup G) = (K : Subgroup G) := congrArg ClosedSubgroup.toSubgroup hmLK
398 have hmLleK : (m.L : Subgroup G) ≤ (K : Subgroup G) := by
399 intro x hx
400 simpa [hLKsub] using hx
401 let σ : G ⧸ (H : Subgroup G) → G ⧸ (K : Subgroup G) :=
402 leftQuotientProjection (m.L : Subgroup G) (K : Subgroup G) hmLleK ∘ m.σ
403 refine ⟨σ, (continuous_leftQuotientProjection
404 (K := (m.L : Subgroup G)) (H := (K : Subgroup G)) hmLleK).comp m.continuous_σ, ?_, ?_⟩
405 · intro y
406 have hproof : hmLleK.trans hKH = m.hLH := Subsingleton.elim _ _
407 calc
408 leftQuotientProjection (K : Subgroup G) (H : Subgroup G) hKH (σ y) =
410 (m.L : Subgroup G)
411 (H : Subgroup G)
412 (hmLleK.trans hKH)
413 (m.σ y) := by
414 simpa only [σ, Function.comp] using
416 (K := (m.L : Subgroup G)) (H := (K : Subgroup G))
417 (L := (H : Subgroup G)) hmLleK hKH (m.σ y))
418 _ = leftQuotientProjection (m.L : Subgroup G) (H : Subgroup G) m.hLH (m.σ y) := by
419 rw [hproof]
420 _ = y := m.rightInv y
421 · calc
422 σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))
423 = leftQuotientProjection (m.L : Subgroup G) (K : Subgroup G) hmLleK
424 (m.σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))) := by
425 rfl
426 _ = leftQuotientProjection (m.L : Subgroup G) (K : Subgroup G) hmLleK
427 (QuotientGroup.mk (s := (m.L : Subgroup G)) (1 : G)) := by
428 rw [m.one_eq]
429 _ = QuotientGroup.mk (s := (K : Subgroup G)) (1 : G) := rfl
431/-- A quotient by a closed normal subgroup of a profinite group admits a continuous section that
432sends the identity coset to the identity. -/
434 (H : Subgroup G) :
435 IsProfiniteGroup G →
436 IsClosed (H : Set G) →
437 ∃ σ : (G ⧸ H) → G,
438 Continuous σ ∧
439 Function.RightInverse σ (QuotientGroup.mk (s := H)) ∧
440 σ (QuotientGroup.mk (s := H) (1 : G)) = 1 := by
441 intro hG hH
442 letI : T2Space G := IsProfiniteGroup.t2Space hG
443 let K0 : ClosedSubgroup G := ⟨⊥, by
444 change IsClosed ({(1 : G)} : Set G)
445 simp only [finite_singleton, Finite.isClosed]⟩
446 let HC : ClosedSubgroup G := ⟨H, hH⟩
447 have hbotH : (⊥ : Subgroup G) ≤ H := by
448 intro x hx
449 have hx1 : x = 1 := by
450 simpa [Subgroup.mem_bot] using hx
451 simp only [hx1, one_mem]
452 obtain ⟨σ0, hσ0cont, hσ0right, hσ0one⟩ :=
453 leftQuotientProjection_hasContinuousSection (G := G) hG K0 HC hbotH
454 let e : G ≃ₜ G ⧸ (⊥ : Subgroup G) := quotientBotHomeomorph (G := G) hG
455 refine ⟨e.symm ∘ σ0, e.symm.continuous.comp hσ0cont, ?_, ?_⟩
456 · intro y
457 calc
458 QuotientGroup.mk (s := H) ((e.symm ∘ σ0) y)
459 = leftQuotientProjection (⊥ : Subgroup G) H hbotH
460 (e ((e.symm ∘ σ0) y)) := by
461 rfl
462 _ = leftQuotientProjection (⊥ : Subgroup G) H hbotH (σ0 y) := by
463 exact congrArg (leftQuotientProjection (⊥ : Subgroup G) H hbotH) (e.right_inv (σ0 y))
464 _ = y := hσ0right y
465 · change e.symm (σ0 (QuotientGroup.mk (s := H) (1 : G))) = 1
466 rw [hσ0one]
467 change e.symm (e (1 : G)) = 1
468 exact e.left_inv (1 : G)
470end ProCGroups.ProC