The graded pieces of a subgroup along 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}, and let K ≤ G be a subgroup. The filtration K_k := K ∩ λ_k(G) induced on K has graded pieces K_k ⧸ K_{k+1}, and since K_{k+1} = K_k ∩ λ_{k+1}(G) these inject into gr_k(G). This file works with their images: the graded piece of K in degree k (TauCeti.gradedPieceOf) is the 𝔽_p-subspace gr_k(K) ≤ gr_k(G) of the classes of the elements of K ∩ λ_k(G). When K is normal, gr(K) = ⨁_k gr_k(K) is an ideal of the graded Lie algebra gr(G): it is stable under the p-power operator π and under the bracket with any class of gr(G) (TauCeti.gradedPow_mem_gradedPieceOf, TauCeti.gradedBracket_mem_gradedPieceOf_left, TauCeti.gradedBracket_mem_gradedPieceOf_right). If K contains the commutator subgroup, then gr(K) contains every bracket, so the bracket span C_{k+1}(G) of Graded/BracketSpan.lean lies in gr_{k+1}(K) (TauCeti.gradedBracketSpan_le_gradedPieceOf).

This is the graded Lie algebra gr(X) of the kernel X of a character of a free pro-p group that Labute's classification of Demushkin groups with q = 2 runs on, identified with its image in gr(F).

Main definitions

• TauCeti.gradedPieceOf: the graded piece gr_k(K) ≤ gr_k(G) of a subgroup K.

Main results

• TauCeti.mem_gradedPieceOf_iff: the elements of gr_k(K) are the classes of the elements of K ∩ λ_k(G).
• TauCeti.gradedPow_mem_gradedPieceOf, TauCeti.gradedPowIter_gradedMkZero_mem_gradedPieceOf: π gr_k(K) ≤ gr_{k+1}(K), and π^j of the class of an element of K lies in gr_j(K).
• TauCeti.gradedBracket_mem_gradedPieceOf_left, TauCeti.gradedBracket_mem_gradedPieceOf_right: for K normal, [gr_j(K), gr_k(G)] and [gr_j(G), gr_k(K)] lie in gr_{j+k+1}(K).
• TauCeti.gradedBracket_mem_gradedPieceOf_of_commutator_le, TauCeti.gradedBracketSpan_le_gradedPieceOf: when K contains the commutator subgroup, every bracket lies in gr(K), and C_{k+1}(G) ≤ gr_{k+1}(K).

References

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

def TauCeti.gradedPieceOf (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (K : Subgroup G) (k : ℕ) : Submodule (ZMod p) (gradedPiece p G k)

The graded piece of a subgroup: for K ≤ G, the 𝔽_p-subspace gr_k(K) ≤ gr_k(G) of the classes of the elements of K ∩ λ_k(G), the image of K_k ⧸ K_{k+1} for the induced filtration K_k = K ∩ λ_k(G) of K. Its elements are characterized by TauCeti.mem_gradedPieceOf_iff.

Equations

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

theorem TauCeti.mem_gradedPieceOf_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K : Subgroup G} {k : ℕ} {z : gradedPiece p G k} : z ∈ gradedPieceOf p K k ↔ ∃ (x : ↥(pLowerCentralSeries p G k)), ↑x ∈ K ∧ gradedMk p G k x = z

The elements of gr_k(K) are the classes in gr_k(G) of the elements of K ∩ λ_k(G).

theorem TauCeti.gradedMk_mem_gradedPieceOf {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K : Subgroup G} {k : ℕ} {x : ↥(pLowerCentralSeries p G k)} (hx : ↑x ∈ K) : gradedMk p G k x ∈ gradedPieceOf p K k

The class of an element of K ∩ λ_k(G) lies in gr_k(K).

theorem TauCeti.gradedPieceOf_mono {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K L : Subgroup G} (h : K ≤ L) (k : ℕ) : gradedPieceOf p K k ≤ gradedPieceOf p L k

@[simp]

theorem TauCeti.gradedPieceOf_top {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : gradedPieceOf p ⊤ k = ⊤

theorem TauCeti.gradedPow_mem_gradedPieceOf {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K : Subgroup G} {k : ℕ} {z : gradedPiece p G k} (hz : z ∈ gradedPieceOf p K k) : gradedPow p G k z ∈ gradedPieceOf p K (k + 1)

π preserves the graded pieces of a subgroup: π gr_k(K) ≤ gr_{k+1}(K).

theorem TauCeti.gradedPowIter_gradedMkZero_mem_gradedPieceOf {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K : Subgroup G} {g : G} (hg : g ∈ K) (j : ℕ) : gradedPowIter p G j (gradedMkZero p G g) ∈ gradedPieceOf p K j

The iterated p-power π^j of the class of an element of K lies in gr_j(K).

theorem TauCeti.gradedBracket_mem_gradedPieceOf_left {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K : Subgroup G} [K.Normal] {j k : ℕ} {x : gradedPiece p G j} (hx : x ∈ gradedPieceOf p K j) (y : gradedPiece p G k) : ((gradedBracket p G j k) x) y ∈ gradedPieceOf p K (j + k + 1)

The graded pieces of a normal subgroup form a left ideal: for K normal, [gr_j(K), gr_k(G)] ≤ gr_{j+k+1}(K).

theorem TauCeti.gradedBracket_mem_gradedPieceOf_right {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K : Subgroup G} [K.Normal] {j k : ℕ} (x : gradedPiece p G j) {y : gradedPiece p G k} (hy : y ∈ gradedPieceOf p K k) : ((gradedBracket p G j k) x) y ∈ gradedPieceOf p K (j + k + 1)

The graded pieces of a normal subgroup form a right ideal: for K normal, [gr_j(G), gr_k(K)] ≤ gr_{j+k+1}(K).

theorem TauCeti.gradedPowIterBracket_mem_gradedPieceOf {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K : Subgroup G} (hK : commutator G ≤ K) (m : ℕ) (g h : G) : gradedPowIterBracket p G m g h ∈ gradedPieceOf p K (m + 1)

The iterated p-powers of brackets lie in gr(K) when K contains the commutator subgroup: π^m [ξ_g, ξ_h] ∈ gr_{m+1}(K).

theorem TauCeti.gradedBracket_mem_gradedPieceOf_of_commutator_le {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K : Subgroup G} (hK : commutator G ≤ K) {j k : ℕ} (x : gradedPiece p G j) (y : gradedPiece p G k) : ((gradedBracket p G j k) x) y ∈ gradedPieceOf p K (j + k + 1)

Every bracket lies in gr(K) when K contains the commutator subgroup.

theorem TauCeti.gradedBracketSpan_le_gradedPieceOf {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K : Subgroup G} (hK : commutator G ≤ K) (k : ℕ) : gradedBracketSpan p G k ≤ gradedPieceOf p K (k + 1)

The bracket span lies in gr(K) when K contains the commutator subgroup: C_{k+1}(G) ≤ gr_{k+1}(K).