Maximal open subgroups of pro-p groups

In a compact pro-p group every maximal subgroup that is open is normal of index p. Such a subgroup M contains an open normal subgroup U, and it is the preimage of a maximal subgroup of the finite p-group G ⧸ U; a maximal subgroup of a finite p-group is normal of index p (it is nilpotent, so satisfies the normalizer condition). Conversely a subgroup of prime index is maximal in any group. So for a pro-p group the open normal subgroups of index p, whose intersection defines TauCeti.proPFrattini, are exactly the maximal open subgroups, and the pro-p Frattini subgroup is the intersection of the maximal open subgroups: the Frattini subgroup in the usual sense.

A subgroup containing an open subgroup is itself open, so a subgroup which is open and maximal among all subgroups is the same thing as a maximal element of the lattice of open subgroups; the statements below use the former reading.

Two consequences are recorded. For a nontrivial profinite pro-p group the pro-p Frattini subgroup is proper, which is Burnside's non-generator property applied to the trivial subgroup. For a finite p-group with the discrete topology, where every subgroup is open, the pro-p Frattini subgroup agrees with Mathlib's abstract frattini.

Main results

• TauCeti.IsProP.normal_of_isCoatom, TauCeti.IsProP.index_eq_of_isCoatom: a maximal open subgroup of a compact pro-p group is normal of index p.
• TauCeti.IsProP.isCoatom_iff_index_eq: an open subgroup of a compact pro-p group is maximal exactly when it has index p.
• TauCeti.iInf_isCoatom_le_proPFrattini: in any topological group, the intersection of the maximal open subgroups lies in the pro-p Frattini subgroup.
• TauCeti.IsProP.proPFrattini_eq_iInf_isCoatom: for a compact pro-p group the pro-p Frattini subgroup is the intersection of the maximal open subgroups.
• TauCeti.IsProP.proPFrattini_ne_top: the pro-p Frattini subgroup of a nontrivial profinite pro-p group is proper.
• IsPGroup.proPFrattini_eq_frattini: for a finite discrete p-group, the pro-p Frattini subgroup is Mathlib's frattini.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 2.8.

theorem TauCeti.iInf_isCoatom_le_proPFrattini {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] : ⨅ (M : Subgroup G), ⨅ (_ : IsOpen ↑M), ⨅ (_ : IsCoatom M), M ≤ proPFrattini p G

In any topological group, the intersection of the maximal open subgroups lies in the pro-p Frattini subgroup: an open normal subgroup of prime index p is a maximal open subgroup.

theorem TauCeti.IsProP.normal_of_isCoatom {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) {M : Subgroup G} (hMo : IsOpen ↑M) (hM : IsCoatom M) : M.Normal

A maximal open subgroup of a pro-p group is normal.

theorem TauCeti.IsProP.index_eq_of_isCoatom {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) {M : Subgroup G} (hMo : IsOpen ↑M) (hM : IsCoatom M) : M.index = p

A maximal open subgroup of a pro-p group has index p.

theorem TauCeti.IsProP.isCoatom_iff_index_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) {M : Subgroup G} (hMo : IsOpen ↑M) : IsCoatom M ↔ M.index = p

An open subgroup of a compact pro-p group is maximal exactly when it has index p.

theorem TauCeti.IsProP.proPFrattini_eq_iInf_isCoatom {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) : proPFrattini p G = ⨅ (M : Subgroup G), ⨅ (_ : IsOpen ↑M), ⨅ (_ : IsCoatom M), M

The pro-p Frattini subgroup is the intersection of the maximal open subgroups. For a compact pro-p group, the open normal subgroups of index p are exactly the maximal open subgroups, so proPFrattini p G is the Frattini subgroup in the usual sense.

theorem TauCeti.IsProP.proPFrattini_ne_top {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Nontrivial G] (hG : IsProP p G) : proPFrattini p G ≠ ⊤

The Frattini subgroup of a nontrivial pro-p group is proper. Otherwise the trivial subgroup together with the Frattini subgroup would generate, and the Frattini subgroup consists of non-generators.

theorem IsPGroup.proPFrattini_eq_frattini {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] (hG : IsPGroup p G) : TauCeti.proPFrattini p G = frattini G

The pro-p Frattini subgroup of a finite p-group is its Frattini subgroup. With the discrete topology every subgroup is open, so the maximal open subgroups are all the maximal subgroups.