The lower p-series of a profinite group

The lower p-series λ_k = TauCeti.pLowerCentralSeries p G k of a topological group is defined and studied for arbitrary topological groups in TauCeti.Topology.Algebra.Group.LowerCentralSeries. This file adds what holds for a profinite group G and a prime p.

For a profinite group and a prime p, the first term λ_1 is the pro-p Frattini subgroup TauCeti.proPFrattini p G. Primality matters: for p = 4 and the cyclic group of order two, fourth powers and commutators are trivial, so λ_1 is trivial, while the pro-4 Frattini subgroup is the whole group.

For a topologically finitely generated profinite group and a prime p, every λ_k is open, hence of finite index, and in a topologically finitely generated pro-p group the quotients G ⧸ λ_k are finite p-groups; in particular the graded pieces gr_k(G) = λ_k ⧸ λ_{k+1} are finite. Without finite generation the terms need not be open: an infinite product of copies of ℤ ⧸ p has λ_1 = 1, so gr_0(G) = G is infinite.

In a pro-p group the series is cofinal among the open normal subgroups: every open normal subgroup contains some λ_k. So the λ_k have trivial intersection, and a pro-p group is the inverse limit of its quotients G ⧸ λ_k: a compatible sequence of cosets comes from a unique element, and a map into G is continuous as soon as its composites with the quotient maps are. Cofinality needs no finite generation. With it, the λ_k are open, so they form a neighbourhood basis of 1 and the quotients G ⧸ λ_k are finite p-groups; this is what lets two topologically finitely generated pro-p groups be compared level by level along their lower p-series.

A continuous homomorphism between the quotients G ⧸ λ_{k+1} → H ⧸ λ_{k+1}, with H compact, carries the image of λ_k(G) into the image of λ_k(H), so it descends to a continuous homomorphism G ⧸ λ_k → H ⧸ λ_k compatible with the quotient projections; surjectivity descends with it. This is the bonding operation of a levelwise comparison along the lower p-series.

Main results

• ContinuousMonoidHom.pLowerCentralSeriesDesc: a continuous homomorphism between the quotients by λ_{k+1} descends to a continuous homomorphism between the quotients by λ_k, compatibly with the quotient projections (ContinuousMonoidHom.pLowerCentralSeriesDesc_mapOfLE); the descent of a surjection is surjective.
• TauCeti.pLowerCentralSeries_one_eq_proPFrattini: for a prime p, λ_1 is the pro-p Frattini subgroup of a profinite group.
• TauCeti.IsProP.surjective_of_forall_inv_mul_mem_pLowerCentralSeries_one: a continuous endomorphism of a pro-p group congruent to the identity modulo λ_1 is surjective.
• TauCeti.IsTopologicallyFinitelyGenerated.isOpen_pLowerCentralSeries: for a prime p, in a topologically finitely generated profinite group every λ_k is open, so TauCeti.IsTopologicallyFinitelyGenerated.finite_quotient_pLowerCentralSeries, TauCeti.IsTopologicallyFinitelyGenerated.finite_gradedPiece and, for a pro-p group, TauCeti.IsProP.isPGroup_quotient_pLowerCentralSeries.
• TauCeti.IsProP.exists_pLowerCentralSeries_le: in a pro-p group every open normal subgroup contains a term of the lower p-series, so TauCeti.IsProP.iInf_pLowerCentralSeries_eq_bot. Since the closed lower central series lies termwise below it, also TauCeti.IsProP.iInf_closedLowerCentralSeries_eq_bot.
• TauCeti.IsProP.eq_bot_of_le_pLowerCentralStep: Nakayama's lemma, a subgroup K of a pro-p group with K ≤ closure (Kᵖ ⬝ [K, G]) is trivial.
• TauCeti.IsProP.le_of_le_topologicalClosure_sup_pLowerCentralStep: Nakayama's lemma, relative form, a subgroup R with R ≤ closure (N ⬝ Rᵖ[R, G]) for a closed normal subgroup N satisfies R ≤ N.
• TauCeti.IsProP.existsUnique_forall_mk_eq_pLowerCentralSeries and TauCeti.IsProP.existsUnique_monoidHom_mk'_comp_eq_pLowerCentralSeries: a pro-p group is the inverse limit of its quotients G ⧸ λ_k, for elements and for homomorphisms.
• TauCeti.IsProP.continuous_iff_forall_continuous_mk_pLowerCentralSeries: a map into a pro-p group is continuous exactly when its composites with the quotient maps G → G ⧸ λ_k are.
• TauCeti.IsProP.hasAntitoneBasis_nhds_one_pLowerCentralSeries: in a topologically finitely generated pro-p group the lower p-series is a neighbourhood basis of 1.
• TauCeti.IsProP.mem_of_forall_mk_mem_map_pLowerCentralSeries: in a pro-p group, membership in a closed subgroup is detected on the quotients G ⧸ λ_k.

