The bracket span of the graded pieces of the lower p-series

Let G be a topological group with lower p-series λ_k = λ_k(G) and graded pieces gr_k(G) = λ_k ⧸ λ_{k+1}. The bracket span C_{k+1}(G) ≤ gr_{k+1}(G) (TauCeti.gradedBracketSpan) is the ZMod p-submodule spanned by the brackets [x, y] with x ∈ gr_k(G) and y ∈ gr_0(G), that is by the classes of the commutators ⁅a, b⁆ with a ∈ λ_k and b ∈ G (TauCeti.gradedBracketSpan_eq_span); membership in it is eliminated by the induction principle TauCeti.gradedBracketSpan_induction. Every element of it is the class of an element of λ_{k+1} lying in the commutator subgroup (TauCeti.exists_mem_commutator_gradedMk_eq_of_mem_gradedBracketSpan), and the p-power operator π carries C_{k+1}(G) into C_{k+2}(G) (TauCeti.gradedPow_mem_gradedBracketSpan).

One identity on the iterated p-powers π^j x of degree-zero classes accompanies it: the symmetrised bracket [π^{k+1} x, y] + [π^{k+1} y, x] lies in the span of the brackets [c, z] with c ∈ C_{k+1}(G) and z ∈ gr_0(G) (TauCeti.gradedBracket_gradedPowIter_add_swap_mem_map₂); for odd p that sum is zero, and for p = 2 it need not be, which is why the statement is a membership rather than a vanishing. The vanishing [π^j x, x] = 0 that it rests on is TauCeti.gradedBracket_gradedPowIter_self in Graded/Pow.lean.

Finally, when λ_{k+2} is open, gr_{k+1}(G) is the sum of C_{k+1}(G) and the span of the iterated p-powers π^{k+1} x of the degree-zero classes (TauCeti.gradedBracketSpan_sup_span_range_gradedPowIter_eq_top): this is the graded form of λ_{k+1} = closure (λ_kᵖ ⬝ [λ_k, G]), iterated down to degree zero.

For the free pro-p group F of finite rank, the bracket span C_{k+1}(F) is the image of the basis-modification map δ_ρ of every relator class ρ ∈ gr_1(F) without p-power part whose partial derivatives span gr_0(F) (TauCeti.freeProP.range_basisModificationDelta_eq_span_of_repr_inl_eq_zero); the statements here are what the pivot-constrained span statement of the classification of Demushkin groups uses.

Main definitions

• TauCeti.gradedBracketSpan: the bracket span C_{k+1}(G) ≤ gr_{k+1}(G).

Main results

• TauCeti.gradedBracketSpan_eq_span and TauCeti.gradedBracketSpan_induction: the bracket span as a span, and induction on its elements.
• TauCeti.exists_mem_commutator_gradedMk_eq_of_mem_gradedBracketSpan: every element of C_{k+1}(G) is the class of an element of λ_{k+1} in the commutator subgroup.
• TauCeti.gradedPow_mem_gradedBracketSpan: π C_{k+1}(G) ≤ C_{k+2}(G).
• TauCeti.gradedBracket_gradedPowIter_add_swap_mem_map₂: [π^{k+1} x, y] + [π^{k+1} y, x] ∈ [C_{k+1}(G), gr_0(G)].
• TauCeti.gradedBracketSpan_sup_span_range_gradedPowIter_eq_top: gr_{k+1}(G) = C_{k+1}(G) + span {π^{k+1} x} when λ_{k+2} is open.

References

• J. Labute, Classification of Demushkin groups, Canadian J. Math. 19 (1967), §1, Propositions 1 and 2, and §3.

The bracket span

