One step of the Frattini series is a pro-p Frattini subgroup

One step TauCeti.proPFrattiniStep p H = closure (Hᵖ [H, H]) of the Frattini series, defined for arbitrary topological groups in TauCeti.Topology.Algebra.Group.FrattiniSeries, is for a prime p and a closed subgroup H of a profinite group the pro-p Frattini subgroup TauCeti.proPFrattini p H of H, transported to the ambient group along the inclusion. This is the verbal description TauCeti.proPFrattini_eq_topologicalClosure applied inside H.

This bridge is kept apart from the rest of the Frattini series so that the relative Frattini argument in TauCeti.Topology.Algebra.Group.Profinite.ProP.Burnside can use it: the Frattini series module itself lies above Burnside in the import graph.

Main results

• TauCeti.proPFrattiniStep_eq_map_proPFrattini: for a prime p and a closed subgroup H of a profinite group, proPFrattiniStep p H is the pro-p Frattini subgroup of H, viewed inside the ambient group.

theorem TauCeti.proPFrattiniStep_eq_map_proPFrattini {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hp : Nat.Prime p) {H : Subgroup G} (hH : IsClosed ↑H) : proPFrattiniStep p H = Subgroup.map H.subtype (proPFrattini p ↥H)

One step of the Frattini series is the pro-p Frattini subgroup. For a prime p and a closed subgroup H of a profinite group, proPFrattiniStep p H is the pro-p Frattini subgroup of H, viewed inside the ambient group along the inclusion.