Spanning the degree-one graded piece of the lower p-series

Let G be a topological group whose second lower p-series term λ_2 is open, and let s be a subset that topologically generates G. For p ≠ 0, the degree-zero classes of the elements of s span gr_0(G) = G ⧸ λ_1 over ZMod p, and the degree-one piece gr_1(G) = λ_1 ⧸ λ_2 is spanned by the p-power classes π g' and the brackets [g', h'] for g, h ∈ s. The generating set s is arbitrary: it need not be finite, and only the closure of the subgroup it generates matters. The degree-zero statement holds for every p and needs only that λ_1 is open. Both statements bound gr_0(G) and gr_1(G) in terms of the generators, which is the first step in computing the graded pieces of a group given by generators.

In every degree, when λ_{k+2} is open, gr_{k+1}(G) = λ_{k+1} ⧸ λ_{k+2} is spanned by the p-powers π x of the classes x ∈ gr_k(G) and the brackets [x, y] of such a class with a degree-zero class y ∈ gr_0(G): this is the graded form of λ_{k+1} = closure (λ_kᵖ ⬝ [λ_k, G]), and it is the induction step for computing the graded pieces degree by degree.

For a linearly ordered index type the generators are packaged as TauCeti.degreeOneFamily: the p-power classes π y'_i together with the brackets [y'_i, y'_j] for i < j. For a free pro-p group on a finite linearly ordered set this family is a basis, which is proved in TauCeti.Topology.Algebra.Group.Profinite.Free.Graded.

The openness hypothesis holds in a topologically finitely generated profinite group (TauCeti.IsTopologicallyFinitelyGenerated.isOpen_pLowerCentralSeries).

Main definitions

