Images of Sylow pro-p subgroups under continuous surjections

A continuous surjective group homomorphism from a compact source onto a Hausdorff target carries a Sylow pro-p subgroup onto a Sylow pro-p subgroup. For each open normal subgroup of the target, pull it back to the source. The induced map between the two quotients is surjective, so the index of the image divides the original prime-to-p index. Compactness of the source and separation of the target enter only to see that the image is closed: it is a continuous image of a closed, hence compact, set.

This is the profinite counterpart of the finite-group fact that a surjective homomorphism carries a Sylow subgroup onto a Sylow subgroup. Unlike invariance under a topological isomorphism, proved in TauCeti.Topology.Algebra.Group.Profinite.Sylow.Basic, it must account for the kernel of the homomorphism.

Main result

• TauCeti.IsProPSylow.map_of_surjective: the image of a Sylow pro-p subgroup under a continuous surjective homomorphism with compact source and Hausdorff target is Sylow pro-p.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 2.3.

theorem TauCeti.IsProPSylow.map_of_surjective {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [CompactSpace G] {H : Type v} [Group H] [TopologicalSpace H] [T2Space H] {P : Subgroup G} (hP : IsProPSylow p P) (f : G →* H) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : IsProPSylow p (Subgroup.map f P)

Surjective functoriality of Sylow pro-p subgroups. The image of a Sylow pro-p subgroup under a continuous surjective homomorphism from a group with a compact topology to a group with a Hausdorff topology is again Sylow pro-p.