Successive approximation inside the kernel of the orientation

Let F = freeProP p (Fin n) with n even, let w = x₁^q (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n) be the normal-form word TauCeti.demushkinWordNeTwo q n with p ∣ q, and let χ : F → ℤ_pˣ be a continuous character with the values of the orientation of this normal form, χ(x₂) (1 - q) = 1 and χ(x_i) = 1 for i ≠ 2. Let X be the kernel of the exponent sum at x₂, so that X ≤ ker χ, and X = ker χ when χ(x₂) has infinite order (ContinuousMonoidHom.exponentSumKer_eq_ker, in TauCeti.Topology.Algebra.Group.Profinite.Free.ExponentSumKernel).

Labute's proof of his Theorem 5 approximates a relator r ≡ w mod λ_2(F) by w through basis modifications x_i ↦ x_i w_i with w_i ∈ X, which do not change the values of χ on the generators. The deviation (φ w)⁻¹ * r after any such modification φ lies in X and is killed by the Kronecker crossed homomorphisms D_i : F → ℤ_p for χ, D_i(x_j) = δ_{ij}, at i ≠ 2, provided r is: D_i (φ w) = 0 because the word is killed at the tabulated character values (TauCeti.IsCrossedHom.map_apply_demushkinWordNeTwo_eq_zero). Labute's Lemma 4 (TauCeti.freeProP.mem_map_basisModificationDelta_iff_forall_gradedFunctional_crossedHom_eq_zero) then writes the class of such a deviation in gr_{m+1}(X) as δ_ρ(ω) with ω ∈ gr_m(X)^n, so the constrained successive-approximation theorem TauCeti.freeProP.exists_continuousMulEquiv_apply_eq applies with Z the set of elements of X killed by the Kronecker crossed homomorphisms and C i = X: an automorphism of F moving each generator inside X carries w to r, which is freeProP.exists_continuousMulEquiv_apply_demushkinWordNeTwo_eq_of_crossedHom_single_eq_zero.

The second half of the file reads the character values modulo p² off the relator. If the Kronecker crossed homomorphisms D_k, k ≠ 1, for a character χ kill a relator r ≡ w mod λ_2(F), then χ(x_i) ≡ 1 mod p² for every i ≠ 2 (TauCeti.freeProP.apply_mem_unitsPrincipal_two_of_crossedHom_single_eq_zero): D_k takes on r the value D_k(w) mod p², and on the commutator factor (x_k, x_{k'}) of w containing x_k it reads off χ(x_{k'}) - 1. This is what pins the values of the canonical character of a Demushkin group to the coset of the normal form, before the exact values are arranged by a basis modification.

Main results

• TauCeti.freeProP.apply_mem_unitsPrincipal_two_of_crossedHom_single_eq_zero: a character whose Kronecker crossed homomorphisms D_k, k ≠ 1, kill a relator in the class of the normal form takes the generators x_i, i ≠ 2, into 1 + p²ℤ_p.
• freeProP.exists_continuousMulEquiv_apply_demushkinWordNeTwo_eq_of_crossedHom_single_eq_zero: the successive approximation inside X: a relator r ∈ X in the class of the normal form, killed by the Kronecker crossed homomorphisms D_i, i ≠ 2, for χ, is the image of the normal-form word under a continuous automorphism of F moving each generator inside X.

References

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

The character values modulo p²

theorem TauCeti.freeProP.apply_mem_unitsPrincipal_two_of_crossedHom_single_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {n q : ℕ} {χ : freeProP p (Fin n) →ₜ* ℤ_[p]ˣ} (hn : Even n) (hn1 : 1 < n) (hq : p ∣ q) (r : ↥(pLowerCentralSeries p (freeProP p (Fin n)) 1)) (hr : gradedMk p (freeProP p (Fin n)) 1 r = gradedMk p (freeProP p (Fin n)) 1 ⟨demushkinWordNeTwo q n (freeProPGen p n), ⋯⟩) (hD : ∀ (k : Fin n), ↑k ≠ 0 → crossedHom χ (Pi.single k 1) ↑r = 0) {j : Fin n} (hj : j ≠ ⟨1, hn1⟩) : χ (of j) ∈ unitsPrincipal p 2

The character values forced by the relator, modulo p² (Labute, proof of Theorem 5). Let n be even, p ∣ q, and let r ∈ λ_1(F) be a relator in the class of w = x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) modulo λ_2(F). If the Kronecker crossed homomorphisms D_k : F → ℤ_p, D_k(x_i) = δ_{ki}, for a continuous character χ kill r for every k ≠ 1, then χ(x_j) ∈ 1 + p²ℤ_p for every j ≠ 2: the Kronecker crossed homomorphism D_k at the partner x_k of x_j in the commutator factor (x_j, x_k) or (x_k, x_j) of w takes on r the value D_k(w) ≡ ±(χ(x_j) - 1) modulo p².

The successive approximation inside X

theorem TauCeti.freeProP.exists_continuousMulEquiv_apply_demushkinWordNeTwo_eq_of_crossedHom_single_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {n q : ℕ} {χ : freeProP p (Fin n) →ₜ* ℤ_[p]ˣ} (hn : Even n) (hn1 : 1 < n) (hq : p ∣ q) (h₁ : ↑(χ (of ⟨1, hn1⟩)) * (1 - ↑q) = 1) (h : ∀ (j : Fin n), j ≠ ⟨1, hn1⟩ → χ (of j) = 1) (r : ↥(pLowerCentralSeries p (freeProP p (Fin n)) 1)) (hr : gradedMk p (freeProP p (Fin n)) 1 r = gradedMk p (freeProP p (Fin n)) 1 ⟨demushkinWordNeTwo q n (freeProPGen p n), ⋯⟩) (hrX : ↑r ∈ exponentSumKer p (Fin n) ⟨1, hn1⟩) (hD : ∀ (i : Fin n), i ≠ ⟨1, hn1⟩ → crossedHom χ (Pi.single i 1) ↑r = 0) : ∃ (e : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)), (∀ (i : Fin n), (of i)⁻¹ * e (of i) ∈ exponentSumKer p (Fin n) ⟨1, hn1⟩) ∧ e (demushkinWordNeTwo q n (freeProPGen p n)) = ↑r

The successive approximation inside the kernel of the orientation (Labute, proof of Theorem 5). Let n be even, p ∣ q, w = x₁^q (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n), and let χ : F → ℤ_pˣ be a continuous character with χ(x₂) (1 - q) = 1 and χ(x_i) = 1 for i ≠ 2. Let r ∈ λ_1(F) be a relator in the class of w modulo λ_2(F), lying in the kernel X of the exponent sum at x₂, and killed by the Kronecker crossed homomorphisms D_i : F → ℤ_p, D_i(x_j) = δ_{ij}, for χ at every i ≠ 2. Then a continuous automorphism of F moving every generator inside X carries w to r.

The deviations (φ w)⁻¹ * r of the approximations lie in X and are killed by the Kronecker crossed homomorphisms D_i, i ≠ 2, and Labute's Lemma 4 writes their classes as δ_ρ(ω) with ω ∈ gr_m(X)^n, which is the constrained span statement of TauCeti.freeProP.exists_continuousMulEquiv_apply_eq.