Burnside generation for pro-`p` groups #

For a pro-p group, the Frattini subgroup detects topological generation. A closed subgroup which is not contained in any open normal subgroup of index p is the whole group, and hence a set topologically generates the group exactly when its image topologically generates the Frattini quotient.

The finite input is that a maximal subgroup of a finite p-group has index p. To apply it to a proper closed subgroup H of a profinite pro-p group, first choose an open normal subgroup U for which H ⊔ U is still proper. The image of H in the finite p-group G/U lies in a maximal subgroup. Its pullback is an open normal subgroup of index p containing H.

As a consequence, a Frattini cover φ : G → H of a pro-p group G, that is a continuous homomorphism whose kernel lies in the Frattini subgroup, is a topological isomorphism as soon as it has a continuous homomorphic section s: the range of s is closed and generates G together with the Frattini subgroup, so s is surjective and is a two-sided inverse of φ.

The Frattini argument also runs relative to a pro-p subgroup of a profinite group which is not itself pro-p. If P is a closed pro-p subgroup of G, a normal subgroup of G contained in Φ(P) consists of non-generators of G. In particular, for a normal pro-p subgroup P, a set generating G modulo ⁅P, P⁆ already generates G. This is how the wild inertia subgroup of the absolute Galois group of a p-adic field is removed when counting generators.

Main results #

IsProP.eq_top_of_forall_not_le_openNormalSubgroup_index_eq: the index-p detection criterion for closed subgroups.
IsProP.eq_top_of_sup_proPFrattini_eq_top: the Frattini subgroup consists of non-generators.
IsProP.surjective_of_forall_inv_mul_mem_proPFrattini: a continuous endomorphism congruent to the identity modulo the Frattini subgroup is surjective.
IsProP.surjective_of_surjective_comp_of_ker_le_proPFrattini: a homomorphism with closed range whose composite with a Frattini cover is surjective is surjective.
IsProP.continuousMulEquivOfLeftInverse: a Frattini cover with a continuous homomorphic section is a topological isomorphism, with the section as inverse.
topologicallyGenerates_iff_frattiniQuotient: a set generates topologically if and only if its image generates the Frattini quotient topologically.
IsProP.eq_top_of_le_map_proPFrattini_of_sup_eq_top: the relative Frattini argument, a normal subgroup of G inside the Frattini subgroup of a closed pro-p subgroup consists of non-generators of G.
IsProP.topologicalClosure_eq_top_of_sup_commutator: a set generating G topologically together with ⁅P, P⁆, for a normal pro-p subgroup P, generates G topologically.

References #

L. Ribes and P. Zalesskii, Profinite Groups, Section 2.8.
J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, (3.9.1) and the proof of (7.4.1).

source

theorem TauCeti.IsProP.eq_top_of_forall_not_le_openNormalSubgroup_index_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {H : Subgroup G} (hH : IsClosed ↑H) (h : ∀ (U : OpenNormalSubgroup G), (↑U.toOpenSubgroup).index = p → ¬H ≤ ↑U.toOpenSubgroup) :

H = ⊤

Index-p detection for closed subgroups. A closed subgroup of a profinite pro-p group which is contained in no open normal subgroup of index p is the whole group.

source

