Gaschütz's lifting lemma for profinite groups

Let f : G →* H be a continuous surjection from a profinite group onto a Hausdorff group, and let G be topologically generated by an ι-tuple, with ι finite. Then every ι-tuple that topologically generates H lifts along f to an ι-tuple that topologically generates G (TauCeti.exists_comp_eq_and_topologicalClosure_closure_range_eq_top). In terms of the generator rank: a generating n-tuple of H lifts to a generating n-tuple of G as soon as topologicalGeneratorRankNat G ≤ n, which is exists_comp_eq_and_topologicalClosure_closure_range_eq_top_of_topologicalGeneratorRankNat_le. This is the mechanism behind minimal presentations: when G and a quotient of it have the same generator rank n, a minimal generating n-tuple of the quotient pulls back to a minimal generating n-tuple of G.

The proof reduces to Gaschütz's lemma for finite groups (MonoidHom.exists_comp_eq_and_closure_range_eq_top_of_surjective) by compactness. For each open normal subgroup U ≤ G, the tuples of G lifting the given tuple whose image generates G ⧸ U form a closed subset of ι → G; it is nonempty by the finite lemma applied to G ⧸ U ↠ H ⧸ U.map f, which is a surjection of finite groups because f is an open map. These sets are directed downwards, so they have a common point, which is the required lift.

Main results

• TauCeti.exists_comp_eq_and_topologicalClosure_closure_range_eq_top: Gaschütz's lifting lemma for profinite groups.
• exists_comp_eq_and_topologicalClosure_closure_range_eq_top_of_topologicalGeneratorRankNat_le: the generator-rank form, for Fin n-tuples with n at least the generator rank of G.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Proposition 2.5.4.

theorem TauCeti.exists_comp_eq_and_topologicalClosure_closure_range_eq_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H] {ι : Type u_3} [Finite ι] {f : G →* H} (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) {g : ι → G} (hg : (Subgroup.closure (Set.range g)).topologicalClosure = ⊤) {h : ι → H} (hh : (Subgroup.closure (Set.range h)).topologicalClosure = ⊤) : ∃ (g' : ι → G), ⇑f ∘ g' = h ∧ (Subgroup.closure (Set.range g')).topologicalClosure = ⊤

Gaschütz's lifting lemma for profinite groups. Along a continuous surjection f : G →* H from a profinite group onto a Hausdorff group, an ι-tuple that topologically generates H lifts to an ι-tuple that topologically generates G, provided G is topologically generated by some ι-tuple, with ι finite.

theorem TauCeti.exists_comp_eq_and_topologicalClosure_closure_range_eq_top_of_topologicalGeneratorRankNat_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H] (hG : IsTopologicallyFinitelyGenerated G) {n : ℕ} (hn : topologicalGeneratorRankNat G hG ≤ n) {f : G →* H} (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) {h : Fin n → H} (hh : (Subgroup.closure (Set.range h)).topologicalClosure = ⊤) : ∃ (g' : Fin n → G), ⇑f ∘ g' = h ∧ (Subgroup.closure (Set.range g')).topologicalClosure = ⊤

Gaschütz's lifting lemma, generator-rank form. Along a continuous surjection f : G →* H from a topologically finitely generated profinite group onto a Hausdorff group, a topologically generating n-tuple of H lifts to a topologically generating n-tuple of G whenever n is at least the topological generator rank of G.