mathlib3 documentation

group_theory.schreier

Schreier's Lemma #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove Schreier's lemma.

Main results #

theorem subgroup.closure_mul_image_mul_eq_top {G : Type u_1} [group G] {H : subgroup G} {R S : set G} (hR : R subgroup.right_transversals H) (hR1 : 1 R) (hS : subgroup.closure S = ) :
theorem subgroup.closure_mul_image_eq {G : Type u_1} [group G] {H : subgroup G} {R S : set G} (hR : R subgroup.right_transversals H) (hR1 : 1 R) (hS : subgroup.closure S = ) :

Schreier's Lemma: If R : set G is a right_transversal of H : subgroup G with 1 ∈ R, and if G is generated by S : set G, then H is generated by the set (R * S).image (λ g, g * (to_fun hR g)⁻¹).

theorem subgroup.closure_mul_image_eq_top {G : Type u_1} [group G] {H : subgroup G} {R S : set G} (hR : R subgroup.right_transversals H) (hR1 : 1 R) (hS : subgroup.closure S = ) :

Schreier's Lemma: If R : set G is a right_transversal of H : subgroup G with 1 ∈ R, and if G is generated by S : set G, then H is generated by the set (R * S).image (λ g, g * (to_fun hR g)⁻¹).

Schreier's Lemma: If R : finset G is a right_transversal of H : subgroup G with 1 ∈ R, and if G is generated by S : finset G, then H is generated by the finset (R * S).image (λ g, g * (to_fun hR g)⁻¹).

@[protected, instance]
def subgroup.fg_of_index_ne_zero {G : Type u_1} [group G] (H : subgroup G) [hG : group.fg G] [H.finite_index] :

Schreier's Lemma: A finite index subgroup of a finitely generated group is finitely generated.

If G has n commutators [g₁, g₂], then |G'| ∣ [G : Z(G)] ^ ([G : Z(G)] * n + 1), where G' denotes the commutator of G.

A bound for the size of the commutator subgroup in terms of the number of commutators.

Equations

A theorem of Schur: The size of the commutator subgroup is bounded in terms of the number of commutators.

@[protected, instance]

A theorem of Schur: A group with finitely many commutators has finite commutator subgroup.