feat(group_theory/schreier): prove Schreier's lemma (#13019)

This PR adds a proof of Schreier's lemma.



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

docs/overview.yaml

@@ -42,6 +42,7 @@ General algebra:
     abelianization: 'abelianization'
     free group: 'free_group'
     presented group: 'presented_group'
+    Schreier's lemma: 'subgroup.closure_mul_eq'
     cyclic group: 'is_cyclic'
     nilpotent group: 'group.is_nilpotent'
     permutation group of a type: 'equiv.perm'

src/group_theory/schreier.lean

@@ -0,0 +1,76 @@
+/-
+Copyright (c) 2022 Thomas Browning. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Browning
+-/
+
+import group_theory.complement
+import tactic.group
+
+/-!
+# Schreier's Lemma
+
+In this file we prove Schreier's lemma.
+
+## Main results
+
+- `closure_mul_eq` : **Schreier's Lemma**: If `R` 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 * (mem_right_transversals.to_fun hR g)⁻¹)`.
+-/
+
+open_locale pointwise
+
+namespace subgroup
+
+variables {G : Type*} [group G] {H : subgroup G} {R S : set G}
+
+lemma closure_mul_eq_top
+  (hR : R ∈ right_transversals (H : set G)) (hR1 : (1 : G) ∈ R) (hS : closure S = ⊤) :
+  (closure ((R * S).image (λ g, g * (mem_right_transversals.to_fun hR g)⁻¹)) : set G) * R = ⊤ :=
+begin
+  let f : G → R := λ g, mem_right_transversals.to_fun hR g,
+  let U : set G := (R * S).image (λ g, g * (f g)⁻¹),
+  change (closure U : set G) * R = ⊤,
+  refine top_le_iff.mp (λ g hg, _),
+  apply closure_induction_right (eq_top_iff.mp hS (mem_top g)),
+  { exact ⟨1, 1, (closure U).one_mem, hR1, one_mul 1⟩ },
+  { rintros - s hs ⟨u, r, hu, hr, rfl⟩,
+    rw show u * r * s = u * ((r * s) * (f (r * s))⁻¹) * f (r * s), by group,
+    refine set.mul_mem_mul ((closure U).mul_mem hu _) (f (r * s)).coe_prop,
+    exact subset_closure ⟨r * s, set.mul_mem_mul hr hs, rfl⟩ },
+  { rintros - s hs ⟨u, r, hu, hr, rfl⟩,
+    rw show u * r * s⁻¹ = u * (f (r * s⁻¹) * s * r⁻¹)⁻¹ * f (r * s⁻¹), by group,
+    refine set.mul_mem_mul ((closure U).mul_mem hu ((closure U).inv_mem _)) (f (r * s⁻¹)).2,
+    refine subset_closure ⟨f (r * s⁻¹) * s, set.mul_mem_mul (f (r * s⁻¹)).2 hs, _⟩,
+    rw [mul_right_inj, inv_inj, ←subtype.coe_mk r hr, ←subtype.ext_iff, subtype.coe_mk],
+    apply (mem_right_transversals_iff_exists_unique_mul_inv_mem.mp hR (f (r * s⁻¹) * s)).unique
+      (mem_right_transversals.mul_inv_to_fun_mem hR (f (r * s⁻¹) * s)),
+    rw [mul_assoc, ←inv_inv s, ←mul_inv_rev, inv_inv],
+    exact mem_right_transversals.to_fun_mul_inv_mem hR (r * s⁻¹) },
+end
+
+/-- **Schreier's Lemma**: If `R` 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 * (mem_right_transversals.to_fun hR g)⁻¹)`. -/
+lemma closure_mul_eq
+  (hR : R ∈ right_transversals (H : set G)) (hR1 : (1 : G) ∈ R) (hS : closure S = ⊤) :
+  closure ((R * S).image (λ g, g * (mem_right_transversals.to_fun hR g)⁻¹)) = H :=
+begin
+  have hU : closure ((R * S).image (λ g, g * (mem_right_transversals.to_fun hR g)⁻¹)) ≤ H,
+  { rw closure_le,
+    rintros - ⟨g, -, rfl⟩,
+    exact mem_right_transversals.mul_inv_to_fun_mem hR g },
+  refine le_antisymm hU (λ h hh, _),
+  obtain ⟨g, r, hg, hr, rfl⟩ :=
+  show h ∈ _, from eq_top_iff.mp (closure_mul_eq_top hR hR1 hS) (mem_top h),
+  suffices : (⟨r, hr⟩ : R) = (⟨1, hR1⟩ : R),
+  { rwa [show r = 1, from subtype.ext_iff.mp this, mul_one] },
+  apply (mem_right_transversals_iff_exists_unique_mul_inv_mem.mp hR r).unique,
+  { rw [subtype.coe_mk, mul_inv_self],
+    exact H.one_mem },
+  { rw [subtype.coe_mk, one_inv, mul_one],
+    exact (H.mul_mem_cancel_left (hU hg)).mp hh },
+end
+
+end subgroup