Source: ProCGroups.Presentations.Profinite
1import Mathlib.GroupTheory.PGroup
2import ProCGroups.FreeProC.Basic
3import ProCGroups.Topologies.TopologicallyCharacteristicSubgroups
5/-!
6# Presentations of profinite and pro-`C` groups
8This module defines closed normal closures of relators and free pro-`C` presentations, together
9with their basic kernel and universal-property consequences.
10-/
12noncomputable section
14namespace ProCGroups.Presentations
16universe u
18section ClosedNormalClosure
20variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
22/-- The closed normal subgroup generated by a set of profinite relators. -/
23def Subgroup.closedNormalClosure (R : Set F) : Subgroup F :=
24 (Subgroup.normalClosure R).topologicalClosure
26/-- The closed normal subgroup generated by a set of profinite relators. -/
27abbrev closedNormalClosure (R : Set F) : Subgroup F :=
28 Subgroup.closedNormalClosure R
30/-- The closed normal closure of a relator set is a normal subgroup. -/
31instance closedNormalClosure_normal (R : Set F) : (closedNormalClosure R).Normal := by
32 dsimp [closedNormalClosure, Subgroup.closedNormalClosure]
33 exact Subgroup.is_normal_topologicalClosure (Subgroup.normalClosure R)
35/-- The closed normal closure of a relator set is a closed subgroup. -/
36theorem closedNormalClosure_isClosed (R : Set F) :
37 IsClosed ((closedNormalClosure R : Subgroup F) : Set F) := by
38 exact Subgroup.isClosed_topologicalClosure _
40/-- Every relator in \(R\) lies in the closed normal closure of \(R\). -/
41theorem subset_closedNormalClosure (R : Set F) :
42 R ⊆ closedNormalClosure R := by
43 intro x hx
44 exact Subgroup.le_topologicalClosure _
45 (Subgroup.subset_normalClosure hx)
48/--
49The closed normal closure of \(R\) is contained in any closed normal subgroup that contains
50\(R\).
51-/
52theorem closedNormalClosure_le_closed_normal
53 {R : Set F} {N : Subgroup F} [N.Normal]
54 (hNclosed : IsClosed (N : Set F)) (hR : R ⊆ N) :
55 closedNormalClosure R ≤ N := by
56 exact Subgroup.topologicalClosure_minimal _
57 (Subgroup.normalClosure_le_normal hR) hNclosed
59end ClosedNormalClosure
61/-- A relator presentation whose source is a chosen free pro-`C` group. -/
62def IsFreePresentationOf
63 (C : ProCGroups.FiniteGroupClass.{u})
64 {X F G : Type u} [TopologicalSpace X]
65 [Group F] [Group G]
66 [TopologicalSpace F] [TopologicalSpace G]
67 [IsTopologicalGroup F] [IsTopologicalGroup G]
68 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
69 (ι : X → F) (R : Set F) : Prop :=
70 ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι ∧
72 ∃ π : F →ₜ* G, Function.Surjective π ∧ π.toMonoidHom.ker = closedNormalClosure R
74namespace IsFreePresentationOf
76variable {C : ProCGroups.FiniteGroupClass.{u}}
77variable {X F G : Type u} [TopologicalSpace X]
78variable [Group F] [Group G]
79variable [TopologicalSpace F] [TopologicalSpace G]
80variable [IsTopologicalGroup F] [IsTopologicalGroup G]
81variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
82variable {ι : X → F} {R : Set F}
84/-- The chosen quotient map recorded by a free pro-`C` presentation. -/
85def π (h : IsFreePresentationOf (G := G) C ι R) : F →ₜ* G :=
86 Classical.choose h.2.2
88/-- The source of a free presentation is free pro-`C`. -/
89theorem freeSource (h : IsFreePresentationOf (G := G) C ι R) :
90 ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι :=
91 h.1
93/-- The target of a free presentation is pro-`C`. -/
94theorem targetProC (h : IsFreePresentationOf (G := G) C ι R) :
96 h.2.1
98/-- The chosen quotient map is surjective. -/
99theorem π_surjective (h : IsFreePresentationOf (G := G) C ι R) :
100 Function.Surjective h.π :=
101 (Classical.choose_spec h.2.2).1
103/-- The kernel of the chosen quotient map is the closed normal closure of the relators. -/
104theorem kernel_eq_closedNormalClosure (h : IsFreePresentationOf (G := G) C ι R) :
105 h.π.toMonoidHom.ker = closedNormalClosure R :=
106 (Classical.choose_spec h.2.2).2
108end IsFreePresentationOf
109end ProCGroups.Presentations