feat(group_theory/perm/cycle/basic): Cycle on a set (#17899)

Define `equiv.perm.is_cycle_on`, a predicate for a permutation to be a cycle on a set.

This has two discrepancies with the existing `equiv.perm.is_cycle_on` (apart from the obvious one that `is_cycle_on` is restricted to a set):
* `is_cycle_on` forbids fixed points (on `s`) while `is_cycle` allows them.
* `is_cycle` forbids the identity while `is_cycle_on` allows it.

I think the first one isn't so bad given that `is_cycle` is meant to be used over the entire type (so you can't just rule out fixed points). The second one is more of a worry as I had to case-split on `s.subsingleton ∨ s.nontrivial` in several `is_cycle_on` lemmas to derive them from the corresponding `is_cycle` ones, while of course the `is_cycle` ones would also have held for a weaker version of `is_cycle` that allows the identity.

src/data/set/function.lean

@@ -1449,6 +1449,12 @@ lemma inv_on : inv_on e e.symm t s :=
 lemma bij_on_image : bij_on e s (e '' s) := (e.injective.inj_on _).bij_on_image
 lemma bij_on_symm_image : bij_on e.symm (e '' s) s := e.bij_on_image.symm e.inv_on
 
+variables {e}
+
+@[simp] lemma bij_on_symm : bij_on e.symm t s ↔ bij_on e s t := bij_on_comm e.symm.inv_on
+
+alias bij_on_symm ↔ _root_.set.bij_on.of_equiv_symm _root_.set.bij_on.equiv_symm
+
 variables [decidable_eq α] {a b : α}
 
 lemma bij_on_swap (ha : a ∈ s) (hb : b ∈ s) : bij_on (swap a b) s s :=

src/dynamics/fixed_points/basic.lean

@@ -87,7 +87,7 @@ h.to_left_inverse e.left_inverse_symm
 protected lemma perm_inv (h : is_fixed_pt e x) : is_fixed_pt ⇑(e⁻¹) x := h.equiv_symm
 
 protected lemma perm_pow (h : is_fixed_pt e x) (n : ℕ) : is_fixed_pt ⇑(e ^ n) x :=
-by { rw ←equiv.perm.iterate_eq_pow, exact h.iterate _ }
+by { rw equiv.perm.coe_pow, exact h.iterate _ }
 
 protected lemma perm_zpow (h : is_fixed_pt e x) : ∀ n : ℤ, is_fixed_pt ⇑(e ^ n) x
 | (int.of_nat n) := h.perm_pow _

src/group_theory/perm/basic.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 import algebra.group.pi
 import algebra.group.prod
 import algebra.hom.iterate
+import logic.equiv.set
 
 /-!
 # The group of permutations (self-equivalences) of a type `α`
@@ -67,9 +68,9 @@ lemma inv_def (f : perm α) : f⁻¹ = f.symm := rfl
 
 @[simp, norm_cast] lemma coe_one : ⇑(1 : perm α) = id := rfl
 @[simp, norm_cast] lemma coe_mul (f g : perm α) : ⇑(f * g) = f ∘ g := rfl
-
 @[norm_cast] lemma coe_pow (f : perm α) (n : ℕ) : ⇑(f ^ n) = (f^[n]) :=
 hom_coe_pow _ rfl (λ _ _, rfl) _ _
+@[simp] lemma iterate_eq_pow (f : perm α) (n : ℕ) : (f^[n]) = ⇑(f ^ n) := (coe_pow _ _).symm
 
 lemma eq_inv_iff_eq {f : perm α} {x y : α} : x = f⁻¹ y ↔ f x = y := f.eq_symm_apply
 
@@ -79,9 +80,9 @@ lemma zpow_apply_comm {α : Type*} (σ : perm α) (m n : ℤ) {x : α} :
   (σ ^ m) ((σ ^ n) x) = (σ ^ n) ((σ ^ m) x) :=
 by rw [←equiv.perm.mul_apply, ←equiv.perm.mul_apply, zpow_mul_comm]
 
-@[simp] lemma iterate_eq_pow (f : perm α) : ∀ n, f^[n] = ⇑(f ^ n)
-| 0       := rfl
-| (n + 1) := by { rw [function.iterate_succ, pow_add, iterate_eq_pow], refl }
+@[simp] lemma image_inv (f : perm α) (s : set α) : ⇑f⁻¹ '' s = f ⁻¹' s := f⁻¹.image_eq_preimage _
+@[simp] lemma preimage_inv (f : perm α) (s : set α) : ⇑f⁻¹ ⁻¹' s = f '' s :=
+(f.image_eq_preimage _).symm
 
 /-! Lemmas about mixing `perm` with `equiv`. Because we have multiple ways to express
 `equiv.refl`, `equiv.symm`, and `equiv.trans`, we want simp lemmas for every combination.
@@ -494,3 +495,25 @@ lemma zpow_mul_right : ∀ n : ℤ, equiv.mul_right a ^ n = equiv.mul_right (a ^
 
 end group
 end equiv
+
+open equiv function
+
+namespace set
+variables {α : Type*} {f : perm α} {s t : set α}
+
+@[simp] lemma bij_on_perm_inv : bij_on ⇑f⁻¹ t s ↔ bij_on f s t := equiv.bij_on_symm
+
+alias bij_on_perm_inv ↔ bij_on.of_perm_inv bij_on.perm_inv
+
+lemma maps_to.perm_pow : maps_to f s s → ∀ n : ℕ, maps_to ⇑(f ^ n) s s :=
+by { simp_rw equiv.perm.coe_pow, exact maps_to.iterate }
+lemma surj_on.perm_pow : surj_on f s s → ∀ n : ℕ, surj_on ⇑(f ^ n) s s :=
+by { simp_rw equiv.perm.coe_pow, exact surj_on.iterate }
+lemma bij_on.perm_pow : bij_on f s s → ∀ n : ℕ, bij_on ⇑(f ^ n) s s :=
+by { simp_rw equiv.perm.coe_pow, exact bij_on.iterate }
+
+lemma bij_on.perm_zpow (hf : bij_on f s s) : ∀ n : ℤ, bij_on ⇑(f ^ n) s s
+| (int.of_nat n) := hf.perm_pow _
+| (int.neg_succ_of_nat n) := by { rw zpow_neg_succ_of_nat, exact (hf.perm_pow _).perm_inv }
+
+end set