FenchelNielsenZomorrodian/Profinite/FGroup.lean
1import FenchelNielsenZomorrodian.Discrete.Core.Signature
2import Mathlib.GroupTheory.Solvable
3import ProCGroups.FiniteStepSolvableQuotients.Commutators.DerivedSeriesAndQuotients
4import ProCGroups.Presentations.SchreierTietze.Restricted
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/FenchelNielsenZomorrodian/Profinite/FGroup.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Profinite Fenchel groups
17Defines profinite Fenchel signatures, generators, inertia, presentations, derived-series notation, torsion-free open subgroups, and quotient-derived-length predicates.
18-/
20namespace FenchelNielsen
22universe u v
24open scoped BigOperators
25open ProCGroups.FiniteStepSolvableQuotients
26open ProCGroups.ProC
28namespace ContinuousMonoidHom
30variable {F G A : Type u}
31variable [Group F] [Group G] [Group A]
32variable [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace A]
34/-- Descend a continuous homomorphism along a continuous surjection, using a kernel inclusion.
36This is the presentation quotient bridge used for profinite `F`-groups: a continuous homomorphism
37out of the free profinite source descends to the presented group once it kills the presentation
38kernel.
39-/
40noncomputable def liftOfSurjective
41 [CompactSpace F] [T2Space G]
43 (φ : F →ₜ* A) (hker : π.toMonoidHom.ker ≤ φ.toMonoidHom.ker) :
44 G →ₜ* A := by
45 let ψ : G →* A :=
46 (π.toMonoidHom.liftOfSurjective hπ) ⟨φ.toMonoidHom, hker⟩
47 have hψcomp : ψ.comp π.toMonoidHom = φ.toMonoidHom := by
48 ext x
49 simp only [ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.liftOfSurjective, MonoidHom.coe_coe,
50 MonoidHom.liftOfRightInverse_comp, ψ]
52 convert φ.continuous_toFun using 1
53 funext x
54 exact MonoidHom.ext_iff.mp hψcomp x
55 exact
56 { toMonoidHom := ψ
57 continuous_toFun :=
58 (IsQuotientMap.of_surjective_continuous
59 hπ π.continuous_toFun).continuous_iff.2 hcomp_continuous }
61@[simp] theorem liftOfSurjective_apply
62 [CompactSpace F] [T2Space G]
64 (φ : F →ₜ* A) (hker : π.toMonoidHom.ker ≤ φ.toMonoidHom.ker)
65 (x : F) :
66 liftOfSurjective π hπ φ hker (π x) = φ x := by
67 change
68 ((π.toMonoidHom.liftOfSurjective hπ) ⟨φ.toMonoidHom, hker⟩)
69 (π.toMonoidHom x) = φ.toMonoidHom x
70 exact
71 MonoidHom.liftOfRightInverse_comp_apply
72 (f := π.toMonoidHom) (f_inv := Function.surjInv hπ)
73 (Function.rightInverse_surjInv hπ) ⟨φ.toMonoidHom, hker⟩ x
75@[simp] theorem liftOfSurjective_comp
76 [CompactSpace F] [T2Space G]
78 (φ : F →ₜ* A) (hker : π.toMonoidHom.ker ≤ φ.toMonoidHom.ker) :
79 (liftOfSurjective π hπ φ hker).toMonoidHom.comp π.toMonoidHom =
80 φ.toMonoidHom := by
81 ext x
82 simp only [ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply,
85end ContinuousMonoidHom
87/-- The closed derived series of a profinite group, starting from the whole group. -/
88abbrev profiniteDerivedSeries
89 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
90 (m : ℕ) : Subgroup G :=
94 (G : Type u) [CommGroup G] [TopologicalSpace G] [T1Space G]
95 [IsTopologicalGroup G] :
96 profiniteDerivedSeries G 1 = ⊥ := by
97 change
98 (⁅(⊤ : Subgroup G), (⊤ : Subgroup G)⁆).topologicalClosure =
99 (⊥ : Subgroup G)
100 have hcomm :
101 ⁅(⊤ : Subgroup G), (⊤ : Subgroup G)⁆ = (⊥ : Subgroup G) := by
102 rw [Subgroup.commutator_eq_bot_iff_le_centralizer]
103 intro x _hx
104 rw [Subgroup.mem_centralizer_iff]
105 intro y _hy
106 exact mul_comm y x
107 rw [hcomm]
108 apply le_antisymm
109 · exact
110 Subgroup.topologicalClosure_minimal
111 (s := (⊥ : Subgroup G)) bot_le (by
112 change IsClosed ({1} : Set G)
113 exact isClosed_singleton)
114 · exact bot_le
117 (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G]
118 [IsTopologicalGroup G] :
119 ∀ m : ℕ, profiniteDerivedSeries G m = derivedSeries G m := by
120 intro m
121 induction m with
123 rfl
124 | succ m ih =>
125 change
126 (⁅profiniteDerivedSeries G m, profiniteDerivedSeries G m⁆).topologicalClosure =
127 derivedSeries G (m + 1)
128 rw [ih, derivedSeries_succ]
129 apply le_antisymm
130 · exact
131 Subgroup.topologicalClosure_minimal
132 (s := ⁅derivedSeries G m, derivedSeries G m⁆) le_rfl
133 (isClosed_discrete _)
134 · exact
135 Subgroup.le_topologicalClosure
136 (s := ⁅derivedSeries G m, derivedSeries G m⁆)
138/-- The Fenchel-Nielsen generator set for a profinite `F`-group presentation. -/
140 {G : Type u} {σ : FenchelSignature}
141 (surfaceA surfaceB : Fin σ.orbitGenus → G)
142 (cusp : Fin σ.numCusps → G)
143 (inertia : Fin σ.numPeriods → G) : Set G :=
144 Set.range surfaceA ∪ Set.range surfaceB ∪ Set.range cusp ∪ Set.range inertia
146/-- The single Fenchel-Nielsen surface relation `∏[αᵢ, βᵢ] * ∏γⱼ * ∏δₗ = 1`. -/
148 {G : Type u} [Group G] {σ : FenchelSignature}
149 (surfaceA surfaceB : Fin σ.orbitGenus → G)
150 (cusp : Fin σ.numCusps → G)
151 (inertia : Fin σ.numPeriods → G) : G :=
152 ((List.finRange σ.orbitGenus).map fun i => ⁅surfaceA i, surfaceB i⁆).prod *
153 ((List.finRange σ.numCusps).map fun j => cusp j).prod *
154 ((List.finRange σ.numPeriods).map fun k => inertia k).prod
156/-- Formal indices for the Fenchel-Nielsen profinite `F`-group generators. -/
157inductive ProfiniteFenchelGenerator (σ : FenchelSignature)
158 | surfaceA : Fin σ.orbitGenus → ProfiniteFenchelGenerator σ
159 | surfaceB : Fin σ.orbitGenus → ProfiniteFenchelGenerator σ
160 | cusp : Fin σ.numCusps → ProfiniteFenchelGenerator σ
161 | inertia : Fin σ.numPeriods → ProfiniteFenchelGenerator σ
163instance instTopologicalSpaceProfiniteFenchelGenerator (σ : FenchelSignature) :
164 TopologicalSpace (ProfiniteFenchelGenerator σ) :=
165 ⊥
167instance instDiscreteTopologyProfiniteFenchelGenerator (σ : FenchelSignature) :
168 DiscreteTopology (ProfiniteFenchelGenerator σ) :=
169 ⟨rfl⟩
171/-- A universe-lifted Fenchel-Nielsen generator index, suitable as a free pro-`C` basis. -/
172abbrev ProfiniteFenchelGeneratorIndex (σ : FenchelSignature) : Type v :=
173 ULift.{v, 0} (ProfiniteFenchelGenerator σ)
175instance instTopologicalSpaceProfiniteFenchelGeneratorIndex (σ : FenchelSignature) :
176 TopologicalSpace (ProfiniteFenchelGeneratorIndex.{v} σ) :=
177 ⊥
179instance instDiscreteTopologyProfiniteFenchelGeneratorIndex (σ : FenchelSignature) :
180 DiscreteTopology (ProfiniteFenchelGeneratorIndex.{v} σ) :=
181 ⟨rfl⟩
183/-- The Fenchel-Nielsen relator set: the total surface relation and all inertia-period relations. -/
185 {F : Type u} [Group F] (σ : FenchelSignature)
186 (basis : ProfiniteFenchelGeneratorIndex.{u} σ → F) : Set F :=
188 (fun i => basis (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
189 (fun i => basis (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
190 (fun j => basis (ULift.up (ProfiniteFenchelGenerator.cusp j)))
191 (fun k => basis (ULift.up (ProfiniteFenchelGenerator.inertia k)))} ∪
192 Set.range fun k : Fin σ.numPeriods =>
193 basis (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^ σ.periods k
195def ProfiniteFenchelGenerator.eval
196 {G : Type u} {σ : FenchelSignature}
197 (surfaceA surfaceB : Fin σ.orbitGenus → G)
198 (cusp : Fin σ.numCusps → G)
199 (inertia : Fin σ.numPeriods → G) :
200 ProfiniteFenchelGenerator σ → G
201 | .surfaceA i => surfaceA i
202 | .surfaceB i => surfaceB i
203 | .cusp j => cusp j
204 | .inertia k => inertia k
206structure ProfiniteFGroup where
207 carrier : Type u
208 [group : Group carrier]
209 [topologicalSpace : TopologicalSpace carrier]
210 [isTopologicalGroup : IsTopologicalGroup carrier]
211 presentationSource : Type u
212 [presentationSourceGroup : Group presentationSource]
213 [presentationSourceTopologicalSpace : TopologicalSpace presentationSource]
214 [presentationSourceIsTopologicalGroup : IsTopologicalGroup presentationSource]
215 isProfinite : ProCGroups.IsProfiniteGroup carrier
216 topologicallyFinitelyGenerated :
218 signature : FenchelSignature
219 firstDerivedSignature : FenchelSignature
220 surfaceA : Fin signature.orbitGenus → carrier
221 surfaceB : Fin signature.orbitGenus → carrier
222 cusp : Fin signature.numCusps → carrier
223 inertia : Fin signature.numPeriods → carrier
224 presentation_relation :
225 profiniteFenchelTotalRelation surfaceA surfaceB cusp inertia = 1
226 presentation_generates :
228 (G := carrier)
229 (profiniteFenchelGeneratorSet surfaceA surfaceB cusp inertia)
230 presentationBasis : ProfiniteFenchelGeneratorIndex.{u} signature → presentationSource
231 presentationRelators : Set presentationSource
232 presentationRelators_eq :
233 presentationRelators =
234 profiniteFenchelRelatorSet signature presentationBasis
235 presentation :
236 ProCGroups.Presentations.IsFreePresentationOfClass
238 ProCGroups.FiniteGroupClass.{u})
239 (X := ProfiniteFenchelGeneratorIndex.{u} signature)
240 (F := presentationSource) (G := carrier)
241 presentationBasis presentationRelators
242 presentation_π_surfaceA :
243 ∀ i : Fin signature.orbitGenus,
244 ProCGroups.Presentations.IsFreePresentationOf.π presentation
245 (presentationBasis
246 (ULift.up (ProfiniteFenchelGenerator.surfaceA i))) = surfaceA i
247 presentation_π_surfaceB :
248 ∀ i : Fin signature.orbitGenus,
249 ProCGroups.Presentations.IsFreePresentationOf.π presentation
250 (presentationBasis
251 (ULift.up (ProfiniteFenchelGenerator.surfaceB i))) = surfaceB i
252 presentation_π_cusp :
253 ∀ j : Fin signature.numCusps,
254 ProCGroups.Presentations.IsFreePresentationOf.π presentation
255 (presentationBasis
256 (ULift.up (ProfiniteFenchelGenerator.cusp j))) = cusp j
257 presentation_π_inertia :
258 ∀ k : Fin signature.numPeriods,
259 ProCGroups.Presentations.IsFreePresentationOf.π presentation
260 (presentationBasis
261 (ULift.up (ProfiniteFenchelGenerator.inertia k))) = inertia k
262 inertia_order : ∀ i, orderOf (inertia i) = signature.periods i
264attribute [instance] ProfiniteFGroup.group
265attribute [instance] ProfiniteFGroup.topologicalSpace
266attribute [instance] ProfiniteFGroup.isTopologicalGroup
267attribute [instance] ProfiniteFGroup.presentationSourceGroup
268attribute [instance] ProfiniteFGroup.presentationSourceTopologicalSpace
269attribute [instance] ProfiniteFGroup.presentationSourceIsTopologicalGroup
271namespace ProfiniteFGroup
273/-- A profinite Fenchel group has only finitely many open subgroups of each fixed index.
277Fenchel-Nielsen theorems. -/
278theorem finiteOpenSubgroupsOfIndex (Δ : ProfiniteFGroup.{u}) :
279 ProCGroups.FiniteGeneration.HasFiniteOpenSubgroupsOfIndex Δ.carrier := by
280 letI : CompactSpace Δ.carrier :=
281 ProCGroups.IsProfiniteGroup.compactSpace Δ.isProfinite
282 exact
283 ProCGroups.FiniteGeneration.hasFiniteOpenSubgroupsOfIndex_of_topologicallyFinitelyGenerated
284 (G := Δ.carrier) Δ.topologicallyFinitelyGenerated
286noncomputable def presentationMap (Δ : ProfiniteFGroup.{u}) :
287 Δ.presentationSource →ₜ* Δ.carrier :=
288 ProCGroups.Presentations.IsFreePresentationOf.π Δ.presentation
290theorem presentationMap_surjective (Δ : ProfiniteFGroup.{u}) :
291 Function.Surjective Δ.presentationMap :=
292 ProCGroups.Presentations.IsFreePresentationOf.π_surjective Δ.presentation
295 (Δ : ProfiniteFGroup.{u}) :
296 Δ.presentationMap.toMonoidHom.ker =
297 ProCGroups.Presentations.closedNormalClosure Δ.presentationRelators :=
298 ProCGroups.Presentations.IsFreePresentationOf.kernel_eq_closedNormalClosure
299 Δ.presentation
302 (Δ : ProfiniteFGroup.{u}) {x : Δ.presentationSource}
303 (hx : x ∈ Δ.presentationRelators) :
304 Δ.presentationMap x = 1 := by
305 have hxClosed :
307 Δ.presentationRelators :=
309 (F := Δ.presentationSource) Δ.presentationRelators hx
310 have hxKer : x ∈ Δ.presentationMap.toMonoidHom.ker := by
312 exact hxClosed
313 exact hxKer
315@[simp] theorem presentationMap_surfaceA (Δ : ProfiniteFGroup.{u})
316 (i : Fin Δ.signature.orbitGenus) :
317 Δ.presentationMap
318 (Δ.presentationBasis
319 (ULift.up (ProfiniteFenchelGenerator.surfaceA i))) =
320 Δ.surfaceA i :=
321 Δ.presentation_π_surfaceA i
323@[simp] theorem presentationMap_surfaceB (Δ : ProfiniteFGroup.{u})
324 (i : Fin Δ.signature.orbitGenus) :
325 Δ.presentationMap
326 (Δ.presentationBasis
327 (ULift.up (ProfiniteFenchelGenerator.surfaceB i))) =
328 Δ.surfaceB i :=
329 Δ.presentation_π_surfaceB i
331@[simp] theorem presentationMap_cusp (Δ : ProfiniteFGroup.{u})
332 (j : Fin Δ.signature.numCusps) :
333 Δ.presentationMap
334 (Δ.presentationBasis
335 (ULift.up (ProfiniteFenchelGenerator.cusp j))) =
336 Δ.cusp j :=
337 Δ.presentation_π_cusp j
339@[simp] theorem presentationMap_inertia (Δ : ProfiniteFGroup.{u})
340 (k : Fin Δ.signature.numPeriods) :
341 Δ.presentationMap
342 (Δ.presentationBasis
343 (ULift.up (ProfiniteFenchelGenerator.inertia k))) =
344 Δ.inertia k :=
345 Δ.presentation_π_inertia k
348 (Δ : ProfiniteFGroup.{u}) :
349 Δ.presentationMap
351 (fun i => Δ.presentationBasis
352 (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
353 (fun i => Δ.presentationBasis
354 (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
355 (fun j => Δ.presentationBasis
356 (ULift.up (ProfiniteFenchelGenerator.cusp j)))
357 (fun k => Δ.presentationBasis
358 (ULift.up (ProfiniteFenchelGenerator.inertia k)))) = 1 :=
360 rw [Δ.presentationRelators_eq]
361 exact Or.inl rfl)
364 (Δ : ProfiniteFGroup.{u}) (k : Fin Δ.signature.numPeriods) :
365 Δ.presentationMap
366 (Δ.presentationBasis
367 (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
368 Δ.signature.periods k) = 1 :=
370 rw [Δ.presentationRelators_eq]
371 exact Or.inr ⟨k, rfl⟩)
373noncomputable def presentationLift
374 (Δ : ProfiniteFGroup.{u})
375 {A : Type u} [Group A] [TopologicalSpace A] [T1Space A]
376 (φ : Δ.presentationSource →ₜ* A)
377 (hφ :
378 Δ.presentationRelators ⊆ φ.toMonoidHom.ker) :
379 Δ.carrier →ₜ* A := by
380 have hSourceProfinite :
381 ProCGroups.IsProfiniteGroup Δ.presentationSource :=
384 ProCGroups.FiniteGroupClass.{u})
385 Δ.presentation.1.isProC
386 letI : CompactSpace Δ.presentationSource :=
387 ProCGroups.IsProfiniteGroup.compactSpace hSourceProfinite
388 letI : T2Space Δ.carrier :=
389 ProCGroups.IsProfiniteGroup.t2Space Δ.isProfinite
390 have hClosedKer :
391 IsClosed ((φ.toMonoidHom.ker : Subgroup Δ.presentationSource) :
392 Set Δ.presentationSource) := by
393 change IsClosed (φ ⁻¹' ({1} : Set A))
394 exact isClosed_singleton.preimage φ.continuous_toFun
395 have hClosedNormal :
396 ProCGroups.Presentations.closedNormalClosure Δ.presentationRelators ≤
397 φ.toMonoidHom.ker :=
399 (F := Δ.presentationSource) hClosedKer hφ
400 have hker : Δ.presentationMap.toMonoidHom.ker ≤ φ.toMonoidHom.ker := by
402 exact hClosedNormal
403 exact
404 ContinuousMonoidHom.liftOfSurjective
405 Δ.presentationMap (presentationMap_surjective Δ) φ hker
407@[simp] theorem presentationLift_comp_presentationMap
408 (Δ : ProfiniteFGroup.{u})
409 {A : Type u} [Group A] [TopologicalSpace A] [T1Space A]
410 (φ : Δ.presentationSource →ₜ* A)
411 (hφ :
412 Δ.presentationRelators ⊆ φ.toMonoidHom.ker) :
413 (Δ.presentationLift φ hφ).toMonoidHom.comp
414 Δ.presentationMap.toMonoidHom =
415 φ.toMonoidHom := by
416 ext x
417 dsimp [presentationLift]
418 simp only [ContinuousMonoidHom.liftOfSurjective_apply]
420@[simp] theorem presentationLift_surfaceA
421 (Δ : ProfiniteFGroup.{u})
422 {A : Type u} [Group A] [TopologicalSpace A] [T1Space A]
423 (φ : Δ.presentationSource →ₜ* A)
424 (hφ :
425 Δ.presentationRelators ⊆ φ.toMonoidHom.ker)
426 (i : Fin Δ.signature.orbitGenus) :
427 Δ.presentationLift φ hφ (Δ.surfaceA i) =
428 φ (Δ.presentationBasis
429 (ULift.up (ProfiniteFenchelGenerator.surfaceA i))) := by
430 rw [← presentationMap_surfaceA Δ i]
431 exact
432 MonoidHom.ext_iff.mp
433 (presentationLift_comp_presentationMap Δ φ hφ)
434 (Δ.presentationBasis
435 (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
437@[simp] theorem presentationLift_surfaceB
438 (Δ : ProfiniteFGroup.{u})
439 {A : Type u} [Group A] [TopologicalSpace A] [T1Space A]
440 (φ : Δ.presentationSource →ₜ* A)
441 (hφ :
442 Δ.presentationRelators ⊆ φ.toMonoidHom.ker)
443 (i : Fin Δ.signature.orbitGenus) :
444 Δ.presentationLift φ hφ (Δ.surfaceB i) =
445 φ (Δ.presentationBasis
446 (ULift.up (ProfiniteFenchelGenerator.surfaceB i))) := by
447 rw [← presentationMap_surfaceB Δ i]
448 exact
449 MonoidHom.ext_iff.mp
450 (presentationLift_comp_presentationMap Δ φ hφ)
451 (Δ.presentationBasis
452 (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
454@[simp] theorem presentationLift_cusp
455 (Δ : ProfiniteFGroup.{u})
456 {A : Type u} [Group A] [TopologicalSpace A] [T1Space A]
457 (φ : Δ.presentationSource →ₜ* A)
458 (hφ :
459 Δ.presentationRelators ⊆ φ.toMonoidHom.ker)
460 (j : Fin Δ.signature.numCusps) :
461 Δ.presentationLift φ hφ (Δ.cusp j) =
462 φ (Δ.presentationBasis
463 (ULift.up (ProfiniteFenchelGenerator.cusp j))) := by
464 rw [← presentationMap_cusp Δ j]
465 exact
466 MonoidHom.ext_iff.mp
467 (presentationLift_comp_presentationMap Δ φ hφ)
468 (Δ.presentationBasis
469 (ULift.up (ProfiniteFenchelGenerator.cusp j)))
471@[simp 900] theorem presentationLift_inertia
472 (Δ : ProfiniteFGroup.{u})
473 {A : Type u} [Group A] [TopologicalSpace A] [T1Space A]
474 (φ : Δ.presentationSource →ₜ* A)
475 (hφ :
476 Δ.presentationRelators ⊆ φ.toMonoidHom.ker)
477 (k : Fin Δ.signature.numPeriods) :
478 Δ.presentationLift φ hφ (Δ.inertia k) =
479 φ (Δ.presentationBasis
480 (ULift.up (ProfiniteFenchelGenerator.inertia k))) := by
481 rw [← presentationMap_inertia Δ k]
482 exact
483 MonoidHom.ext_iff.mp
484 (presentationLift_comp_presentationMap Δ φ hφ)
485 (Δ.presentationBasis
486 (ULift.up (ProfiniteFenchelGenerator.inertia k)))
488/-- Lift an arbitrary assignment of the Fenchel-Nielsen presentation generators to a finite discrete group
489to the free profinite presentation source. -/
490noncomputable def presentationSourceLiftToFinite
491 (Δ : ProfiniteFGroup.{u})
492 {A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
493 (χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A) :
494 Δ.presentationSource →ₜ* A := by
495 letI : IsTopologicalGroup A := inferInstance
496 have hCG :
498 ProCGroups.FiniteGroupClass.{u}).pred A := by
499 change Finite A
500 infer_instance
501 have hA :
505 exact
507 (C := (ProCGroups.FiniteGroupClass.allFinite :
508 ProCGroups.FiniteGroupClass.{u}))
510 have hχ : Continuous χ := continuous_of_discreteTopology
511 exact
512 { toMonoidHom := Δ.presentation.1.lift hA χ hχ
513 continuous_toFun := (Δ.presentation.1.lift_spec hA χ hχ).1 }
515@[simp 900] theorem presentationSourceLiftToFinite_basis
516 (Δ : ProfiniteFGroup.{u})
517 {A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
518 (χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
519 (x : ProfiniteFenchelGeneratorIndex.{u} Δ.signature) :
520 Δ.presentationSourceLiftToFinite χ (Δ.presentationBasis x) = χ x := by
521 letI : IsTopologicalGroup A := inferInstance
522 have hCG :
524 ProCGroups.FiniteGroupClass.{u}).pred A := by
525 change Finite A
526 infer_instance
527 have hA :
531 exact
533 (C := (ProCGroups.FiniteGroupClass.allFinite :
534 ProCGroups.FiniteGroupClass.{u}))
536 have hχ : Continuous χ := continuous_of_discreteTopology
537 change (Δ.presentation.1.lift hA χ hχ) (Δ.presentationBasis x) = χ x
538 exact (Δ.presentation.1.lift_spec hA χ hχ).2 x
541 (Δ : ProfiniteFGroup.{u})
542 {A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
543 (χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A) :
544 Δ.presentationSourceLiftToFinite χ
546 (fun i => Δ.presentationBasis
547 (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
548 (fun i => Δ.presentationBasis
549 (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
550 (fun j => Δ.presentationBasis
551 (ULift.up (ProfiniteFenchelGenerator.cusp j)))
552 (fun k => Δ.presentationBasis
553 (ULift.up (ProfiniteFenchelGenerator.inertia k)))) =
555 (fun i => χ (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
556 (fun i => χ (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
557 (fun j => χ (ULift.up (ProfiniteFenchelGenerator.cusp j)))
558 (fun k => χ (ULift.up (ProfiniteFenchelGenerator.inertia k))) := by
559 simp only [profiniteFenchelTotalRelation, map_mul, map_list_prod, List.map_map, Function.comp_def,
560 map_commutatorElement, presentationSourceLiftToFinite_basis]
563 (Δ : ProfiniteFGroup.{u})
564 {A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
565 (χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
566 (k : Fin Δ.signature.numPeriods) :
567 Δ.presentationSourceLiftToFinite χ
568 (Δ.presentationBasis
569 (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
570 Δ.signature.periods k) =
571 χ (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
572 Δ.signature.periods k := by
573 simp only [map_pow, presentationSourceLiftToFinite_basis]
576 (Δ : ProfiniteFGroup.{u})
577 {A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
578 (χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
579 (hTotal :
581 (fun i => χ (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
582 (fun i => χ (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
583 (fun j => χ (ULift.up (ProfiniteFenchelGenerator.cusp j)))
584 (fun k => χ (ULift.up (ProfiniteFenchelGenerator.inertia k))) = 1)
585 (hPeriod :
586 ∀ k : Fin Δ.signature.numPeriods,
587 χ (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
588 Δ.signature.periods k = 1) :
589 Δ.presentationRelators ⊆
590 (Δ.presentationSourceLiftToFinite χ).toMonoidHom.ker := by
591 intro x hx
592 rw [Δ.presentationRelators_eq] at hx
593 rcases hx with hxTotal | ⟨k, rfl⟩
594 · rw [Set.mem_singleton_iff] at hxTotal
595 subst x
596 simpa [presentationSourceLiftToFinite_totalRelator] using hTotal
597 · simpa [presentationSourceLiftToFinite_periodRelator] using hPeriod k
599/-- Descend a finite-generator assignment to the presented profinite `F`-group once the
601noncomputable def presentationLiftToFinite
602 (Δ : ProfiniteFGroup.{u})
603 {A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
604 (χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
605 (hχ :
606 Δ.presentationRelators ⊆
607 (Δ.presentationSourceLiftToFinite χ).toMonoidHom.ker) :
608 Δ.carrier →ₜ* A :=
609 Δ.presentationLift (Δ.presentationSourceLiftToFinite χ) hχ
611/-- A finite target assignment satisfying exactly the Fenchel-Nielsen total and period relations descends to
612the profinite `F`-group. -/
613noncomputable def presentationLiftToFiniteOfRelations
614 (Δ : ProfiniteFGroup.{u})
615 {A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
616 (χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
617 (hTotal :
619 (fun i => χ (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
620 (fun i => χ (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
621 (fun j => χ (ULift.up (ProfiniteFenchelGenerator.cusp j)))
622 (fun k => χ (ULift.up (ProfiniteFenchelGenerator.inertia k))) = 1)
623 (hPeriod :
624 ∀ k : Fin Δ.signature.numPeriods,
625 χ (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
626 Δ.signature.periods k = 1) :
627 Δ.carrier →ₜ* A :=
628 Δ.presentationLiftToFinite χ
629 (presentationSourceLiftToFinite_relators_subset_ker Δ χ hTotal hPeriod)
631@[simp] theorem presentationLiftToFinite_surfaceA
632 (Δ : ProfiniteFGroup.{u})
633 {A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
634 (χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
635 (hχ :
636 Δ.presentationRelators ⊆
637 (Δ.presentationSourceLiftToFinite χ).toMonoidHom.ker)
638 (i : Fin Δ.signature.orbitGenus) :
639 Δ.presentationLiftToFinite χ hχ (Δ.surfaceA i) =
640 χ (ULift.up (ProfiniteFenchelGenerator.surfaceA i)) := by
641 simp only [presentationLiftToFinite, presentationLift_surfaceA, presentationSourceLiftToFinite_basis]
643@[simp] theorem presentationLiftToFinite_surfaceB
644 (Δ : ProfiniteFGroup.{u})
645 {A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
646 (χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
647 (hχ :
648 Δ.presentationRelators ⊆
649 (Δ.presentationSourceLiftToFinite χ).toMonoidHom.ker)
650 (i : Fin Δ.signature.orbitGenus) :
651 Δ.presentationLiftToFinite χ hχ (Δ.surfaceB i) =
652 χ (ULift.up (ProfiniteFenchelGenerator.surfaceB i)) := by
653 simp only [presentationLiftToFinite, presentationLift_surfaceB, presentationSourceLiftToFinite_basis]
655@[simp] theorem presentationLiftToFinite_cusp
656 (Δ : ProfiniteFGroup.{u})
657 {A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
658 (χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
659 (hχ :
660 Δ.presentationRelators ⊆
661 (Δ.presentationSourceLiftToFinite χ).toMonoidHom.ker)
662 (j : Fin Δ.signature.numCusps) :
663 Δ.presentationLiftToFinite χ hχ (Δ.cusp j) =
664 χ (ULift.up (ProfiniteFenchelGenerator.cusp j)) := by
665 simp only [presentationLiftToFinite, presentationLift_cusp, presentationSourceLiftToFinite_basis]
667@[simp] theorem presentationLiftToFinite_inertia
668 (Δ : ProfiniteFGroup.{u})
669 {A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
670 (χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
671 (hχ :
672 Δ.presentationRelators ⊆
673 (Δ.presentationSourceLiftToFinite χ).toMonoidHom.ker)
674 (k : Fin Δ.signature.numPeriods) :
675 Δ.presentationLiftToFinite χ hχ (Δ.inertia k) =
676 χ (ULift.up (ProfiniteFenchelGenerator.inertia k)) := by
677 simp only [presentationLiftToFinite, presentationLift_inertia, presentationSourceLiftToFinite_basis]
679def IsHyperbolic (Δ : ProfiniteFGroup) : Prop :=
680 Δ.signature.IsHyperbolic
682def IsPerfect (Δ : ProfiniteFGroup) : Prop :=
683 profiniteDerivedSeries Δ.carrier 1 = ⊤
685def IsNonPerfect (Δ : ProfiniteFGroup) : Prop :=
686 ¬ Δ.IsPerfect
688def PairwiseCoprimePeriods (Δ : ProfiniteFGroup) : Prop :=
689 ∀ i j : Fin Δ.signature.numPeriods,
690 i ≠ j → Nat.Coprime (Δ.signature.periods i) (Δ.signature.periods j)
692def CharPerfectNumericalCondition (Δ : ProfiniteFGroup) : Prop :=
693 Δ.signature.orbitGenus = 0 ∧
694 Δ.signature.numCusps = 0 ∧
695 Δ.PairwiseCoprimePeriods
700 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
701 (U : OpenNormalSubgroup G) (m : ℕ) : Prop :=
702 profiniteDerivedSeries (G ⧸ (U : Subgroup G)) m = ⊥
705 (G : Type u) [Group G] [TopologicalSpace G]
706 (U : OpenNormalSubgroup G) : Prop :=
707 ∀ x : G, x ∈ (U : Subgroup G) → IsOfFinOrder x → x = 1
710 (G : Type u) [Group G] [TopologicalSpace G] : Type u :=
711 { U : OpenNormalSubgroup G //
712 ProCGroups.FiniteGeneration.IsTopologicallyCharacteristic (G := G) (U : Subgroup G) }
714def ProfiniteOpenCharacteristicSubgroup.toOpenNormalSubgroup
715 {G : Type u} [Group G] [TopologicalSpace G]
716 (U : ProfiniteOpenCharacteristicSubgroup G) :
717 OpenNormalSubgroup G :=
718 U.1
721 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
722 (U : ProfiniteOpenCharacteristicSubgroup G) (m : ℕ) : Prop :=
723 ProfiniteOpenNormalQuotientHasDerivedLengthAtMost G U.toOpenNormalSubgroup m
726 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : ℕ) : Prop :=
727 ∃ U : OpenNormalSubgroup G,
732 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : ℕ) : Prop :=
733 ∃ U : ProfiniteOpenCharacteristicSubgroup G,
734 ProfiniteOpenNormalSubgroupTorsionFree G U.toOpenNormalSubgroup ∧
737theorem ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.of_topDerived_le
738 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
739 (U : OpenNormalSubgroup G) {m : ℕ}
740 (hU : profiniteDerivedSeries G m ≤ (U : Subgroup G)) :
741 ProfiniteOpenNormalQuotientHasDerivedLengthAtMost G U m := by
742 let q : G →ₜ* G ⧸ (U : Subgroup G) := OpenNormalSubgroup.quotientProj U
743 have hclosed_comm :
744 ∀ n : ℕ,
745 IsClosed
746 (((closedCommutator
747 (topDerivedTop G n) (topDerivedTop G n)).map
748 (q : G →* G ⧸ (U : Subgroup G)) :
749 Subgroup (G ⧸ (U : Subgroup G))) :
750 Set (G ⧸ (U : Subgroup G))) := by
751 intro n
752 exact isClosed_discrete _
753 have hmap :
754 (topDerivedTop G m).map (q : G →* G ⧸ (U : Subgroup G)) =
755 topDerivedTop (G ⧸ (U : Subgroup G)) m := by
756 exact
757 topDerived_map_eq_of_surj (f := q)
758 (OpenNormalSubgroup.quotientProj_surjective U) hclosed_comm m
760 ← hmap]
761 apply le_bot_iff.mp
762 intro y hy
763 rcases hy with ⟨x, hx, rfl⟩
764 change QuotientGroup.mk' (U : Subgroup G) x = 1
765 exact (QuotientGroup.eq_one_iff (N := (U : Subgroup G)) x).2 (hU hx)
767theorem ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.topDerived_le
768 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
769 (U : OpenNormalSubgroup G) {m : ℕ}
770 (hU : ProfiniteOpenNormalQuotientHasDerivedLengthAtMost G U m) :
771 profiniteDerivedSeries G m ≤ (U : Subgroup G) := by
772 let q : G →ₜ* G ⧸ (U : Subgroup G) := OpenNormalSubgroup.quotientProj U
773 have hle := topDerivedTop_le_comap (f := q) (m := m)
774 intro x hx
775 have hxq :
776 q x ∈ topDerivedTop (G ⧸ (U : Subgroup G)) m :=
777 hle hx
778 have hderbot :
779 topDerivedTop (G ⧸ (U : Subgroup G)) m = ⊥ := by
781 profiniteDerivedSeries] using hU
782 have hxqbot :
783 q x ∈ (⊥ : Subgroup (G ⧸ (U : Subgroup G))) := by
784 simpa [hderbot] using hxq
785 have hq1 : q x = 1 := Subgroup.mem_bot.mp hxqbot
786 simpa [q] using
787 (OpenNormalSubgroup.quotientProj_eq_one_iff (U := U) (x := x)).1 hq1
790 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
791 {U : OpenNormalSubgroup G} {m : ℕ} :
793 profiniteDerivedSeries G m ≤ (U : Subgroup G) := by
794 constructor
795 · exact ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.topDerived_le U
796 · exact ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.of_topDerived_le U
798theorem ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.mono
799 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
800 {U : OpenNormalSubgroup G} {m n : ℕ}
801 (hmn : m ≤ n)
802 (hU : ProfiniteOpenNormalQuotientHasDerivedLengthAtMost G U m) :
803 ProfiniteOpenNormalQuotientHasDerivedLengthAtMost G U n := by
805 intro x hx
806 exact hU ((topDerivedTop_antitone hmn) hx)
808theorem HasTorsionFreeOpenNormalSubgroupQuotientDerivedLengthAtMost.mono
809 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
810 {m n : ℕ} (hmn : m ≤ n)
811 (h :
814 rcases h with ⟨U, htf, hquot⟩
815 exact ⟨U, htf,
816 ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.mono hmn hquot⟩
818theorem HasTorsionFreeOpenCharacteristicSubgroupQuotientDerivedLengthAtMost.mono
819 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
820 {m n : ℕ} (hmn : m ≤ n)
821 (h :
823 G m) :
825 G n := by
826 rcases h with ⟨U, htf, hquot⟩
827 exact ⟨U, htf,
828 ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.mono hmn hquot⟩
831 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {m : ℕ}
832 (h :
834 G m) :
836 rcases h with ⟨U, htf, hquot⟩
837 exact ⟨U.toOpenNormalSubgroup, htf, hquot⟩
839end FenchelNielsen