Gaschütz's lemma on lifting generators

Let f : G →* H be a surjective homomorphism of finite groups and suppose that G is generated by n elements. Gaschütz's lemma says that every generating n-tuple of H lifts to a generating n-tuple of G: not merely to some n-tuple, which is trivial, but to one that still generates.

The proof is a counting argument. For a subgroup K ≤ G and a tuple h generating H, let N(K, h) be the number of tuples generating K and lifting h. The tuples in K lifting h are counted by |K ∩ ker f|^n whenever K maps onto H, a number independent of h, and they are partitioned by the subgroup they generate, so |K ∩ ker f|^n = ∑_{L ≤ K} N(L, h). Induction on K then shows that N(K, h) does not depend on h (MonoidHom.card_comp_eq_and_closure_range_eq_congr). As N(G, f ∘ g) ≥ 1 for a generating tuple g of G, also N(G, h) ≥ 1, which is the lifting statement.

Main results

• MonoidHom.card_forall_mem_and_comp_eq_congr: the number of tuples in a subgroup K lifting a tuple of H along f does not depend on the tuple, as long as K maps onto H.
• MonoidHom.card_comp_eq_and_closure_range_eq_congr: Gaschütz's counting lemma: the number of tuples generating K and lifting a generating tuple of H does not depend on that tuple.
• MonoidHom.exists_comp_eq_and_closure_range_eq_top_of_surjective: Gaschütz's lemma: along a surjection of finite groups, a generating tuple of the target lifts to a generating tuple of the source, provided the source is generated by a tuple of the same shape.

References

• W. Gaschütz, Zu einem von B. H. und H. Neumann gestellten Problem, Math. Nachr. 14 (1955), 249–252.
• L. Ribes and P. Zalesskii, Profinite Groups, Lemma 2.5.3.

theorem MonoidHom.card_forall_mem_and_comp_eq_congr {G : Type u_1} {H : Type u_2} {ι : Type u_3} [Group G] [Group H] (f : G →* H) {K : Subgroup G} (hK : Subgroup.map f K = ⊤) (h h' : ι → H) : Nat.card { x : ι → G // (∀ (i : ι), x i ∈ K) ∧ ⇑f ∘ x = h } = Nat.card { x : ι → G // (∀ (i : ι), x i ∈ K) ∧ ⇑f ∘ x = h' }

If the subgroup K maps onto H, the number of ι-tuples in K lifting a tuple of H along f does not depend on the tuple.

theorem MonoidHom.card_comp_eq_and_closure_range_eq_congr {G : Type u_1} {H : Type u_2} {ι : Type u_3} [Group G] [Group H] (f : G →* H) [Finite G] [Finite ι] (K : Subgroup G) {h h' : ι → H} (hh : Subgroup.closure (Set.range h) = ⊤) (hh' : Subgroup.closure (Set.range h') = ⊤) : Nat.card { x : ι → G // ⇑f ∘ x = h ∧ Subgroup.closure (Set.range x) = K } = Nat.card { x : ι → G // ⇑f ∘ x = h' ∧ Subgroup.closure (Set.range x) = K }

Gaschütz's counting lemma. For a subgroup K of a finite group G, the number of ι-tuples that generate K and lift a given generating tuple of H along f does not depend on that generating tuple.

theorem MonoidHom.exists_comp_eq_and_closure_range_eq_top_of_surjective {G : Type u_1} {H : Type u_2} {ι : Type u_3} [Group G] [Group H] (f : G →* H) [Finite G] [Finite ι] (hf : Function.Surjective ⇑f) {g : ι → G} (hg : Subgroup.closure (Set.range g) = ⊤) {h : ι → H} (hh : Subgroup.closure (Set.range h) = ⊤) : ∃ (g' : ι → G), ⇑f ∘ g' = h ∧ Subgroup.closure (Set.range g') = ⊤

Gaschütz's lemma. Let f : G →* H be a surjective homomorphism from a finite group, and let G be generated by an ι-tuple. Then every generating ι-tuple of H lifts along f to a generating ι-tuple of G.