Finite generation and the Frattini quotient

A profinite pro-p group is topologically finitely generated if and only if its Frattini quotient is finite, equivalently if and only if its Frattini subgroup is open. This turns topological finite generation into a finiteness condition on the maximal elementary abelian quotient, as needed for the finite-dimensional form of the Burnside basis theorem.

Openness of the Frattini subgroup passes to open subgroups: an open subgroup of a compact topologically finitely generated group is itself compact and topologically finitely generated, so TauCeti.IsTopologicallyFinitelyGenerated.isOpen_map_subtype_proPFrattini sees its Frattini subgroup as an open subgroup of the ambient group. This is the inductive step that makes the lower p-series and the Frattini series of such a group consist of open subgroups.

The forward implication holds for any compact topologically finitely generated group: there are only finitely many open normal subgroups of index p, so their intersection is open. For the converse, lift the finite set of all elements of the quotient and apply the topological Burnside theorem. In particular, the converse uses the pro-p hypothesis.

References

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

theorem TauCeti.IsTopologicallyFinitelyGenerated.isOpen_proPFrattini {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsTopologicallyFinitelyGenerated G) (p : ℕ) : IsOpen ↑(proPFrattini p G)

In a compact topologically finitely generated group, the intersection of the open normal subgroups of any fixed index is open. In particular, its pro-p Frattini subgroup is open.

theorem TauCeti.IsTopologicallyFinitelyGenerated.isOpen_map_subtype_proPFrattini {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsTopologicallyFinitelyGenerated G) (p : ℕ) (U : OpenSubgroup G) : IsOpen ↑(Subgroup.map (↑U).subtype (proPFrattini p ↥↑U))

The pro-p Frattini subgroup of an open subgroup U of a compact topologically finitely generated group is open in the ambient group: U is again topologically finitely generated and compact, so its Frattini subgroup is open in U, and U is open in the ambient group.

theorem TauCeti.IsTopologicallyFinitelyGenerated.finite_quotient_proPFrattini {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsTopologicallyFinitelyGenerated G) (p : ℕ) : Finite (G ⧸ proPFrattini p G)

The pro-p Frattini quotient of a compact topologically finitely generated group is finite. Neither primality of p nor the pro-p condition on the group is needed in this direction.

theorem TauCeti.IsProP.isTopologicallyFinitelyGenerated_iff_finite_quotient_proPFrattini {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {p : ℕ} [Fact (Nat.Prime p)] [TotallyDisconnectedSpace G] (hG : IsProP p G) : IsTopologicallyFinitelyGenerated G ↔ Finite (G ⧸ proPFrattini p G)

Finite generation detected by the Frattini quotient. A profinite pro-p group is topologically finitely generated exactly when its Frattini quotient is finite.

theorem TauCeti.IsProP.isTopologicallyFinitelyGenerated_iff_isOpen_proPFrattini {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {p : ℕ} [Fact (Nat.Prime p)] [TotallyDisconnectedSpace G] (hG : IsProP p G) : IsTopologicallyFinitelyGenerated G ↔ IsOpen ↑(proPFrattini p G)

The open Frattini criterion. A profinite pro-p group is topologically finitely generated exactly when its Frattini subgroup is open.