Documentation

Mathlib.GroupTheory.Schreier

Schreier's Lemma #

In this file we prove Schreier's lemma.

Main results #

source
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 = ⊤
source
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)⁻¹).

source
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 := (_ : g * (↑(Subgroup.MemRightTransversals.toFun hR g))⁻¹ ∈ H) }) '' (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)⁻¹).

source
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 := (_ : g * (↑(Subgroup.MemRightTransversals.toFun hR g))⁻¹ ∈ H) }) (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)⁻¹).

source
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 = ⊤
source
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
source
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
source
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.

source
def Subgroup.cardCommutatorBound (n : ℕ) :
ℕ

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

Equations
Instances For
    source
    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.

    source
    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