References

• 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.

noncomputable def ContinuousMonoidHom.pLowerCentralSeriesDesc {p : ℕ} {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] {k : ℕ} (ψ : G ⧸ TauCeti.pLowerCentralSeries p G (k + 1) →ₜ* H ⧸ TauCeti.pLowerCentralSeries p H (k + 1)) : G ⧸ TauCeti.pLowerCentralSeries p G k →ₜ* H ⧸ TauCeti.pLowerCentralSeries p H k

Descent along the lower p-series. A continuous homomorphism between the quotients by λ_{k+1} of two topological groups, the target compact, carries the image of λ_k into the image of λ_k, hence descends to a continuous homomorphism between the quotients by λ_k. Its defining equation is ContinuousMonoidHom.pLowerCentralSeriesDesc_mk.

Equations

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

@[simp]

theorem ContinuousMonoidHom.pLowerCentralSeriesDesc_mk {p : ℕ} {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] {k : ℕ} (ψ : G ⧸ TauCeti.pLowerCentralSeries p G (k + 1) →ₜ* H ⧸ TauCeti.pLowerCentralSeries p H (k + 1)) (g : G) : ψ.pLowerCentralSeriesDesc ↑g = (TauCeti.QuotientGroup.mapOfLE ⋯) (ψ ↑g)

The descended homomorphism on the class of g is the class of ψ ⟦g⟧.

@[simp]

theorem ContinuousMonoidHom.pLowerCentralSeriesDesc_mapOfLE {p : ℕ} {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] {k : ℕ} (ψ : G ⧸ TauCeti.pLowerCentralSeries p G (k + 1) →ₜ* H ⧸ TauCeti.pLowerCentralSeries p H (k + 1)) (x : G ⧸ TauCeti.pLowerCentralSeries p G (k + 1)) : ψ.pLowerCentralSeriesDesc ((TauCeti.QuotientGroup.mapOfLE ⋯) x) = (TauCeti.QuotientGroup.mapOfLE ⋯) (ψ x)

The descended homomorphism commutes with the quotient projections.

theorem ContinuousMonoidHom.pLowerCentralSeriesDesc_surjective {p : ℕ} {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] {k : ℕ} (ψ : G ⧸ TauCeti.pLowerCentralSeries p G (k + 1) →ₜ* H ⧸ TauCeti.pLowerCentralSeries p H (k + 1)) (h : Function.Surjective ⇑ψ) : Function.Surjective ⇑ψ.pLowerCentralSeriesDesc

The descent of a surjective homomorphism is surjective.

theorem TauCeti.pLowerCentralSeries_one_eq_proPFrattini {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hp : Nat.Prime p) : pLowerCentralSeries p G 1 = proPFrattini p G

For a profinite group and a prime p, the first term of the lower p-series is the pro-p Frattini subgroup.

theorem TauCeti.IsProP.surjective_of_forall_inv_mul_mem_pLowerCentralSeries_one {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Fact (Nat.Prime p)] (hG : IsProP p G) {φ : G →* G} (hφ : Continuous ⇑φ) (h : ∀ (g : G), g⁻¹ * φ g ∈ pLowerCentralSeries p G 1) : Function.Surjective ⇑φ

Burnside's criterion modulo λ_1. A continuous endomorphism of a pro-p group congruent to the identity modulo λ_1 = Φ is surjective.

theorem TauCeti.IsTopologicallyFinitelyGenerated.isOpen_pLowerCentralSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) (hp : Nat.Prime p) (k : ℕ) : IsOpen ↑(pLowerCentralSeries p G k)

Openness of the lower p-series. For a prime p, in a topologically finitely generated profinite group every term of the lower p-series is open.

theorem TauCeti.IsTopologicallyFinitelyGenerated.finite_quotient_pLowerCentralSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) (hp : Nat.Prime p) (k : ℕ) : Finite (G ⧸ pLowerCentralSeries p G k)

For a prime p, in a topologically finitely generated profinite group every quotient G ⧸ λ_k is finite.

theorem TauCeti.IsTopologicallyFinitelyGenerated.finite_gradedPiece {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) (hp : Nat.Prime p) (k : ℕ) : Finite (gradedPiece p G k)

For a prime p, in a topologically finitely generated profinite group every graded piece gr_k(G) = λ_k ⧸ λ_{k+1} of the lower p-series is finite.

theorem TauCeti.IsProP.isPGroup_quotient_pLowerCentralSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (hp : Nat.Prime p) (k : ℕ) : IsPGroup p (G ⧸ pLowerCentralSeries p G k)

For a prime p, in a topologically finitely generated pro-p group every quotient G ⧸ λ_k is a finite p-group.

