Finite normal generation of closed normal subgroups with commutative quotient

Let G be a topologically finitely generated pro-p group. A closed normal subgroup N of G with commutative quotient is the closed normal closure of a finite set. Indeed N contains the closure of the commutator subgroup, which is normally generated by the commutators of a finite topological generating set of G, and the image of N in the topological abelianization G^{ab} is a closed subgroup of a topologically finitely generated abelian pro-p group, hence topologically generated by finitely many elements (IsProP.exists_finite_subset_le_topologicalClosure_closure), which lift to N.

The case of interest is the kernel X of a continuous character χ : G → A to a commutative group: finite normal generation of X is what makes its topological abelianization X ⧸ (X, X) a finitely generated module over the completed group algebra of G ⧸ X.

Main results

• IsProP.exists_finite_topologicalClosure_normalClosure_eq: a closed normal subgroup with commutative quotient of a topologically finitely generated pro-p group is the closed normal closure of a finite set.
• IsProP.exists_finite_topologicalClosure_normalClosure_eq_ker: the kernel of a continuous homomorphism from a topologically finitely generated pro-p group to a commutative T1 group is the closed normal closure of a finite set.

theorem TauCeti.IsProP.exists_finite_topologicalClosure_normalClosure_eq {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) {N : Subgroup G} [N.Normal] (hN : IsClosed ↑N) (hc : commutator G ≤ N) : ∃ (S : Set G), S.Finite ∧ (Subgroup.normalClosure S).topologicalClosure = N

A closed normal subgroup with commutative quotient of a topologically finitely generated pro-p group is the closed normal closure of a finite set. The subgroup contains the closure of the commutator subgroup, which is normally generated by the commutators of a finite topological generating set, and its image in the abelianization is a closed subgroup of a topologically finitely generated abelian pro-p group, hence topologically generated by finitely many elements, which lift to the subgroup.

theorem TauCeti.IsProP.exists_finite_topologicalClosure_normalClosure_eq_ker {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) {A : Type u_2} [CommGroup A] [TopologicalSpace A] [T1Space A] (χ : G →* A) (hχ : Continuous ⇑χ) : ∃ (S : Set G), S.Finite ∧ (Subgroup.normalClosure S).topologicalClosure = χ.ker

The kernel of a character of a topologically finitely generated pro-p group is the closed normal closure of a finite set: it is a closed normal subgroup with commutative quotient (IsProP.exists_finite_topologicalClosure_normalClosure_eq).