Yamaguchi Lean 4 Library
ProCGroups/Presentations/Profinite.lean
ProCGroups/Presentations/Profinite/Source

ProCGroups/Presentations/Profinite.lean

1import Mathlib.GroupTheory.PGroup
2import ProCGroups.FreeProC.Basic
3import ProCGroups.Topologies.TopologicallyCharacteristicSubgroups
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/Presentations/Profinite.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Profinite presentations
16Presentation-level API for profinite groups, finite quotients, relators, and Schreier-Tietze restrictions.
17-/
19noncomputable section
21namespace ProCGroups.Presentations
23universe u
25section ClosedNormalClosure
27variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
29/-- The closed normal subgroup generated by a set of profinite relators. -/
30def Subgroup.closedNormalClosure (R : Set F) : Subgroup F :=
31 (Subgroup.normalClosure R).topologicalClosure
33/-- The closed normal subgroup generated by a set of profinite relators. -/
34abbrev closedNormalClosure (R : Set F) : Subgroup F :=
35 Subgroup.closedNormalClosure R
37instance closedNormalClosure_normal (R : Set F) : (closedNormalClosure R).Normal := by
38 dsimp [closedNormalClosure, Subgroup.closedNormalClosure]
39 exact Subgroup.is_normal_topologicalClosure (Subgroup.normalClosure R)
41theorem closedNormalClosure_isClosed (R : Set F) :
42 IsClosed ((closedNormalClosure R : Subgroup F) : Set F) := by
43 exact Subgroup.isClosed_topologicalClosure _
45theorem subset_closedNormalClosure (R : Set F) :
46 R ⊆ closedNormalClosure R := by
47 intro x hx
48 exact Subgroup.le_topologicalClosure _
49 (Subgroup.subset_normalClosure hx)
51theorem one_mem_closedNormalClosure (R : Set F) :
52 (1 : F) ∈ closedNormalClosure R :=
53 Subgroup.one_mem _
56 ({1} : Set F) ⊆ closedNormalClosure R := by
57 intro x hx
58 subst x
62 {R D : Set F} (hD : D ⊆ ({1} : Set F)) :
63 D ⊆ closedNormalClosure R := by
64 intro x hx
68 {R : Set F} {N : Subgroup F} [N.Normal]
69 (hNclosed : IsClosed (N : Set F)) (hR : R ⊆ N) :
70 closedNormalClosure R ≤ N := by
71 exact Subgroup.topologicalClosure_minimal _
72 (Subgroup.normalClosure_le_normal hR) hNclosed
74theorem closedNormalClosure_mono {R S : Set F} (hRS : R ⊆ S) :
75 closedNormalClosure R ≤ closedNormalClosure S := by
77 (F := F) (N := closedNormalClosure S)
79 exact fun x hx => subset_closedNormalClosure (F := F) S (hRS hx)
82 {R S : Set F}
83 (hRS : R ⊆ closedNormalClosure S)
84 (hSR : S ⊆ closedNormalClosure R) :
85 closedNormalClosure R = closedNormalClosure S := by
86 apply le_antisymm
88 (F := F) (N := closedNormalClosure S)
91 (F := F) (N := closedNormalClosure R)
94theorem closedNormalClosure_union_eq_left
95 {R D : Set F} (hD : D ⊆ closedNormalClosure R) :
96 closedNormalClosure (R ∪ D) = closedNormalClosure R := by
97 apply le_antisymm
99 (F := F) (N := closedNormalClosure R)
101 intro x hx
102 exact hx.elim
103 (fun hxR => subset_closedNormalClosure (F := F) R hxR)
104 (fun hxD => hD hxD)
105 · exact closedNormalClosure_mono (F := F) (Set.subset_union_left)
107end ClosedNormalClosure
109/-- A quotient-by-kernel record `1 → K → F → G → 1`.
111The source `F` is left explicit: in applications it is normally supplied by
112`FreeProC.IsFreeProCGroup`, while Tietze moves only need to know the kernel and the
113continuous epimorphism being transported. -/
114def IsQuotientByKernel (C : ProCGroups.FiniteGroupClass.{u})
115 {F G : Type u} [Group F] [Group G]
116 [TopologicalSpace F] [TopologicalSpace G]
117 [IsTopologicalGroup F] [IsTopologicalGroup G]
118 (K : Subgroup F) : Prop :=
119 ProCGroups.ProC.IsProCGroup C G ∧
120 ∃ π : F →ₜ* G, Function.Surjective π ∧ π.toMonoidHom.ker = K
122/-- A relator presentation whose source is a chosen free pro-`C` group. -/
124 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
125 {X F G : Type u} [TopologicalSpace X]
126 [Group F] [Group G]
127 [TopologicalSpace F] [TopologicalSpace G]
128 [IsTopologicalGroup F] [IsTopologicalGroup G]
129 (ι : X → F) (R : Set F) : Prop :=
131 ProC (G := G) ∧
132 ∃ π : F →ₜ* G, Function.Surjective π ∧ π.toMonoidHom.ker = closedNormalClosure R
134/-- The concrete finite-class specialization of `IsFreePresentationOf`. -/
135def IsFreePresentationOfClass (C : ProCGroups.FiniteGroupClass.{u})
136 {X F G : Type u} [TopologicalSpace X]
137 [Group F] [Group G]
138 [TopologicalSpace F] [TopologicalSpace G]
139 [IsTopologicalGroup F] [IsTopologicalGroup G]
140 (ι : X → F) (R : Set F) : Prop :=
143 (G := G) ι R
147variable {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}
148variable {X F G : Type u} [TopologicalSpace X]
149variable [Group F] [Group G]
150variable [TopologicalSpace F] [TopologicalSpace G]
151variable [IsTopologicalGroup F] [IsTopologicalGroup G]
152variable {ι : X → F} {R : Set F}
154/-- The chosen quotient map recorded by a free pro-`C` presentation. -/
155def π (h : IsFreePresentationOf (G := G) ProC ι R) : F →ₜ* G :=
156 Classical.choose h.2.2
158/-- The source of a free presentation is free pro-`C`. -/
159theorem freeSource (h : IsFreePresentationOf (G := G) ProC ι R) :
161 h.1
163/-- The target of a free presentation is pro-`C`. -/
164theorem targetProC (h : IsFreePresentationOf (G := G) ProC ι R) :
165 ProC (G := G) :=
166 h.2.1
168/-- The chosen quotient map is surjective. -/
169theorem π_surjective (h : IsFreePresentationOf (G := G) ProC ι R) :
170 Function.Surjective h.π :=
171 (Classical.choose_spec h.2.2).1
173/-- The kernel of the chosen quotient map is the closed normal closure of the relators. -/
174theorem kernel_eq_closedNormalClosure (h : IsFreePresentationOf (G := G) ProC ι R) :
175 h.π.toMonoidHom.ker = closedNormalClosure R :=
176 (Classical.choose_spec h.2.2).2
180/-- Forget the chosen free source from a concrete free pro-`C` relator presentation. -/
181theorem IsFreePresentationOfClass.isQuotientByKernel
182 (C : ProCGroups.FiniteGroupClass.{u})
183 {X F G : Type u} [TopologicalSpace X]
184 [Group F] [Group G]
185 [TopologicalSpace F] [TopologicalSpace G]
186 [IsTopologicalGroup F] [IsTopologicalGroup G]
187 {ι : X → F} {R : Set F} :
188 IsFreePresentationOfClass (G := G) C ι R →
189 IsQuotientByKernel C (F := F) (G := G) (closedNormalClosure R) := by
190 intro h
191 rcases h with ⟨_hfree, hG, π, hπsurj, hπker⟩
192 exact ⟨hG, π, hπsurj, hπker⟩
194/-- Transport a pro-`C'` presentation to a pro-`C` presentation along inclusion of
195finite classes. -/
197 (C' C : ProCGroups.FiniteGroupClass.{u})
198 {F G : Type u} [Group F] [Group G]
199 [TopologicalSpace F] [TopologicalSpace G]
200 [IsTopologicalGroup F] [IsTopologicalGroup G]
201 (K : Subgroup F) :
202 (∀ {Q : Type u} [Group Q], C' Q → C Q) →
203 IsQuotientByKernel C' (F := F) (G := G) K →
204 IsQuotientByKernel C (F := F) (G := G) K := by
205 intro hsub hpres
206 rcases hpres with ⟨hG, π, hπsurj, hπker⟩
207 exact ⟨hG.mono hsub, π, hπsurj, hπker⟩
209/-- Continuous Tietze data between two presentation kernels. It is the profinite
210analogue of the mutual-map data used in the discrete ReidemeisterSchreier library, but stated directly
211for closed kernels rather than syntactic relator sets. -/
213 {F E : Type u} [Group F] [Group E]
214 [TopologicalSpace F] [TopologicalSpace E]
215 (K : Subgroup F) (L : Subgroup E) where
216 toHom : F →ₜ* E
217 invHom : E →ₜ* F
218 mapsKernel : K ≤ Subgroup.comap toHom.toMonoidHom L
219 mapsTargetKernel : L ≤ Subgroup.comap invHom.toMonoidHom K
220 inv_toHom : ∀ x : F, invHom (toHom x) * x⁻¹ ∈ K
221 to_invHom : ∀ y : E, toHom (invHom y) * y⁻¹ ∈ L
225variable {F E H : Type u}
226variable [Group F] [Group E] [Group H]
227variable [TopologicalSpace F] [TopologicalSpace E] [TopologicalSpace H]
228variable {K : Subgroup F} {L : Subgroup E} {M : Subgroup H}
230/-- The identity Tietze datum. -/
231def refl (K : Subgroup F) : KernelTietzeData K K where
232 toHom := ContinuousMonoidHom.id F
233 invHom := ContinuousMonoidHom.id F
234 mapsKernel := by intro x hx; exact hx
235 mapsTargetKernel := by intro x hx; exact hx
236 inv_toHom := by intro x; simp only [ContinuousMonoidHom.id_toFun, mul_inv_cancel, one_mem]
237 to_invHom := by intro x; simp only [ContinuousMonoidHom.id_toFun, mul_inv_cancel, one_mem]
239/-- Reverse a Tietze datum. -/
240def symm (D : KernelTietzeData K L) : KernelTietzeData L K where
241 toHom := D.invHom
242 invHom := D.toHom
243 mapsKernel := D.mapsTargetKernel
244 mapsTargetKernel := D.mapsKernel
245 inv_toHom := D.to_invHom
246 to_invHom := D.inv_toHom
248/-- Compose Tietze data. -/
249def trans (D₁ : KernelTietzeData K L) (D₂ : KernelTietzeData L M) :
251 toHom := D₂.toHom.comp D₁.toHom
252 invHom := D₁.invHom.comp D₂.invHom
253 mapsKernel := by
254 intro x hx
255 exact D₂.mapsKernel (D₁.mapsKernel hx)
256 mapsTargetKernel := by
257 intro x hx
258 exact D₁.mapsTargetKernel (D₂.mapsTargetKernel hx)
259 inv_toHom := by
260 intro x
261 let y : E := D₁.toHom x
262 have h₂ : D₂.invHom (D₂.toHom y) * y⁻¹ ∈ L :=
263 D₂.inv_toHom y
264 have h₂map : D₁.invHom (D₂.invHom (D₂.toHom y) * y⁻¹) ∈ K :=
265 D₁.mapsTargetKernel h₂
266 have h₂map' :
267 D₁.invHom (D₂.invHom (D₂.toHom y)) *
268 (D₁.invHom y)⁻¹ ∈ K := by
269 simpa using h₂map
270 have h₁ : D₁.invHom y * x⁻¹ ∈ K :=
271 D₁.inv_toHom x
272 have hprod := K.mul_mem h₂map' h₁
273 have hmul :
274 (D₁.invHom (D₂.invHom (D₂.toHom y)) *
275 (D₁.invHom y)⁻¹) *
276 (D₁.invHom y * x⁻¹) =
277 D₁.invHom (D₂.invHom (D₂.toHom y)) * x⁻¹ := by
278 group
279 simpa [MonoidHom.comp_apply, y, hmul] using hprod
280 to_invHom := by
281 intro z
282 let y : E := D₂.invHom z
283 have h₁ : D₁.toHom (D₁.invHom y) * y⁻¹ ∈ L :=
284 D₁.to_invHom y
285 have h₁map : D₂.toHom (D₁.toHom (D₁.invHom y) * y⁻¹) ∈ M :=
286 D₂.mapsKernel h₁
287 have h₁map' :
288 D₂.toHom (D₁.toHom (D₁.invHom y)) *
289 (D₂.toHom y)⁻¹ ∈ M := by
290 simpa using h₁map
291 have h₂ : D₂.toHom y * z⁻¹ ∈ M :=
292 D₂.to_invHom z
293 have hprod := M.mul_mem h₁map' h₂
294 have hmul :
295 (D₂.toHom (D₁.toHom (D₁.invHom y)) *
296 (D₂.toHom y)⁻¹) *
297 (D₂.toHom y * z⁻¹) =
298 D₂.toHom (D₁.toHom (D₁.invHom y)) * z⁻¹ := by
299 group
300 simpa [MonoidHom.comp_apply, y, hmul] using hprod
302/-- Tietze data induce an algebraic equivalence of quotient groups. -/
303def quotientMulEquiv (D : KernelTietzeData K L) [K.Normal] [L.Normal] :
304 F ⧸ K ≃* E ⧸ L := by
305 let F₁ : F ⧸ K →* E ⧸ L :=
306 QuotientGroup.lift K ((QuotientGroup.mk' L).comp D.toHom.toMonoidHom) (by
307 intro x hx
308 rw [MonoidHom.mem_ker]
309 exact (QuotientGroup.eq_one_iff (N := L) (D.toHom x)).2 (D.mapsKernel hx))
310 let F₂ : E ⧸ L →* F ⧸ K :=
311 QuotientGroup.lift L ((QuotientGroup.mk' K).comp D.invHom.toMonoidHom) (by
312 intro y hy
313 rw [MonoidHom.mem_ker]
314 exact (QuotientGroup.eq_one_iff (N := K) (D.invHom y)).2
315 (D.mapsTargetKernel hy))
316 refine
317 { toFun := F₁
318 invFun := F₂
319 left_inv := ?_
320 right_inv := ?_
321 map_mul' := fun a b => F₁.map_mul a b }
322 · intro x
323 rcases QuotientGroup.mk'_surjective K x with ⟨x, rfl⟩
324 simp only [QuotientGroup.mk'_apply]
325 exact (QuotientGroup.eq_iff_div_mem (N := K)
326 (x := D.invHom (D.toHom x)) (y := x)).2
327 (by simpa [div_eq_mul_inv] using D.inv_toHom x)
328 · intro y
329 rcases QuotientGroup.mk'_surjective L y with ⟨y, rfl⟩
330 simp only [QuotientGroup.mk'_apply]
331 exact (QuotientGroup.eq_iff_div_mem (N := L)
332 (x := D.toHom (D.invHom y)) (y := y)).2
333 (by simpa [div_eq_mul_inv] using D.to_invHom y)
335/-- A continuous multiplicative equivalence gives Tietze data for matching kernels. -/
336def ofContinuousMulEquiv
337 {K : Subgroup F} {L : Subgroup E} (e : F ≃ₜ* E)
338 (hK : ∀ x : F, x ∈ K ↔ e x ∈ L)
339 (hL : ∀ y : E, y ∈ L ↔ e.symm y ∈ K) :
341 toHom := e.toContinuousMonoidHom
342 invHom := e.symm.toContinuousMonoidHom
343 mapsKernel := by
344 intro x hx
345 exact (hK x).1 hx
346 mapsTargetKernel := by
347 intro y hy
348 exact (hL y).1 hy
349 inv_toHom := by
350 intro x
351 simp only [ContinuousMulEquiv.toContinuousMonoidHom_apply, ContinuousMulEquiv.symm_apply_apply,
352 mul_inv_cancel, one_mem]
353 to_invHom := by
354 intro y
355 simp only [ContinuousMulEquiv.toContinuousMonoidHom_apply, ContinuousMulEquiv.apply_symm_apply,
356 mul_inv_cancel, one_mem]
358/-- A continuous multiplicative equivalence gives Tietze data when it maps one kernel
359onto the other. -/
361 {K : Subgroup F} {L : Subgroup E} (e : F ≃ₜ* E)
362 (hmap : K.map e.toContinuousMonoidHom.toMonoidHom = L) :
364 toHom := e.toContinuousMonoidHom
365 invHom := e.symm.toContinuousMonoidHom
366 mapsKernel := by
367 intro x hx
368 change e x ∈ L
369 rw [← hmap]
370 exact ⟨x, hx, rfl⟩
371 mapsTargetKernel := by
372 intro y hy
373 have hyMap : y ∈ K.map e.toContinuousMonoidHom.toMonoidHom := by
374 rw [hmap]
375 exact hy
376 rcases hyMap with ⟨x, hx, hxy⟩
377 have hsymm : e.symm y = x := by
378 simp only [← hxy, ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.coe_coe,
379 ContinuousMulEquiv.toContinuousMonoidHom_apply, ContinuousMulEquiv.symm_apply_apply]
380 simpa [hsymm] using hx
381 inv_toHom := by
382 intro x
383 simp only [ContinuousMulEquiv.toContinuousMonoidHom_apply, ContinuousMulEquiv.symm_apply_apply,
384 mul_inv_cancel, one_mem]
385 to_invHom := by
386 intro y
387 simp only [ContinuousMulEquiv.toContinuousMonoidHom_apply, ContinuousMulEquiv.apply_symm_apply,
388 mul_inv_cancel, one_mem]
392/-- Transport a presentation along profinite Tietze data between its source kernels. -/
394 (C : ProCGroups.FiniteGroupClass.{u})
395 {F E G : Type u} [Group F] [Group E] [Group G]
396 [TopologicalSpace F] [TopologicalSpace E] [TopologicalSpace G]
397 [IsTopologicalGroup F] [IsTopologicalGroup E] [IsTopologicalGroup G]
398 {K : Subgroup F} {L : Subgroup E}
399 (D : KernelTietzeData K L) :
400 IsQuotientByKernel C (F := F) (G := G) K →
401 IsQuotientByKernel C (F := E) (G := G) L := by
402 intro hpres
403 rcases hpres with ⟨hG, π, hπsurj, hπker⟩
404 subst K
405 let ρ : E →ₜ* G := π.comp D.invHom
406 have hρsurj : Function.Surjective ρ := by
407 intro g
408 rcases hπsurj g with ⟨x, rfl⟩
409 refine ⟨D.toHom x, ?_⟩
410 have hx : D.invHom (D.toHom x) * x⁻¹ ∈ π.toMonoidHom.ker := by
411 exact D.inv_toHom x
412 have hmul : π (D.invHom (D.toHom x) * x⁻¹) = 1 := by
413 simpa [MonoidHom.mem_ker] using hx
414 have hmain : π (D.invHom (D.toHom x)) = π x := by
415 have h := congrArg (fun z : G => z * π x) hmul
416 simpa [map_mul, map_inv, mul_assoc] using h
417 exact hmain
418 have hρker : ρ.toMonoidHom.ker = L := by
419 ext y
420 constructor
421 · intro hy
422 have hyK : D.invHom y ∈ π.toMonoidHom.ker := by
423 simpa [ρ, MonoidHom.mem_ker] using hy
424 have hmap : D.toHom (D.invHom y) ∈ L := D.mapsKernel hyK
425 have hrel : D.toHom (D.invHom y) * y⁻¹ ∈ L := D.to_invHom y
426 have hinv : (D.toHom (D.invHom y) * y⁻¹)⁻¹ ∈ L := L.inv_mem hrel
427 have hprod := L.mul_mem hinv hmap
428 simpa using hprod
429 · intro hy
430 have hyKer : D.invHom y ∈ π.toMonoidHom.ker := D.mapsTargetKernel hy
431 rw [MonoidHom.mem_ker]
432 change π (D.invHom y) = 1
433 simpa [MonoidHom.mem_ker] using hyKer
434 exact ⟨hG, ρ, hρsurj, hρker⟩
436/-- Transport a presentation along a continuous multiplicative equivalence of sources. -/
438 (C : ProCGroups.FiniteGroupClass.{u})
439 {F E G : Type u} [Group F] [Group E] [Group G]
440 [TopologicalSpace F] [TopologicalSpace E] [TopologicalSpace G]
441 [IsTopologicalGroup F] [IsTopologicalGroup E] [IsTopologicalGroup G]
442 {K : Subgroup F} {L : Subgroup E}
443 (e : F ≃ₜ* E)
444 (hK : ∀ x : F, x ∈ K ↔ e x ∈ L)
445 (hL : ∀ y : E, y ∈ L ↔ e.symm y ∈ K) :
446 IsQuotientByKernel C (F := F) (G := G) K →
447 IsQuotientByKernel C (F := E) (G := G) L :=
449 (KernelTietzeData.ofContinuousMulEquiv (K := K) (L := L) e hK hL)
451/-- Transport a presentation along a continuous multiplicative equivalence of targets,
452recording the pro-`C` witness for the new target explicitly. -/
454 (C : ProCGroups.FiniteGroupClass.{u})
455 {F G H : Type u} [Group F] [Group G] [Group H]
456 [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H]
457 [IsTopologicalGroup F] [IsTopologicalGroup G] [IsTopologicalGroup H]
458 {K : Subgroup F}
459 (e : G ≃ₜ* H)
460 (hH : ProCGroups.ProC.IsProCGroup C H) :
461 IsQuotientByKernel C (F := F) (G := G) K →
462 IsQuotientByKernel C (F := F) (G := H) K := by
463 intro hpres
464 rcases hpres with ⟨_hG, π, hπsurj, hπker⟩
465 subst K
466 let ρ : F →ₜ* H := e.toContinuousMonoidHom.comp π
467 have hρsurj : Function.Surjective ρ := by
468 intro h
469 rcases hπsurj (e.symm h) with ⟨x, hx⟩
470 refine ⟨x, ?_⟩
471 change e (π x) = h
472 rw [hx]
473 simp only [ContinuousMulEquiv.apply_symm_apply]
474 have hρker : ρ.toMonoidHom.ker = π.toMonoidHom.ker := by
475 ext x
476 constructor
477 · intro hx
478 have hxKer : x ∈ π.toMonoidHom.ker := by
479 rw [MonoidHom.mem_ker] at hx ⊢
480 have hsame : e (π x) = e (1 : G) := by
481 simpa [ρ] using hx
482 exact e.injective hsame
483 exact hxKer
484 · intro hx
485 rw [MonoidHom.mem_ker] at hx ⊢
486 change e (π x) = 1
487 simpa using congrArg e hx
488 exact ⟨hH, ρ, hρsurj, hρker⟩
490end ProCGroups.Presentations