The kernel of a character of a pro-p group, from its values on topological generators

Let G be a pro-p group topologically generated by a set S together with one further element a, and let χ : G → A be a homomorphism with closed kernel (for instance a continuous homomorphism to a T1 group, by ContinuousMonoidHom.isClosed_ker) that is trivial on S and takes a to an element of infinite order. Then the kernel of χ is the closed normal closure of S (TauCeti.IsProP.ker_eq_topologicalClosure_normalClosure_of_not_isOfFinOrder).

The closed normal closure N of S lies in the kernel, and the closed subgroup H topologically generated by a satisfies H ⊔ N = ⊤: since N is normal, H normalizes it, so the carrier of H ⊔ N is the product H * N of two compact subsets of the compact group G, and the join is compact, hence closed (Subgroup.isCompact_sup_of_le_normalizer); and it contains the topological generators. Every element of H is a p-adic power a ^ l, and χ (a ^ l) = 1 forces l = 0, since otherwise some a ^ (p ^ k) would lie in the closed kernel (TauCeti.IsProP.eq_zero_of_padicPow_mem); so H ⊓ ker χ = ⊥, and Dedekind's modular law (Subgroup.inf_sup_assoc_of_le) gives ker χ = N.

If a further generator b has χ b = χ (a ^ l) for a p-adic exponent l, then b may be traded for b * (a ^ l)⁻¹, which χ kills, so the kernel is the closed normal closure of S together with that element. For finite S, the abelianized kernel (ker χ)^{ab}, a module over the completed group algebra ℤ_p[[G ⧸ ker χ]] through conjugation (TauCeti.IsProP.completedGroupAlgebraModule), is then spanned by the classes of the elements of S in the first case, and by the classes of the elements of S together with the class of b * (a ^ l)⁻¹ in the second: this is each kernel equality read through TauCeti.IsProP.span_completedGroupAlgebraModule_topologicalAbelianization_eq_top.

This is the situation of the orientation character of a Demushkin group in Labute's normal form (Labute, §4, p. 121): the character is trivial on all but one or two of the generators, and the module E = X ⧸ (X, X), X = ker χ, on which his classification argument runs is generated over Λ = ℤ_p[[Γ]], Γ = Im χ, by the classes of the generators lying in X, together with the class of the corrected second marked generator when there are two.

Main results

• TauCeti.IsProP.topologicalClosure_closure_singleton_inf_ker_eq_bot: the closed subgroup generated by a meets ker χ trivially when χ a has infinite order.
• TauCeti.IsProP.ker_eq_topologicalClosure_normalClosure_of_not_isOfFinOrder: the kernel of χ is the closed normal closure of S when G is topologically generated by insert a S, χ kills S, and χ a has infinite order.
• MonoidHom.ker_eq_topologicalClosure_normalClosure_insert_pow_of_orderOf_eq: when χ a instead has order m > 0, the kernel is the closed normal closure of S and a ^ m.
• TauCeti.IsProP.ker_eq_topologicalClosure_normalClosure_insert_mul_padicPow_inv: the same with a second marked generator b whose value is the p-adic power χ (a ^ l), which is traded for b * (a ^ l)⁻¹.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, §4, p. 121.

theorem TauCeti.IsProP.topologicalClosure_closure_singleton_inf_ker_eq_bot {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {A : Type u_2} [Group A] (χ : G →* A) (hker : IsClosed ↑χ.ker) {a : G} (ha : ¬IsOfFinOrder (χ a)) : (Subgroup.closure {a}).topologicalClosure ⊓ χ.ker = ⊥

The closed subgroup generated by a meets the kernel trivially when χ a has infinite order and ker χ is closed: an element of that subgroup is a p-adic power a ^ l, and χ (a ^ l) = 1 forces l = 0, since no a ^ (p ^ k) lies in the kernel.

theorem TauCeti.IsProP.ker_eq_topologicalClosure_normalClosure_of_not_isOfFinOrder {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {A : Type u_2} [Group A] (χ : G →* A) (hker : IsClosed ↑χ.ker) {S : Set G} {a : G} (hgen : (Subgroup.closure (insert a S)).topologicalClosure = ⊤) (hS : ∀ s ∈ S, χ s = 1) (ha : ¬IsOfFinOrder (χ a)) : χ.ker = (Subgroup.normalClosure S).topologicalClosure

The kernel of a character, from its values on topological generators. If the pro-p group G is topologically generated by insert a S, χ has closed kernel, kills S and χ a has infinite order, then ker χ is the closed normal closure of S.

theorem TauCeti.IsProP.ker_eq_topologicalClosure_normalClosure_insert_mul_padicPow_inv {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {A : Type u_2} [Group A] (χ : G →* A) (hker : IsClosed ↑χ.ker) {S : Set G} {a b : G} (hgen : (Subgroup.closure (insert a (insert b S))).topologicalClosure = ⊤) (hS : ∀ s ∈ S, χ s = 1) (ha : ¬IsOfFinOrder (χ a)) {l : ℤ_[p]} (hb : χ b = χ (hG.padicPow a l)) : χ.ker = (Subgroup.normalClosure (insert (b * (hG.padicPow a l)⁻¹) S)).topologicalClosure

The kernel of a character with two marked generators. If G is topologically generated by a, b and S, χ has closed kernel, kills S, χ a has infinite order and χ b = χ (a ^ l) for a p-adic exponent l, then ker χ is the closed normal closure of S together with b * (a ^ l)⁻¹.