The Frattini subgroup of a profinite group

The Frattini subgroup profiniteFrattini G of a topological group G is the intersection of its maximal open subgroups, written Φ(G). For a profinite group this is the Frattini subgroup of Ribes–Zalesskii. It is closed and normal, it is preserved by every continuous automorphism, and a continuous surjection carries it into the Frattini subgroup of the target. With the discrete topology every subgroup is open, and profiniteFrattini G is Mathlib's abstract frattini G.

The abstract Frattini subgroup is the wrong object for an infinite profinite group: a maximal subgroup need not be open, and topological generation, not abstract generation, is what the theory of profinite groups measures. The topological version consists of non-generators in the topological sense: a closed subgroup H with H ⊔ Φ(G) = G is all of G. The input is that in a compact group a proper open subgroup lies in a maximal subgroup, which is again open; this is the finite statement for the finite quotient by an open normal subgroup inside it. A proper closed subgroup H of a profinite group lies in a proper open subgroup H ⊔ U, for an open normal subgroup U, hence in a maximal open subgroup, which also contains Φ(G).

The consequence is the lifting of generators along Frattini covers. Let f : G → K be a continuous surjection of a profinite group onto a Hausdorff group whose kernel lies in Φ(G). A set topologically generates G exactly when its image topologically generates K; in particular every lift of a topologically generating family of K topologically generates G. Unlike Gaschütz's lifting lemma (TauCeti.exists_comp_eq_and_topologicalClosure_closure_range_eq_top), this needs no finiteness of the family, and the lift is arbitrary.

Main definitions

• TauCeti.profiniteFrattini: the intersection of the maximal open subgroups.

Main results

• TauCeti.isTopCharacteristic_profiniteFrattini: the Frattini subgroup is preserved by every continuous automorphism, and so it is normal (TauCeti.profiniteFrattini_normal).
• MonoidHom.map_profiniteFrattini_le: a continuous surjection carries the Frattini subgroup into the Frattini subgroup of the target.
• TauCeti.profiniteFrattini_eq_frattini: for a discrete group, the Frattini subgroup is Mathlib's frattini.
• TauCeti.eq_top_of_sup_profiniteFrattini_eq_top: the Frattini subgroup of a profinite group consists of non-generators.
• TauCeti.topologicalClosure_closure_eq_top_iff_of_ker_le_profiniteFrattini: along a continuous surjection with kernel in the Frattini subgroup, a set topologically generates the source exactly when its image topologically generates the target.
• TauCeti.topologicalClosure_closure_range_eq_top_of_ker_le_profiniteFrattini: every lift of a topologically generating family along a continuous homomorphism to a Hausdorff group with kernel in the Frattini subgroup is topologically generating; surjectivity is automatic.
• TauCeti.topologicalClosure_closure_eq_top_iff_quotient_profiniteFrattini: a set topologically generates a profinite group exactly when its image topologically generates the quotient by the Frattini subgroup.

The non-generator argument generalizes the formal proofs TauCeti.IsProP.eq_top_of_forall_not_le_openNormalSubgroup_index_eq and TauCeti.IsProP.eq_top_of_sup_proPFrattini_eq_top in TauCeti.Topology.Algebra.Group.Profinite.ProP.Burnside, replacing open normal subgroups of index p by maximal open subgroups.

References

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

def TauCeti.profiniteFrattini (G : Type u) [Group G] [TopologicalSpace G] : Subgroup G

The Frattini subgroup Φ(G) of a topological group: the intersection of its maximal open subgroups. For a profinite group this is the Frattini subgroup of Ribes–Zalesskii; with the discrete topology it is Mathlib's frattini (TauCeti.profiniteFrattini_eq_frattini).

theorem TauCeti.profiniteFrattini_def {G : Type u} [Group G] [TopologicalSpace G] : profiniteFrattini G = ⨅ (M : Subgroup G), ⨅ (_ : IsOpen ↑M), ⨅ (_ : IsCoatom M), M

The defining equation of the Frattini subgroup: the body of TauCeti.profiniteFrattini is not exposed, so unfolding it goes through this lemma.

theorem TauCeti.mem_profiniteFrattini_iff {G : Type u} [Group G] [TopologicalSpace G] {x : G} : x ∈ profiniteFrattini G ↔ ∀ (M : Subgroup G), IsOpen ↑M → IsCoatom M → x ∈ M

An element lies in the Frattini subgroup exactly when it lies in every maximal open subgroup.

