English
Let G be a group, H a subgroup, R a right transversal of H with 1 ∈ R, and let G be generated by a set S. Then H is generated by the elements g (h_R(g))^{-1} as g runs over the product set R · S.
Русский
Пусть G — группа, H — подпгруппа, R — правая транспедукция H в G с 1 ∈ R, и G порождается множеством S. Тогда H порождается элементами g (h_R(g))^{-1} при каждом g ∈ R · S.
LaTeX
$$$\\overline{\\langle (R*S) \\mapsto g \\cdot (h_R(g))^{-1} \\;:\\; g \\in R*S \\rangle} = H$$$
Lean4
/-- **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 * (hR.toRightFun g)⁻¹)`. -/
theorem closure_mul_image_eq (hR : IsComplement H R) (hR1 : (1 : G) ∈ R) (hS : closure S = ⊤) :
closure ((R * S).image fun g => g * (hR.toRightFun g : G)⁻¹) = H :=
by
have hU : closure ((R * S).image fun g => g * (hR.toRightFun g : G)⁻¹) ≤ H :=
by
rw [closure_le]
rintro - ⟨g, -, rfl⟩
exact hR.mul_inv_toRightFun_mem g
refine le_antisymm hU fun h hh => ?_
obtain ⟨g, hg, r, hr, rfl⟩ := show h ∈ _ from eq_top_iff.mp (closure_mul_image_mul_eq_top hR hR1 hS) (mem_top h)
suffices (⟨r, hr⟩ : R) = (⟨1, hR1⟩ : R) by simpa only [show r = 1 from Subtype.ext_iff.mp this, mul_one]
apply (isComplement_iff_existsUnique_mul_inv_mem.mp hR r).unique
· rw [Subtype.coe_mk, mul_inv_cancel]
exact H.one_mem
· rw [Subtype.coe_mk, inv_one, mul_one]
exact (H.mul_mem_cancel_left (hU hg)).mp hh
