Normal generation in pro-p groups

Let R be a closed normal subgroup of a pro-p group F, and let Rᵖ[R, F] be the closed subgroup TauCeti.pLowerCentralStep p R generated by the p-th powers of R and the commutators ⁅R, F⁆. The quotient R ⧸ Rᵖ[R, F] is the largest quotient of R that is elementary abelian with trivial conjugation action of F, and it controls generation of R as a closed normal subgroup of F exactly as the Frattini quotient F ⧸ Φ(F) controls generation of F (TauCeti.topologicallyGenerates_iff_frattiniQuotient): a subset of R generates R as a closed normal subgroup of F if and only if its image topologically generates R ⧸ Rᵖ[R, F]. In particular R is generated as a closed normal subgroup of F by n elements exactly when R ⧸ Rᵖ[R, F] is topologically generated by n elements, so when this quotient is topologically finitely generated, the least number of generators of R as a closed normal subgroup of F is its topological generator rank.

The input is Nakayama's lemma for pro-p groups in its relative form, TauCeti.IsProP.le_of_le_topologicalClosure_sup_pLowerCentralStep: if R ≤ closure (N ⬝ Rᵖ[R, F]) for a closed normal subgroup N, then R ≤ N.

For a minimal presentation 1 → R → F → G → 1 of a pro-p group, with F free pro-p, the transgression identifies H¹(R, 𝔽_p)^F with H²(G, 𝔽_p), and the F-invariant continuous homomorphisms R → 𝔽_p are exactly those factoring through R ⧸ Rᵖ[R, F] (TauCeti.pLowerCentralStep_subgroupOf_le_ker_iff). The results here are therefore what make dim H²(G, 𝔽_p) count relations: it is the least number of generators of the relation subgroup R as a closed normal subgroup of F.

Main results

• TauCeti.proPFrattini_quotient_pLowerCentralStep_eq_bot: the quotient R ⧸ Rᵖ[R, F] of a closed normal subgroup of a profinite group has trivial pro-p Frattini subgroup, that is, it is elementary abelian.
• TauCeti.IsProP.topologicalClosure_normalClosure_eq_iff_topologicalClosure_sup_eq: a subset s of R generates R as a closed normal subgroup exactly when s and Rᵖ[R, F] together topologically generate R.
• TauCeti.IsProP.topologicalClosure_normalClosure_eq_iff_quotient_pLowerCentralStep: Burnside's basis theorem for normal generation. A subset of R generates R as a closed normal subgroup of F exactly when its image topologically generates R ⧸ Rᵖ[R, F].
• TauCeti.IsProP.exists_finset_card_le_topologicalClosure_normalClosure_eq_iff, TauCeti.IsProP.isTopologicallyFinitelyGenerated_quotient_pLowerCentralStep_iff, TauCeti.IsProP.topologicalGeneratorRankNat_quotient_pLowerCentralStep_le_iff: R is generated as a closed normal subgroup by n elements exactly when R ⧸ Rᵖ[R, F] is topologically generated by n elements; so when R ⧸ Rᵖ[R, F] is topologically finitely generated, the least number of generators of R as a closed normal subgroup is its topological generator rank.

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, Proposition 3.9.5.
• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), Section 1.4.
• L. Ribes and P. Zalesskii, Profinite Groups, Section 2.8.

theorem TauCeti.proPFrattini_quotient_pLowerCentralStep_eq_bot {p : ℕ} {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hp : Nat.Prime p) (R : Subgroup F) [R.Normal] (hR : IsClosed ↑R) : proPFrattini p (↥R ⧸ (pLowerCentralStep p R).subgroupOf R) = ⊥

R ⧸ Rᵖ[R, F] is elementary abelian. The quotient of a closed normal subgroup R of a profinite group by Rᵖ[R, F] is commutative and killed by p, so for a prime p its pro-p Frattini subgroup is trivial.

