Documentation

Mathlib.GroupTheory.Schreier

Schreier's Lemma #

In this file we prove Schreier's lemma.

Main results #

theorem card_dvd_exponent_nsmul_rank' (G : Type u_1) [AddCommGroup G] [AddGroup.FG G] {n : } (hG : ∀ (g : G), n g = 0) :
theorem card_dvd_exponent_pow_rank' (G : Type u_1) [CommGroup G] [Group.FG G] {n : } (hG : ∀ (g : G), g ^ n = 1) :
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) => g * (↑(Subgroup.MemRightTransversals.toFun hR 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 * (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) => g * (↑(Subgroup.MemRightTransversals.toFun hR 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 * (toFun hR g)⁻¹).

theorem Subgroup.exists_finset_card_le_mul {G : Type u_1} [Group G] (H : Subgroup G) [H.FiniteIndex] {S : Finset G} (hS : Subgroup.closure S = ) :
∃ (T : Finset H), T.card H.index * 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] [H.FiniteIndex] :

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] [H.FiniteIndex] :
Group.rank H H.index * Group.rank G

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
Instances For

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

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

    Equations
    • =