The pivot-constrained span statement for basis modifications

Let F = freeProP p X be the free pro-p group on a finite linearly ordered type, and let ρ ∈ gr_1(F) be a class without p-power part whose partial derivatives ∂_i ρ span gr_0(F), the class of a relator x₀^q (x₀, x₁) (x₂, x₃) ⋯ with q ≠ p in which every generator occurs in a commutator. The image of the basis-modification map δ_ρ : gr_m(F)^X → gr_{m+1}(F) is the commutator part [gr_m(F), gr_0(F)] of gr_{m+1}(F) (TauCeti.freeProP.range_basisModificationDelta_eq_span_of_repr_inl_eq_zero). The successive approximation of such a relator has to keep its exponent vector fixed, so its basis corrections x_i ↦ x_i w_i must take w_{x₀} in the commutator subgroup at the pivot x₀ carrying the p-power: the correction is allowed to be arbitrary at the other generators only.

This file shows that the constraint costs nothing: every element of Im δ_ρ is δ_ρ(ω) for a family ω whose component at any prescribed generator x₀ lies in the bracket span C_m(F) = [gr_{m-1}(F), gr_0(F)] (TauCeti.freeProP.exists_apply_mem_gradedBracketSpan_basisModificationDelta_eq), hence is the class of an element of λ_m(F) in the commutator subgroup (TauCeti.freeProP.exists_apply_mem_commutator_basisModificationDelta_eq_of_mem_range). No hypothesis on x₀ is needed.

Main results

• TauCeti.freeProP.exists_apply_mem_gradedBracketSpan_basisModificationDelta_eq: every element of Im δ_ρ is δ_ρ(ω) with ω_{x₀} ∈ C_m(F).
• TauCeti.freeProP.exists_apply_mem_commutator_basisModificationDelta_eq_of_mem_range: every element of Im δ_ρ is δ_ρ(⟦ω⟧) for a family ω : X → λ_m(F) with ω_{x₀} in the commutator subgroup of F.

References

• J. Labute, Classification of Demushkin groups, Canadian J. Math. 19 (1967), §3, Proposition 5 and the proof of Theorem 3.

theorem TauCeti.freeProP.exists_apply_mem_gradedBracketSpan_basisModificationDelta_eq {p : ℕ} {X : Type u} [Fact (Nat.Prime p)] [Finite X] [LinearOrder X] {k : ℕ} {ρ : gradedPiece p (freeProP p X) 1} (hρ : Submodule.span (ZMod p) (Set.range fun (i : X) => (degreeOneDeriv p X i) ρ) = ⊤) (hc : ∀ (i : X), ((degreeOneBasis p X).repr ρ) (Sum.inl i) = 0) (x₀ : X) {y : gradedPiece p (freeProP p X) (k + 1 + 1)} (hy : y ∈ ((basisModificationDelta p X ⋯) ρ).range) : ∃ (ω : X → gradedPiece p (freeProP p X) (k + 1)), ω x₀ ∈ gradedBracketSpan p (freeProP p X) k ∧ ((basisModificationDelta p X ⋯) ρ) ω = y

The pivot-constrained span statement, graded form. Let ρ ∈ gr_1(F) have no p-power part and partial derivatives spanning gr_0(F). Every element of the image of δ_ρ : gr_{k+1}(F)^X → gr_{k+2}(F) is δ_ρ(ω) for a family ω whose component at the prescribed generator x₀ lies in the bracket span C_{k+1}(F) = [gr_k(F), gr_0(F)].

theorem TauCeti.freeProP.exists_apply_mem_commutator_basisModificationDelta_eq_of_mem_range {p : ℕ} {X : Type u} {m : ℕ} [Fact (Nat.Prime p)] [Finite X] [LinearOrder X] (hm : 1 ≤ m) {ρ : gradedPiece p (freeProP p X) 1} (hρ : Submodule.span (ZMod p) (Set.range fun (i : X) => (degreeOneDeriv p X i) ρ) = ⊤) (hc : ∀ (i : X), ((degreeOneBasis p X).repr ρ) (Sum.inl i) = 0) (x₀ : X) {y : gradedPiece p (freeProP p X) (m + 1)} (hy : y ∈ ((basisModificationDelta p X hm) ρ).range) : ∃ (ω : X → ↥(pLowerCentralSeries p (freeProP p X) m)), ↑(ω x₀) ∈ commutator (freeProP p X) ∧ (((basisModificationDelta p X hm) ρ) fun (i : X) => gradedMk p (freeProP p X) m (ω i)) = y

The pivot-constrained span statement. Let ρ ∈ gr_1(F) have no p-power part and partial derivatives spanning gr_0(F), and let m ≥ 1. Every element of the image of δ_ρ : gr_m(F)^X → gr_{m+1}(F) is δ_ρ(⟦ω⟧) for a family ω : X → λ_m(F) whose component at the prescribed generator x₀ lies in the commutator subgroup of F. For a relator whose exponent vector is supported at x₀, the basis modification x_i ↦ x_i ω_i therefore preserves the exponent vector while moving the relator by the class δ_ρ(⟦ω⟧).