The abelianized kernel of a character as a module over the completed group algebra

Let G be a pro-p group and N a closed normal subgroup. The topological abelianization N^{ab} = N ⧸ (N, N) is an abelian pro-p group on which G ⧸ N acts continuously by conjugation, so it is a compact module over the completed group algebra ℤ_p[[G ⧸ N]] (TauCeti.IsProP.completedGroupAlgebraModule). This file proves that this module is finitely generated as soon as N is the closed normal closure of a finite set S: the conjugates of S generate a dense subgroup of N, so the (G ⧸ N)-orbit of the classes of the elements of S generates a dense subgroup of N^{ab}, and a finite set with a dense orbit spans a compact module over a compact ring.

A closed normal subgroup N with commutative quotient, for G topologically finitely generated, is such a subgroup (IsProP.exists_finite_topologicalClosure_normalClosure_eq, in TauCeti.Topology.Algebra.Group.Profinite.ProP.NormalClosure). The kernel of a continuous character χ : G → A to a commutative group is the case of interest.

For F free pro-p of finite rank and χ : F → ℤ_pˣ an orientation character, the module obtained is E = X ⧸ (X, X), X = ker χ, over Λ = ℤ_p[[Γ]], Γ = F ⧸ X ≅ Im χ, on which Labute's classification of Demushkin groups runs (Labute, §4, p. 121): E is generated over Λ by finitely many classes of elements of X, and it is this finite generation that lets the relator class be expressed as a Λ-combination of generators.

The convention for the action. Labute writes the action of Γ on E as [y] · [x] = [y⁻¹ x y] (§4 Definition, p. 121). The module structure used here is Mathlib's conjugation action [y] • [x] = [y x y⁻¹] (TopologicalAbelianization.mk_smul_mk, extended to the group elements of Λ by TauCeti.IsProP.completedGroupAlgebraModule_of_smul), so Labute's action is [y]⁻¹ • [x] (TopologicalAbelianization.mk_inv_smul_mk): the two differ by the inversion of Γ. Since Γ ≅ Im χ is commutative, inversion is a continuous automorphism of Γ, and TauCeti.completedGroupAlgebra.map turns it into an involutive algebra automorphism ι of Λ with Labute's scalar action l ·_L ξ = ι l • ξ. The two module structures therefore have the same submodules, the same spans and the same generating sets, and the finite generation proved here holds verbatim for Labute's action; only the coefficients of a Λ-combination of given generators change, by ι. No such coefficients are computed in this file.

Main results

• IsProP.span_completedGroupAlgebraModule_topologicalAbelianization_eq_top, IsProP.module_finite_completedGroupAlgebraModule_topologicalAbelianization: if N is the closed normal closure of a finite set S in a pro-p group G, then the classes of the elements of S span N^{ab} over ℤ_p[[G ⧸ N]], so N^{ab} is a finitely generated module.
• IsProP.exists_finite_span_completedGroupAlgebraModule_topologicalAbelianization_eq_top, IsProP.module_finite_completedGroupAlgebraModule_topologicalAbelianization_of_commutator_le: for such an N, the classes of some finite subset of N span N^{ab} over ℤ_p[[G ⧸ N]], so N^{ab} is a finitely generated module.
• IsProP.exists_finite_span_completedGroupAlgebraModule_topologicalAbelianization_ker_eq_top, IsProP.module_finite_completedGroupAlgebraModule_topologicalAbelianization_ker: Labute's module, the abelianized kernel of a continuous character of a topologically finitely generated pro-p group, is spanned over the completed group algebra of the image by the classes of some finite subset of the kernel, so it is a finitely generated module.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), §4.

