ProCGroups.Presentations.Profinite
This module studies profinite for pro cgroups. The closed normal subgroup generated by a set of profinite relators. The closed normal closure of a relator set is a normal subgroup.
import
- Mathlib.GroupTheory.PGroup
- ProCGroups.FreeProC.Basic
- ProCGroups.Topologies.TopologicallyCharacteristicSubgroups
def Subgroup.closedNormalClosure (R : Set F) : Subgroup F :=
(Subgroup.normalClosure R).topologicalClosureThe closed normal subgroup generated by a set of profinite relators.
abbrev closedNormalClosure (R : Set F) : Subgroup F :=
Subgroup.closedNormalClosure RThe closed normal subgroup generated by a set of profinite relators.
instance closedNormalClosure_normal (R : Set F) : (closedNormalClosure R).Normal := by
dsimp [closedNormalClosure, Subgroup.closedNormalClosure]
exact Subgroup.is_normal_topologicalClosure (Subgroup.normalClosure R)The closed normal closure of a relator set is a normal subgroup.
theorem closedNormalClosure_isClosed (R : Set F) :
IsClosed ((closedNormalClosure R : Subgroup F) : Set F)The closed normal closure of a relator set is a closed subgroup.
Show proof
by
exact Subgroup.isClosed_topologicalClosure _Proof. Unfold the closed normal closure as the topological closure of the normal closure. A topological closure is closed, so the resulting subgroup is closed as a set.
□theorem subset_closedNormalClosure (R : Set F) :
R ⊆ closedNormalClosure REvery relator in \(R\) lies in the closed normal closure of \(R\).
Show proof
by
intro x hx
exact Subgroup.le_topologicalClosure _
(Subgroup.subset_normalClosure hx)Proof. A relator is in the ordinary normal closure by definition, and the ordinary normal closure is contained in its topological closure.
□theorem one_mem_closedNormalClosure (R : Set F) :
(1 : F) ∈ closedNormalClosure RThe identity belongs to the closed normal closure.
Show proof
Subgroup.one_mem _Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem singleton_one_subset_closedNormalClosure (R : Set F) :
({1} : Set F) ⊆ closedNormalClosure RThe singleton containing the identity is contained in the closed normal closure of any relator set.
Show proof
by
intro x hx
subst x
exact one_mem_closedNormalClosure (F := F) RProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem subset_closedNormalClosure_of_subset_singleton_one
{R D : Set F} (hD : D ⊆ ({1} : Set F)) :
D ⊆ closedNormalClosure RAny relator set contained in the singleton identity set is contained in the closed normal closure.
Show proof
by
intro x hx
exact singleton_one_subset_closedNormalClosure (F := F) R (hD hx)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem closedNormalClosure_le_closed_normal
{R : Set F} {N : Subgroup F} [N.Normal]
(hNclosed : IsClosed (N : Set F)) (hR : R ⊆ N) :
closedNormalClosure R ≤ NThe closed normal closure of \(R\) is contained in any closed normal subgroup that contains \(R\).
Show proof
by
exact Subgroup.topologicalClosure_minimal _
(Subgroup.normalClosure_le_normal hR) hNclosedProof. First the ordinary normal closure of \(R\) is contained in the given normal subgroup. Since that subgroup is closed, minimality of topological closure puts the closed normal closure inside it as well.
□theorem closedNormalClosure_mono {R S : Set F} (hRS : R ⊆ S) :
closedNormalClosure R ≤ closedNormalClosure SClosed normal closure is monotone with respect to inclusion of relator sets.
Show proof
by
refine closedNormalClosure_le_closed_normal
(F := F) (N := closedNormalClosure S)
(closedNormalClosure_isClosed (F := F) S) ?_
exact fun x hx => subset_closedNormalClosure (F := F) S (hRS hx)Proof. If \(R\subseteq S\), then every element of \(R\) lies in the closed normal closure of \(S\). The minimality property of the closed normal closure gives the desired subgroup inclusion.
□theorem closedNormalClosure_eq_of_mutual_le
{R S : Set F}
(hRS : R ⊆ closedNormalClosure S)
(hSR : S ⊆ closedNormalClosure R) :
closedNormalClosure R = closedNormalClosure STwo relator sets have the same closed normal closure when each is contained in the other set's closed normal closure.
Show proof
by
apply le_antisymm
· exact closedNormalClosure_le_closed_normal
(F := F) (N := closedNormalClosure S)
(closedNormalClosure_isClosed (F := F) S) hRS
· exact closedNormalClosure_le_closed_normal
(F := F) (N := closedNormalClosure R)
(closedNormalClosure_isClosed (F := F) R) hSRProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem closedNormalClosure_union_eq_left
{R D : Set F} (hD : D ⊆ closedNormalClosure R) :
closedNormalClosure (R ∪ D) = closedNormalClosure RAdding relators already contained in the closed normal closure does not change the closed normal closure.
Show proof
by
apply le_antisymm
· refine closedNormalClosure_le_closed_normal
(F := F) (N := closedNormalClosure R)
(closedNormalClosure_isClosed (F := F) R) ?_
intro x hx
exact hx.elim
(fun hxR => subset_closedNormalClosure (F := F) R hxR)
(fun hxD => hD hxD)
· exact closedNormalClosure_mono (F := F) (Set.subset_union_left)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□def IsQuotientByKernel (C : ProCGroups.FiniteGroupClass.{u})
{F G : Type u} [Group F] [Group G]
[TopologicalSpace F] [TopologicalSpace G]
[IsTopologicalGroup F] [IsTopologicalGroup G]
(K : Subgroup F) : Prop :=
ProCGroups.ProC.IsProCGroup C G ∧
∃ π : F →ₜ* G, Function.Surjective π ∧ π.toMonoidHom.ker = KA quotient-by-kernel record \(1 \to K \to F \to G \to 1\). The source \(F\) is left explicit: in applications it is normally supplied by FreeProC.IsFreeProCGroup, while Tietze moves only need to know the kernel and the continuous epimorphism being transported.
def IsFreePresentationOf
(ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
{X F G : Type u} [TopologicalSpace X]
[Group F] [Group G]
[TopologicalSpace F] [TopologicalSpace G]
[IsTopologicalGroup F] [IsTopologicalGroup G]
(ι : X → F) (R : Set F) : Prop :=
ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι ∧
ProC (G := G) ∧
∃ π : F →ₜ* G, Function.Surjective π ∧ π.toMonoidHom.ker = closedNormalClosure RA relator presentation whose source is a chosen free pro-\(C\) group.
def IsFreePresentationOfClass (C : ProCGroups.FiniteGroupClass.{u})
{X F G : Type u} [TopologicalSpace X]
[Group F] [Group G]
[TopologicalSpace F] [TopologicalSpace G]
[IsTopologicalGroup F] [IsTopologicalGroup G]
(ι : X → F) (R : Set F) : Prop :=
IsFreePresentationOf
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
(G := G) ι RThe concrete finite-class specialization of IsFreePresentationOf.
def π (h : IsFreePresentationOf (G := G) ProC ι R) : F →ₜ* G :=
Classical.choose h.2.2The projection map of a free presentation is the prescribed quotient homomorphism.
theorem freeSource (h : IsFreePresentationOf (G := G) ProC ι R) :
ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ιThe chosen quotient map recorded by a free pro-\(C\) presentation.
Show proof
h.1Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem targetProC (h : IsFreePresentationOf (G := G) ProC ι R) :
ProC (G := G)The target of a free presentation is pro-\(C\).
Show proof
h.2.1Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem π_surjective (h : IsFreePresentationOf (G := G) ProC ι R) :
Function.Surjective h.πThe projection map of a free presentation is surjective.
Show proof
(Classical.choose_spec h.2.2).1Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem kernel_eq_closedNormalClosure (h : IsFreePresentationOf (G := G) ProC ι R) :
h.π.toMonoidHom.ker = closedNormalClosure RThe kernel of the chosen quotient map is the closed normal closure of the relators.
Show proof
(Classical.choose_spec h.2.2).2Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem IsFreePresentationOfClass.isQuotientByKernel
(C : ProCGroups.FiniteGroupClass.{u})
{X F G : Type u} [TopologicalSpace X]
[Group F] [Group G]
[TopologicalSpace F] [TopologicalSpace G]
[IsTopologicalGroup F] [IsTopologicalGroup G]
{ι : X → F} {R : Set F} :
IsFreePresentationOfClass (G := G) C ι R →
IsQuotientByKernel C (F := F) (G := G) (closedNormalClosure R)Forget the chosen free source from a concrete free pro-\(C\) relator presentation.
Show proof
by
intro h
rcases h with ⟨_hfree, hG, π, hπsurj, hπker⟩
exact ⟨hG, π, hπsurj, hπker⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem isPresentationOf_of_class_subset
(C' C : ProCGroups.FiniteGroupClass.{u})
{F G : Type u} [Group F] [Group G]
[TopologicalSpace F] [TopologicalSpace G]
[IsTopologicalGroup F] [IsTopologicalGroup G]
(K : Subgroup F) :
(∀ {Q : Type u} [Group Q], C' Q → C Q) →
IsQuotientByKernel C' (F := F) (G := G) K →
IsQuotientByKernel C (F := F) (G := G) KTransport a pro-\(C\) presentation along inclusion of finite classes.
Show proof
by
intro hsub hpres
rcases hpres with ⟨hG, π, hπsurj, hπker⟩
exact ⟨hG.mono hsub, π, hπsurj, hπker⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□structure KernelTietzeData
{F E : Type u} [Group F] [Group E]
[TopologicalSpace F] [TopologicalSpace E]
(K : Subgroup F) (L : Subgroup E) where
toHom : F →ₜ* E
invHom : E →ₜ* F
mapsKernel : K ≤ Subgroup.comap toHom.toMonoidHom L
mapsTargetKernel : L ≤ Subgroup.comap invHom.toMonoidHom K
inv_toHom : ∀ x : F, invHom (toHom x) * x⁻¹ ∈ K
to_invHom : ∀ y : E, toHom (invHom y) * y⁻¹ ∈ LContinuous Tietze data between two presentation kernels. It is the profinite analogue of the mutual-map data used in the discrete ReidemeisterSchreier theory, but written directly for closed kernels rather than syntactic relator sets.
def refl (K : Subgroup F) : KernelTietzeData K K where
toHom := ContinuousMonoidHom.id F
invHom := ContinuousMonoidHom.id F
mapsKernel := by intro x hx; exact hx
mapsTargetKernel := by intro x hx; exact hx
inv_toHom := by intro x; simp only [ContinuousMonoidHom.id_toFun, mul_inv_cancel, one_mem]
to_invHom := by intro x; simp only [ContinuousMonoidHom.id_toFun, mul_inv_cancel, one_mem]Kernel Tietze equivalence is reflexive.
def symm (D : KernelTietzeData K L) : KernelTietzeData L K where
toHom := D.invHom
invHom := D.toHom
mapsKernel := D.mapsTargetKernel
mapsTargetKernel := D.mapsKernel
inv_toHom := D.to_invHom
to_invHom := D.inv_toHomKernel Tietze equivalence is symmetric.
def trans (D₁ : KernelTietzeData K L) (D₂ : KernelTietzeData L M) :
KernelTietzeData K M where
toHom := D₂.toHom.comp D₁.toHom
invHom := D₁.invHom.comp D₂.invHom
mapsKernel := by
intro x hx
exact D₂.mapsKernel (D₁.mapsKernel hx)
mapsTargetKernel := by
intro x hx
exact D₁.mapsTargetKernel (D₂.mapsTargetKernel hx)
inv_toHom := by
intro x
let y : E := D₁.toHom x
have h₂ : D₂.invHom (D₂.toHom y) * y⁻¹ ∈ L :=
D₂.inv_toHom y
have h₂map : D₁.invHom (D₂.invHom (D₂.toHom y) * y⁻¹) ∈ K :=
D₁.mapsTargetKernel h₂
have h₂map' :
D₁.invHom (D₂.invHom (D₂.toHom y)) *
(D₁.invHom y)⁻¹ ∈ K := by
simpa using h₂map
have h₁ : D₁.invHom y * x⁻¹ ∈ K :=
D₁.inv_toHom x
have hprod := K.mul_mem h₂map' h₁
have hmul :
(D₁.invHom (D₂.invHom (D₂.toHom y)) *
(D₁.invHom y)⁻¹) *
(D₁.invHom y * x⁻¹) =
D₁.invHom (D₂.invHom (D₂.toHom y)) * x⁻¹ := by
group
simpa [MonoidHom.comp_apply, y, hmul] using hprod
to_invHom := by
intro z
let y : E := D₂.invHom z
have h₁ : D₁.toHom (D₁.invHom y) * y⁻¹ ∈ L :=
D₁.to_invHom y
have h₁map : D₂.toHom (D₁.toHom (D₁.invHom y) * y⁻¹) ∈ M :=
D₂.mapsKernel h₁
have h₁map' :
D₂.toHom (D₁.toHom (D₁.invHom y)) *
(D₂.toHom y)⁻¹ ∈ M := by
simpa using h₁map
have h₂ : D₂.toHom y * z⁻¹ ∈ M :=
D₂.to_invHom z
have hprod := M.mul_mem h₁map' h₂
have hmul :
(D₂.toHom (D₁.toHom (D₁.invHom y)) *
(D₂.toHom y)⁻¹) *
(D₂.toHom y * z⁻¹) =
D₂.toHom (D₁.toHom (D₁.invHom y)) * z⁻¹ := by
group
simpa [MonoidHom.comp_apply, y, hmul] using hprodKernel Tietze equivalence is transitive.
def quotientMulEquiv (D : KernelTietzeData K L) [K.Normal] [L.Normal] :
F ⧸ K ≃* E ⧸ L := by
let F₁ : F ⧸ K →* E ⧸ L :=
QuotientGroup.lift K ((QuotientGroup.mk' L).comp D.toHom.toMonoidHom) (by
intro x hx
rw [MonoidHom.mem_ker]
exact (QuotientGroup.eq_one_iff (N := L) (D.toHom x)).2 (D.mapsKernel hx))
let F₂ : E ⧸ L →* F ⧸ K :=
QuotientGroup.lift L ((QuotientGroup.mk' K).comp D.invHom.toMonoidHom) (by
intro y hy
rw [MonoidHom.mem_ker]
exact (QuotientGroup.eq_one_iff (N := K) (D.invHom y)).2
(D.mapsTargetKernel hy))
refine
{ toFun := F₁
invFun := F₂
left_inv := ?_
right_inv := ?_
map_mul' := fun a b => F₁.map_mul a b }
· intro x
rcases QuotientGroup.mk'_surjective K x with ⟨x, rfl⟩
simp only [QuotientGroup.mk'_apply]
exact (QuotientGroup.eq_iff_div_mem (N := K)
(x := D.invHom (D.toHom x)) (y := x)).2
(by simpa [div_eq_mul_inv] using D.inv_toHom x)
· intro y
rcases QuotientGroup.mk'_surjective L y with ⟨y, rfl⟩
simp only [QuotientGroup.mk'_apply]
exact (QuotientGroup.eq_iff_div_mem (N := L)
(x := D.toHom (D.invHom y)) (y := y)).2
(by simpa [div_eq_mul_inv] using D.to_invHom y)Tietze data induce an algebraic equivalence of quotient groups.
def ofContinuousMulEquiv
{K : Subgroup F} {L : Subgroup E} (e : F ≃ₜ* E)
(hK : ∀ x : F, x ∈ K ↔ e x ∈ L)
(hL : ∀ y : E, y ∈ L ↔ e.symm y ∈ K) :
KernelTietzeData K L where
toHom := e.toContinuousMonoidHom
invHom := e.symm.toContinuousMonoidHom
mapsKernel := by
intro x hx
exact (hK x).1 hx
mapsTargetKernel := by
intro y hy
exact (hL y).1 hy
inv_toHom := by
intro x
simp only [ContinuousMulEquiv.toContinuousMonoidHom_apply, ContinuousMulEquiv.symm_apply_apply,
mul_inv_cancel, one_mem]
to_invHom := by
intro y
simp only [ContinuousMulEquiv.toContinuousMonoidHom_apply, ContinuousMulEquiv.apply_symm_apply,
mul_inv_cancel, one_mem]A continuous multiplicative equivalence gives Tietze data for matching kernels.
def ofContinuousMulEquivMapEq
{K : Subgroup F} {L : Subgroup E} (e : F ≃ₜ* E)
(hmap : K.map e.toContinuousMonoidHom.toMonoidHom = L) :
KernelTietzeData K L where
toHom := e.toContinuousMonoidHom
invHom := e.symm.toContinuousMonoidHom
mapsKernel := by
intro x hx
change e x ∈ L
rw [← hmap]
exact ⟨x, hx, rfl⟩
mapsTargetKernel := by
intro y hy
have hyMap : y ∈ K.map e.toContinuousMonoidHom.toMonoidHom := by
rw [hmap]
exact hy
rcases hyMap with ⟨x, hx, hxy⟩
have hsymm : e.symm y = x := by
simp only [← hxy, ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.coe_coe,
ContinuousMulEquiv.toContinuousMonoidHom_apply, ContinuousMulEquiv.symm_apply_apply]
simpa [hsymm] using hx
inv_toHom := by
intro x
simp only [ContinuousMulEquiv.toContinuousMonoidHom_apply, ContinuousMulEquiv.symm_apply_apply,
mul_inv_cancel, one_mem]
to_invHom := by
intro y
simp only [ContinuousMulEquiv.toContinuousMonoidHom_apply, ContinuousMulEquiv.apply_symm_apply,
mul_inv_cancel, one_mem]A continuous multiplicative equivalence gives Tietze data when it maps one kernel onto the other.
theorem isPresentationOf_of_kernelTietzeData
(C : ProCGroups.FiniteGroupClass.{u})
{F E G : Type u} [Group F] [Group E] [Group G]
[TopologicalSpace F] [TopologicalSpace E] [TopologicalSpace G]
[IsTopologicalGroup F] [IsTopologicalGroup E] [IsTopologicalGroup G]
{K : Subgroup F} {L : Subgroup E}
(D : KernelTietzeData K L) :
IsQuotientByKernel C (F := F) (G := G) K →
IsQuotientByKernel C (F := E) (G := G) LTransport a presentation along profinite Tietze data between its source kernels.
Show proof
by
intro hpres
rcases hpres with ⟨hG, π, hπsurj, hπker⟩
subst K
let ρ : E →ₜ* G := π.comp D.invHom
have hρsurj : Function.Surjective ρ := by
intro g
rcases hπsurj g with ⟨x, rfl⟩
refine ⟨D.toHom x, ?_⟩
have hx : D.invHom (D.toHom x) * x⁻¹ ∈ π.toMonoidHom.ker := by
exact D.inv_toHom x
have hmul : π (D.invHom (D.toHom x) * x⁻¹) = 1 := by
simpa [MonoidHom.mem_ker] using hx
have hmain : π (D.invHom (D.toHom x)) = π x := by
have h := congrArg (fun z : G => z * π x) hmul
simpa [map_mul, map_inv, mul_assoc] using h
exact hmain
have hρker : ρ.toMonoidHom.ker = L := by
ext y
constructor
· intro hy
have hyK : D.invHom y ∈ π.toMonoidHom.ker := by
simpa [ρ, MonoidHom.mem_ker] using hy
have hmap : D.toHom (D.invHom y) ∈ L := D.mapsKernel hyK
have hrel : D.toHom (D.invHom y) * y⁻¹ ∈ L := D.to_invHom y
have hinv : (D.toHom (D.invHom y) * y⁻¹)⁻¹ ∈ L := L.inv_mem hrel
have hprod := L.mul_mem hinv hmap
simpa using hprod
· intro hy
have hyKer : D.invHom y ∈ π.toMonoidHom.ker := D.mapsTargetKernel hy
rw [MonoidHom.mem_ker]
change π (D.invHom y) = 1
simpa [MonoidHom.mem_ker] using hyKer
exact ⟨hG, ρ, hρsurj, hρker⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem isPresentationOf_of_source_equiv
(C : ProCGroups.FiniteGroupClass.{u})
{F E G : Type u} [Group F] [Group E] [Group G]
[TopologicalSpace F] [TopologicalSpace E] [TopologicalSpace G]
[IsTopologicalGroup F] [IsTopologicalGroup E] [IsTopologicalGroup G]
{K : Subgroup F} {L : Subgroup E}
(e : F ≃ₜ* E)
(hK : ∀ x : F, x ∈ K ↔ e x ∈ L)
(hL : ∀ y : E, y ∈ L ↔ e.symm y ∈ K) :
IsQuotientByKernel C (F := F) (G := G) K →
IsQuotientByKernel C (F := E) (G := G) LTransport a presentation along a continuous multiplicative equivalence of sources.
Show proof
isPresentationOf_of_kernelTietzeData C
(KernelTietzeData.ofContinuousMulEquiv (K := K) (L := L) e hK hL)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem isPresentationOf_of_target_equiv
(C : ProCGroups.FiniteGroupClass.{u})
{F G H : Type u} [Group F] [Group G] [Group H]
[TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H]
[IsTopologicalGroup F] [IsTopologicalGroup G] [IsTopologicalGroup H]
{K : Subgroup F}
(e : G ≃ₜ* H)
(hH : ProCGroups.ProC.IsProCGroup C H) :
IsQuotientByKernel C (F := F) (G := G) K →
IsQuotientByKernel C (F := F) (G := H) KTransport a presentation along a continuous multiplicative equivalence of targets, recording the pro-\(C\) witness for the new target explicitly.
Show proof
by
intro hpres
rcases hpres with ⟨_hG, π, hπsurj, hπker⟩
subst K
let ρ : F →ₜ* H := e.toContinuousMonoidHom.comp π
have hρsurj : Function.Surjective ρ := by
intro h
rcases hπsurj (e.symm h) with ⟨x, hx⟩
refine ⟨x, ?_⟩
change e (π x) = h
rw [hx]
simp only [ContinuousMulEquiv.apply_symm_apply]
have hρker : ρ.toMonoidHom.ker = π.toMonoidHom.ker := by
ext x
constructor
· intro hx
have hxKer : x ∈ π.toMonoidHom.ker := by
rw [MonoidHom.mem_ker] at hx ⊢
have hsame : e (π x) = e (1 : G) := by
simpa [ρ] using hx
exact e.injective hsame
exact hxKer
· intro hx
rw [MonoidHom.mem_ker] at hx ⊢
change e (π x) = 1
simpa using congrArg e hx
exact ⟨hH, ρ, hρsurj, hρker⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□