The span statement and the graded functionals at x₁² (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯

Let F = freeProP 2 (Fin n) with n ≥ 4 even, let r = x₁² (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n) be the normal-form word TauCeti.demushkinWordTwoEven 0 f n with f ≥ 2 on the generators of F, and let ρ ∈ gr_1(F) be its class. Its orientation is the character χ : F → ℤ_2ˣ with χ(x₂) = -1, χ(x₄) = (1 - 2^f)⁻¹ and χ(x_i) = 1 otherwise, whose image is {±1} × U^(f). Throughout, indices in the Lean statements are the 0-based indices of Fin n: x₂ is of ⟨1, _⟩ and x₄ is of ⟨3, _⟩.

For f ≥ 2 the factor x₃^{2^f} lies in λ_2(F), so ρ is also the class of the q ≠ 2 word x₁² (x₁, x₂)(x₃, x₄) ⋯ (TauCeti.gradedMk_demushkinWordTwoEven_eq_gradedMk_demushkinWordNeTwo), and the basis-modification map δ_ρ is the one of that word. What changes is the kernel of the orientation. Its intersection with λ_1(F) is the intersection with λ_1(F) of the kernel X of the exponent sum at x₄, because χ(x₂) = -1 has order two and λ_1(F) is generated by squares and commutators (ContinuousMonoidHom.apply_eq_one_of_mem_exponentSumKer_of_mem_pLowerCentralSeries_one). In gr(X) the generator class ξ₂ is reached only through the derivative ∂₁ ρ = ξ₁ + ξ₂ at the 2-power generator x₁, so it is the exceptional generator of the constrained span statement of Free/ExponentSumKernel.lean: Labute's Lemma 3 for this family reads, for every m ≥ 1,

gr_{m+1}(X) = δ_ρ(gr_m(X)^n) + ⟨π^{m+1} ξ_j : j ≠ 2, 4⟩ + 𝔽_2 π^m [ξ₂, ξ₄]

(gradedPieceOf_exponentSumKer_demushkinWordTwoEven_eq_map_basisModificationDelta_sup in TauCeti.freeProP). The extra spanning vector π^m [ξ₂, ξ₄] is the class of (x₂, x₄)^{2^m}; it is not in the image of δ_ρ, because the graded functional Δ_{m+1}(D₄) of the crossed homomorphism D₄ for χ with D₄(x_j) = δ_{4j} takes the value 1 on it (TauCeti.freeProP.gradedFunctional_crossedHom_gradedPowIterBracket_of_apply_eq_neg_one), while every graded functional of a crossed homomorphism for χ vanishes on δ_ρ(gr_m(X)^n) (TauCeti.freeProP.gradedFunctional_basisModificationDelta_demushkinWordTwoEven_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 (mem_map_basisModificationDelta_demushkinWordTwoEven_iff_forall_gradedFunctional_eq_zero in TauCeti.freeProP). This is Labute's Lemma 4 for the second even-rank dyadic family, the finite step of the successive approximation showing that a Demushkin group at p = 2 of even rank whose orientation has image {±1} × U^(f) is presented by this word: the deviation of its relator from the word, once it lies in gr_{m+1}(X) and is killed by all crossed homomorphisms for χ, is removed by a basis correction inside X.

Main results

All results are in the namespace TauCeti.freeProP.

• gradedPieceOf_exponentSumKer_demushkinWordTwoEven_eq_map_basisModificationDelta_sup: the constrained span statement at this normal form, with the exceptional spanning vector π^m [ξ₂, ξ₄].
• gradedFunctional_basisModificationDelta_demushkinWordTwoEven_eq_zero: the graded functional of a crossed homomorphism for the orientation vanishes on δ_ρ(gr_m(X)^n).
• gradedFunctional_crossedHom_gradedPowIterBracket_of_apply_eq_neg_one: the graded functionals Δ_{m+1}(D_i), i ≠ 2, read off the coefficient of π^m [ξ₂, ξ₄].
• mem_map_basisModificationDelta_demushkinWordTwoEven_iff_forall_gradedFunctional_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.2, Lemmas 1–4 and the proof of Theorem 6.

The constrained span statement

theorem TauCeti.freeProP.gradedPieceOf_exponentSumKer_demushkinWordTwoEven_eq_map_basisModificationDelta_sup {n : ℕ} (hn : Even n) (hn3 : 3 < n) {f : ℕ} (hf : 2 ≤ f) {m : ℕ} (hm : 1 ≤ m) : gradedPieceOf 2 (exponentSumKer 2 (Fin n) ⟨3, hn3⟩) (m + 1) = Submodule.map ((basisModificationDelta 2 (Fin n) hm) (gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordTwoEven 0 f n (freeProPGen 2 n), ⋯⟩)) (Submodule.pi Set.univ fun (x : Fin n) => gradedPieceOf 2 (exponentSumKer 2 (Fin n) ⟨3, hn3⟩) m) ⊔ Submodule.span (ZMod 2) (Set.range fun (a : { a : Fin n // a ≠ ⟨3, hn3⟩ ∧ a ≠ ⟨1, ⋯⟩ }) => gradedPowIter 2 (freeProP 2 (Fin n)) (m + 1) (gradedMkZero 2 (freeProP 2 (Fin n)) (of ↑a))) ⊔ ZMod 2 ∙ gradedPowIterBracket 2 (freeProP 2 (Fin n)) m (of ⟨1, ⋯⟩) (of ⟨3, hn3⟩)

The constrained span statement at the normal form x₁² (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (Labute, §4.2, Lemma 3). For n ≥ 4 even, f ≥ 2, the class ρ of the word, X the kernel of the exponent sum at the generator x_3 (in the 0-based indexing of Fin n) and every m ≥ 1,

gr_{m+1}(X) = δ_ρ(gr_m(X)^n) + ⟨π^{m+1} ξ_j : j ≠ 1, 3⟩ + 𝔽_2 π^m [ξ_1, ξ_3].

This is the span statement on which the uniqueness argument for the dyadic even-rank Demushkin groups with orientation image {±1} × U^(f) runs: the basis corrections must be taken inside the kernel of the orientation, which meets λ_1(F) in X ∩ λ_1(F).

The graded functionals of the orientation

theorem TauCeti.IsCrossedHom.map_inv_mul_basisModification_demushkinWordTwoEven_eq_zero {n : ℕ} {χ : freeProP 2 (Fin n) →ₜ* ℤ_[2]ˣ} (hn3 : 3 < n) {f : ℕ} (h₁ : χ (freeProP.of ⟨1, ⋯⟩) = -1) (h₃ : ↑(χ (freeProP.of ⟨3, hn3⟩)) * (1 - 2 ^ f) = 1) (h : ∀ (j : Fin n), j ≠ ⟨1, ⋯⟩ → j ≠ ⟨3, hn3⟩ → χ (freeProP.of j) = 1) {F : freeProP 2 (Fin n) → ℤ_[2]} (hF : IsCrossedHom (⇑χ) F) {m : ℕ} (w : Fin n → ↥(pLowerCentralSeries 2 (freeProP 2 (Fin n)) m)) (hw : ∀ (i : Fin n), χ ↑(w i) = 1) : F ((demushkinWordTwoEven 0 f n (freeProPGen 2 n))⁻¹ * (freeProP.basisModification w) (demushkinWordTwoEven 0 f n (freeProPGen 2 n))) = 0

A crossed homomorphism for the orientation kills the relator moved by a basis modification inside the kernel of the character. For n ≥ 4, χ with χ(x₂) = -1, χ(x₄) (1 - 2^f) = 1 and χ(x_i) = 1 for i ≠ 2, 4, a crossed homomorphism F for χ, and a family w of elements of λ_m(F) on which χ is trivial, F (r⁻¹ · θ_w(r)) = 0 for r = x₁² (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯: 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_demushkinWordTwoEven_eq_zero {n : ℕ} {χ : freeProP 2 (Fin n) →ₜ* ℤ_[2]ˣ} (hn3 : 3 < n) {f : ℕ} (hf : 0 < f) {m : ℕ} (hm : 1 ≤ m) (h₁ : χ (of ⟨1, ⋯⟩) = -1) (h₃ : ↑(χ (of ⟨3, hn3⟩)) * (1 - 2 ^ f) = 1) (h : ∀ (j : Fin n), j ≠ ⟨1, ⋯⟩ → j ≠ ⟨3, hn3⟩ → χ (of j) = 1) {F : freeProP 2 (Fin n) → ℤ_[2]} (hF : IsCrossedHom (⇑χ) F) (hFc : Continuous F) {v : Fin n → gradedPiece 2 (freeProP 2 (Fin n)) m} (hv : ∀ (i : Fin n), v i ∈ gradedPieceOf 2 (exponentSumKer 2 (Fin n) ⟨3, hn3⟩) m) : (hF.gradedFunctional ⋯ hFc (m + 1)) (((basisModificationDelta 2 (Fin n) hm) (gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordTwoEven 0 f n (freeProPGen 2 n), ⋯⟩)) v) = 0

The graded functional of a crossed homomorphism for the orientation vanishes on δ_ρ(gr_m(X)^n) (Labute, §4.2, Lemma 4 (2)). For n ≥ 4, f ≥ 1, χ with χ(x₂) = -1, χ(x₄) (1 - 2^f) = 1 and χ(x_i) = 1 for i ≠ 2, 4, a continuous crossed homomorphism F for χ, the class ρ of r = x₁² (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ 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 ∩ λ_m(F) ≤ ker χ, which F kills.

theorem TauCeti.freeProP.gradedFunctional_crossedHom_gradedPowIterBracket_of_apply_eq_neg_one {n : ℕ} {χ : freeProP 2 (Fin n) →ₜ* ℤ_[2]ˣ} (hn3 : 3 < n) (h₁ : χ (of ⟨1, ⋯⟩) = -1) (m : ℕ) {i : Fin n} (hi : i ≠ ⟨1, ⋯⟩) : (⋯.gradedFunctional ⋯ ⋯ (m + 1)) (gradedPowIterBracket 2 (freeProP 2 (Fin n)) m (of ⟨1, ⋯⟩) (of ⟨3, hn3⟩)) = if i = ⟨3, hn3⟩ then 1 else 0

The graded functionals of the orientation on the exceptional class π^m [ξ₂, ξ₄] (Labute, §4.2, Lemma 4 (3)). For χ with χ(x₂) = -1, χ(x₄) (1 - 2^f) = 1 and the crossed homomorphism D_i for χ with D_i(x_j) = δ_{ij}, i ≠ 2, the value of Δ_{m+1}(D_i) on π^m [ξ₂, ξ₄], the class of (x₂, x₄)^{2^m}, is 1 for i = 4 and 0 otherwise: D_i (x₂, x₄) = -2 D_i(x₄) up to a unit, because χ(x₂) - 1 = -2.

theorem TauCeti.freeProP.mem_map_basisModificationDelta_demushkinWordTwoEven_iff_forall_gradedFunctional_eq_zero {n : ℕ} {χ : freeProP 2 (Fin n) →ₜ* ℤ_[2]ˣ} (hn : Even n) (hn3 : 3 < n) {f : ℕ} (hf : 2 ≤ f) {m : ℕ} (hm : 1 ≤ m) (h₁ : χ (of ⟨1, ⋯⟩) = -1) (h₃ : ↑(χ (of ⟨3, hn3⟩)) * (1 - 2 ^ f) = 1) (h : ∀ (j : Fin n), j ≠ ⟨1, ⋯⟩ → j ≠ ⟨3, hn3⟩ → χ (of j) = 1) {ε : gradedPiece 2 (freeProP 2 (Fin n)) (m + 1)} (hε : ε ∈ gradedPieceOf 2 (exponentSumKer 2 (Fin n) ⟨3, hn3⟩) (m + 1)) : ε ∈ Submodule.map ((basisModificationDelta 2 (Fin n) hm) (gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordTwoEven 0 f n (freeProPGen 2 n), ⋯⟩)) (Submodule.pi Set.univ fun (x : Fin n) => gradedPieceOf 2 (exponentSumKer 2 (Fin n) ⟨3, hn3⟩) m) ↔ ∀ (i : Fin n), i ≠ ⟨1, ⋯⟩ → (⋯.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.2, Lemma 4 (4)). Let n ≥ 4 be even, f ≥ 2, ρ the class of x₁² (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯, χ a continuous character with χ(x₂) = -1, χ(x₄) (1 - 2^f) = 1 and χ(x_i) = 1 for i ≠ 2, 4, 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}: the functionals Δ_{m+1}(D_i), i ≠ 2, 4, read off the coefficients of the tail π^{m+1} ξ_i, and Δ_{m+1}(D₄) that of the exceptional class π^m [ξ₂, ξ₄].