From 68acd760b61ce3b7498438c294114acbb92402fc Mon Sep 17 00:00:00 2001
From: Chris Hughes <chrishughes24@gmail.com>
Date: Sat, 22 Sep 2018 20:42:16 +0100
Subject: [PATCH] feat(group_theory/perm): perm.fintype and card_perm (closed
 #366)

---
 data/fintype.lean      | 123 ++++++++++++++++++++++++++++++++++++++++-
 group_theory/perm.lean |  11 ++--
 2 files changed, 127 insertions(+), 7 deletions(-)

diff --git a/data/fintype.lean b/data/fintype.lean
index 7035b6dbd1439..bdfb97fca8e54 100644
--- a/data/fintype.lean
+++ b/data/fintype.lean
@@ -442,7 +442,6 @@ quotient.lift_on (@quotient.rec_on _ _ (λ l : multiset ι,
   (λ f, ⟦λ i, f i (finset.mem_univ _)⟧)
   (λ a b h, quotient.sound $ λ i, h _ _)
 
-
 theorem quotient.fin_choice_eq {ι : Type*} [fintype ι] [decidable_eq ι]
   {α : ι → Type*} [∀ i, setoid (α i)]
   (f : ∀ i, α i) : quotient.fin_choice (λ i, ⟦f i⟧) = ⟦f⟧ :=
@@ -453,4 +452,124 @@ begin
     exact quotient.induction_on
       (@finset.univ ι _).1 (λ l, quotient.fin_choice_aux_eq _ _) },
   simp [this], exact setoid.refl _
-end
\ No newline at end of file
+end
+
+section equiv
+
+open list equiv equiv.perm
+
+variables [decidable_eq α] [decidable_eq β]
+
+def perms_of_list : list α → list (perm α)
+| []       := [1]
+| (a :: l) := perms_of_list l ++ l.bind (λ b, (perms_of_list l).map (λ f, swap a b * f))
+
+lemma length_perms_of_list : ∀ l : list α, length (perms_of_list l) = l.length.fact
+| []       := rfl
+| (a :: l) := by rw [length_cons, nat.fact_succ];
+  simp [perms_of_list, length_bind, length_perms_of_list, function.comp, nat.succ_mul]
+
+lemma mem_perms_of_list_of_mem : ∀ {l : list α} {f : perm α} (h : ∀ x, f x ≠ x → x ∈ l), f ∈ perms_of_list l
+| []     f h := list.mem_singleton.2 $ equiv.ext _ _$ λ x, by simp [imp_false, *] at *
+| (a::l) f h :=
+if hfa : f a = a
+then
+  mem_append_left _ $ mem_perms_of_list_of_mem
+    (λ x hx, mem_of_ne_of_mem (λ h, by rw h at hx; exact hx hfa) (h x hx))
+else
+have hfa' : f (f a) ≠ f a, from mt (λ h, f.bijective.1 h) hfa,
+have ∀ (x : α), (swap a (f a) * f) x ≠ x → x ∈ l,
+  from λ x hx, have hxa : x ≠ a, from λ h, by simpa [h, mul_apply] using hx,
+    have hfxa : f x ≠ f a, from mt (λ h, f.bijective.1 h) hxa,
+    list.mem_of_ne_of_mem hxa
+      (h x (λ h, by simp [h, mul_apply, swap_apply_def] at hx; split_ifs at hx; cc)),
+suffices f ∈ perms_of_list l ∨ ∃ (b : α), b ∈ l ∧ ∃ g : perm α, g ∈ perms_of_list l ∧ swap a b * g = f,
+  by simpa [perms_of_list],
+(@or_iff_not_imp_left _ _ (classical.prop_decidable _)).2
+  (λ hfl, ⟨f a,
+    if hffa : f (f a) = a then mem_of_ne_of_mem hfa (h _ (mt (λ h, f.bijective.1 h) hfa))
+      else this _ $ by simp [mul_apply, swap_apply_def]; split_ifs; cc,
+    ⟨swap a (f a) * f, mem_perms_of_list_of_mem this,
+      by rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← one_def, one_mul]⟩⟩)
+
+lemma mem_of_mem_perms_of_list : ∀ {l : list α} {f : perm α}, f ∈ perms_of_list l → ∀ {x}, f x ≠ x → x ∈ l
+| []     f h := have f = 1 := by simpa [perms_of_list] using h, by rw this; simp
+| (a::l) f h :=
+(mem_append.1 h).elim
+  (λ h x hx, mem_cons_of_mem _ (mem_of_mem_perms_of_list h hx))
+  (λ h x hx,
+    let ⟨y, hy, hy'⟩ := list.mem_bind.1 h in
+    let ⟨g, hg₁, hg₂⟩ := list.mem_map.1 hy' in
+    if hxa : x = a then by simp [hxa]
+    else if hxy : x = y then mem_cons_of_mem _ $ by rwa hxy
+    else mem_cons_of_mem _ $
+    mem_of_mem_perms_of_list hg₁ $
+      by rw [eq_inv_mul_iff_mul_eq.2 hg₂, mul_apply, swap_inv, swap_apply_def];
+        split_ifs; cc)
+
+lemma mem_perms_of_list_iff {l : list α} {f : perm α} : f ∈ perms_of_list l ↔ ∀ {x}, f x ≠ x → x ∈ l :=
+⟨mem_of_mem_perms_of_list, mem_perms_of_list_of_mem⟩
+
+lemma nodup_perms_of_list : ∀ {l : list α} (hl : l.nodup), (perms_of_list l).nodup
+| []     hl := by simp [perms_of_list]
+| (a::l) hl :=
+have hl' : l.nodup, from nodup_of_nodup_cons hl,
+have hln' : (perms_of_list l).nodup, from nodup_perms_of_list hl',
+have hmeml : ∀ {f : perm α}, f ∈ perms_of_list l → f a = a,
+  from λ f hf, not_not.1 (mt (mem_of_mem_perms_of_list hf) (nodup_cons.1 hl).1),
+by rw [perms_of_list, list.nodup_append, list.nodup_bind, pairwise_iff_nth_le]; exact
+⟨hln', ⟨λ _ _, nodup_map (λ _ _, (mul_left_inj _).1) hln',
+  λ i j hj hij x hx₁ hx₂,
+    let ⟨f, hf⟩ := list.mem_map.1 hx₁ in
+    let ⟨g, hg⟩ := list.mem_map.1 hx₂ in
+    have hix : x a = nth_le l i (lt_trans hij hj),
+      by rw [← hf.2, mul_apply, hmeml hf.1, swap_apply_left],
+    have hiy : x a = nth_le l j hj,
+      by rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left],
+    absurd (hf.2.trans (hg.2.symm)) $
+      λ h, ne_of_lt hij $ nodup_iff_nth_le_inj.1 hl' i j (lt_trans hij hj) hj $
+        by rw [← hix, hiy]⟩,
+  λ f hf₁ hf₂,
+    let ⟨x, hx, hx'⟩ := list.mem_bind.1 hf₂ in
+    let ⟨g, hg⟩ := list.mem_map.1 hx' in
+    have hgxa : g⁻¹ x = a, from f.bijective.1 $
+      by rw [hmeml hf₁, ← hg.2]; simp,
+    have hxa : x ≠ a, from λ h, (list.nodup_cons.1 hl).1 (h ▸ hx),
+    (list.nodup_cons.1 hl).1 $
+      hgxa ▸ mem_of_mem_perms_of_list hg.1 (by rwa [apply_inv_self, hgxa])⟩
+
+def perms_of_finset (s : finset α) : finset (perm α) :=
+quotient.hrec_on s.1 (λ l hl, ⟨perms_of_list l, nodup_perms_of_list hl⟩)
+  (λ a b hab, hfunext (congr_arg _ (quotient.sound hab))
+    (λ ha hb _, heq_of_eq $ finset.ext.2 $
+      by simp [mem_perms_of_list_iff,mem_of_perm hab]))
+  s.2
+
+lemma mem_perms_of_finset_iff : ∀ {s : finset α} {f : perm α},
+  f ∈ perms_of_finset s ↔ ∀ {x}, f x ≠ x → x ∈ s :=
+by rintros ⟨⟨l⟩, hs⟩ f; exact mem_perms_of_list_iff
+
+lemma card_perms_of_finset : ∀ (s : finset α),
+  (perms_of_finset s).card = s.card.fact :=
+by rintros ⟨⟨l⟩, hs⟩; exact length_perms_of_list l
+
+def fintype_perm [fintype α] : fintype (perm α) :=
+⟨perms_of_finset (@finset.univ α _), by simp [mem_perms_of_finset_iff]⟩
+
+instance [fintype α] [fintype β] : fintype (α ≃ β) :=
+if h : fintype.card β = fintype.card α
+then trunc.rec_on_subsingleton (fintype.equiv_fin α)
+  (λ eα, trunc.rec_on_subsingleton (fintype.equiv_fin β)
+    (λ eβ, @fintype.of_equiv _ (perm α) fintype_perm
+      (equiv_congr (equiv.refl α) (eα.trans (eq.rec_on h eβ.symm)) : (α ≃ α) ≃ (α ≃ β))))
+else ⟨∅, λ x, false.elim (h (fintype.card_eq.2 ⟨x.symm⟩))⟩
+
+lemma fintype.card_perm [fintype α] : fintype.card (perm α) = (fintype.card α).fact :=
+subsingleton.elim (@fintype_perm α _ _) (@equiv.fintype α α _ _ _ _) ▸
+card_perms_of_finset _
+
+lemma fintype.card_equiv [fintype α] [fintype β] (e : α ≃ β) :
+  fintype.card (α ≃ β) = (fintype.card α).fact :=
+fintype.card_congr (equiv_congr (equiv.refl α) e) ▸ fintype.card_perm
+
+end equiv
\ No newline at end of file
diff --git a/group_theory/perm.lean b/group_theory/perm.lean
index 4dc0fc5b9b5fb..4fd3b855a8e96 100644
--- a/group_theory/perm.lean
+++ b/group_theory/perm.lean
@@ -6,7 +6,7 @@ Authors: Chris Hughes
 import data.fintype
 
 universes u v
