Schreier's Lemma #
In this file we prove Schreier's lemma.
Main results #
closure_mul_image_eq
: Schreier's Lemma: IfR : set G
is a right_transversal ofH : subgroup G
with1 ∈ R
, and ifG
is generated byS : set G
, thenH
is generated by theset
(R * S).image (λ g, g * (to_fun hR g)⁻¹)
.fg_of_index_ne_zero
: Schreier's Lemma: A finite index subgroup of a finitely generated group is finitely generated.
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 = ⊤) :
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)⁻¹)
.
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)⁻¹)
.
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)⁻¹)
.
theorem
subgroup.rank_le_index_mul_rank
{G : Type u_1}
[group G]
[hG : group.fg G]
{H : subgroup G}
(hH : H.index ≠ 0)
[decidable_pred (λ (n : ℕ), ∃ (S : finset G), S.card = n ∧ subgroup.closure ↑S = ⊤)]
[decidable_pred (λ (n : ℕ), ∃ (S : finset ↥H), S.card = n ∧ subgroup.closure ↑S = ⊤)] :
group.rank ↥H ≤ H.index * group.rank G