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 #

source
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 = ⊤) :
↑(subgroup.closure ((λ (g : G), g * (↑(subgroup.mem_right_transversals.to_fun hR g))⁻¹) '' (R * S))) * R = ⊤
source
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 = ⊤) :
subgroup.closure ((λ (g : G), g * (↑(subgroup.mem_right_transversals.to_fun hR g))⁻¹) '' (R * S)) = H

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

source
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 = ⊤) :
subgroup.closure ((λ (g : G), ⟨g * (↑(subgroup.mem_right_transversals.to_fun hR g))⁻¹, _⟩) '' (R * 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)⁻¹).

source
theorem subgroup.closure_mul_image_eq_top' {G : Type u_1} [group G] {H : subgroup G} [decidable_eq G] {R S : finset G} (hR : ↑R ∈ subgroup.right_transversals ↑H) (hR1 : 1 ∈ R) (hS : subgroup.closure ↑S = ⊤) :
subgroup.closure ↑(finset.image (λ (g : G), ⟨g * (↑(subgroup.mem_right_transversals.to_fun hR g))⁻¹, _⟩) (R * S)) = ⊤

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

source
theorem subgroup.exists_finset_card_le_mul {G : Type u_1} [group G] (H : subgroup G) [H.finite_index] {S : finset G} (hS : subgroup.closure ↑S = ⊤) :
∃ (T : finset ↥H), T.card ≤ H.index * S.card ∧ subgroup.closure ↑T = ⊤
source
@[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] :
group.fg ↥H

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

source
theorem subgroup.rank_le_index_mul_rank {G : Type u_1} [group G] (H : subgroup G) [hG : group.fg G] [H.finite_index] :
group.rank ↥H ≤ H.index * group.rank G
source
theorem subgroup.card_commutator_dvd_index_center_pow (G : Type u_1) [group G] [finite ↥(commutator_set G)] :
nat.card ↥(commutator G) ∣ (subgroup.center G).index ^ ((subgroup.center G).index * nat.card ↥(commutator_set 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.card_commutator_bound (n : ℕ) :
ℕ

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

Equations
source
theorem subgroup.card_commutator_le_of_finite_commutator_set (G : Type u_1) [group G] [finite ↥(commutator_set G)] :
nat.card ↥(commutator G) ≤ subgroup.card_commutator_bound (nat.card ↥(commutator_set G))

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

source
@[protected, instance]
def subgroup.commutator.finite (G : Type u_1) [group G] [finite ↥(commutator_set G)] :
finite ↥(commutator G)

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