-open equiv function finset fintype
+open equiv function fintype finset
 variables {α : Type u} {β : Type v}
 
 namespace equiv.perm
@@ -545,7 +545,8 @@ lemma is_cycle_swap_mul {f : perm α} (hf : is_cycle f) {x : α}
   is_cycle_swap_mul_aux₂ (i - 1) hf hy hi⟩
 
 lemma support_swap_mul_cycle [fintype α] {f : perm α} (hf : is_cycle f) {x : α}
-  (hx : f x ≠ x) (hffx : f (f x) ≠ x) : (swap x (f x) * f).support = f.support.erase x :=
+  (hffx : f (f x) ≠ x) : (swap x (f x) * f).support = f.support.erase x :=
+have hfx : f x ≠ x, from λ hfx, by simpa [hfx] using hffx,
 finset.ext.2 $ λ y, begin
   have h1 : swap x (f x) * f ≠ 1,
     from λ h1, hffx $ by
@@ -553,7 +554,7 @@ finset.ext.2 $ λ y, begin
       rw ← h1; simp,
   have hfyxor : f y ≠ x ∨ f x ≠ y :=
     not_and_distrib.1 (λ h, h1 $
-      by have := eq_swap_of_is_cycle_of_apply_apply_eq_self hf hx (by rw [h.2, h.1]);
+      by have := eq_swap_of_is_cycle_of_apply_apply_eq_self hf hfx (by rw [h.2, h.1]);
       rw [← this, this, mul_def, swap_swap, one_def]),
   rw [mem_support, mem_erase, mem_support],
   split,
@@ -561,7 +562,7 @@ finset.ext.2 $ λ y, begin
     refine not_or_distrib.1 (λ h₁, h₁.elim
       (λ hyx, by simpa [hyx, mul_apply] using h) _),
     assume hfy,
-    have hyx : x ≠ y := λ h, by rw h at hx; tauto,
+    have hyx : x ≠ y := λ h, by rw h at hfx; tauto,
     have hfyx : f x ≠ y := by rwa [← hfy, ne.def, injective.eq_iff f.bijective.1],
     simpa [mul_apply, hfy, swap_apply_of_ne_of_ne hyx.symm hfyx.symm] using h },
   { assume h,
@@ -592,7 +593,7 @@ calc sign f = sign (swap x (f x) * (swap x (f x) * f)) :
         card_support_swap hx.1.symm]; refl
   else
     have h : card (support (swap x (f x) * f)) + 1 = card (support f),
-      by rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_cycle hf hx.1 h1,
+      by rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_cycle hf h1,
         card_insert_of_not_mem (not_mem_erase _ _)],
     have wf : card (support (swap x (f x) * f)) < card (support f),
       from h ▸ nat.lt_succ_self _,