Subgroups of pro-p groups

The pro-p property passes from a profinite group to each of its subgroups. Given an open normal subgroup V of a subgroup H, profiniteness supplies an open normal subgroup N of the ambient group whose pullback to H lies in V. The quotient H / V is then a quotient of a subgroup of the finite p-group G / N.

Closedness of H is not needed for this result. It is needed only when the subgroup itself must inherit the profinite typeclass stack.

The same factorization characterizes the pro-p property of an arbitrary subgroup by its images in the ambient finite quotients. It also shows that taking the topological closure neither creates nor destroys the pro-p property. This closure form is useful when a subgroup is first generated algebraically and then promoted to a profinite subgroup.

Main results

• Subgroup.isProP_iff_isPGroup_map_mk': a subgroup is pro-p exactly when all its images in the ambient finite continuous quotients are p-groups.
• IsProP.subgroup, IsProP.mono: the pro-p property passes to subgroups.
• IsProP.topologicalAbelianization: the topological abelianization of a subgroup of a pro-p group is pro-p.
• IsProP.topologicalClosure, Subgroup.isProP_topologicalClosure_iff: the topological closure of a pro-p subgroup is pro-p, and the converse holds as well.

References

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

theorem Subgroup.isProP_iff_isPGroup_map_mk' {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G) : TauCeti.IsProP p ↥H ↔ ∀ (U : OpenNormalSubgroup G), IsPGroup p ↥(map (QuotientGroup.mk' ↑U.toOpenSubgroup) H)

A subgroup of a profinite group is pro-p exactly when its image in every finite continuous quotient of the ambient group is a p-group.

theorem TauCeti.IsProP.subgroup {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (H : Subgroup G) : IsProP p ↥H

Every subgroup of a pro-p profinite group is pro-p in the subspace topology.

In particular, a closed subgroup is again a profinite pro-p group, since closed subgroups inherit the remaining profinite instances.

theorem TauCeti.IsProP.mono {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {K H : Subgroup G} (hH : IsProP p ↥H) (hKH : K ≤ H) : IsProP p ↥K

The pro-p property is antitone on the subgroups of a profinite group.

theorem TauCeti.IsProP.topologicalAbelianization {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (N : Subgroup G) : IsProP p (TopologicalAbelianization ↥N)

The topological abelianization of a subgroup of a pro-p group is pro-p.

@[simp]

theorem Subgroup.isProP_topologicalClosure_iff {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G) : TauCeti.IsProP p ↥H.topologicalClosure ↔ TauCeti.IsProP p ↥H

Taking the topological closure of a subgroup of a profinite group preserves and reflects the pro-p property.

theorem TauCeti.IsProP.topologicalClosure {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {H : Subgroup G} (hH : IsProP p ↥H) : IsProP p ↥H.topologicalClosure

The topological closure of a pro-p subgroup of a profinite group is pro-p.