The lower p-central series of a subgroup

For a subgroup S of a group G and a natural number p, the lower p-central series of S, computed in G, is the descending chain

• λ₀ = S,
• λₙ₊₁ = ⟨x ^ p | x ∈ λₙ⟩ ⊔ ⁅λₙ, S⁆.

Each factor λₙ ⧸ λₙ₊₁ is central in S ⧸ λₙ₊₁ and killed by p, so for a prime p the factors are elementary abelian p-groups. The series refines Mathlib's Subgroup.lowerCentralSeries by the p-th powers and is defined in the same relative way, with the series of G itself being the case S = ⊤. Its purpose is to filter a finite p-group in finitely many steps by subgroups that are normal in every group in which the p-group is normal, with elementary abelian factors: this is the reduction that passes from embedding problems with elementary abelian kernel to embedding problems with p-group kernel, and it is the abstract shadow of the lower p-series of a pro-p group.

Main results

• Subgroup.pLowerCentralSeries_succ_le_iff: the successor term is the least subgroup containing the p-th powers of the current term and its commutators with S.
• Subgroup.pLowerCentralSeries_map: the series is natural for group homomorphisms.
• Subgroup.pLowerCentralSeries_mono: the series is monotone in the subgroup.
• Subgroup.pLowerCentralSeries_zero_left: at p = 0 the series is the lower central series.
• Subgroup.normalizer_le_normalizer_pLowerCentralSeries: whatever normalises S normalises every term; in particular the terms are normal when S is, and characteristic when S is.
• IsPGroup.exists_pLowerCentralSeries_eq_bot: the series of a finite p-subgroup reaches ⊥.
• Subgroup.exists_pLowerCentral_filtration_of_isPGroup: the packaged filtration of a finite normal p-subgroup by normal subgroups with elementary abelian factors.

References

• J. D. Dixon, M. P. F. du Sautoy, A. Mann, D. Segal, Analytic pro-p groups, §1.2, where the series is written Pᵢ(G).
• L. Ribes, P. Zalesskii, Profinite Groups, §2.8.

def Subgroup.pLowerCentralSeries {G : Type u_1} [Group G] (p : ℕ) (S : Subgroup G) : ℕ → Subgroup G

The lower p-central series of a subgroup S of G, computed in the ambient group G: λ₀ = S, and λₙ₊₁ is generated by the p-th powers of the elements of λₙ together with the commutators ⁅λₙ, S⁆. The lower p-central series of G itself is the case S = ⊤.

Equations

• Subgroup.pLowerCentralSeries p S 0 = S
• Subgroup.pLowerCentralSeries p S n.succ = Subgroup.closure ((fun (x : G) => x ^ p) '' ↑(Subgroup.pLowerCentralSeries p S n)) ⊔ ⁅Subgroup.pLowerCentralSeries p S n, S⁆

@[simp]

theorem Subgroup.pLowerCentralSeries_zero {G : Type u_1} [Group G] (p : ℕ) (S : Subgroup G) : pLowerCentralSeries p S 0 = S

theorem Subgroup.pLowerCentralSeries_succ {G : Type u_1} [Group G] (p : ℕ) (S : Subgroup G) (n : ℕ) : pLowerCentralSeries p S (n + 1) = closure ((fun (x : G) => x ^ p) '' ↑(pLowerCentralSeries p S n)) ⊔ ⁅pLowerCentralSeries p S n, S⁆

The recursion defining the successor term of the lower p-central series.

theorem Subgroup.pow_mem_pLowerCentralSeries_succ {G : Type u_1} [Group G] (p : ℕ) (S : Subgroup G) {n : ℕ} {x : G} (hx : x ∈ pLowerCentralSeries p S n) : x ^ p ∈ pLowerCentralSeries p S (n + 1)

The p-th power of an element of λₙ lies in λₙ₊₁.