Cofinality of the lower p-series in a pro-p group

theorem TauCeti.IsProP.exists_pLowerCentralSeries_le {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) (hp : Nat.Prime p) (U : OpenNormalSubgroup G) : ∃ (k : ℕ), pLowerCentralSeries p G k ≤ ↑U.toOpenSubgroup

Cofinality of the lower p-series. In a compact pro-p group every open normal subgroup contains a term of the lower p-series. No finite generation is needed.

theorem TauCeti.IsProP.iInf_pLowerCentralSeries_eq_bot {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hp : Nat.Prime p) : ⨅ (k : ℕ), pLowerCentralSeries p G k = ⊥

In a pro-p group the terms of the lower p-series have trivial intersection.

theorem TauCeti.IsProP.iInf_closedLowerCentralSeries_eq_bot {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hp : Nat.Prime p) : ⨅ (n : ℕ), closedLowerCentralSeries G n = ⊥

In a pro-p group the terms of the closed lower central series have trivial intersection.

theorem TauCeti.IsProP.eq_bot_of_le_pLowerCentralStep {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hp : Nat.Prime p) {K : Subgroup G} (h : K ≤ pLowerCentralStep p K) : K = ⊥

Nakayama's lemma for pro-p groups. In a profinite pro-p group a subgroup K with K ≤ closure (Kᵖ ⬝ [K, G]) is trivial: it lies in every term of the lower p-series.

theorem TauCeti.IsProP.le_of_le_topologicalClosure_sup_pLowerCentralStep {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hp : Nat.Prime p) {R N : Subgroup G} [N.Normal] (hN : IsClosed ↑N) (h : R ≤ (N ⊔ pLowerCentralStep p R).topologicalClosure) : R ≤ N

Nakayama's lemma for pro-p groups, relative form. If a subgroup R of a pro-p group lies in the closure of N ⬝ Rᵖ[R, G] for a closed normal subgroup N, then R ≤ N: the image of R in G ⧸ N is contained in its own pLowerCentralStep, hence trivial.

theorem TauCeti.IsProP.existsUnique_forall_mk_eq_pLowerCentralSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hp : Nat.Prime p) (x : (k : ℕ) → G ⧸ pLowerCentralSeries p G k) (hcompat : ∀ (k : ℕ) (g : G), ↑g = x (k + 1) → ↑g = x k) : ∃! g : G, ∀ (k : ℕ), ↑g = x k

A pro-p group is the inverse limit of its quotients by the lower p-series. A sequence of cosets of the λ_k, compatible along the quotient maps, is realized by a unique element.

theorem TauCeti.IsProP.existsUnique_monoidHom_mk'_comp_eq_pLowerCentralSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hp : Nat.Prime p) {H : Type u_2} [MulOneClass H] (x : (k : ℕ) → H →* G ⧸ pLowerCentralSeries p G k) (hx : ∀ (k : ℕ), (QuotientGroup.mapOfLE ⋯).comp (x (k + 1)) = x k) : ∃! φ : H →* G, ∀ (k : ℕ), (QuotientGroup.mk' (pLowerCentralSeries p G k)).comp φ = x k

A pro-p group is the inverse limit of its quotients by the lower p-series, for homomorphisms. A sequence of homomorphisms H →* G ⧸ λ_k, compatible along the quotient maps, is induced by a unique homomorphism H →* G.

theorem TauCeti.IsProP.hasAntitoneBasis_nhds_one_pLowerCentralSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (hp : Nat.Prime p) : (nhds 1).HasAntitoneBasis fun (k : ℕ) => ↑(pLowerCentralSeries p G k)

The lower p-series is a neighbourhood basis of 1 in a topologically finitely generated pro-p group.

theorem TauCeti.IsProP.mem_of_forall_mk_mem_map_pLowerCentralSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hp : Nat.Prime p) {H : Subgroup G} (hH : IsClosed ↑H) {g : G} (h : ∀ (k : ℕ), ↑g ∈ Subgroup.map (QuotientGroup.mk' (pLowerCentralSeries p G k)) H) : g ∈ H

Membership in a closed subgroup is detected on the lower p-series. In a compact pro-p group, an element whose class modulo every λ_k is the class of an element of the closed subgroup H lies in H: it lies in H ⊔ U for every open normal subgroup U, since U contains a term of the series, and H is the infimum of those. No finite generation is needed.

theorem TauCeti.IsProP.continuous_iff_forall_continuous_mk_pLowerCentralSeries {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hp : Nat.Prime p) {X : Type u_2} [TopologicalSpace X] {f : X → G} : Continuous f ↔ ∀ (k : ℕ), Continuous fun (x : X) => ↑(f x)

A map into a pro-p group is continuous exactly when all of its composites with the quotient maps G → G ⧸ λ_k are. No finite generation is needed.