Schreier's Lemma

In this file we prove Schreier's lemma.

Main results

• closure_mul_image_eq : 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 (fun g ↦ g * (hR.toRightFun g)⁻¹).
• fg_of_index_ne_zero : Schreier's Lemma: A finite index subgroup of a finitely generated group is finitely generated.
• card_commutator_le_of_finite_commutatorSet: A theorem of Schur: The size of the commutator subgroup is bounded in terms of the number of commutators.

theorem card_dvd_exponent_pow_rank (G : Type u_1) [CommGroup G] [Group.FG G] : Nat.card G ∣ Monoid.exponent G ^ Group.rank G

theorem card_dvd_exponent_nsmul_rank (G : Type u_1) [AddCommGroup G] [AddGroup.FG G] : Nat.card G ∣ AddMonoid.exponent G ^ AddGroup.rank G

theorem card_dvd_exponent_pow_rank' (G : Type u_1) [CommGroup G] [Group.FG G] {n : ℕ} (hG : ∀ (g : G), g ^ n = 1) : Nat.card G ∣ n ^ Group.rank G

theorem card_dvd_exponent_nsmul_rank' (G : Type u_1) [AddCommGroup G] [AddGroup.FG G] {n : ℕ} (hG : ∀ (g : G), n • g = 0) : Nat.card G ∣ n ^ AddGroup.rank G

theorem Subgroup.closure_mul_image_mul_eq_top {G : Type u_1} [Group G] {H : Subgroup G} {R S : Set G} (hR : IsComplement (↑H) R) (hR1 : 1 ∈ R) (hS : closure S = ⊤) : ↑(closure ((fun (g : G) => g * (↑(hR.toRightFun g))⁻¹) '' (R * S))) * R = ⊤

theorem Subgroup.closure_mul_image_eq {G : Type u_1} [Group G] {H : Subgroup G} {R S : Set G} (hR : IsComplement (↑H) R) (hR1 : 1 ∈ R) (hS : closure S = ⊤) : closure ((fun (g : G) => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) = H

Schreier's Lemma: If R : Set G is a rightTransversal 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 (fun g ↦ g * (hR.toRightFun g)⁻¹).

theorem Subgroup.closure_mul_image_eq_top {G : Type u_1} [Group G] {H : Subgroup G} {R S : Set G} (hR : IsComplement (↑H) R) (hR1 : 1 ∈ R) (hS : closure S = ⊤) : closure ((fun (g : G) => ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) '' (R * S)) = ⊤

Schreier's Lemma: If R : Set G is a rightTransversal 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 (fun g ↦ g * (hR.toRightFun g)⁻¹).

theorem Subgroup.closure_mul_image_eq_top' {G : Type u_1} [Group G] {H : Subgroup G} [DecidableEq G] {R S : Finset G} (hR : IsComplement ↑H ↑R) (hR1 : 1 ∈ R) (hS : closure ↑S = ⊤) : closure ↑(Finset.image (fun (g : G) => ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) (R * S)) = ⊤

Schreier's Lemma: If R : Finset G is a rightTransversal 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 (fun g ↦ g * (hR.toRightFun g)⁻¹).

theorem Subgroup.exists_finset_card_le_mul {G : Type u_1} [Group G] (H : Subgroup G) [H.FiniteIndex] {S : Finset G} (hS : closure ↑S = ⊤) : ∃ (T : Finset ↥H), T.card ≤ H.index * S.card ∧ closure ↑T = ⊤

instance Subgroup.fg_of_index_ne_zero {G : Type u_1} [Group G] (H : Subgroup G) [hG : Group.FG G] [H.FiniteIndex] : Group.FG ↥H

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

theorem Subgroup.rank_le_index_mul_rank {G : Type u_1} [Group G] (H : Subgroup G) [hG : Group.FG G] [H.FiniteIndex] : Group.rank ↥H ≤ H.index * Group.rank G

theorem Subgroup.card_commutator_dvd_index_center_pow (G : Type u_1) [Group G] [Finite ↑(commutatorSet G)] : Nat.card ↥(_root_.commutator G) ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G) + 1)

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

def Subgroup.cardCommutatorBound (n : ℕ) : ℕ

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

theorem Subgroup.card_commutator_le_of_finite_commutatorSet (G : Type u_1) [Group G] [Finite ↑(commutatorSet G)] : Nat.card ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))

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

instance Subgroup.instFiniteSubtypeMemCommutatorOfElemCommutatorSet (G : Type u_1) [Group G] [Finite ↑(commutatorSet G)] : Finite ↥(_root_.commutator G)

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