theorem Subgroup.commutator_mem_pLowerCentralSeries_succ {G : Type u_1} [Group G] (p : ℕ) (S : Subgroup G) {n : ℕ} {x y : G} (hx : x ∈ pLowerCentralSeries p S n) (hy : y ∈ S) : ⁅x, y⁆ ∈ pLowerCentralSeries p S (n + 1)

The commutator of an element of λₙ with an element of S lies in λₙ₊₁.

theorem Subgroup.pLowerCentralSeries_succ_le_iff {G : Type u_1} [Group G] {p : ℕ} {S : Subgroup G} {n : ℕ} {H : Subgroup G} : pLowerCentralSeries p S (n + 1) ≤ H ↔ (∀ x ∈ pLowerCentralSeries p S n, x ^ p ∈ H) ∧ ∀ x ∈ pLowerCentralSeries p S n, ∀ y ∈ S, ⁅x, y⁆ ∈ H

The successor term λₙ₊₁ is the least subgroup containing the p-th powers of the elements of λₙ and the commutators of λₙ with S.

theorem Subgroup.pLowerCentralSeries_mono {G : Type u_1} [Group G] (p n : ℕ) : Monotone fun (S : Subgroup G) => pLowerCentralSeries p S n

The lower p-central series is monotone in the subgroup: S ≤ T gives λₙ(S) ≤ λₙ(T).

@[simp]