• TauCeti.degreeOneFamily: the degree-one family of a family y : ι → G, indexed by ι ⊕ {ij : ι × ι // ij.1 < ij.2}.

Main results

• TauCeti.span_gradedMkZero_image_eq_top: the degree-zero classes of a topological generating set span gr_0(G), when λ_1 is open.
• TauCeti.span_gradedPow_gradedMkZero_union_gradedBracket_eq_top: the p-power classes and brackets of a topological generating set span gr_1(G), when λ_2 is open.
• TauCeti.linearMap_ext_gradedPiece_one: linear maps out of gr_1(G) are determined by their values on those p-power classes and brackets.
• TauCeti.span_range_degreeOneFamily_eq_top: the ordered form of the previous statement.
• TauCeti.span_range_gradedPow_union_range_gradedBracket_eq_top, TauCeti.eq_top_of_forall_gradedPow_mem_of_forall_gradedBracket_mem: in every degree, the p-powers π x of x ∈ gr_k(G) and the brackets [x, y] with y ∈ gr_0(G) span gr_{k+1}(G), when λ_{k+2} is open.

References

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

Degree zero

theorem TauCeti.span_gradedMkZero_image_eq_top {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (h₁ : IsOpen ↑(pLowerCentralSeries p G 1)) {s : Set G} (hs : (Subgroup.closure s).topologicalClosure = ⊤) : Submodule.span (ZMod p) (gradedMkZero p G '' s) = ⊤

The degree-zero classes of a topological generating set span gr_0(G), when λ_1 is open: the image of a dense subgroup in the discrete quotient G ⧸ λ_1 is everything.

Degree one

theorem TauCeti.gradedBracket_mem_of_mem_span {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (W : Submodule (ZMod p) (gradedPiece p G 1)) {S : Set (gradedPiece p G 0)} (hS : ∀ x ∈ S, ∀ y ∈ S, ((gradedBracket p G 0 0) x) y ∈ W) {x y : gradedPiece p G 0} (hx : x ∈ Submodule.span (ZMod p) S) (hy : y ∈ Submodule.span (ZMod p) S) : ((gradedBracket p G 0 0) x) y ∈ W

The bracket of two elements of a span lies in any submodule containing the brackets of the generators: the bracket is ZMod p-bilinear.

theorem TauCeti.gradedPow_mem_of_mem_span {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (W : Submodule (ZMod p) (gradedPiece p G 1)) {S : Set (gradedPiece p G 0)} (hpow : ∀ x ∈ S, gradedPow p G 0 x ∈ W) (hS : ∀ x ∈ S, ∀ y ∈ S, ((gradedBracket p G 0 0) x) y ∈ W) {x : gradedPiece p G 0} (hx : x ∈ Submodule.span (ZMod p) S) : gradedPow p G 0 x ∈ W

The p-power of an element of a span lies in any submodule containing the p-powers and the brackets of the generators: the degree-zero defect of additivity of π is a bracket.

theorem TauCeti.span_gradedPow_gradedMkZero_union_gradedBracket_eq_top {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (h₂ : IsOpen ↑(pLowerCentralSeries p G 2)) {s : Set G} (hs : (Subgroup.closure s).topologicalClosure = ⊤) : Submodule.span (ZMod p) ((fun (g : G) => gradedPow p G 0 (gradedMkZero p G g)) '' s ∪ (fun (gh : G × G) => ((gradedBracket p G 0 0) (gradedMkZero p G gh.1)) (gradedMkZero p G gh.2)) '' s ×ˢ s) = ⊤

The p-power classes and the brackets of a topological generating set span gr_1(G), when λ_2 is open.

theorem TauCeti.linearMap_ext_gradedPiece_one {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type u_1} [AddCommMonoid M] [Module (ZMod p) M] (h₂ : IsOpen ↑(pLowerCentralSeries p G 2)) {s : Set G} (hs : (Subgroup.closure s).topologicalClosure = ⊤) {f g : gradedPiece p G 1 →ₗ[ZMod p] M} (hpow : ∀ x ∈ s, f (gradedPow p G 0 (gradedMkZero p G x)) = g (gradedPow p G 0 (gradedMkZero p G x))) (hbr : ∀ x ∈ s, ∀ y ∈ s, f (((gradedBracket p G 0 0) (gradedMkZero p G x)) (gradedMkZero p G y)) = g (((gradedBracket p G 0 0) (gradedMkZero p G x)) (gradedMkZero p G y))) : f = g

Linear maps out of gr_1(G) are determined on a topological generating set, when λ_2 is open: two ZMod p-linear maps agreeing on the p-power classes π ⟦x⟧ and the brackets [⟦x⟧, ⟦y⟧] of the elements x, y of a topological generating set are equal.

Higher degrees

theorem TauCeti.span_range_gradedPow_union_range_gradedBracket_eq_top {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (h : IsOpen ↑(pLowerCentralSeries p G (k + 1 + 1))) : Submodule.span (ZMod p) (Set.range (gradedPow p G k) ∪ Set.range fun (xy : gradedPiece p G k × gradedPiece p G 0) => ((gradedBracket p G k 0) xy.1) xy.2) = ⊤

The p-powers and the brackets with degree-zero classes span the next graded piece: when λ_{k+2} is open, gr_{k+1}(G) is spanned over ZMod p by the classes π x for x ∈ gr_k(G) and the brackets [x, y] for x ∈ gr_k(G) and y ∈ gr_0(G). This is the graded form of λ_{k+1} = closure (λ_kᵖ ⬝ [λ_k, G]).

theorem TauCeti.eq_top_of_forall_gradedPow_mem_of_forall_gradedBracket_mem {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {W : Submodule (ZMod p) (gradedPiece p G (k + 1))} (h : IsOpen ↑(pLowerCentralSeries p G (k + 1 + 1))) (hpow : ∀ (x : gradedPiece p G k), gradedPow p G k x ∈ W) (hbracket : ∀ (x : gradedPiece p G k) (y : gradedPiece p G 0), ((gradedBracket p G k 0) x) y ∈ W) : W = ⊤

A submodule of gr_{k+1}(G) containing all p-powers π x and all brackets [x, y] with y of degree zero is everything, when λ_{k+2} is open.

theorem TauCeti.forall_gradedPow_mem_of_span_eq_top {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (hk : 1 ≤ k) {S : Set (gradedPiece p G k)} (hS : Submodule.span (ZMod p) S = ⊤) {W : Submodule (ZMod p) (gradedPiece p G (k + 1))} (hpow : ∀ x ∈ S, gradedPow p G k x ∈ W) (x : gradedPiece p G k) : gradedPow p G k x ∈ W

It suffices to check π on a spanning set above degree zero: if S spans gr_k(G) and the p-power of every element of S belongs to W, then the p-power of every element of gr_k(G) belongs to W.

The degree-one family of an ordered family

def TauCeti.degreeOneFamily (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {ι : Type u_1} [LT ι] (y : ι → G) : ι ⊕ { ij : ι × ι // ij.1 < ij.2 } → gradedPiece p G 1

The degree-one family of a family y : ι → G indexed by a linearly ordered type: the p-power classes π y'_i and the brackets [y'_i, y'_j] for i < j, in gr_1(G). When y topologically generates G and λ_2 is open it spans gr_1(G) (TauCeti.span_range_degreeOneFamily_eq_top); for the canonical generators of a free pro-p group on a finite linearly ordered type it is a basis.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.degreeOneFamily_inl {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {ι : Type u_1} [LT ι] (y : ι → G) (i : ι) : degreeOneFamily p y (Sum.inl i) = gradedPow p G 0 (gradedMkZero p G (y i))

@[simp]

theorem TauCeti.degreeOneFamily_inr {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {ι : Type u_1} [LT ι] (y : ι → G) (ij : { ij : ι × ι // ij.1 < ij.2 }) : degreeOneFamily p y (Sum.inr ij) = ((gradedBracket p G 0 0) (gradedMkZero p G (y (↑ij).1))) (gradedMkZero p G (y (↑ij).2))

@[simp]

theorem TauCeti.gradedMap_degreeOneFamily {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {ι : Type u_1} [LT ι] (y : ι → G) {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (k : ι ⊕ { ij : ι × ι // ij.1 < ij.2 }) : (gradedMap p f hf 1) (degreeOneFamily p y k) = degreeOneFamily p (⇑f ∘ y) k

Naturality of the degree-one family: a continuous homomorphism carries the degree-one family of y to the degree-one family of f ∘ y.

theorem TauCeti.span_range_degreeOneFamily_eq_top {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {ι : Type u_1} [LinearOrder ι] {y : ι → G} (h₂ : IsOpen ↑(pLowerCentralSeries p G 2)) (hy : (Subgroup.closure (Set.range y)).topologicalClosure = ⊤) : Submodule.span (ZMod p) (Set.range (degreeOneFamily p y)) = ⊤

The degree-one family of a topological generating family spans gr_1(G), when λ_2 is open: the ordered form of TauCeti.span_gradedPow_gradedMkZero_union_gradedBracket_eq_top, using that the bracket is alternating and skew-symmetric.