theorem TauCeti.profiniteFrattini_le {G : Type u} [Group G] [TopologicalSpace G] {M : Subgroup G} (hMo : IsOpen ↑M) (hM : IsCoatom M) : profiniteFrattini G ≤ M

The Frattini subgroup is contained in every maximal open subgroup.

instance TauCeti.isClosed_profiniteFrattini {G : Type u} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] : IsClosed ↑(profiniteFrattini G)

The Frattini subgroup is closed whenever translations are continuous, as an intersection of open, hence closed, subgroups.

Functoriality

theorem MonoidHom.profiniteFrattini_le_comap {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : TauCeti.profiniteFrattini G ≤ Subgroup.comap f (TauCeti.profiniteFrattini H)

A continuous surjection carries the Frattini subgroup into the Frattini subgroup of the target: the preimage of a maximal open subgroup is again a maximal open subgroup.

theorem MonoidHom.map_profiniteFrattini_le {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : Subgroup.map f (TauCeti.profiniteFrattini G) ≤ TauCeti.profiniteFrattini H

The image of the Frattini subgroup under a continuous surjection lies in the Frattini subgroup of the target.

@[simp]

theorem ContinuousMulEquiv.map_profiniteFrattini_eq {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (e : G ≃ₜ* H) : Subgroup.map (↑↑e) (TauCeti.profiniteFrattini G) = TauCeti.profiniteFrattini H

Continuous multiplicative equivalences identify the Frattini subgroups of their source and target.

theorem TauCeti.isTopCharacteristic_profiniteFrattini {G : Type u} [Group G] [TopologicalSpace G] : IsTopCharacteristic G (profiniteFrattini G)

The Frattini subgroup is topologically characteristic: every continuous automorphism maps it onto itself.

instance TauCeti.profiniteFrattini_normal {G : Type u} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] : (profiniteFrattini G).Normal

The Frattini subgroup is normal whenever translations are continuous.

theorem TauCeti.profiniteFrattini_eq_frattini {G : Type u} [Group G] [TopologicalSpace G] [DiscreteTopology G] : profiniteFrattini G = frattini G

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

Non-generators

theorem TauCeti.eq_top_of_sup_profiniteFrattini_eq_top {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {H : Subgroup G} (hH : IsClosed ↑H) (hsup : H ⊔ profiniteFrattini G = ⊤) : H = ⊤

The Frattini subgroup of a profinite group consists of non-generators. A closed subgroup H with H ⊔ Φ(G) = G is all of G.

theorem TauCeti.profiniteFrattini_ne_top {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Nontrivial G] : profiniteFrattini G ≠ ⊤

The Frattini subgroup of a nontrivial profinite group is proper. Otherwise the trivial subgroup would generate together with it.

Lifting generators along Frattini covers

theorem TauCeti.topologicalClosure_closure_eq_top_iff_of_ker_le_profiniteFrattini {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [T2Space K] {f : G →* K} (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) (hker : f.ker ≤ profiniteFrattini G) (s : Set G) : (Subgroup.closure s).topologicalClosure = ⊤ ↔ (Subgroup.closure (⇑f '' s)).topologicalClosure = ⊤

Generators lift along Frattini covers. Let f : G →* K be a continuous surjection from a profinite group onto a Hausdorff group with kernel in the Frattini subgroup of G. A set topologically generates G if and only if its image topologically generates K.

theorem TauCeti.topologicalClosure_closure_range_eq_top_of_ker_le_profiniteFrattini {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [T2Space K] {f : G →* K} (hf : Continuous ⇑f) (hker : f.ker ≤ profiniteFrattini G) {ι : Type u_1} {g : ι → G} (hg : (Subgroup.closure (Set.range (⇑f ∘ g))).topologicalClosure = ⊤) : (Subgroup.closure (Set.range g)).topologicalClosure = ⊤

Every lift of a generating family along a Frattini cover generates. Let f : G →* K be a continuous homomorphism from a profinite group to a Hausdorff group with kernel in the Frattini subgroup of G. A family g of elements of G whose image under f topologically generates K topologically generates G. No finiteness of the index type is needed, and f is automatically surjective: its range is compact, hence closed in K, and contains the generating family.

theorem TauCeti.topologicalClosure_closure_eq_top_iff_quotient_profiniteFrattini {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (s : Set G) : (Subgroup.closure s).topologicalClosure = ⊤ ↔ (Subgroup.closure (⇑(QuotientGroup.mk' (profiniteFrattini G)) '' s)).topologicalClosure = ⊤

Generation modulo the Frattini subgroup. A set topologically generates a profinite group if and only if its image topologically generates the quotient by the Frattini subgroup.