theorem Subgroup.pLowerCentralSeries_map {G : Type u_1} [Group G] (p : ℕ) (S : Subgroup G) {G' : Type u_2} [Group G'] (f : G →* G') (n : ℕ) : map f (pLowerCentralSeries p S n) = pLowerCentralSeries p (map f S) n

The lower p-central series is natural: a homomorphism carries the series of S onto the series of the image of S.

theorem Subgroup.normalizer_le_normalizer_pLowerCentralSeries {G : Type u_1} [Group G] (p : ℕ) (S : Subgroup G) (n : ℕ) : normalizer ↑S ≤ normalizer ↑(pLowerCentralSeries p S n)

An element normalising S normalises every term of the lower p-central series of S.

theorem Subgroup.self_le_normalizer_pLowerCentralSeries {G : Type u_1} [Group G] (p : ℕ) (S : Subgroup G) (n : ℕ) : S ≤ normalizer ↑(pLowerCentralSeries p S n)

S normalises every term of its own lower p-central series.

theorem Subgroup.pLowerCentralSeries_succ_le {G : Type u_1} [Group G] (p : ℕ) (S : Subgroup G) (n : ℕ) : pLowerCentralSeries p S (n + 1) ≤ pLowerCentralSeries p S n

The lower p-central series is descending: λₙ₊₁ ≤ λₙ.

theorem Subgroup.pLowerCentralSeries_antitone {G : Type u_1} [Group G] (p : ℕ) (S : Subgroup G) : Antitone (pLowerCentralSeries p S)

The lower p-central series is antitone in the index.

theorem Subgroup.pLowerCentralSeries_le {G : Type u_1} [Group G] (p : ℕ) (S : Subgroup G) (n : ℕ) : pLowerCentralSeries p S n ≤ S

Every term of the lower p-central series of S is contained in S.

theorem Subgroup.commutator_pLowerCentralSeries_le_succ {G : Type u_1} [Group G] (p : ℕ) (S : Subgroup G) (n : ℕ) : ⁅pLowerCentralSeries p S n, pLowerCentralSeries p S n⁆ ≤ pLowerCentralSeries p S (n + 1)

Consecutive factors of the lower p-central series are abelian: ⁅λₙ, λₙ⁆ ≤ λₙ₊₁.

instance Subgroup.pLowerCentralSeries_normal {G : Type u_1} [Group G] (p : ℕ) (S : Subgroup G) [S.Normal] (n : ℕ) : (pLowerCentralSeries p S n).Normal

The terms of the lower p-central series of a normal subgroup are normal.

theorem Subgroup.mk_pow_eq_one_of_mem_pLowerCentralSeries {G : Type u_1} [Group G] (p : ℕ) (S : Subgroup G) [S.Normal] {n : ℕ} {x : G} (hx : x ∈ pLowerCentralSeries p S n) : ↑x ^ p = 1

In the quotient by λₙ₊₁, the class of an element of λₙ is killed by p.

theorem Subgroup.commute_mk_of_mem_pLowerCentralSeries {G : Type u_1} [Group G] (p : ℕ) (S : Subgroup G) [S.Normal] {n : ℕ} {x y : G} (hx : x ∈ pLowerCentralSeries p S n) (hy : y ∈ pLowerCentralSeries p S n) : Commute ↑x ↑y

In the quotient by λₙ₊₁, the classes of two elements of λₙ commute.

instance Subgroup.pLowerCentralSeries_characteristic {G : Type u_1} [Group G] (p : ℕ) (S : Subgroup G) [S.Characteristic] (n : ℕ) : (pLowerCentralSeries p S n).Characteristic

The terms of the lower p-central series of a characteristic subgroup are characteristic.

theorem Subgroup.lowerCentralSeries_le_pLowerCentralSeries {G : Type u_1} [Group G] (p : ℕ) (S : Subgroup G) (n : ℕ) : S.lowerCentralSeries n ≤ pLowerCentralSeries p S n

The lower p-central series refines the lower central series.

@[simp]

theorem Subgroup.pLowerCentralSeries_zero_left {G : Type u_1} [Group G] (S : Subgroup G) (n : ℕ) : pLowerCentralSeries 0 S n = S.lowerCentralSeries n

At p = 0 the lower p-central series is the lower central series: the 0-th powers are trivial, so only the commutators remain.

theorem Subgroup.top_pLowerCentralSeries_one {G : Type u_1} [Group G] (p : ℕ) : pLowerCentralSeries p ⊤ 1 = closure (Set.range fun (g : G) => g ^ p) ⊔ _root_.commutator G

The first term of the lower p-central series of G is generated by the p-th powers and the commutators.

theorem Subgroup.top_pLowerCentralSeries_eq_range_powMonoidHom {G : Type u_2} [CommGroup G] (p n : ℕ) : pLowerCentralSeries p ⊤ n = (powMonoidHom (p ^ n)).range

The lower p-central series of a commutative group is the chain of subgroups of p ^ n-th powers: the commutators vanish, so λₙ₊₁ is generated by the p-th powers of λₙ.

theorem IsPGroup.exists_pLowerCentralSeries_eq_bot {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [Group G] {S : Subgroup G} [Finite ↥S] (hS : IsPGroup p ↥S) : ∃ (n : ℕ), Subgroup.pLowerCentralSeries p S n = ⊥

The lower p-central series of a finite p-group reaches the trivial subgroup. For a finite p-subgroup S of any group G, some term of S.pLowerCentralSeries p is ⊥.

theorem Subgroup.exists_pLowerCentral_filtration_of_isPGroup {p : ℕ} [Fact (Nat.Prime p)] {E : Type u_1} [Group E] (N : Subgroup E) [N.Normal] [Finite ↥N] (hN : IsPGroup p ↥N) : ∃ (m : ℕ) (lam : ℕ → Subgroup E), lam 0 = N ∧ lam m = ⊥ ∧ (∀ (k : ℕ), lam (k + 1) ≤ lam k) ∧ (∀ (k : ℕ), (lam k).Normal) ∧ (∀ (k : ℕ), ∀ x ∈ lam k, x ^ p ∈ lam (k + 1)) ∧ ∀ (k : ℕ), ∀ x ∈ lam k, ∀ y ∈ N, ⁅x, y⁆ ∈ lam (k + 1)

The lower p-central filtration of a finite normal p-subgroup. A finite normal p-subgroup N of a group E carries a finite descending chain of subgroups of E, starting at N and ending at ⊥, each normal in E, along which p-th powers and commutators with N drop one step. So every factor is an elementary abelian p-group on which E acts by conjugation. The chain is the lower p-central series Subgroup.pLowerCentralSeries p N.