The constrained span statement at the normal form x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n)

Let F = freeProP p (Fin n) with n even, let r 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. Throughout this file indices are the 0-based indices of Fin n: x_j = of j is the j-th generator, ξ_j its class in gr_0(F), and ∂_j is the partial derivative TauCeti.freeProP.degreeOneDeriv p (Fin n) j at x_j; in these indices the word is r = x_0^q (x_0, x_1)(x_2, x_3) ⋯ (x_{n-2}, x_{n-1}). The partial derivatives of ρ at the generators other than x_0 are ∂_{2a+1} ρ = -ξ_{2a} whenever 2a + 1 < n, and ∂_{2a} ρ = ξ_{2a+1} whenever 1 ≤ a and 2a + 1 < n (TauCeti.freeProP.degreeOneDeriv_gradedMk_demushkinWordNeTwo_odd, TauCeti.freeProP.degreeOneDeriv_gradedMk_demushkinWordNeTwo_even). So every generator class ξ_j with j ≠ 1 is a combination of these derivatives, which is the hypothesis of the constrained span statement of Free/ExponentSumKernel.lean with i₀ = 0 and i₁ = 1. The conclusion is Labute's Lemma 3: for the kernel X of the exponent sum at x_1 and every m ≥ 1,

gr_{m+1}(X) = δ_ρ(gr_m(X)^n) + T_{m+1},

where T_{m+1} is spanned by the π^{m+1} ξ_j with j ≠ 1. This is the span statement that the uniqueness argument for the dyadic even-rank Demushkin groups with orientation image U^[f] runs on: their relator x₁^{2+2^f} (x₁, x₂)(x₃, x₄) ⋯ is this word at p = 2 and q = 2 + 2^f, the orientation is the exponent sum at x_1 composed with γ ↦ χ(x_1)^γ, and the basis corrections must be taken inside its kernel.

Main results

• TauCeti.freeProP.degreeOneDeriv_gradedMk_demushkinWordNeTwo_odd, TauCeti.freeProP.degreeOneDeriv_gradedMk_demushkinWordNeTwo_even, TauCeti.freeProP.degreeOneDeriv_gradedMk_demushkinWordNeTwo_zero: the partial derivatives of the class of the word at the generators.
• gradedPieceOf_exponentSumKer_demushkinWordNeTwo_eq_map_basisModificationDelta_sup (in TauCeti.freeProP): the constrained span statement at this normal form.

References

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

theorem TauCeti.freeProP.demushkinWordNeTwo_freeProPGen_mem_exponentSumKer {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (hn1 : 1 < n) (q : ℕ) : demushkinWordNeTwo q n (freeProPGen p n) ∈ exponentSumKer p (Fin n) ⟨1, hn1⟩

The normal-form word x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) lies in the kernel X of the exponent sum at x₂: its exponent vector is q at x₁ and 0 elsewhere.

theorem TauCeti.freeProP.degreeOneDeriv_gradedMk_demushkinWordNeTwo_even {p : ℕ} [Fact (Nat.Prime p)] {n q : ℕ} (hq : p ∣ q) {a : ℕ} (ha₀ : 0 < a) (ha : 2 * a + 1 < n) : (degreeOneDeriv p (Fin n) ⟨2 * a, ⋯⟩) (gradedMk p (freeProP p (Fin n)) 1 ⟨demushkinWordNeTwo q n (freeProPGen p n), ⋯⟩) = gradedMkZero p (freeProP p (Fin n)) (freeProPGen p n (2 * a + 1))

The derivative of the class of x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) at the generator x_{2a} (in the 0-based indexing of Fin n), for a ≥ 1: ∂_{2a} ρ = ξ_{2a+1}.

theorem TauCeti.freeProP.degreeOneDeriv_gradedMk_demushkinWordNeTwo_odd {p : ℕ} [Fact (Nat.Prime p)] {n q : ℕ} (hq : p ∣ q) {a : ℕ} (ha : 2 * a + 1 < n) : (degreeOneDeriv p (Fin n) ⟨2 * a + 1, ha⟩) (gradedMk p (freeProP p (Fin n)) 1 ⟨demushkinWordNeTwo q n (freeProPGen p n), ⋯⟩) = -gradedMkZero p (freeProP p (Fin n)) (freeProPGen p n (2 * a))

The derivative of the class of x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) at the generator x_{2a+1} (in the 0-based indexing of Fin n): ∂_{2a+1} ρ = -ξ_{2a}.

theorem TauCeti.freeProP.degreeOneDeriv_gradedMk_demushkinWordNeTwo_zero {p : ℕ} [Fact (Nat.Prime p)] {n q : ℕ} (hq : p ∣ q) (hn1 : 1 < n) : (degreeOneDeriv p (Fin n) ⟨0, ⋯⟩) (gradedMk p (freeProP p (Fin n)) 1 ⟨demushkinWordNeTwo q n (freeProPGen p n), ⋯⟩) = (q / p) • p.choose 2 • gradedMkZero p (freeProP p (Fin n)) (of ⟨0, ⋯⟩) + gradedMkZero p (freeProP p (Fin n)) (of ⟨1, hn1⟩)

The derivative of the class of x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) at the generator x_0 (in the 0-based indexing of Fin n), for n ≥ 2: ∂_0 ρ = (q / p) • (p choose 2) • ξ_0 + ξ_1, the first term from the p-power factor x_0^q and the second from the bracket [ξ_0, ξ_1].

theorem TauCeti.freeProP.exists_sum_smul_degreeOneDeriv_gradedMk_demushkinWordNeTwo_eq {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (hn : Even n) {q : ℕ} (hq : p ∣ q) (hn1 : 1 < n) (j : Fin n) (hj : j ≠ ⟨1, hn1⟩) : ∃ (b : Fin n → ZMod p), b ⟨0, ⋯⟩ = 0 ∧ ∑ k : Fin n, b k • (degreeOneDeriv p (Fin n) k) (gradedMk p (freeProP p (Fin n)) 1 ⟨demushkinWordNeTwo q n (freeProPGen p n), ⋯⟩) = gradedMkZero p (freeProP p (Fin n)) (of j)

Every generator class other than ξ_1 is a combination of the derivatives at the generators other than x_0 (in the 0-based indexing of Fin n), for the class of x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) with n even.

theorem TauCeti.freeProP.gradedPieceOf_exponentSumKer_demushkinWordNeTwo_eq_map_basisModificationDelta_sup {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (hn : Even n) (hn1 : 1 < n) {q : ℕ} (hq : p ∣ q) {m : ℕ} (hm : 1 ≤ m) : 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) ⊔ Submodule.span (ZMod p) (Set.range fun (a : { a : Fin n // a ≠ ⟨1, hn1⟩ }) => gradedPowIter p (freeProP p (Fin n)) (m + 1) (gradedMkZero p (freeProP p (Fin n)) (of ↑a)))

The constrained span statement at the normal form x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) (Labute, §4, Lemma 3). For n even, p ∣ q, the class ρ of the word, X the kernel of the exponent sum at the generator x_1 (in the 0-based indexing of Fin n) and every m ≥ 1,

gr_{m+1}(X) = δ_ρ(gr_m(X)^n) + T_{m+1},

where the tail T_{m+1} is spanned by the p-powers π^{m+1} ξ_j with j ≠ 1. At p = 2 and q = 2 + 2^f this is the span statement for the relators x₁^{2+2^f} (x₁, x₂)(x₃, x₄) ⋯ whose basis corrections must respect the orientation.