Generator rank and the Frattini quotient

For a topologically finitely generated pro-p group, Burnside's basis theorem identifies the least number of topological generators with the dimension of the Frattini quotient over ZMod p. Consequently the quotient has order p raised to the generator rank.

Counting orders through this identifies when a continuous surjection f : G ↠ H of pro-p groups preserves the rank: the preimage Φ(G) ⊔ ker f of Φ(H) has index p ^ d(H) in G, while Φ(G) has index p ^ d(G), so d(H) = d(G) holds exactly when ker f ≤ Φ(G).

Main results

• TauCeti.IsProP.topologicalGeneratorRankNat_eq_finrank_quotient_proPFrattini: the generator rank is the dimension of the Frattini quotient.
• TauCeti.IsProP.natCard_quotient_proPFrattini: the Frattini quotient has order p ^ d(G).
• TauCeti.isPGroup_of_proPFrattini_eq_bot, TauCeti.isProP_of_proPFrattini_eq_bot: a topological group with trivial pro-p Frattini subgroup is a p-group, hence pro-p.
• TauCeti.natCard_of_proPFrattini_eq_bot, TauCeti.topologicalGeneratorRankNat_eq_of_natCard_eq_pow: a topologically finitely generated profinite group with trivial pro-p Frattini subgroup has order p ^ d(G), so its order determines d(G).
• TauCeti.IsProP.topologicalGeneratorRank_quotient_proPFrattini: a pro-p group and its Frattini quotient have the same cardinal topological generator rank.
• TauCeti.IsProP.index_proPFrattini_sup_ker: along a continuous surjection f : G ↠ H onto a topologically finitely generated pro-p group, Φ(G) ⊔ ker f has index p ^ d(H).
• TauCeti.IsProP.topologicalGeneratorRankNat_eq_iff_ker_le_proPFrattini: for a continuous surjection f : G ↠ H of pro-p groups with G topologically finitely generated, d(H) = d(G) exactly when ker f ≤ Φ(G).

References

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

theorem TauCeti.isPGroup_of_proPFrattini_eq_bot {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] (hΦ : proPFrattini p G = ⊥) : IsPGroup p G

A topological group with trivial pro-p Frattini subgroup is a p-group, since the p-th power of every element lies in the pro-p Frattini subgroup.

theorem TauCeti.isProP_of_proPFrattini_eq_bot {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] (hΦ : proPFrattini p G = ⊥) : IsProP p G

A topological group with trivial pro-p Frattini subgroup is pro-p.

theorem TauCeti.IsProP.topologicalGeneratorRankNat_eq_finrank_quotient_proPFrattini {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) : topologicalGeneratorRankNat G hfg = Module.finrank (ZMod p) (Additive (G ⧸ proPFrattini p G))

For a topologically finitely generated pro-p group, the natural-number topological generator rank is the dimension of its Frattini quotient over ZMod p.

theorem TauCeti.IsProP.natCard_quotient_proPFrattini {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) : Nat.card (G ⧸ proPFrattini p G) = p ^ topologicalGeneratorRankNat G hfg

The Frattini quotient of a topologically finitely generated pro-p group has order p raised to the natural-number topological generator rank.

theorem TauCeti.IsProP.topologicalGeneratorRank_quotient_proPFrattini {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) : topologicalGeneratorRank (G ⧸ proPFrattini p G) = topologicalGeneratorRank G

A profinite pro-p group and its Frattini quotient have the same topological generator rank. Generation passes to the quotient; conversely a generating set of the quotient converging to 1 has a set of representatives converging to 1, which generates G by Burnside's basis theorem.

theorem TauCeti.IsProP.index_proPFrattini_sup_ker {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (hH : IsProP p H) (hfg : IsTopologicallyFinitelyGenerated H) (f : G →* H) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : (proPFrattini p G ⊔ f.ker).index = p ^ topologicalGeneratorRankNat H hfg

Along a continuous surjection f : G ↠ H from a compact group onto a topologically finitely generated profinite pro-p group, the subgroup Φ(G) ⊔ ker f, the preimage of the Frattini subgroup of H, has index p ^ d(H) in G.

theorem TauCeti.IsProP.topologicalGeneratorRankNat_eq_iff_ker_le_proPFrattini {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (f : G →* H) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : topologicalGeneratorRankNat H ⋯ = topologicalGeneratorRankNat G hfg ↔ f.ker ≤ proPFrattini p G

Rank preservation along a surjection. For a continuous surjection f : G ↠ H of profinite pro-p groups with G topologically finitely generated, the topological generator rank of H equals that of G exactly when the kernel of f lies in the Frattini subgroup of G. The inequality d(H) ≤ d(G) is TauCeti.topologicalGeneratorRankNat_le_of_surjective.

theorem TauCeti.natCard_of_proPFrattini_eq_bot {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hfg : IsTopologicallyFinitelyGenerated G) (hΦ : proPFrattini p G = ⊥) : Nat.card G = p ^ topologicalGeneratorRankNat G hfg

A topologically finitely generated profinite group with trivial pro-p Frattini subgroup has order p raised to its natural-number topological generator rank.

theorem TauCeti.topologicalGeneratorRankNat_eq_of_natCard_eq_pow {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hfg : IsTopologicallyFinitelyGenerated G) (hΦ : proPFrattini p G = ⊥) {n : ℕ} (h : Nat.card G = p ^ n) : topologicalGeneratorRankNat G hfg = n

A topologically finitely generated profinite group with trivial pro-p Frattini subgroup and p ^ n elements has natural-number topological generator rank n.