theorem TauCeti.IsProP.eq_top_of_sup_proPFrattini_eq_top {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {H : Subgroup G} (hH : IsClosed ↑H) (hsup : H ⊔ proPFrattini p G = ⊤) :

H = ⊤

The pro-p Frattini subgroup consists of non-generators: if a closed subgroup together with the Frattini subgroup generates the whole group, then the subgroup was already the whole group.

source

theorem TauCeti.IsProP.surjective_of_surjective_comp_of_ker_le_proPFrattini {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {K : Type u_1} {H : Type u_2} [Group K] [Group H] {s : K →* G} (hs : IsClosed ↑s.range) {φ : G →* H} (hφs : Function.Surjective (⇑φ ∘ ⇑s)) (hker : φ.ker ≤ proPFrattini p G) :

Function.Surjective ⇑s

A homomorphism onto a Frattini cover is surjective. Let φ : G →* H have kernel in the Frattini subgroup Φ(G) of the pro-p group G. A homomorphism s into G with closed range whose composite with φ is surjective is itself surjective.

source

theorem TauCeti.IsProP.surjective_of_forall_inv_mul_mem_proPFrattini {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {φ : G →* G} (hφ : Continuous ⇑φ) (h : ∀ (g : G), g⁻¹ * φ g ∈ proPFrattini p G) :

Function.Surjective ⇑φ

An endomorphism congruent to the identity modulo the Frattini subgroup is surjective. A continuous endomorphism φ of a pro-p group with g⁻¹ * φ g ∈ Φ(G) for every g is surjective.

The relative Frattini argument #

A closed pro-p subgroup P of a profinite group G has its own Frattini subgroup Φ(P). When a normal subgroup N of G lies in Φ(P), its elements are non-generators of G itself, even though G need not be pro-p: if H ⊔ N = G, the modular law gives P = (H ⊓ P) ⊔ N, so H ⊓ P and Φ(P) generate P, whence P ≤ H and H = G. The closure of the commutator subgroup ⁅P, P⁆ of a closed normal pro-p subgroup is such an N.

source

theorem TauCeti.IsProP.eq_top_of_le_map_proPFrattini_of_sup_eq_top {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {P : Subgroup G} (hPc : IsClosed ↑P) (hP : IsProP p ↥P) {N : Subgroup G} [N.Normal] (hN : N ≤ Subgroup.map P.subtype (proPFrattini p ↥P)) {H : Subgroup G} (hH : IsClosed ↑H) (hsup : H ⊔ N = ⊤) :

H = ⊤

The relative Frattini argument. Let P be a closed pro-p subgroup of a profinite group G, and N a normal subgroup of G contained in the pro-p Frattini subgroup Φ(P) of P. A closed subgroup H of G with H ⊔ N = G is all of G.

source

theorem TauCeti.IsProP.topologicalClosure_eq_top_of_sup_commutator {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {P : Subgroup G} [P.Normal] (hP : IsProP p ↥P) {s : Set G} (hs : (Subgroup.closure s ⊔ ⁅P, P⁆).topologicalClosure = ⊤) :

(Subgroup.closure s).topologicalClosure = ⊤

Relative Frattini reduction along a normal pro-p subgroup (NSW (3.9.1)). Let P be a normal pro-p subgroup of a profinite group G. A set which topologically generates G together with the commutator subgroup ⁅P, P⁆ already topologically generates G.

source

theorem TauCeti.topologicallyGenerates_iff_frattiniQuotient {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (s : Set G) :

(Subgroup.closure s).topologicalClosure = ⊤ ↔ (Subgroup.closure (⇑(QuotientGroup.mk' (proPFrattini p G)) '' s)).topologicalClosure = ⊤

Burnside's basis theorem, generation form. A set topologically generates a profinite pro-p group if and only if its image topologically generates the Frattini quotient.

Frattini covers with a continuous homomorphic section #

source

theorem TauCeti.IsProP.surjective_of_leftInverse_of_ker_le_proPFrattini {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {H : Type v} [Group H] [TopologicalSpace H] (hG : IsProP p G) {φ : G →ₜ* H} {s : H →ₜ* G} (hs : Function.LeftInverse ⇑φ ⇑s) (hker : φ.ker ≤ proPFrattini p G) :

Function.Surjective ⇑s

A continuous homomorphic section of a Frattini cover of a pro-p group is surjective, since its range is a closed subgroup generating the group together with the Frattini subgroup.

source

noncomputable def TauCeti.IsProP.continuousMulEquivOfLeftInverse {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {H : Type v} [Group H] [TopologicalSpace H] (hG : IsProP p G) (φ : G →ₜ* H) (s : H →ₜ* G) (hs : Function.LeftInverse ⇑φ ⇑s) (hker : φ.ker ≤ proPFrattini p G) :

G ≃ₜ* H

A Frattini cover with a continuous homomorphic section is an isomorphism. A continuous homomorphism φ : G → H out of a pro-p group G, whose kernel lies in the Frattini subgroup Φ(G) and which has a continuous homomorphic section s, is a topological isomorphism whose inverse is s.

Equations

hG.continuousMulEquivOfLeftInverse φ s hs hker = { toFun := ⇑φ, invFun := ⇑s, left_inv := ⋯, right_inv := hs, map_mul' := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }