feat(group_theory/perm/*): Generating S_n (#7211)

This PR proves several lemmas about generating S_n, culminating in the following result:
If H is a subgroup of S_p, and if H has cardinality divisible by p, and if H contains a transposition, then H is all of S_p.



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

src/group_theory/perm/cycle_type.lean

@@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 -/
 
-import group_theory.perm.cycles
 import combinatorics.partition
 import data.multiset.gcd
+import group_theory.perm.cycles
+import group_theory.sylow
 
 /-!
 # Cycle Types
@@ -223,6 +224,22 @@ begin
   exact one_lt_two,
 end
 
+lemma subgroup_eq_top_of_swap_mem [decidable_eq α] {H : subgroup (perm α)}
+  [d : decidable_pred (∈ H)] {τ : perm α} (h0 : (fintype.card α).prime)
+  (h1 : fintype.card α ∣ fintype.card H) (h2 : τ ∈ H) (h3 : is_swap τ) :
+  H = ⊤ :=
+begin
+  haveI : fact (fintype.card α).prime := ⟨h0⟩,
+  obtain ⟨σ, hσ⟩ := sylow.exists_prime_order_of_dvd_card (fintype.card α) h1,
+  have hσ1 : order_of (σ : perm α) = fintype.card α := (order_of_subgroup σ).trans hσ,
+  have hσ2 : is_cycle ↑σ := is_cycle_of_prime_order'' h0 hσ1,
+  have hσ3 : (σ : perm α).support = ⊤ :=
+    finset.eq_univ_of_card (σ : perm α).support ((order_of_is_cycle hσ2).symm.trans hσ1),
+  have hσ4 : subgroup.closure {↑σ, τ} = ⊤ := closure_prime_cycle_swap h0 hσ2 hσ3 h3,
+  rw [eq_top_iff, ←hσ4, subgroup.closure_le, set.insert_subset, set.singleton_subset_iff],
+  exact ⟨subtype.mem σ, h2⟩,
+end
+
 section partition
 
 variables [decidable_eq α]

src/group_theory/perm/cycles.lean

@@ -22,6 +22,17 @@ The following two definitions require that `β` is a `fintype`:
 * `equiv.perm.cycle_factors`: `f.cycle_factors` is a list of disjoint cyclic permutations that
   multiply to `f`.
 
+## Main results
+
+* This file contains several closure results:
+  - `closure_is_cycle` : The symmetric group is generated by cycles
+  - `closure_cycle_adjacent_swap` : The symmetric group is generated by
+    a cycle and an adjacent transposition
+  - `closure_cycle_coprime_swap` : The symmetric group is generated by
+    a cycle and a coprime transposition
+  - `closure_prime_cycle_swap` : The symmetric group is generated by
+    a prime cycle and a transposition
+
 -/
 namespace equiv.perm
 open equiv function finset
@@ -47,12 +58,18 @@ lemma is_cycle.two_le_card_support {f : perm α} (h : is_cycle f) :
   2 ≤ f.support.card :=
 two_le_card_support_of_ne_one h.ne_one
 
-lemma is_cycle.swap {α : Type*} [decidable_eq α] {x y : α} (hxy : x ≠ y) : is_cycle (swap x y) :=
+lemma is_cycle_swap {α : Type*} [decidable_eq α] {x y : α} (hxy : x ≠ y) : is_cycle (swap x y) :=
 ⟨y, by rwa swap_apply_right,
   λ a (ha : ite (a = x) y (ite (a = y) x a) ≠ a),
     if hya : y = a then ⟨0, hya⟩
     else ⟨1, by { rw [gpow_one, swap_apply_def], split_ifs at *; cc }⟩⟩
 
+lemma is_swap.is_cycle {α : Type*} [decidable_eq α] {f : perm α} (hf : is_swap f) : is_cycle f :=
+begin
+  obtain ⟨x, y, hxy, rfl⟩ := hf,
+  exact is_cycle_swap hxy,
+end
+
 lemma is_cycle.inv {f : perm β} (hf : is_cycle f) : is_cycle (f⁻¹) :=
 let ⟨x, hx⟩ := hf in
 ⟨x, by { simp only [inv_eq_iff_eq, *, forall_prop_of_true, ne.def] at *, cc },
@@ -437,6 +454,96 @@ begin
       (ih (λ τ hτ, h1 τ (list.mem_cons_of_mem σ hτ)) (list.pairwise_of_pairwise_cons h2)) },
 end
 
+section generation
+
+variables [fintype α] [fintype β]
+
+open subgroup
+
+lemma closure_is_cycle : closure {σ : perm β | is_cycle σ} = ⊤ :=
+begin
+  classical,
+  exact top_le_iff.mp (le_trans (ge_of_eq closure_is_swap) (closure_mono (λ _, is_swap.is_cycle))),
+end
+
+lemma closure_cycle_adjacent_swap {σ : perm α} (h1 : is_cycle σ) (h2 : σ.support = ⊤) (x : α) :
+  closure ({σ, swap x (σ x)} : set (perm α)) = ⊤ :=
+begin
+  let H := closure ({σ, swap x (σ x)} : set (perm α)),
+  have h3 : σ ∈ H := subset_closure (set.mem_insert σ _),
+  have h4 : swap x (σ x) ∈ H := subset_closure (set.mem_insert_of_mem _ (set.mem_singleton _)),
+  have step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ^(n+1)) x) ∈ H,
+  { intro n,
+    induction n with n ih,
+    { exact subset_closure (set.mem_insert_of_mem _ (set.mem_singleton _)) },
+    { convert H.mul_mem (H.mul_mem h3 ih) (H.inv_mem h3),
+      rw [mul_swap_eq_swap_mul, mul_inv_cancel_right], refl } },
+  have step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H,
+  { intro n,
+    induction n with n ih,
+    { convert H.one_mem,
+      exact swap_self x },
+    { by_cases h5 : x = (σ ^ n) x,
+      { rw [pow_succ, mul_apply, ←h5], exact h4 },
+      by_cases h6 : x = (σ^(n+1)) x,
+      { rw [←h6, swap_self], exact H.one_mem },
+      rw [swap_comm, ←swap_mul_swap_mul_swap h5 h6],
+      exact H.mul_mem (H.mul_mem (step1 n) ih) (step1 n) } },
+  have step3 : ∀ (y : α), swap x y ∈ H,
+  { intro y,
+    have hx : x ∈ (⊤ : finset α) := finset.mem_univ x,
+    rw [←h2, mem_support] at hx,
+    have hy : y ∈ (⊤ : finset α) := finset.mem_univ y,
+    rw [←h2, mem_support] at hy,
+    cases is_cycle.exists_pow_eq h1 hx hy with n hn,
+    rw ← hn,
+    exact step2 n },
+  have step4 : ∀ (y z : α), swap y z ∈ H,
+  { intros y z,
+    by_cases h5 : z = x,
+    { rw [h5, swap_comm], exact step3 y },
+    by_cases h6 : z = y,
+    { rw [h6, swap_self], exact H.one_mem },
+    rw [←swap_mul_swap_mul_swap h5 h6, swap_comm z x],
+    exact H.mul_mem (H.mul_mem (step3 y) (step3 z)) (step3 y) },
+  rw [eq_top_iff, ←closure_is_swap, closure_le],
+  rintros τ ⟨y, z, h5, h6⟩,
+  rw h6,
+  exact step4 y z,
+end
+
+lemma closure_cycle_coprime_swap {n : ℕ} {σ : perm α} (h0 : nat.coprime n (fintype.card α))
+  (h1 : is_cycle σ) (h2 : σ.support = finset.univ) (x : α) :
+  closure ({σ, swap x ((σ ^ n) x)} : set (perm α)) = ⊤ :=
+begin
+  rw [←finset.card_univ, ←h2, ←order_of_is_cycle h1] at h0,
+  cases exists_pow_eq_self_of_coprime h0 with m hm,
+  have h2' : (σ ^ n).support = ⊤ := eq.trans (support_pow_coprime h0) h2,
+  have h1' : is_cycle ((σ ^ n) ^ (m : ℤ)) := by rwa ← hm at h1,
+  replace h1' : is_cycle (σ ^ n) := is_cycle_of_is_cycle_pow h1'
+    (le_trans (support_pow_le σ n) (ge_of_eq (congr_arg support hm))),
+  rw [eq_top_iff, ←closure_cycle_adjacent_swap h1' h2' x, closure_le, set.insert_subset],
+  exact ⟨subgroup.pow_mem (closure _) (subset_closure (set.mem_insert σ _)) n,
+    set.singleton_subset_iff.mpr (subset_closure (set.mem_insert_of_mem _ (set.mem_singleton _)))⟩,
+end
+
+lemma closure_prime_cycle_swap {σ τ : perm α} (h0 : (fintype.card α).prime) (h1 : is_cycle σ)
+  (h2 : σ.support = finset.univ) (h3 : is_swap τ) : closure ({σ, τ} : set (perm α)) = ⊤ :=
+begin
+  obtain ⟨x, y, h4, h5⟩ := h3,
+  obtain ⟨i, hi⟩ := h1.exists_pow_eq (mem_support.mp
+  ((finset.ext_iff.mp h2 x).mpr (finset.mem_univ x)))
+    (mem_support.mp ((finset.ext_iff.mp h2 y).mpr (finset.mem_univ y))),
+  rw [h5, ←hi],
+  refine closure_cycle_coprime_swap (nat.coprime.symm
+    (h0.coprime_iff_not_dvd.mpr (λ h, h4 _))) h1 h2 x,
+  cases h with m hm,
+  rwa [hm, pow_mul, ←finset.card_univ, ←h2, ←order_of_is_cycle h1,
+    pow_order_of_eq_one, one_pow, one_apply] at hi,
+end
+
+end generation
+
 section
 variables [fintype α] {σ τ : perm α}
 

src/group_theory/perm/sign.lean

@@ -292,6 +292,14 @@ lemma support_pow_le (σ : perm α) (n : ℤ) :
   (σ ^ n).support ≤ σ.support :=
 λ x h1, mem_support.mpr (λ h2, mem_support.mp h1 (gpow_apply_eq_self_of_apply_eq_self h2 n))
 
+lemma support_pow_coprime {σ : perm α} {n : ℕ} (h : nat.coprime n (order_of σ)) :
+  (σ ^ n).support = σ.support :=
+begin
+  obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h,
+  exact le_antisymm (support_pow_le σ n) (le_trans (ge_of_eq (congr_arg support hm))
+    (support_pow_le (σ ^ n) m)),
+end
+
 @[simp] lemma support_inv (σ : perm α) : support (σ⁻¹) = σ.support :=
 by simp_rw [finset.ext_iff, mem_support, not_iff_not,
   (inv_eq_iff_eq).trans eq_comm, iff_self, imp_true_iff]
@@ -445,15 +453,12 @@ begin
       (ih _ ⟨rfl, λ v hv, hl.2 _ (list.mem_cons_of_mem _ hv)⟩ h1 hmul_swap) }
 end
 
-lemma closure_swaps_eq_top [fintype α] :
-  subgroup.closure {σ : perm α | is_swap σ} = ⊤ :=
+lemma closure_is_swap [fintype α] : subgroup.closure {σ : perm α | is_swap σ} = ⊤ :=
 begin
-  ext σ,
-  simp only [subgroup.mem_top, iff_true],
-  apply swap_induction_on σ,
-  { exact subgroup.one_mem _ },
-  { intros σ a b ab hσ,
-    refine subgroup.mul_mem _ (subgroup.subset_closure ⟨_, _, ab, rfl⟩) hσ }
+  refine eq_top_iff.mpr (λ x hx, _),
+  obtain ⟨h1, h2⟩ := subtype.mem (trunc_swap_factors x).out,
+  rw ← h1,
+  exact subgroup.list_prod_mem _ (λ y hy, subgroup.subset_closure (h2 y hy)),
 end
 
 /-- Like `swap_induction_on`, but with the composition on the right of `f`.