theorem TauCeti.IsProP.span_completedGroupAlgebraModule_topologicalAbelianization_eq_top {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (N : Subgroup G) [N.Normal] {S : Set G} (hS : S.Finite) (hSN : (Subgroup.normalClosure S).topologicalClosure = N) : Submodule.span (completedGroupAlgebra ℤ_[p] (G ⧸ N)) (⇑Additive.ofMul '' QuotientGroup.mk '' Subtype.val ⁻¹' S) = ⊤

The classes of the normal generators of a closed subgroup span its abelianization over the completed group algebra. If N is the closed normal closure of a finite set S in a pro-p group G, then the classes of the elements of S span N^{ab} over ℤ_p[[G ⧸ N]], for the module structure TauCeti.IsProP.completedGroupAlgebraModule through conjugation: their (G ⧸ N)-orbit generates a dense subgroup, and a finite set with a dense orbit spans a compact module over a compact ring.

theorem TauCeti.IsProP.module_finite_completedGroupAlgebraModule_topologicalAbelianization {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (N : Subgroup G) [N.Normal] {S : Set G} (hS : S.Finite) (hSN : (Subgroup.normalClosure S).topologicalClosure = N) : Module.Finite (completedGroupAlgebra ℤ_[p] (G ⧸ N)) (Additive (TopologicalAbelianization ↥N))

The abelianization of a finitely normally generated closed subgroup is a finitely generated module over the completed group algebra. If N is the closed normal closure of a finite set S in a pro-p group G, then N^{ab} is a finitely generated ℤ_p[[G ⧸ N]]-module, for the module structure TauCeti.IsProP.completedGroupAlgebraModule through conjugation, spanned by the classes of the elements of S (IsProP.span_completedGroupAlgebraModule_topologicalAbelianization_eq_top).

theorem TauCeti.IsProP.exists_finite_span_completedGroupAlgebraModule_topologicalAbelianization_eq_top {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] [IsClosed ↑N] (hc : commutator G ≤ N) : ∃ (S : Set G), S.Finite ∧ S ⊆ ↑N ∧ Submodule.span (completedGroupAlgebra ℤ_[p] (G ⧸ N)) (⇑Additive.ofMul '' QuotientGroup.mk '' Subtype.val ⁻¹' S) = ⊤

A closed normal subgroup with commutative quotient has finitely generated abelianization over the completed group algebra, with named generators. For N a closed normal subgroup of a topologically finitely generated pro-p group G containing the commutator subgroup, the classes of the elements of some finite subset of N span N^{ab} over ℤ_p[[G ⧸ N]], for the module structure TauCeti.IsProP.completedGroupAlgebraModule through conjugation.

theorem TauCeti.IsProP.module_finite_completedGroupAlgebraModule_topologicalAbelianization_of_commutator_le {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] [IsClosed ↑N] (hc : commutator G ≤ N) : Module.Finite (completedGroupAlgebra ℤ_[p] (G ⧸ N)) (Additive (TopologicalAbelianization ↥N))

A closed normal subgroup with commutative quotient has finitely generated abelianization over the completed group algebra. For N a closed normal subgroup of a topologically finitely generated pro-p group G containing the commutator subgroup, N^{ab} is a finitely generated ℤ_p[[G ⧸ N]]-module, for the module structure TauCeti.IsProP.completedGroupAlgebraModule through conjugation; the generators are the classes of a finite subset of N (IsProP.exists_finite_span_completedGroupAlgebraModule_topologicalAbelianization_eq_top).

theorem TauCeti.IsProP.exists_finite_span_completedGroupAlgebraModule_topologicalAbelianization_ker_eq_top {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 ∧ S ⊆ ↑χ.ker ∧ Submodule.span (completedGroupAlgebra ℤ_[p] (G ⧸ χ.ker)) (⇑Additive.ofMul '' QuotientGroup.mk '' Subtype.val ⁻¹' S) = ⊤

Labute's module is generated by the classes of finitely many elements of the kernel. For a continuous character χ : G → A of a topologically finitely generated pro-p group G to a commutative T1 group, the topological abelianization E = X ⧸ (X, X) of X = ker χ is spanned over the completed group algebra Λ = ℤ_p[[G ⧸ X]] by the classes of the elements of some finite subset of X, for the module structure TauCeti.IsProP.completedGroupAlgebraModule through conjugation [y] • [x] = [y x y⁻¹]. The finite subset is the normal generating set of X produced by exists_finite_topologicalClosure_normalClosure_eq_ker, not a set of prescribed basis elements of G; the expression of the relator class in a normalized basis is a later step of the classification.

theorem TauCeti.IsProP.module_finite_completedGroupAlgebraModule_topologicalAbelianization_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 ⇑χ) : Module.Finite (completedGroupAlgebra ℤ_[p] (G ⧸ χ.ker)) (Additive (TopologicalAbelianization ↥χ.ker))

Labute's module is finitely generated. For a continuous character χ : G → A of a topologically finitely generated pro-p group G to a commutative T1 group, the topological abelianization E = X ⧸ (X, X) of X = ker χ is a finitely generated module over the completed group algebra Λ = ℤ_p[[G ⧸ X]], for the module structure TauCeti.IsProP.completedGroupAlgebraModule through conjugation [y] • [x] = [y x y⁻¹]. For G free pro-p of finite rank and χ an orientation G → ℤ_pˣ this is the module of Labute, §4, on which the classification of Demushkin groups runs, with his action [y] · [x] = [y⁻¹ x y] composed with the inversion of Γ; finite generation is the same statement for both conventions (see the module docstring). The generators are the classes of a finite subset of X (IsProP.exists_finite_span_completedGroupAlgebraModule_topologicalAbelianization_ker_eq_top).