Pro-p groups are closed under extensions

Let f : E →* G be an open surjection between groups with topologies. If G is pro-p and the kernel of f is pro-p in the subspace topology, then E is pro-p (TauCeti.IsProP.of_ker_isProP). The algebraic input is that an extension of a p-group by a p-group is a p-group, IsPGroup.comap_of_ker_isPGroup. The topological input is that the image of an open normal subgroup U ≤ E under an open surjection is an open normal subgroup f(U) ≤ G; this exhibits E ⧸ U as an extension of the p-group G ⧸ f(U) by a quotient of the kernel.

For an extension 1 → M → E → G → 1 whose inclusion is continuous and whose projection is a open map, this says that E is pro-p as soon as M and G are (GroupExtension.isProP). Quotient group homomorphisms from groups with continuous multiplication are open; in particular, continuous surjections from compact topological groups onto Hausdorff groups satisfy the hypothesis. This makes the universal property of a free pro-p group available for lifting generators through such an extension.

Main results

• TauCeti.IsProP.of_ker_isProP: a group mapping onto a pro-p group by an open surjection with pro-p kernel is pro-p.
• GroupExtension.isProP: the total group of an extension of a pro-p group by a pro-p group is pro-p.

References

• L. Ribes and P. Zalesskii, Profinite Groups, 2nd ed., Section 2.2.

theorem TauCeti.IsProP.of_ker_isProP {p : ℕ} {E : Type u_1} [Group E] [TopologicalSpace E] {G : Type u_2} [Group G] [TopologicalSpace G] (hG : IsProP p G) {f : E →* G} (hopen : IsOpenMap ⇑f) (hsurj : Function.Surjective ⇑f) (hker : IsProP p ↥f.ker) : IsProP p E

Pro-p is closed under extensions. A group E is pro-p when it maps onto a pro-p group by an open surjection whose kernel is pro-p in the subspace topology.

theorem GroupExtension.isProP {p : ℕ} {M : Type u_1} [Group M] [TopologicalSpace M] {E : Type u_2} [Group E] [TopologicalSpace E] {G : Type u_3} [Group G] [TopologicalSpace G] (S : GroupExtension M E G) (hinl : Continuous ⇑S.inl) (hrh : IsOpenMap ⇑S.rightHom) (hM : TauCeti.IsProP p M) (hG : TauCeti.IsProP p G) : TauCeti.IsProP p E

The total group of an extension 1 → M → E → G → 1 with continuous inclusion and open projection is pro-p when M and G are.