def TauCeti.gradedBracketSpan (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : Submodule (ZMod p) (gradedPiece p G (k + 1))

The bracket span C_{k+1}(G) ≤ gr_{k+1}(G): the ZMod p-submodule spanned by the brackets [x, y] with x ∈ gr_k(G) and y ∈ gr_0(G), that is by the classes of the commutators ⁅a, b⁆ with a ∈ λ_k(G) and b ∈ G; it is the bilinear image Submodule.map₂ of the bracket TauCeti.gradedBracketLinear on the whole of gr_k(G) × gr_0(G) (TauCeti.gradedBracketSpan_eq_span restates it as a span). Its elements are classes of elements of the commutator subgroup (TauCeti.exists_mem_commutator_gradedMk_eq_of_mem_gradedBracketSpan), and π carries it into C_{k+2}(G) (TauCeti.gradedPow_mem_gradedBracketSpan).

Equations

• TauCeti.gradedBracketSpan p G k = Submodule.map₂ (TauCeti.gradedBracketLinear p G k 0) ⊤ ⊤

@[simp]

theorem TauCeti.gradedBracket_mem_gradedBracketSpan {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (x : gradedPiece p G k) (y : gradedPiece p G 0) : ((gradedBracket p G k 0) x) y ∈ gradedBracketSpan p G k

A bracket [x, y] with y of degree zero lies in the bracket span.

theorem TauCeti.gradedBracketSpan_eq_span {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : gradedBracketSpan p G k = Submodule.span (ZMod p) (Set.range fun (xy : gradedPiece p G k × gradedPiece p G 0) => ((gradedBracket p G k 0) xy.1) xy.2)

The bracket span as a span: C_{k+1}(G) is the span of the brackets [x, y] with x ∈ gr_k(G) and y ∈ gr_0(G).

theorem TauCeti.gradedBracketSpan_induction {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {motive : (z : gradedPiece p G (k + 1)) → z ∈ gradedBracketSpan p G k → Prop} (bracket : ∀ (x : gradedPiece p G k) (y : gradedPiece p G 0), motive (((gradedBracket p G k 0) x) y) ⋯) (zero : motive 0 ⋯) (add : ∀ (x y : gradedPiece p G (k + 1)) (hx : x ∈ gradedBracketSpan p G k) (hy : y ∈ gradedBracketSpan p G k), motive x hx → motive y hy → motive (x + y) ⋯) (smul : ∀ (c : ZMod p) (x : gradedPiece p G (k + 1)) (hx : x ∈ gradedBracketSpan p G k), motive x hx → motive (c • x) ⋯) {z : gradedPiece p G (k + 1)} (hz : z ∈ gradedBracketSpan p G k) : motive z hz

Induction on the bracket span: a predicate that holds on the brackets [x, y] with y of degree zero and on 0, and is closed under addition and scalar multiplication, holds on all of C_{k+1}(G).

@[simp]

theorem TauCeti.gradedBracketSpan_le_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {W : Submodule (ZMod p) (gradedPiece p G (k + 1))} : gradedBracketSpan p G k ≤ W ↔ ∀ (x : gradedPiece p G k) (y : gradedPiece p G 0), ((gradedBracket p G k 0) x) y ∈ W

A submodule contains the bracket span if and only if it contains every bracket [x, y] with y of degree zero.

theorem TauCeti.exists_mem_commutator_gradedMk_eq_of_mem_gradedBracketSpan {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {y : gradedPiece p G (k + 1)} (hy : y ∈ gradedBracketSpan p G k) : ∃ (z : ↥(pLowerCentralSeries p G (k + 1))), ↑z ∈ commutator G ∧ gradedMk p G (k + 1) z = y

Elements of the bracket span are classes of commutators: every element of C_{k+1}(G) is the class of an element of λ_{k+1}(G) lying in the commutator subgroup of G.

theorem TauCeti.gradedPow_mem_gradedBracketSpan {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {x : gradedPiece p G (k + 1)} (hx : x ∈ gradedBracketSpan p G k) : gradedPow p G (k + 1) x ∈ gradedBracketSpan p G (k + 1)

π carries the bracket span into the next bracket span: π C_{k+1}(G) ≤ C_{k+2}(G). Away from degree zero π [x, y] = [π x, y], and in degree zero π [x, y] = [π x, y] + (p choose 2) • [[x, y], x] is again a sum of brackets.

theorem TauCeti.gradedPow_mem_map₂_gradedBracketLinear_gradedBracketSpan {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {w : gradedPiece p G (k + 1 + 1)} (hw : w ∈ Submodule.map₂ (gradedBracketLinear p G (k + 1) 0) (gradedBracketSpan p G k) ⊤) : gradedPow p G (k + 1 + 1) w ∈ Submodule.map₂ (gradedBracketLinear p G (k + 1 + 1) 0) (gradedBracketSpan p G (k + 1)) ⊤

π carries brackets with the bracket span into brackets with the next bracket span: if w is a sum of brackets [c, z] with c ∈ C_{k+1}(G) and z ∈ gr_0(G), then π w is a sum of brackets [c', z] with c' ∈ C_{k+2}(G).

theorem TauCeti.gradedBracket_gradedPowIter_add_swap_mem_map₂ {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) (x y : gradedPiece p G 0) : ((gradedBracket p G (k + 1) 0) (gradedPowIter p G (k + 1) x)) y + ((gradedBracket p G (k + 1) 0) (gradedPowIter p G (k + 1) y)) x ∈ Submodule.map₂ (gradedBracketLinear p G (k + 1) 0) (gradedBracketSpan p G k) ⊤

The symmetrised bracket of iterated p-powers: for x, y ∈ gr_0(G), [π^{k+1} x, y] + [π^{k+1} y, x] is a sum of brackets [c, z] with c ∈ C_{k+1}(G) and z ∈ gr_0(G). For odd p the sum is zero, and for p = 2 it is the trace of the degree-zero defect of π against the bracket.

The bracket span and the iterated p-powers span the graded piece

theorem TauCeti.gradedBracketSpan_sup_span_range_gradedPowIter_eq_top {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (h : IsOpen ↑(pLowerCentralSeries p G (k + 1 + 1))) : gradedBracketSpan p G k ⊔ Submodule.span (ZMod p) (Set.range (gradedPowIter p G (k + 1))) = ⊤

The bracket span and the iterated p-powers span the graded piece: when λ_{k+2} is open, gr_{k+1}(G) = C_{k+1}(G) + span {π^{k+1} x | x ∈ gr_0(G)}. This is the graded form of λ_{k+1} = closure (λ_kᵖ ⬝ [λ_k, G]) iterated down to degree zero.