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 * (toFun hR 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 Subgroup.closure_mul_image_mul_eq_top {G : Type u_1} [Group G] {H : Subgroup G} {R : Set G} {S : Set G} (hR : R ∈ Subgroup.rightTransversals ↑H) (hR1 : 1 ∈ R) (hS : Subgroup.closure S = ⊤) : ↑(Subgroup.closure ((fun (g : G) => g * (↑(Subgroup.MemRightTransversals.toFun hR g))⁻¹) '' (R * S))) * R = ⊤

theorem Subgroup.closure_mul_image_eq {G : Type u_1} [Group G] {H : Subgroup G} {R : Set G} {S : Set G} (hR : R ∈ Subgroup.rightTransversals ↑H) (hR1 : 1 ∈ R) (hS : Subgroup.closure S = ⊤) : Subgroup.closure ((fun (g : G) => g * (↑(Subgroup.MemRightTransversals.toFun hR 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 * (toFun hR g)⁻¹).

theorem Subgroup.closure_mul_image_eq_top {G : Type u_1} [Group G] {H : Subgroup G} {R : Set G} {S : Set G} (hR : R ∈ Subgroup.rightTransversals ↑H) (hR1 : 1 ∈ R) (hS : Subgroup.closure S = ⊤) : Subgroup.closure ((fun (g : G) => { val := g * (↑(Subgroup.MemRightTransversals.toFun hR g))⁻¹, property := ⋯ }) '' (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 * (toFun hR g)⁻¹).

theorem Subgroup.closure_mul_image_eq_top' {G : Type u_1} [Group G] {H : Subgroup G} [DecidableEq G] {R : Finset G} {S : Finset G} (hR : ↑R ∈ Subgroup.rightTransversals ↑H) (hR1 : 1 ∈ R) (hS : Subgroup.closure ↑S = ⊤) : Subgroup.closure ↑(Finset.image (fun (g : G) => { val := g * (↑(Subgroup.MemRightTransversals.toFun hR g))⁻¹, property := ⋯ }) (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 * (toFun hR g)⁻¹).

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

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

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

Equations

• ⋯ = ⋯

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

theorem Subgroup.card_commutator_dvd_index_center_pow (G : Type u_1) [Group G] [Finite ↑(commutatorSet G)] : Nat.card ↥(commutator G) ∣ Subgroup.index (Subgroup.center G) ^ (Subgroup.index (Subgroup.center G) * 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.

Equations

• Subgroup.cardCommutatorBound n = (n ^ (2 * n)) ^ (n ^ (2 * n + 1) + 1)

theorem Subgroup.card_commutator_le_of_finite_commutatorSet (G : Type u_1) [Group G] [Finite ↑(commutatorSet G)] : Nat.card ↥(commutator G) ≤ Subgroup.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.instFiniteSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupCommutator (G : Type u_1) [Group G] [Finite ↑(commutatorSet G)] : Finite ↥(commutator G)

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

Equations

• ⋯ = ⋯