Automorphisms acting trivially modulo the Frattini subgroup

Assume IsCoatomic (Subgroup G). The Frattini subgroup consists of non-generators (frattini_nongenerating), so a family that agrees with a generating family modulo a subgroup N ≤ frattini G generates G again. This file uses that fact to bound the group of automorphisms of G that act trivially modulo N.

Fix a family s : ι → G generating G, with ι finite. An automorphism α that fixes every class modulo N permutes the families y : ι → G with y i ≡ s i modulo N, of which there are Nat.card N ^ Nat.card ι. Each of these families generates G, so an automorphism fixing one of them is the identity. A group H of such automorphisms therefore acts freely on these families, every orbit has Nat.card H elements, and Nat.card H divides Nat.card N ^ Nat.card ι.

For a finite p-group P this says that the kernel of MulAut P →* MulAut (P ⧸ frattini P) is a p-group. This finite statement is the input to the corresponding statement for a topologically finitely generated pro-p group, whose continuous automorphisms acting trivially on its Frattini quotient form a pro-p group, obtained by passing to the limit over finite quotients.

Main statements

• TauCeti.closure_range_eq_top_of_le_frattini: a family agreeing modulo N ≤ frattini G with a generating family generates, assuming IsCoatomic (Subgroup G).
• TauCeti.card_dvd_card_pow_of_le_frattini: a group of automorphisms acting trivially modulo N ≤ frattini G has order dividing Nat.card N ^ Nat.card ι whenever G is generated by a family indexed by the finite type ι and IsCoatomic (Subgroup G) holds.
• TauCeti.isPGroup_of_le_frattini: if G is finite and N ≤ frattini G is a p-group, every group of automorphisms acting trivially modulo N is a p-group.
• IsPGroup.isPGroup_ker_mapQuotient_frattini: the automorphisms of a finite p-group acting trivially on its Frattini quotient form a p-group.

References

• D. Gorenstein, Finite Groups, Chapter 5, §1.
• B. Huppert, Endliche Gruppen I, Kapitel III, §3.

theorem TauCeti.closure_range_eq_top_of_le_frattini {G : Type u_1} [Group G] {ι : Type u_2} {N : Subgroup G} [IsCoatomic (Subgroup G)] {s y : ι → G} (hs : Subgroup.closure (Set.range s) = ⊤) (hN : N ≤ frattini G) (hy : ∀ (i : ι), ↑(y i) = ↑(s i)) : Subgroup.closure (Set.range y) = ⊤

A family agreeing with a generating family modulo a subgroup of the Frattini subgroup generates the group, assuming IsCoatomic (Subgroup G).

theorem TauCeti.card_dvd_card_pow_of_le_frattini {G : Type u_1} [Group G] {ι : Type u_2} {N : Subgroup G} {H : Subgroup (MulAut G)} [IsCoatomic (Subgroup G)] [Finite ι] {s : ι → G} (hs : Subgroup.closure (Set.range s) = ⊤) (hN : N ≤ frattini G) (hH : ∀ α ∈ H, ∀ (x : G), ↑(α x) = ↑x) : Nat.card ↥H ∣ Nat.card ↥N ^ Nat.card ι

Automorphisms acting trivially modulo a subgroup of the Frattini subgroup. If G is generated by a family indexed by a finite type ι, N ≤ frattini G, and IsCoatomic (Subgroup G) holds, then the order of a group of automorphisms of G fixing every class modulo N divides Nat.card N ^ Nat.card ι.

theorem TauCeti.isPGroup_of_le_frattini {G : Type u_1} [Group G] {N : Subgroup G} {H : Subgroup (MulAut G)} [Finite G] {p : ℕ} [hp : Fact (Nat.Prime p)] (hN : N ≤ frattini G) (hNp : IsPGroup p ↥N) (hH : ∀ α ∈ H, ∀ (x : G), ↑(α x) = ↑x) : IsPGroup p ↥H

Automorphisms acting trivially modulo a p-subgroup of the Frattini subgroup. If G is finite and N ≤ frattini G is a p-group, then every group of automorphisms of G fixing each class modulo N is a p-group.

theorem IsPGroup.isPGroup_ker_mapQuotient_frattini {G : Type u_1} [Group G] [Finite G] {p : ℕ} [Fact (Nat.Prime p)] (hG : IsPGroup p G) : IsPGroup p ↥(MulAut.mapQuotient (frattini G)).ker

The automorphisms of a finite p-group acting trivially on its Frattini quotient form a p-group.