The graded functionals of the orientation cut out the image of δ in gr(X)

Let F = freeProP p (Fin n) with n even, let r = x₁^q (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n) be the normal-form word TauCeti.demushkinWordNeTwo q n on the generators of F with p ∣ q, and let ρ ∈ gr_1(F) be its class. 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, and let X be the kernel of the exponent sum at x₂, with graded pieces gr_m(X) ≤ gr_m(F). Since χ is trivial on the generators x_i, i ≠ 2, which topologically generate X as a normal subgroup, X ≤ ker χ (ContinuousMonoidHom.exponentSumKer_le_ker); for the orientation itself, where χ(x₂) has infinite order, X is the kernel of χ, Labute's X = ker χ. Throughout, indices in the Lean statements are the 0-based indices of Fin n, so x₂ is of ⟨1, _⟩ and X is TauCeti.freeProP.exponentSumKer p (Fin n) ⟨1, _⟩.

The constrained span statement of Demushkin/NormalForm/Kernel/Span.lean (Labute's Lemma 3) writes every class of gr_{m+1}(X) as δ_ρ(ω) + Σ_{i ≠ 2} c_i π^{m+1} ξ_i with ω ∈ gr_m(X)^n. This file supplies the functionals that read off the coefficients c_i, and so cuts the image of the basis-modification map δ_ρ out of gr_{m+1}(X). They are the graded functionals Δ_{m+1}(D_i) : gr_{m+1}(F) → 𝔽_p (TauCeti.IsCrossedHom.gradedFunctional) of the crossed homomorphisms D_i : F → ℤ_p for χ with D_i(x_j) = δ_{ij} (TauCeti.freeProP.crossedHom):

• on the p-power π^{m+1} ξ_j with j ≠ 2, Δ_{m+1}(D_i) takes the value δ_{ij}, because χ(x_j) = 1 (TauCeti.IsCrossedHom.gradedFunctional_gradedPowIter_gradedMkZero);
• on δ_ρ(ω) with ω ∈ gr_m(X)^n every Δ_{m+1}(D) vanishes (TauCeti.freeProP.gradedFunctional_basisModificationDelta_demushkinWordNeTwo_eq_zero): δ_ρ(ω) is the class of r⁻¹ · θ_w(r) for a basis modification θ_w : x_i ↦ x_i w_i with w_i ∈ X ≤ ker χ, and a crossed homomorphism for χ kills both r and θ_w(r), since χ takes the same values on the tuple (x_i w_i) as on (x_i) and at those values the word is killed (TauCeti.IsCrossedHom.map_demushkinWordNeTwo_eq_zero).

Hence a class of gr_{m+1}(X) lies in δ_ρ(gr_m(X)^n) exactly when it is killed by every Δ_{m+1}(D_i) with i ≠ 2 (TauCeti.freeProP.mem_map_basisModificationDelta_iff_forall_gradedFunctional_crossedHom_eq_zero). This is Labute's Lemma 4. At p = 2 and q = 2 + 2^f with f ≥ 2, χ is the orientation of the Demushkin relator x₁^{2+2^f} (x₁, x₂)(x₃, x₄) ⋯ with image U^[f], and the lemma is the finite step of the successive approximation proving that every Demushkin group with these invariants has a basis in which its relator is exactly this word: the deviation of the relator from the word, once it lies in gr_{m+1}(X) and is killed by all crossed homomorphisms of F into ℤ_p, is removed by a basis correction inside X.

Main results

• TauCeti.IsCrossedHom.map_apply_demushkinWordNeTwo_eq_zero: a crossed homomorphism for χ kills φ(r) for every endomorphism φ preserving the values of χ on the generators.
• TauCeti.IsCrossedHom.map_inv_mul_basisModification_demushkinWordNeTwo_eq_zero: a crossed homomorphism for χ kills r⁻¹ · θ_w(r) for every basis modification by elements of ker χ.
• TauCeti.freeProP.gradedFunctional_basisModificationDelta_demushkinWordNeTwo_eq_zero: the graded functional of a crossed homomorphism for χ vanishes on δ_ρ(gr_m(X)^n).
• TauCeti.freeProP.mem_map_basisModificationDelta_iff_forall_gradedFunctional_crossedHom_eq_zero: a class of gr_{m+1}(X) lies in δ_ρ(gr_m(X)^n) exactly when the graded functionals of the D_i, i ≠ 2, kill it.

References

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

theorem TauCeti.IsCrossedHom.map_apply_demushkinWordNeTwo_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {n q : ℕ} {χ : freeProP p (Fin n) →ₜ* ℤ_[p]ˣ} (hn1 : 1 < n) (h₁ : ↑(χ (freeProP.of ⟨1, hn1⟩)) * (1 - ↑q) = 1) (h : ∀ (j : Fin n), j ≠ ⟨1, hn1⟩ → χ (freeProP.of j) = 1) {f : freeProP p (Fin n) → ℤ_[p]} (hf : IsCrossedHom (⇑χ) f) (φ : freeProP p (Fin n) →ₜ* freeProP p (Fin n)) (hφ : ∀ (i : ℕ), χ (φ (freeProPGen p n i)) = χ (freeProPGen p n i)) : f (φ (demushkinWordNeTwo q n (freeProPGen p n))) = 0

A crossed homomorphism for the orientation kills the image of the normal-form word under an endomorphism preserving the character values on the generators: for χ with χ(x₂) (1 - q) = 1 and χ(x_i) = 1 for i ≠ 2, the word on the tuple (φ x_i) is killed at the same character values.

theorem TauCeti.IsCrossedHom.map_inv_mul_basisModification_demushkinWordNeTwo_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {n q : ℕ} {χ : freeProP p (Fin n) →ₜ* ℤ_[p]ˣ} (hn1 : 1 < n) (h₁ : ↑(χ (freeProP.of ⟨1, hn1⟩)) * (1 - ↑q) = 1) (h : ∀ (j : Fin n), j ≠ ⟨1, hn1⟩ → χ (freeProP.of j) = 1) {f : freeProP p (Fin n) → ℤ_[p]} (hf : IsCrossedHom (⇑χ) f) {m : ℕ} (w : Fin n → ↥(pLowerCentralSeries p (freeProP p (Fin n)) m)) (hw : ∀ (i : Fin n), χ ↑(w i) = 1) : f ((demushkinWordNeTwo q n (freeProPGen p n))⁻¹ * (freeProP.basisModification w) (demushkinWordNeTwo q n (freeProPGen p n))) = 0

A crossed homomorphism for the orientation kills the relator moved by a basis modification inside the kernel of the character. For χ with χ(x₂) (1 - q) = 1 and χ(x_i) = 1 for i ≠ 2, a crossed homomorphism f for χ, and a family w of elements of λ_m(F) on which χ is trivial (for instance elements of the kernel X of the exponent sum at x₂, since X ≤ ker χ), f (r⁻¹ · θ_w(r)) = 0 for r = x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n): the character takes the same values on the modified tuple (x_i w_i) as on (x_i), and at those values a crossed homomorphism kills the word.

@[simp]

theorem TauCeti.freeProP.gradedFunctional_basisModificationDelta_demushkinWordNeTwo_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {n q : ℕ} {χ : freeProP p (Fin n) →ₜ* ℤ_[p]ˣ} (hn1 : 1 < n) (hq : p ∣ q) {m : ℕ} (hm : 1 ≤ m) (h₁ : ↑(χ (of ⟨1, hn1⟩)) * (1 - ↑q) = 1) (h : ∀ (j : Fin n), j ≠ ⟨1, hn1⟩ → χ (of j) = 1) {f : freeProP p (Fin n) → ℤ_[p]} (hf : IsCrossedHom (⇑χ) f) (hfc : Continuous f) {v : Fin n → gradedPiece p (freeProP p (Fin n)) m} (hv : ∀ (i : Fin n), v i ∈ gradedPieceOf p (exponentSumKer p (Fin n) ⟨1, hn1⟩) m) : (hf.gradedFunctional ⋯ hfc (m + 1)) (((basisModificationDelta p (Fin n) hm) (gradedMk p (freeProP p (Fin n)) 1 ⟨demushkinWordNeTwo q n (freeProPGen p n), ⋯⟩)) v) = 0

The graded functional of a crossed homomorphism for the orientation vanishes on δ_ρ(gr_m(X)^n) (Labute, §4, Lemma 4 (2)). For χ with χ(x₂) (1 - q) = 1 and χ(x_i) = 1 for i ≠ 2, a continuous crossed homomorphism f for χ, the class ρ of r = x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) and a family v of classes in gr_m(X), where X is the kernel of the exponent sum at x₂, Δ_{m+1}(f) (δ_ρ(v)) = 0: δ_ρ(v) is the class of r⁻¹ · θ_w(r) for a basis modification θ_w by elements of X, which f kills.

theorem TauCeti.freeProP.mem_map_basisModificationDelta_iff_forall_gradedFunctional_crossedHom_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {n q : ℕ} {χ : freeProP p (Fin n) →ₜ* ℤ_[p]ˣ} (hn : Even n) (hn1 : 1 < n) (hq : p ∣ q) {m : ℕ} (hm : 1 ≤ m) (h₁ : ↑(χ (of ⟨1, hn1⟩)) * (1 - ↑q) = 1) (h : ∀ (j : Fin n), j ≠ ⟨1, hn1⟩ → χ (of j) = 1) {ε : gradedPiece p (freeProP p (Fin n)) (m + 1)} (hε : ε ∈ gradedPieceOf p (exponentSumKer p (Fin n) ⟨1, hn1⟩) (m + 1)) : ε ∈ Submodule.map ((basisModificationDelta p (Fin n) hm) (gradedMk p (freeProP p (Fin n)) 1 ⟨demushkinWordNeTwo q n (freeProPGen p n), ⋯⟩)) (Submodule.pi Set.univ fun (x : Fin n) => gradedPieceOf p (exponentSumKer p (Fin n) ⟨1, hn1⟩) m) ↔ ∀ (i : Fin n), i ≠ ⟨1, hn1⟩ → (⋯.gradedFunctional ⋯ ⋯ (m + 1)) ε = 0

The image of δ_ρ on gr_m(X)^n is the common kernel in gr_{m+1}(X) of the graded functionals of the orientation (Labute, §4, Lemma 4 (4)). Let n be even, p ∣ q, ρ the class of x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n), χ a continuous character with χ(x₂) (1 - q) = 1 and χ(x_i) = 1 for i ≠ 2, and X the kernel of the exponent sum at x₂. For m ≥ 1, a class ε ∈ gr_{m+1}(X) lies in δ_ρ(gr_m(X)^n) exactly when Δ_{m+1}(D_i) ε = 0 for every i ≠ 2, where D_i is the crossed homomorphism for χ with D_i(x_j) = δ_{ij}.