The lower p-series of a topological group

The lower p-series (descending p-central series) of a topological group G is the sequence of closed normal subgroups

λ₀ = G,   λ_{k+1} = closure (λ_kᵖ ⬝ [λ_k, G]),

where the right-hand side is the topological closure of the subgroup generated by the p-th powers of elements of λ_k and the commutators of elements of λ_k with elements of G. The indexing is 0-based, as for Mathlib's lowerCentralSeries, so that λ_1 is the topological closure of Gᵖ [G, G]. One step of the recursion is TauCeti.pLowerCentralStep, whose characteristic property TauCeti.pLowerCentralStep_le_iff characterizes containment in a closed subgroup.

That step is a special case of the two-argument verbal step TauCeti.pVerbalStep p H K = closure (Hᵖ ⬝ [H, K]), the closed subgroup generated by the values of the words x ^ p on H and ⁅x, y⁆ on H × K: the lower p-series step is the case K = ⊤, and the case K = H is the step of the Frattini series (TauCeti.Topology.Algebra.Group.FrattiniSeries). Closedness, monotonicity, normality, the characteristic property and the behaviour under continuous homomorphisms are proved once for the verbal step and specialized to each.

The series is descending, each term is closed and normal, and its successive quotients are central and killed by p: ⁅λ_k, G⁆ ≤ λ_{k+1} and x ^ p ∈ λ_{k+1} for x ∈ λ_k. The main theorem is the degree-raising law ⁅λ_j, λ_k⁆ ≤ λ_{j+k+1}, which lets the group commutator induce a bracket λ_j ⧸ λ_{j+1} × λ_k ⧸ λ_{k+1} → λ_{j+k+1} ⧸ λ_{j+k+2} on the graded pieces. Continuous homomorphisms carry λ_k into λ_k, continuous closed surjections (for instance from a compact group onto a Hausdorff group) carry it onto λ_k, and continuous isomorphisms match the two series term by term. Each λ_k is the topological closure of the corresponding term of the abstract lower p-central series Subgroup.pLowerCentralSeries p ⊤ of the underlying group, so on a discrete group the two series agree.

Nothing here assumes p prime or G profinite. For a profinite G and a prime p, λ_1 is the pro-p Frattini subgroup and, when G is topologically finitely generated, every λ_k is open; see TauCeti.Topology.Algebra.Group.Profinite.ProP.LowerCentralSeries.

Main definitions

• TauCeti.pVerbalStep: the verbal step H, K ↦ closure (Hᵖ ⬝ [H, K]), of which both the lower p-series step and the Frattini series step are special cases.
• TauCeti.pLowerCentralStep: one step H ↦ closure (Hᵖ ⬝ [H, G]) of the recursion.
• TauCeti.pLowerCentralSeries: the lower p-series λ_k.

Main results

• TauCeti.pVerbalStep_le_iff, TauCeti.pLowerCentralStep_le_iff: a closed subgroup contains pVerbalStep p H K exactly when it contains the p-th powers of H and the commutators ⁅H, K⁆, and pLowerCentralStep p H exactly when it contains the p-th powers of H and the commutators ⁅H, G⁆.
• TauCeti.normal_of_pLowerCentralStep_le_of_le: a subgroup between pLowerCentralStep p R and R is normal.
• TauCeti.instIsMulCommutativeQuotientPLowerCentralStep, TauCeti.exponent_quotient_pLowerCentralStep_subgroupOf_dvd, TauCeti.isPGroup_quotient_pLowerCentralStep_subgroupOf: N ⧸ Nᵖ[N, G] is commutative and killed by p.
• TauCeti.mk_conjNormal_eq: conjugation by G acts trivially on N ⧸ Nᵖ[N, G].
• TauCeti.pLowerCentralStep_subgroupOf_le_ker_iff: a homomorphism on a closed normal subgroup R with closed kernel kills pLowerCentralStep p R exactly when it kills p-th powers and is invariant under conjugation by G.
• TauCeti.pLowerCentralSeries_antitone, TauCeti.isClosed_pLowerCentralSeries, TauCeti.pLowerCentralSeries_normal: the series is descending, closed and normal.
• TauCeti.pow_mem_pLowerCentralSeries, TauCeti.commutator_pLowerCentralSeries_top_le, TauCeti.map_mk'_pLowerCentralSeries_le_center: λ_k ⧸ λ_{k+1} is central in G ⧸ λ_{k+1} and killed by p.
• TauCeti.commutator_pLowerCentralSeries_le, TauCeti.commutator_mem_pLowerCentralSeries: the degree-raising law ⁅λ_j, λ_k⁆ ≤ λ_{j+k+1}.
• MonoidHom.map_pLowerCentralSeries_le, MonoidHom.map_pLowerCentralSeries_eq_of_surjective, ContinuousMulEquiv.map_pLowerCentralSeries_eq: functoriality of the series.
• TauCeti.isTopCharacteristic_pLowerCentralSeries: every term is topologically characteristic.
• TauCeti.pLowerCentralSeries_eq_topologicalClosure, TauCeti.pLowerCentralSeries_eq_of_discreteTopology: comparison with the abstract lower p-central series of the underlying group.
• TauCeti.top_pLowerCentralSeries_multiplicative_zmod_pow_eq_bot, MulEquiv.pLowerCentralSeries_eq_bot_multiplicative_zmod_pow: the cyclic group ℤ/pⁿ, and any discrete group isomorphic to it, has p-class at most n.

