feat(group_theory/perm/cycle_type): Fixed points of permutations of p…

…rime order (#8832)

A few basic lemmas about fixed points of permutations of prime order.

src/group_theory/perm/cycle_type.lean

@@ -317,6 +317,39 @@ end
 
 end cycle_type
 
+lemma card_compl_support_modeq [decidable_eq α] {p n : ℕ} [hp : fact p.prime] {σ : perm α}
+  (hσ : σ ^ p ^ n = 1) : σ.supportᶜ.card ≡ fintype.card α [MOD p] :=
+begin
+  rw [nat.modeq_iff_dvd' σ.supportᶜ.card_le_univ, ←finset.card_compl, compl_compl],
+  refine (congr_arg _ σ.sum_cycle_type).mp (multiset.dvd_sum (λ k hk, _)),
+  obtain ⟨m, -, hm⟩ := (nat.dvd_prime_pow hp.out).mp (order_of_dvd_of_pow_eq_one hσ),
+  obtain ⟨l, -, rfl⟩ := (nat.dvd_prime_pow hp.out).mp
+    ((congr_arg _ hm).mp (dvd_of_mem_cycle_type hk)),
+  exact dvd_pow (dvd_refl p) (λ h, ne_of_lt (one_lt_of_mem_cycle_type hk) (by rw [h, pow_zero])),
+end
+
+lemma exists_fixed_point_of_prime {p n : ℕ} [hp : fact p.prime] (hα : ¬ p ∣ fintype.card α)
+  {σ : perm α} (hσ : σ ^ p ^ n = 1) : ∃ a : α, σ a = a :=
+begin
+  classical,
+  contrapose! hα,
+  simp_rw ← mem_support at hα,
+  exact nat.modeq_zero_iff_dvd.mp ((congr_arg _ (finset.card_eq_zero.mpr (compl_eq_bot.mpr
+    (finset.eq_univ_iff_forall.mpr hα)))).mp (card_compl_support_modeq hσ).symm),
+end
+
+lemma exists_fixed_point_of_prime' {p n : ℕ} [hp : fact p.prime] (hα : p ∣ fintype.card α)
+  {σ : perm α} (hσ : σ ^ p ^ n = 1) {a : α} (ha : σ a = a) : ∃ b : α, σ b = b ∧ b ≠ a :=
+begin
+  classical,
+  have h : ∀ b : α, b ∈ σ.supportᶜ ↔ σ b = b :=
+  λ b, by rw [finset.mem_compl, mem_support, not_not],
+  obtain ⟨b, hb1, hb2⟩ := finset.exists_ne_of_one_lt_card (lt_of_lt_of_le hp.out.one_lt
+    (nat.le_of_dvd (finset.card_pos.mpr ⟨a, (h a).mpr ha⟩) (nat.modeq_zero_iff_dvd.mp
+    ((card_compl_support_modeq hσ).trans (nat.modeq_zero_iff_dvd.mpr hα))))) a,
+  exact ⟨b, (h b).mp hb1, hb2⟩,
+end
+
 lemma is_cycle_of_prime_order' {σ : perm α} (h1 : (order_of σ).prime)
   (h2 : fintype.card α < 2 * (order_of σ)) : σ.is_cycle :=
 begin