The Frattini series of a topological group

The Frattini series Φ_k = TauCeti.proPFrattiniSeries p G k of a topological group is the sequence of closed normal subgroups

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

obtained by iterating the verbal form of the pro-p Frattini subgroup. One step of the recursion is TauCeti.proPFrattiniStep, the verbal step TauCeti.pVerbalStep of a subgroup against itself; its characteristic property TauCeti.proPFrattiniStep_le_iff characterizes containment in a closed subgroup. The series is descending with closed normal terms, and continuous homomorphisms carry Φ_k into Φ_k.

The Frattini series lies below the lower p-series λ_k = TauCeti.pLowerCentralSeries p G k of TauCeti.Topology.Algebra.Group.LowerCentralSeries, term by term: the two steps differ only in that the Frattini step takes commutators inside the subgroup while the lower p-series step takes them against the whole group.

Nothing here assumes p prime or G profinite. For a profinite G and a prime p the step is the honest pro-p Frattini subgroup, so Φ_{k+1} = Φ(Φ_k); and in a topologically finitely generated pro-p group the inclusion Φ_k ≤ λ_k reverses cofinally — every Φ_k contains some λ_j — so there the two series are cofinal in one another. See TauCeti.Topology.Algebra.Group.Profinite.ProP.Frattini.Series.

Main definitions

• TauCeti.proPFrattiniStep: one step H ↦ closure (Hᵖ ⬝ [H, H]) of the recursion.
• TauCeti.proPFrattiniSeries: the Frattini series Φ_k.

Main results

• TauCeti.proPFrattiniStep_le_iff: a closed subgroup contains proPFrattiniStep p H exactly when it contains the p-th powers of H and the commutators ⁅H, H⁆.
• TauCeti.proPFrattiniSeries_le_pLowerCentralSeries: Φ_k ≤ λ_k.
• MonoidHom.map_proPFrattiniSeries_le, MonoidHom.map_proPFrattiniSeries_eq_of_surjective, ContinuousMulEquiv.map_proPFrattiniSeries_eq: functoriality of the series.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 2.8, Proposition 2.8.13.
• J. D. Dixon, M. P. F. du Sautoy, A. Mann and D. Segal, Analytic pro-p groups, Section 1.2.

One step of the recursion

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

One step of the Frattini series: H ↦ closure (Hᵖ ⬝ [H, H]), the verbal step TauCeti.pVerbalStep of H against itself. For a prime p and a closed subgroup of a profinite group it is the pro-p Frattini subgroup of H, viewed inside the ambient group (TauCeti.proPFrattiniStep_eq_map_proPFrattini). Its characteristic property is TauCeti.proPFrattiniStep_le_iff.

Equations

• TauCeti.proPFrattiniStep p H = TauCeti.pVerbalStep p H H

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

One step of the Frattini series is the verbal step of a subgroup against itself.

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

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

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

One step of the Frattini series is a closed subgroup.

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

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

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

The commutators ⁅H, H⁆ lie in proPFrattiniStep p H.

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

The commutator of two elements of H lies in proPFrattiniStep p H.

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

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

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

One step of the Frattini series is monotone in the subgroup.

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

One step of the Frattini series lies in the corresponding step of the lower p-series: the two differ only in that the latter takes commutators against the whole group.

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

One step of the Frattini series of a normal subgroup is normal.

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

One step of the Frattini series of a closed subgroup lies in that subgroup.

theorem MonoidHom.map_proPFrattiniStep_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.proPFrattiniStep p K) ≤ TauCeti.proPFrattiniStep p (Subgroup.map f K)

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

theorem MonoidHom.map_proPFrattiniStep_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 : Subgroup G) : Subgroup.map f (TauCeti.proPFrattiniStep p K) = TauCeti.proPFrattiniStep p (Subgroup.map f K)

A continuous closed map (for instance a continuous homomorphism from a compact group to a Hausdorff group, by Continuous.isClosedMap) carries one step of the Frattini series of a subgroup onto the corresponding step for its image. Unlike for the lower p-series, no surjectivity is needed: the Frattini step of K refers to K alone.

The series

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

The Frattini series of a topological group, 0-based like the lower p-series: Φ₀ = G and Φ_{k+1} = closure (Φ_kᵖ ⬝ [Φ_k, Φ_k]). For a prime p and a profinite group it is the iterated pro-p Frattini subgroup (TauCeti.proPFrattiniSeries_succ_eq_map_proPFrattini), and it always lies below the lower p-series (TauCeti.proPFrattiniSeries_le_pLowerCentralSeries); in a topologically finitely generated pro-p group the two series are moreover cofinal in one another (TauCeti.IsProP.exists_pLowerCentralSeries_le_proPFrattiniSeries).

Equations

• TauCeti.proPFrattiniSeries p G 0 = ⊤
• TauCeti.proPFrattiniSeries p G k.succ = TauCeti.proPFrattiniStep p (TauCeti.proPFrattiniSeries p G k)

@[simp]

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

@[simp]

theorem TauCeti.proPFrattiniSeries_succ (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : proPFrattiniSeries p G (k + 1) = proPFrattiniStep p (proPFrattiniSeries p G k)

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

Every term of the Frattini series is a normal subgroup.

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

Every term of the Frattini series is closed.

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

The Frattini series is descending.

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

The Frattini series is antitone.

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

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

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

The commutators of Φ_k with itself lie in Φ_{k+1}.

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

The Frattini series lies below the lower p-series, term by term: the Frattini step takes commutators inside the subgroup, the lower p-series step takes them against the whole group.

Functoriality

theorem MonoidHom.map_proPFrattiniSeries_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.proPFrattiniSeries p G k) ≤ TauCeti.proPFrattiniSeries p H k

A continuous homomorphism carries Φ_k into Φ_k.

theorem MonoidHom.map_proPFrattiniSeries_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.proPFrattiniSeries p G k) = TauCeti.proPFrattiniSeries 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_proPFrattiniSeries_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.proPFrattiniSeries p G k) = TauCeti.proPFrattiniSeries p H k

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