References

• J. Labute, Classification of Demushkin groups, Canadian J. Math. 19 (1967), §1.
• L. Ribes and P. Zalesskii, Profinite Groups, Section 2.8.
• J. D. Dixon, M. P. F. du Sautoy, A. Mann and D. Segal, Analytic pro-p groups, Section 1.2.

The verbal step

def TauCeti.pVerbalStep (p : ℕ) {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H K : Subgroup G) : Subgroup G

The p-verbal step H, K ↦ closure (Hᵖ ⬝ [H, K]): the topological closure of the subgroup generated by the values of the words x ^ p on H and ⁅x, y⁆ on H × K. Taking K = ⊤ gives one step of the lower p-series (TauCeti.pLowerCentralStep) and taking K = H one step of the Frattini series (TauCeti.proPFrattiniStep). Its characteristic property is TauCeti.pVerbalStep_le_iff.

Equations

• TauCeti.pVerbalStep p H K = (Subgroup.closure ((fun (x : G) => x ^ p) '' ↑H) ⊔ ⁅H, K⁆).topologicalClosure

theorem TauCeti.pVerbalStep_def (p : ℕ) {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H K : Subgroup G) : pVerbalStep p H K = (Subgroup.closure ((fun (x : G) => x ^ p) '' ↑H) ⊔ ⁅H, K⁆).topologicalClosure

The defining equation pVerbalStep p H K = closure (Hᵖ ⬝ [H, K]), with topological closure, expresses the verbal step in terms of powers and commutators.

theorem TauCeti.isClosed_pVerbalStep {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H K : Subgroup G) : IsClosed ↑(pVerbalStep p H K)

The verbal step is a closed subgroup.

theorem TauCeti.pow_mem_pVerbalStep {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H K : Subgroup G} {x : G} (hx : x ∈ H) : x ^ p ∈ pVerbalStep p H K

The p-th power of an element of H lies in pVerbalStep p H K.

theorem TauCeti.commutator_le_pVerbalStep {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H K : Subgroup G) : ⁅H, K⁆ ≤ pVerbalStep p H K

The commutators ⁅H, K⁆ lie in pVerbalStep p H K.

theorem TauCeti.pVerbalStep_le_iff {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H K L : Subgroup G} (hL : IsClosed ↑L) : pVerbalStep p H K ≤ L ↔ (∀ x ∈ H, x ^ p ∈ L) ∧ ⁅H, K⁆ ≤ L

The characteristic property of the verbal step. A closed subgroup contains pVerbalStep p H K exactly when it contains the p-th powers of the elements of H and the commutators ⁅H, K⁆.

theorem TauCeti.pVerbalStep_mono {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H K H' K' : Subgroup G} (hH : H ≤ H') (hK : K ≤ K') : pVerbalStep p H K ≤ pVerbalStep p H' K'

The verbal step is monotone in both arguments.

instance TauCeti.pVerbalStep_normal {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H K : Subgroup G) [H.Normal] [K.Normal] : (pVerbalStep p H K).Normal