theorem TauCeti.IsProP.topologicalClosure_normalClosure_eq_iff_topologicalClosure_sup_eq {p : ℕ} {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (hp : Nat.Prime p) {R : Subgroup F} [R.Normal] (hR : IsClosed ↑R) {s : Set F} (hs : s ⊆ ↑R) : (Subgroup.normalClosure s).topologicalClosure = R ↔ (Subgroup.closure s ⊔ pLowerCentralStep p R).topologicalClosure = R

Normal generation modulo Rᵖ[R, F], subgroup form. A subset s of a closed normal subgroup R of a pro-p group generates R as a closed normal subgroup exactly when s together with Rᵖ[R, F] topologically generates R.

theorem TauCeti.IsProP.topologicalClosure_normalClosure_eq_iff_quotient_pLowerCentralStep {p : ℕ} {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (hp : Nat.Prime p) {R : Subgroup F} [R.Normal] (hR : IsClosed ↑R) (s : Set ↥R) : (Subgroup.normalClosure (Subtype.val '' s)).topologicalClosure = R ↔ (Subgroup.closure (⇑(QuotientGroup.mk' ((pLowerCentralStep p R).subgroupOf R)) '' s)).topologicalClosure = ⊤

Burnside's basis theorem for normal generation. A subset s of a closed normal subgroup R of a pro-p group F generates R as a closed normal subgroup of F exactly when its image topologically generates the quotient R ⧸ Rᵖ[R, F].

theorem TauCeti.IsProP.exists_finset_card_le_topologicalClosure_normalClosure_eq_iff {p : ℕ} {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (hp : Nat.Prime p) {R : Subgroup F} [R.Normal] (hR : IsClosed ↑R) (n : ℕ) : (∃ (s : Finset ↥R), s.card ≤ n ∧ (Subgroup.normalClosure (Subtype.val '' ↑s)).topologicalClosure = R) ↔ ∃ (t : Finset (↥R ⧸ (pLowerCentralStep p R).subgroupOf R)), t.card ≤ n ∧ (Subgroup.closure ↑t).topologicalClosure = ⊤

A closed normal subgroup R of a pro-p group is generated as a closed normal subgroup by at most n elements exactly when R ⧸ Rᵖ[R, F] is topologically generated by at most n elements.

theorem TauCeti.IsProP.isTopologicallyFinitelyGenerated_quotient_pLowerCentralStep_iff {p : ℕ} {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (hp : Nat.Prime p) {R : Subgroup F} [R.Normal] (hR : IsClosed ↑R) : IsTopologicallyFinitelyGenerated (↥R ⧸ (pLowerCentralStep p R).subgroupOf R) ↔ ∃ (s : Finset ↥R), (Subgroup.normalClosure (Subtype.val '' ↑s)).topologicalClosure = R

The quotient R ⧸ Rᵖ[R, F] of a closed normal subgroup R of a pro-p group is topologically finitely generated exactly when R is generated as a closed normal subgroup by finitely many elements.

theorem TauCeti.IsProP.topologicalGeneratorRankNat_quotient_pLowerCentralStep_le_iff {p : ℕ} {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (hp : Nat.Prime p) {R : Subgroup F} [R.Normal] (hR : IsClosed ↑R) (h : IsTopologicallyFinitelyGenerated (↥R ⧸ (pLowerCentralStep p R).subgroupOf R)) (n : ℕ) : topologicalGeneratorRankNat (↥R ⧸ (pLowerCentralStep p R).subgroupOf R) h ≤ n ↔ ∃ (s : Finset ↥R), s.card ≤ n ∧ (Subgroup.normalClosure (Subtype.val '' ↑s)).topologicalClosure = R

The least number of generators of R as a closed normal subgroup. The topological generator rank of R ⧸ Rᵖ[R, F] is at most n exactly when the closed normal subgroup R of the pro-p group F is generated as a closed normal subgroup by at most n elements.