[Merged by Bors] - feat(group_theory/perm/*): facts about the cardinality of the support of a permutation

docs/undergrad.yaml

@@ -98,7 +98,7 @@ Group Theory:
   Permutation group:
     permutation group of a type: 'equiv.perm'
     decomposition into transpositions: ''
-    decomposition into cycles with disjoint support: 'equiv.perm.cycle_factors'
+    decomposition into cycles with disjoint support: 'equiv.perm.trunc_cycle_factors'
     signature: 'equiv.perm.sign'
     alternating group: ''
   Classical automorphism groups:

src/group_theory/perm/cycles.lean

@@ -39,6 +39,13 @@ variables [fintype α]
   application of the permutation. -/
 def is_cycle (f : perm β) : Prop := ∃ x, f x ≠ x ∧ ∀ y, f y ≠ y → ∃ i : ℤ, (f ^ i) x = y
 
+lemma is_cycle.ne_one {f : perm β} (h : is_cycle f) : f ≠ 1 :=
+λ hf, by simpa [hf, is_cycle] using h
+
+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) :=
 ⟨y, by rwa swap_apply_right,
   λ a (ha : ite (a = x) y (ite (a = y) x a) ≠ a),
@@ -207,15 +214,16 @@ lemma is_cycle.same_cycle {f : perm β} (hf : is_cycle f) {x y : β}
   (hx : f x ≠ x) (hy : f y ≠ y) : same_cycle f x y :=
 hf.exists_gpow_eq hx hy
 
-noncomputable instance [fintype α] (f : perm α) : decidable_rel (same_cycle f) :=
-λ x y, decidable_of_iff (∃ n ∈ list.range (order_of f), (f ^ n) x = y)
+instance [fintype α] (f : perm α) : decidable_rel (same_cycle f) :=
+λ x y, decidable_of_iff (∃ n ∈ list.range (fintype.card (perm α)), (f ^ n) x = y)
 ⟨λ ⟨n, _, hn⟩, ⟨n, hn⟩, λ ⟨i, hi⟩, ⟨(i % order_of f).nat_abs, list.mem_range.2
   (int.coe_nat_lt.1 $
     by { rw int.nat_abs_of_nonneg (int.mod_nonneg _
         (int.coe_nat_ne_zero_iff_pos.2 (order_of_pos _))),
-      calc _ < _ : int.mod_lt _ (int.coe_nat_ne_zero_iff_pos.2 (order_of_pos _))
-          ... = _ : by simp,
-          exact fintype_perm, }),
+      { apply lt_of_lt_of_le (int.mod_lt _ (int.coe_nat_ne_zero_iff_pos.2 (order_of_pos _))),
+        { simp [order_of_le_card_univ] },
+        exact fintype_perm },
+      exact fintype_perm, }),
   by { rw [← gpow_coe_nat, int.nat_abs_of_nonneg (int.mod_nonneg _
       (int.coe_nat_ne_zero_iff_pos.2 (order_of_pos _))), ← gpow_eq_mod_order_of, hi],
     exact fintype_perm }⟩⟩
@@ -244,7 +252,7 @@ by rw [← same_cycle_inv, same_cycle_apply, same_cycle_inv]
 -/
 
 /-- `f.cycle_of x` is the cycle of the permutation `f` to which `x` belongs. -/
-noncomputable def cycle_of [fintype α] (f : perm α) (x : α) : perm α :=
+def cycle_of [fintype α] (f : perm α) (x : α) : perm α :=
 of_subtype (@subtype_perm _ f (same_cycle f x) (λ _, same_cycle_apply.symm))
 
 lemma cycle_of_apply [fintype α] (f : perm α) (x y : α) :
@@ -303,7 +311,7 @@ have cycle_of f x x ≠ x, by rwa [(same_cycle.refl _ _).cycle_of_apply],
 
 /-- Given a list `l : list α` and a permutation `f : perm α` whose nonfixed points are all in `l`,
   recursively factors `f` into cycles. -/
-noncomputable def cycle_factors_aux [fintype α] : Π (l : list α) (f : perm α),
+def cycle_factors_aux [fintype α] : Π (l : list α) (f : perm α),
   (∀ {x}, f x ≠ x → x ∈ l) →
   {l : list (perm α) // l.prod = f ∧ (∀ g ∈ l, is_cycle g) ∧ l.pairwise disjoint}
 | []     f h := ⟨[], by { simp only [imp_false, list.pairwise.nil, list.not_mem_nil, forall_const,
@@ -337,34 +345,51 @@ else let ⟨m, hm₁, hm₂, hm₃⟩ := cycle_factors_aux l ((cycle_of f x)⁻
         hm₃⟩⟩
 
 /-- Factors a permutation `f` into a list of disjoint cyclic permutations that multiply to `f`. -/
-noncomputable def cycle_factors [fintype α] [linear_order α] (f : perm α) :
+def cycle_factors [fintype α] [linear_order α] (f : perm α) :
   {l : list (perm α) // l.prod = f ∧ (∀ g ∈ l, is_cycle g) ∧ l.pairwise disjoint} :=
 cycle_factors_aux (univ.sort (≤)) f (λ _ _, (mem_sort _).2 (mem_univ _))
 
+/-- Factors a permutation `f` into a list of disjoint cyclic permutations that multiply to `f`,
+  without a linear order. -/
+def trunc_cycle_factors [fintype α] (f : perm α) :
+  trunc {l : list (perm α) // l.prod = f ∧ (∀ g ∈ l, is_cycle g) ∧ l.pairwise disjoint} :=
+quotient.rec_on_subsingleton (@univ α _).1
+  (λ l h, trunc.mk (cycle_factors_aux l f h))
+  (show ∀ x, f x ≠ x → x ∈ (@univ α _).1, from λ _ _, mem_univ _)
+
+@[elab_as_eliminator] lemma cycle_induction_on [fintype β] {P : perm β → Prop} (σ : perm β)
+  (base_one : P 1) (base_cycles : ∀ σ : perm β, σ.is_cycle → P σ)
+  (induction_disjoint : ∀ σ τ : perm β, disjoint σ τ → P σ → P τ → P (σ * τ)) :
+  P σ :=
+begin
+  classical,
+  suffices :
+    ∀ l : list (perm β), (∀ τ : perm β, τ ∈ l → τ.is_cycle) → l.pairwise disjoint → P l.prod,
+  { let x := σ.trunc_cycle_factors.out,
+    exact (congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2) },
+  intro l,
+  induction l with σ l ih,
+  { exact λ _ _, base_one },
+  { intros h1 h2,
+    rw list.prod_cons,
+    exact induction_disjoint σ l.prod
+      (disjoint_prod_list_of_disjoint (list.pairwise_cons.mp h2).1)
+      (base_cycles σ (h1 σ (l.mem_cons_self σ)))
+      (ih (λ τ hτ, h1 τ (list.mem_cons_of_mem σ hτ)) (list.pairwise_of_pairwise_cons h2)) },
+end
+
 section fixed_points
 
 /-!
 ### Fixed points
 -/
 
-lemma one_lt_nonfixed_point_card_of_ne_one [fintype α] {σ : perm α} (h : σ ≠ 1) :
-  1 < (filter (λ x, σ x ≠ x) univ).card :=
-begin
-  rw one_lt_card_iff,
-  contrapose! h,
-  ext x,
-  dsimp,
-  have := h (σ x) x,
-  contrapose! this,
-  simpa,
-end
-
 lemma fixed_point_card_lt_of_ne_one [fintype α] {σ : perm α} (h : σ ≠ 1) :
   (filter (λ x, σ x = x) univ).card < fintype.card α - 1 :=
 begin
   rw [nat.lt_sub_left_iff_add_lt, ← nat.lt_sub_right_iff_add_lt, ← finset.card_compl,
     finset.compl_filter],
-  exact one_lt_nonfixed_point_card_of_ne_one h
+  exact one_lt_card_support_of_ne_one h
 end
 
 end fixed_points

src/group_theory/perm/sign.lean

@@ -207,16 +207,56 @@ lemma gpow_apply_eq_of_apply_apply_eq_self {f : perm α} {x : α} (hffx : f (f x
 
 variable [decidable_eq α]
 
+section fintype
+variable [fintype α]
+
 /-- The `finset` of nonfixed points of a permutation. -/
-def support [fintype α] (f : perm α) : finset α := univ.filter (λ x, f x ≠ x)
+def support (f : perm α) : finset α := univ.filter (λ x, f x ≠ x)
+
+@[simp] lemma mem_support {f : perm α} {x : α} : x ∈ f.support ↔ f x ≠ x :=
+by rw [support, mem_filter, and_iff_right (mem_univ x)]
 
-@[simp] lemma mem_support [fintype α] {f : perm α} {x : α} : x ∈ f.support ↔ f x ≠ x :=
-by simp only [support, true_and, mem_filter, mem_univ]
+@[simp] lemma support_eq_empty_iff {σ : perm α} : σ.support = ∅ ↔ σ = 1 :=
+by simp_rw [finset.ext_iff, mem_support, finset.not_mem_empty, iff_false, not_not,
+  equiv.perm.ext_iff, one_apply]
+
+@[simp] lemma support_one : (1 : perm α).support = ∅ :=
+by rw support_eq_empty_iff
+
+lemma support_mul_le (f g : perm α) :
+  (f * g).support ≤ f.support ∪ g.support :=
+λ x, begin
+  rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ←not_and_distrib, not_imp_not],
+  rintro ⟨hf, hg⟩,
+  rw [hg, hf]
+end
 
-lemma support_pow_le [fintype α] (σ : perm α) (n : ℤ) :
+lemma exists_mem_support_of_mem_support_prod {l : list (perm α)} {x : α}
+  (hx : x ∈ l.prod.support) :
+  ∃ f : perm α, f ∈ l ∧ x ∈ f.support :=
+begin
+  contrapose! hx,
+  simp_rw [mem_support, not_not] at hx ⊢,
+  induction l with f l ih generalizing hx,
+  { refl },
+  { rw [list.prod_cons, mul_apply, ih (λ g hg, hx g (or.inr hg)), hx f (or.inl rfl)] },
+end
+
+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))
 
+@[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]
+
+@[simp]
+lemma apply_mem_support {f : perm α} {x : α} :
+  f x ∈ f.support ↔ x ∈ f.support :=
+by rw [mem_support, mem_support, ne.def, ne.def, not_iff_not, apply_eq_iff_eq]
+
+end fintype
+
 /-- `f.is_swap` indicates that the permutation `f` is a transposition of two elements. -/
 def is_swap (f : perm α) : Prop := ∃ x y, x ≠ y ∧ f = swap x y
 
@@ -240,7 +280,10 @@ begin
   { split_ifs at hy; cc }
 end
 
-lemma support_swap_mul_eq [fintype α] {f : perm α} {x : α}
+section fintype
+variables [fintype α]
+
+lemma support_swap_mul_eq {f : perm α} {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 $ λ y,
@@ -252,12 +295,44 @@ finset.ext $ λ y,
   λ hy, by simp only [mem_erase, mem_support, swap_apply_def, mul_apply] at *;
     intro; split_ifs at *; simp only [*, eq_self_iff_true, not_true, ne.def] at *⟩
 
-lemma card_support_swap_mul [fintype α] {f : perm α} {x : α}
+@[simp]
+lemma card_support_eq_zero {f : perm α} :
+  f.support.card = 0 ↔ f = 1 :=
+by rw [finset.card_eq_zero, support_eq_empty_iff]
+
+lemma one_lt_card_support_of_ne_one {f : perm α} (h : f ≠ 1) :
+  1 < f.support.card :=
+begin
+  simp_rw [one_lt_card_iff, mem_support, ←not_or_distrib],
+  contrapose! h,
+  ext a,
+  specialize h (f a) a,
+  rwa [apply_eq_iff_eq, or_self, or_self] at h,
+end
+
+lemma card_support_ne_one (f : perm α) : f.support.card ≠ 1 :=
+begin
+  by_cases h : f = 1,
+  { exact ne_of_eq_of_ne (card_support_eq_zero.mpr h) zero_ne_one },
+  { exact ne_of_gt (one_lt_card_support_of_ne_one h) },
+end
+
+@[simp] lemma card_support_le_one {f : perm α} : f.support.card ≤ 1 ↔ f = 1 :=
+by rw [le_iff_lt_or_eq, nat.lt_succ_iff, nat.le_zero_iff, card_support_eq_zero,
+  or_iff_not_imp_right, imp_iff_right f.card_support_ne_one]
+
+lemma two_le_card_support_of_ne_one {f : perm α} (h : f ≠ 1) :
+  2 ≤ f.support.card :=
+one_lt_card_support_of_ne_one h
+
+lemma card_support_swap_mul {f : perm α} {x : α}
   (hx : f x ≠ x) : (swap x (f x) * f).support.card < f.support.card :=
 finset.card_lt_card
   ⟨λ z hz, mem_support.2 (ne_and_ne_of_swap_mul_apply_ne_self (mem_support.1 hz)).1,
     λ h, absurd (h (mem_support.2 hx)) (mt mem_support.1 (by simp))⟩
 
+end fintype
+
 /-- Given a list `l : list α` and a permutation `f : perm α` such that the nonfixed points of `f`
   are in `l`, recursively factors `f` as a product of transpositions. -/
 def swap_factors_aux : Π (l : list α) (f : perm α), (∀ {x}, f x ≠ x → x ∈ l) →
@@ -666,6 +741,27 @@ lemma card_support_swap {x y : α} (hxy : x ≠ y) : (swap x y).support.card = 2
 show (swap x y).support.card = finset.card ⟨x ::ₘ y ::ₘ 0, by simp [hxy]⟩,
 from congr_arg card $ by simp [support_swap hxy, *, finset.ext_iff]
 
+@[simp]
+lemma card_support_eq_two {f : perm α} : f.support.card = 2 ↔ is_swap f :=
+begin
+  split; intro h,
+  { obtain ⟨x, t, hmem, hins, ht⟩ := card_eq_succ.1 h,
+    obtain ⟨y, rfl⟩ := card_eq_one.1 ht,
+    rw mem_singleton at hmem,
+    refine ⟨x, y, hmem, _⟩,
+    ext a,
+    have key : ∀ b, f b ≠ b ↔ _ := λ b, by rw [←mem_support, ←hins, mem_insert, mem_singleton],
+    by_cases ha : f a = a,
+    { have ha' := not_or_distrib.mp (mt (key a).mpr (not_not.mpr ha)),
+      rw [ha, swap_apply_of_ne_of_ne ha'.1 ha'.2] },
+    { have ha' := (key (f a)).mp (mt f.apply_eq_iff_eq.mp ha),
+      obtain rfl | rfl := ((key a).mp ha),
+      { rw [or.resolve_left ha' ha, swap_apply_left] },
+      { rw [or.resolve_right ha' ha, swap_apply_right] } } },
+  { obtain ⟨x, y, hxy, rfl⟩ := h,
+    exact card_support_swap hxy }
+end
+
 /-- If we apply `prod_extend_right a (σ a)` for all `a : α` in turn,
 we get `prod_congr_right σ`. -/
 lemma prod_prod_extend_right {α : Type*} [decidable_eq α] (σ : α → perm β)
@@ -760,4 +856,55 @@ end congr
 
 end sign
 
+section disjoint
+variables [fintype α] {f g : perm α}
+
+lemma disjoint_iff_disjoint_support :
+  disjoint f g ↔ _root_.disjoint f.support g.support :=
+begin
+  change (∀ x, f x = x ∨ g x = x) ↔ (∀ x, x ∉ (f.support ∩ g.support)),
+  simp_rw [finset.mem_inter, not_and_distrib, mem_support, not_not],
+end
+
+lemma disjoint.disjoint_support (h : disjoint f g) :
+  _root_.disjoint f.support g.support :=
+disjoint_iff_disjoint_support.1 h
+
+lemma disjoint.support_mul (h : disjoint f g) :
+  (f * g).support = f.support ∪ g.support :=
+begin
+  refine le_antisymm (support_mul_le _ _) (λ a, _),
+  rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ←not_and_distrib, not_imp_not],
+  exact (h a).elim (λ hf h, ⟨hf, f.apply_eq_iff_eq.mp (h.trans hf.symm)⟩)
+    (λ hg h, ⟨(congr_arg f hg).symm.trans h, hg⟩),
+end
+
+lemma disjoint.card_support_mul (h : disjoint f g) :
+  (f * g).support.card = f.support.card + g.support.card :=
+(congr_arg card h.support_mul).trans (finset.card_disjoint_union h.disjoint_support)
+
+lemma disjoint_prod_list_of_disjoint [fintype β] {f : perm β} {l : list (perm β)}
+  (h : ∀ g, g ∈ l → disjoint f g) : disjoint f l.prod :=
+begin
+  classical,
+  intro x,
+  by_cases hx : l.prod x = x,
+  { exact or.inr hx },
+  { obtain ⟨f, fl, fx⟩ := exists_mem_support_of_mem_support_prod (mem_support.mpr hx),
+    exact (h f fl x).imp_right (λ fx', ((mem_support.mp fx) fx').elim) }
+end
+
+lemma card_support_prod_list_of_pairwise_disjoint {l : list (perm α)}
+  (h : l.pairwise disjoint) :
+  l.prod.support.card = (l.map (finset.card ∘ support)).sum :=
+begin
+  induction l with a t ih,
+  { exact card_support_eq_zero.mpr rfl, },
+  { obtain ⟨ha, ht⟩ := list.pairwise_cons.1 h,
+    rw [list.prod_cons, list.map_cons, list.sum_cons, ←ih ht],
+    exact (disjoint_prod_list_of_disjoint ha).card_support_mul }
+end
+
+end disjoint
+
 end equiv.perm