The verbal step of two normal subgroups is normal.

theorem MonoidHom.map_pVerbalStep_le {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (K L : Subgroup G) : Subgroup.map f (TauCeti.pVerbalStep p K L) ≤ TauCeti.pVerbalStep p (Subgroup.map f K) (Subgroup.map f L)

A continuous homomorphism carries the verbal step of two subgroups into the verbal step of their images.

theorem MonoidHom.map_pVerbalStep_eq_of_isClosedMap {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (hfc : IsClosedMap ⇑f) (K L : Subgroup G) : Subgroup.map f (TauCeti.pVerbalStep p K L) = TauCeti.pVerbalStep p (Subgroup.map f K) (Subgroup.map f L)

A continuous closed map (for instance a continuous homomorphism from a compact group to a Hausdorff group, by Continuous.isClosedMap) carries the verbal step of two subgroups onto the verbal step of their images. No surjectivity is needed: the verbal step refers to K and L alone.

One step of the recursion

def TauCeti.pLowerCentralStep (p : ℕ) {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H : Subgroup G) : Subgroup G

One step of the lower p-series: H ↦ closure (Hᵖ ⬝ [H, G]), the verbal step TauCeti.pVerbalStep of H against the whole group. Its characteristic property is TauCeti.pLowerCentralStep_le_iff.

Equations

• TauCeti.pLowerCentralStep p H = TauCeti.pVerbalStep p H ⊤

theorem TauCeti.pLowerCentralStep_eq_pVerbalStep (p : ℕ) {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H : Subgroup G) : pLowerCentralStep p H = pVerbalStep p H ⊤

One step of the lower p-series is the verbal step taken against the whole group.

theorem TauCeti.pLowerCentralStep_def (p : ℕ) {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H : Subgroup G) : pLowerCentralStep p H = (Subgroup.closure ((fun (x : G) => x ^ p) '' ↑H) ⊔ ⁅H, ⊤⁆).topologicalClosure

The defining equation pLowerCentralStep p H = closure (Hᵖ ⬝ [H, G]), with topological closure, expresses the next lower p-series step in terms of powers and commutators.

theorem TauCeti.isClosed_pLowerCentralStep {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H : Subgroup G) : IsClosed ↑(pLowerCentralStep p H)

One step of the lower p-series is a closed subgroup.

theorem TauCeti.pow_mem_pLowerCentralStep {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Subgroup G} {x : G} (hx : x ∈ H) : x ^ p ∈ pLowerCentralStep p H

The p-th power of an element of H lies in pLowerCentralStep p H.

theorem TauCeti.commutator_le_pLowerCentralStep {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H : Subgroup G) : ⁅H, ⊤⁆ ≤ pLowerCentralStep p H

The commutators ⁅H, G⁆ lie in pLowerCentralStep p H.

theorem TauCeti.commutator_mem_pLowerCentralStep {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Subgroup G} {x : G} (hx : x ∈ H) (y : G) : ⁅x, y⁆ ∈ pLowerCentralStep p H

The commutator of an element of H with any element lies in pLowerCentralStep p H.

theorem TauCeti.pLowerCentralStep_le_iff {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H K : Subgroup G} (hK : IsClosed ↑K) : pLowerCentralStep p H ≤ K ↔ (∀ x ∈ H, x ^ p ∈ K) ∧ ⁅H, ⊤⁆ ≤ K

The characteristic property of one step. A closed subgroup contains pLowerCentralStep p H exactly when it contains the p-th powers of the elements of H and the commutators ⁅H, G⁆.

theorem TauCeti.pLowerCentralStep_mono {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H K : Subgroup G} (h : H ≤ K) : pLowerCentralStep p H ≤ pLowerCentralStep p K

One step of the lower p-series is monotone in the subgroup.

instance TauCeti.pLowerCentralStep_normal {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H : Subgroup G) [H.Normal] : (pLowerCentralStep p H).Normal

One step of the lower p-series of a normal subgroup is normal.

theorem TauCeti.pLowerCentralStep_le {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Subgroup G} [H.Normal] (hH : IsClosed ↑H) : pLowerCentralStep p H ≤ H

One step of the lower p-series of a closed normal subgroup lies in that subgroup.

theorem TauCeti.normal_of_pLowerCentralStep_le_of_le {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {R K : Subgroup G} (hRK : pLowerCentralStep p R ≤ K) (hKR : K ≤ R) : K.Normal

A subgroup squeezed between pLowerCentralStep p R and R is normal: it contains the commutators ⁅R, G⁆, hence its own commutators with G.

theorem TauCeti.isClosed_pLowerCentralStep_subgroupOf {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) : IsClosed ↑((pLowerCentralStep p N).subgroupOf N)

One step of the lower p-series of a subgroup N, read inside N, is a closed subgroup of N.

instance TauCeti.instIsMulCommutativeQuotientPLowerCentralStep {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] : IsMulCommutative (↥N ⧸ (pLowerCentralStep p N).subgroupOf N)

N ⧸ Nᵖ[N, G] is commutative: the commutators ⁅N, G⁆ lie in pLowerCentralStep p N.

theorem TauCeti.exponent_quotient_pLowerCentralStep_subgroupOf_dvd {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] : Monoid.exponent (↥N ⧸ (pLowerCentralStep p N).subgroupOf N) ∣ p

N ⧸ Nᵖ[N, G] has exponent dividing p: the p-th powers of the elements of N lie in pLowerCentralStep p N.

theorem TauCeti.isPGroup_quotient_pLowerCentralStep_subgroupOf {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] : IsPGroup p (↥N ⧸ (pLowerCentralStep p N).subgroupOf N)

N ⧸ Nᵖ[N, G] is an abstract p-group, since its exponent divides p.

@[simp]

theorem TauCeti.mk_conjNormal_eq {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] (g : G) (n : ↥N) : ↑((MulAut.conjNormal g) n) = ↑n

Conjugation acts trivially on N ⧸ Nᵖ[N, G]. For a normal subgroup N, the class of the conjugate g n g⁻¹ in the quotient of N by pLowerCentralStep p N is the class of n.

theorem TauCeti.pLowerCentralStep_subgroupOf_le_ker_iff {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {R : Subgroup G} [R.Normal] (hR : IsClosed ↑R) {A : Type u_2} [Group A] (φ : ↥R →* A) (hφ : IsClosed ↑φ.ker) : (pLowerCentralStep p R).subgroupOf R ≤ φ.ker ↔ (∀ (r : ↥R), φ r ^ p = 1) ∧ ∀ (g : G) (r : ↥R), φ ((MulAut.conjNormal g) r) = φ r

Homomorphisms out of R that factor through R ⧸ Rᵖ[R, G]. For a closed normal subgroup R and a homomorphism φ on R with closed kernel, φ kills pLowerCentralStep p R exactly when it kills the p-th powers and is invariant under conjugation by G.

theorem MonoidHom.map_pLowerCentralStep_le {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (K : Subgroup G) : Subgroup.map f (TauCeti.pLowerCentralStep p K) ≤ TauCeti.pLowerCentralStep p (Subgroup.map f K)

A continuous homomorphism carries one step of the lower p-series of a subgroup into the corresponding step for the image of that subgroup.

theorem MonoidHom.map_pLowerCentralStep_eq_of_surjective {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (hfc : IsClosedMap ⇑f) (hsurj : Function.Surjective ⇑f) (K : Subgroup G) : Subgroup.map f (TauCeti.pLowerCentralStep p K) = TauCeti.pLowerCentralStep p (Subgroup.map f K)

A continuous closed surjection (for instance a continuous surjection from a compact group onto a Hausdorff group, by Continuous.isClosedMap) carries one step of the lower p-series of a subgroup onto the corresponding step for its image.

The series

def TauCeti.pLowerCentralSeries (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ℕ → Subgroup G

The lower p-series (descending p-central series) of a topological group, 0-based to match Mathlib's lowerCentralSeries: λ₀ = G and λ_{k+1} = closure (λ_kᵖ ⬝ [λ_k, G]). Its terms are closed normal subgroups with ⁅λ_j, λ_k⁆ ≤ λ_{j+k+1} (TauCeti.commutator_pLowerCentralSeries_le). For a profinite group and a prime p, λ_1 is the pro-p Frattini subgroup (TauCeti.pLowerCentralSeries_one_eq_proPFrattini).

Equations

• TauCeti.pLowerCentralSeries p G 0 = ⊤
• TauCeti.pLowerCentralSeries p G k.succ = TauCeti.pLowerCentralStep p (TauCeti.pLowerCentralSeries p G k)

@[simp]

theorem TauCeti.pLowerCentralSeries_zero (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : pLowerCentralSeries p G 0 = ⊤

theorem TauCeti.mem_pLowerCentralSeries_zero (p : ℕ) {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) : g ∈ pLowerCentralSeries p G 0

Every element lies in λ_0 = G.

@[simp]

theorem TauCeti.pLowerCentralSeries_succ (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : pLowerCentralSeries p G (k + 1) = pLowerCentralStep p (pLowerCentralSeries p G k)

instance TauCeti.pLowerCentralSeries_normal {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : (pLowerCentralSeries p G k).Normal

Every term of the lower p-series is a normal subgroup.

theorem TauCeti.isClosed_pLowerCentralSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : IsClosed ↑(pLowerCentralSeries p G k)

Every term of the lower p-series is closed.

theorem TauCeti.pLowerCentralSeries_succ_le {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : pLowerCentralSeries p G (k + 1) ≤ pLowerCentralSeries p G k

The lower p-series is descending.

theorem TauCeti.pLowerCentralSeries_antitone {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Antitone (pLowerCentralSeries p G)

The lower p-series is antitone.

theorem TauCeti.pow_mem_pLowerCentralSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {x : G} (hx : x ∈ pLowerCentralSeries p G k) : x ^ p ∈ pLowerCentralSeries p G (k + 1)

The p-th power of an element of λ_k lies in λ_{k+1}.

theorem TauCeti.pow_pow_mem_pLowerCentralSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {x : G} (hx : x ∈ pLowerCentralSeries p G k) (j : ℕ) : x ^ p ^ j ∈ pLowerCentralSeries p G (k + j)

The p ^ j-th power of an element of λ_k lies in λ_{k+j}.

theorem TauCeti.pow_mul_mem_pLowerCentralSeries_one (p : ℕ) {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : G) (c : ℕ) : x ^ (p * c) ∈ pLowerCentralSeries p G 1

The p * c-th power of every element lies in λ_1.

theorem TauCeti.commutator_pLowerCentralSeries_top_le {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : ⁅pLowerCentralSeries p G k, ⊤⁆ ≤ pLowerCentralSeries p G (k + 1)

The commutators ⁅λ_k, G⁆ lie in λ_{k+1}.

theorem TauCeti.commutator_mem_pLowerCentralSeries_succ {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {x : G} (hx : x ∈ pLowerCentralSeries p G k) (y : G) : ⁅x, y⁆ ∈ pLowerCentralSeries p G (k + 1)

The commutator of an element of λ_k with any element lies in λ_{k+1}.

theorem TauCeti.map_mk'_pLowerCentralSeries_le_center {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : Subgroup.map (QuotientGroup.mk' (pLowerCentralSeries p G (k + 1))) (pLowerCentralSeries p G k) ≤ Subgroup.center (G ⧸ pLowerCentralSeries p G (k + 1))

Centrality of the graded pieces. The image of λ_k in G ⧸ λ_{k+1} is central.

theorem TauCeti.pLowerCentralSeries_one {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : pLowerCentralSeries p G 1 = (Subgroup.closure (Set.range fun (g : G) => g ^ p) ⊔ commutator G).topologicalClosure

The first term of the lower p-series is the topological closure of Gᵖ [G, G].

theorem TauCeti.pLowerCentralSeries_one_zero {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : pLowerCentralSeries 0 G 1 = (commutator G).topologicalClosure

The first term of the closed lower central series is the closure of the commutator subgroup.

theorem MonoidHom.pLowerCentralSeries_one_le_ker {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K : Type u_2} [CommGroup K] (φ : G →* K) (hφ : IsClosed ↑φ.ker) (hp : ∀ (g : G), φ g ^ p = 1) : TauCeti.pLowerCentralSeries p G 1 ≤ φ.ker

λ_1(G) lies in the kernel of a homomorphism to an abelian group that kills p-th powers. For a homomorphism φ : G →* K with closed kernel into a commutative group, λ_1(G) ≤ ker φ as soon as φ kills the p-th powers of G: the kernel is closed and contains Gᵖ and [G, G].

theorem TauCeti.commutator_pLowerCentralSeries_le {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (j k : ℕ) : ⁅pLowerCentralSeries p G j, pLowerCentralSeries p G k⁆ ≤ pLowerCentralSeries p G (j + k + 1)

The degree-raising law. Commutators of λ_j with λ_k lie in λ_{j+k+1}.

theorem TauCeti.commutator_mem_pLowerCentralSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j k : ℕ} {x y : G} (hx : x ∈ pLowerCentralSeries p G j) (hy : y ∈ pLowerCentralSeries p G k) : ⁅x, y⁆ ∈ pLowerCentralSeries p G (j + k + 1)

The degree-raising law, elementwise. The commutator of an element of λ_j with an element of λ_k lies in λ_{j+k+1}.

Comparison with the abstract lower p-central series

theorem TauCeti.pLowerCentralSeries_eq_topologicalClosure {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : pLowerCentralSeries p G k = (Subgroup.pLowerCentralSeries p ⊤ k).topologicalClosure

Every term of the lower p-series is the topological closure of the corresponding term of the abstract lower p-central series Subgroup.pLowerCentralSeries p ⊤ of the underlying group.

theorem TauCeti.pLowerCentralSeries_eq_of_discreteTopology {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] (k : ℕ) : pLowerCentralSeries p G k = Subgroup.pLowerCentralSeries p ⊤ k

On a discrete group the lower p-series is the abstract lower p-central series of the group.

Functoriality

theorem MonoidHom.map_pLowerCentralSeries_le {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (k : ℕ) : Subgroup.map f (TauCeti.pLowerCentralSeries p G k) ≤ TauCeti.pLowerCentralSeries p H k

A continuous homomorphism carries λ_k into λ_k.

theorem MonoidHom.map_pLowerCentralSeries_eq_of_surjective {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (hfc : IsClosedMap ⇑f) (hsurj : Function.Surjective ⇑f) (k : ℕ) : Subgroup.map f (TauCeti.pLowerCentralSeries p G k) = TauCeti.pLowerCentralSeries p H k

A continuous closed surjection (for instance a continuous surjection from a compact group onto a Hausdorff group, by Continuous.isClosedMap) carries λ_k onto λ_k.

theorem ContinuousMulEquiv.map_pLowerCentralSeries_eq {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) (k : ℕ) : Subgroup.map e.toMonoidHom (TauCeti.pLowerCentralSeries p G k) = TauCeti.pLowerCentralSeries p H k

A topological group isomorphism matches the lower p-series of its source and target term by term. In particular, every term of the lower p-series is stable under continuous automorphisms.

theorem TauCeti.isTopCharacteristic_pLowerCentralSeries (p : ℕ) {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : IsTopCharacteristic G (pLowerCentralSeries p G k)

Every term of the lower p-series is topologically characteristic, for every topological group and every natural number p.

theorem MulEquiv.map_pLowerCentralSeries_eq_of_discreteTopology {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology G] [DiscreteTopology H] (e : G ≃* H) (k : ℕ) : Subgroup.map e.toMonoidHom (TauCeti.pLowerCentralSeries p G k) = TauCeti.pLowerCentralSeries p H k

A group isomorphism between discrete groups matches their lower p-series term by term.

The cyclic groups ℤ/pⁿ

theorem TauCeti.top_pLowerCentralSeries_multiplicative_zmod_pow_eq_bot {p : ℕ} (n : ℕ) : Subgroup.pLowerCentralSeries p ⊤ n = ⊥

The cyclic group ℤ/pⁿ has p-class at most n: its lower p-series consists of the subgroups of p ^ k-th powers, and the p ^ n-th powers are trivial.

theorem MulEquiv.pLowerCentralSeries_eq_bot_multiplicative_zmod_pow {p : ℕ} {H : Type u_1} [Group H] [TopologicalSpace H] [DiscreteTopology H] {n : ℕ} (e : H ≃* Multiplicative (ZMod (p ^ n))) : TauCeti.pLowerCentralSeries p H n = ⊥

A discrete group isomorphic to ℤ/pⁿ has p-class at most n.