The kernel of an exponent sum of a free pro-`p` group and its graded pieces #

Let F = freeProP p X be the free pro-p group on a finite type X with generators x_i, and fix i ∈ X. The kernel of the i-th exponent sum X_i := ker (F → ℤ_p, y ↦ (exponentSum y)_i) (TauCeti.freeProP.exponentSumKer) is the closed normal subgroup of F topologically generated, as a normal subgroup, by the generators x_j with j ≠ i; it contains the closed commutator subgroup. When a continuous character χ : F → ℤ_pˣ is trivial on the x_j with j ≠ i and takes x_i to an element of infinite order, its kernel is exactly X_i: this is the kernel X = ker χ of the orientation of a Demushkin group in Labute's normal form, on whose graded Lie algebra his classification of the dyadic even-rank Demushkin groups runs (Labute, §4).

The graded pieces gr_m(X_i) ≤ gr_m(F) of X_i along the lower p-series (TauCeti.gradedPieceOf) are computed by three statements, which are Labute's Lemmas 1–3 in our 0-based indexing:

Complement (Lemma 1). The class of y ∈ λ_m(F) lies in gr_m(X_i) exactly when p ^ (m + 1) divides the i-th exponent sum of y, and gr_m(F) = gr_m(X_i) ⊕ 𝔽_p π^m ξ_i, where ξ_i is the class of x_i and π the p-power operator (TauCeti.freeProP.isCompl_gradedPieceOf_exponentSumKer_span_gradedPowIter).
Generation (Lemma 2). For m ≥ 1, gr_{m+1}(X_i) is generated by the p-powers π τ and the brackets [τ, ξ_j] with τ ∈ gr_m(X_i), stated as a criterion for a subspace to contain gr_{m+1}(X_i) (TauCeti.freeProP.gradedPieceOf_exponentSumKer_succ_le). The proof decomposes a class of gr_m(F) along the complement of Lemma 1; the only bracket not covered by the hypotheses is [π^m ξ_i, y], which is π [π^{m-1} ξ_i, y] for m ≥ 2 and π [ξ_i, y] - (p choose 2) • [[ξ_i, y], ξ_i] for m = 1.
The constrained span statement (Lemma 3). Let ρ ∈ gr_1(F) be the class of a relator whose partial derivatives ∂_k ρ span gr_0(F), whose p-power part sits on a single generator x_{i₀}, and whose derivatives at the generators other than x_{i₀} span every generator class ξ_j with j ≠ i₁. Then for every m ≥ 1
gr_{m+1}(X_{i₁}) = δ_ρ(gr_m(X_{i₁})^X) + T_{m+1},
where δ_ρ is the basis-modification map of TauCeti.freeProP.basisModificationDelta and the tail T_{m+1} is spanned by the π^{m+1} ξ_a with a ≠ i₁ (gradedPieceOf_exponentSumKer_eq_map_basisModificationDelta_sup_span_gradedPowIter in TauCeti.freeProP). This refines the unconstrained span statements of Free/BasisModification.lean: the basis corrections ω ∈ gr_m(F)^X realizing a discrepancy in gr_{m+1}(X_{i₁}) may be chosen in gr_m(X_{i₁})^X, that is, inside the kernel of the orientation, which is what keeps the orientation fixed along a successive approximation. The statement holds for every prime p; the relators x₁^q (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n) with p ∣ q satisfy its hypotheses with i₀ = x₁ and i₁ = x₂.
The exceptional generator (Lemma 3 of Labute's §4.2). When one further generator class ξ_{i₂} can only be reached through the derivative ∂_{i₀} ρ at the p-power generator, the same argument gives
gr_{m+1}(X_{i₁}) = δ_ρ(gr_m(X_{i₁})^X) + T_{m+1} + 𝔽_p π^m [ξ_{i₂}, ξ_{i₁}]
(gradedPieceOf_exponentSumKer_eq_map_basisModificationDelta_sup_gradedPowIterBracket), and when the coefficient of ∂_{i₀} ρ in ξ_{i₂} is nonzero the tail π^{m+1} ξ_{i₂} lies in the image of δ_ρ, so the tail may be taken over the a ≠ i₁, i₂ (gradedPieceOf_exponentSumKer_eq_map_basisModificationDelta_sup_gradedPowIterBracket_of_ne). The extra vector π^m [ξ_{i₂}, ξ_{i₁}] is genuinely needed at p = 2: the relator x₁² (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ has i₀ = x₁, i₁ = x₄ and i₂ = x₂.

Main definitions #

TauCeti.freeProP.exponentSumKer: the kernel X_i of the i-th exponent sum.

Main results #

TauCeti.freeProP.exponentSumKer_eq_topologicalClosure_normalClosure: X_i is the closed normal closure of the generators x_j, j ≠ i; hence a continuous homomorphism trivial on those generators is trivial on X_i (ContinuousMonoidHom.exponentSumKer_le_ker), and a dyadic character whose values at those generators square to 1 is trivial on X_i ∩ λ_1(F) (ContinuousMonoidHom.apply_eq_one_of_mem_exponentSumKer_of_mem_pLowerCentralSeries_one).
ContinuousMonoidHom.exponentSumKer_eq_ker: X_i is the kernel of every continuous character trivial on the generators x_j, j ≠ i, and of infinite order at x_i.
ContinuousMonoidHom.apply_mem_exponentSumKer_iff_of_forall_inv_mul_apply_mem: a continuous endomorphism moving each generator inside X_i preserves X_i.
TauCeti.freeProP.gradedMk_mem_gradedPieceOf_exponentSumKer_iff: the class of y ∈ λ_m(F) lies in gr_m(X_i) exactly when p ^ (m + 1) divides its i-th exponent sum.
TauCeti.freeProP.isCompl_gradedPieceOf_exponentSumKer_span_gradedPowIter: gr_m(F) = gr_m(X_i) ⊕ 𝔽_p π^m ξ_i.
TauCeti.freeProP.gradedPieceOf_exponentSumKer_le_of_le_sup_span_gradedPowIter: a subspace of gr_m(X_i) which together with π^m ξ_i spans gr_m(X_i) is gr_m(X_i).
TauCeti.freeProP.gradedPieceOf_exponentSumKer_succ_le: the generation criterion for gr_{m+1}(X_i).
gradedPieceOf_exponentSumKer_eq_map_basisModificationDelta_sup_span_gradedPowIter, gradedPieceOf_exponentSumKer_eq_map_basisModificationDelta_sup_gradedPowIterBracket and gradedPieceOf_exponentSumKer_eq_map_basisModificationDelta_sup_gradedPowIterBracket_of_ne (in TauCeti.freeProP): the constrained span statement, without and with an exceptional generator.

References #

J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, §4, Lemmas 1–3.

The kernel of an exponent sum of a free pro-p group and its graded pieces #

Main definitions #

Main results #

References #

The kernel of an exponent sum #

Endomorphisms preserving the kernel of an exponent sum #

The graded pieces of the kernel of an exponent sum #

Generation of the graded pieces of the kernel #

The constrained span statement #

The kernel of an exponent sum of a free pro-`p` group and its graded pieces #