feat(group_theory/perm/cycles): same_cycle and cycle_of lemmas (#8835)

Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>

src/group_theory/perm/cycles.lean

@@ -327,10 +327,10 @@ def same_cycle (f : perm β) (x y : β) : Prop := ∃ i : ℤ, (f ^ i) x = y
 
 @[refl] lemma same_cycle.refl (f : perm β) (x : β) : same_cycle f x x := ⟨0, rfl⟩
 
-@[symm] lemma same_cycle.symm (f : perm β) {x y : β} : same_cycle f x y → same_cycle f y x :=
+@[symm] lemma same_cycle.symm {f : perm β} {x y : β} : same_cycle f x y → same_cycle f y x :=
 λ ⟨i, hi⟩, ⟨-i, by rw [gpow_neg, ← hi, inv_apply_self]⟩
 
-@[trans] lemma same_cycle.trans (f : perm β) {x y z : β} :
+@[trans] lemma same_cycle.trans {f : perm β} {x y z : β} :
   same_cycle f x y → same_cycle f y z → same_cycle f x z :=
 λ ⟨i, hi⟩ ⟨j, hj⟩, ⟨j + i, by rw [gpow_add, mul_apply, hi, hj]⟩
 
@@ -420,6 +420,14 @@ begin
     rw [←gpow_coe_nat, ←mul_apply, ←gpow_add, int.sub_add_cancel] }
 end
 
+@[simp] lemma same_cycle_gpow_left_iff {f : perm β} {x y : β} {n : ℤ} :
+  same_cycle f ((f ^ n) x) y ↔ same_cycle f x y :=
+begin
+  cases n,
+  { exact same_cycle_pow_left_iff },
+  { rw [gpow_neg_succ_of_nat, ←inv_pow, ←same_cycle_inv, same_cycle_pow_left_iff, same_cycle_inv] }
+end
+
 /-- Unlike `support_congr`, which assumes that `∀ (x ∈ g.support), f x = g x)`, here
 we have the weaker assumption that `∀ (x ∈ f.support), f x = g x`. -/
 lemma is_cycle.support_congr [fintype α] {f g : perm α} (hf : is_cycle f) (hg : is_cycle g)
@@ -583,6 +591,16 @@ lemma same_cycle.cycle_of_apply [fintype α] {f : perm α} {x y : α} (h : same_
 lemma cycle_of_apply_of_not_same_cycle [fintype α] {f : perm α} {x y : α} (h : ¬same_cycle f x y) :
   cycle_of f x y = y := dif_neg h
 
+lemma same_cycle.cycle_of_eq [fintype α] {f : perm α} {x y : α} (h : same_cycle f x y) :
+  cycle_of f x = cycle_of f y :=
+begin
+  ext z,
+  rw cycle_of_apply,
+  split_ifs with hz hz,
+  { exact (h.symm.trans hz).cycle_of_apply.symm },
+  { exact (cycle_of_apply_of_not_same_cycle (mt h.trans hz)).symm }
+end
+
 @[simp] lemma cycle_of_apply_apply_gpow_self [fintype α] (f : perm α) (x : α) (k : ℤ) :
   cycle_of f x ((f ^ k) x) = (f ^ (k + 1)) x :=
 begin
@@ -617,6 +635,18 @@ begin
   { exact if_neg (mt same_cycle.apply_eq_self_iff (by tauto)) },
 end
 
+@[simp] lemma cycle_of_self_apply [fintype α] (f : perm α) (x : α) :
+  cycle_of f (f x) = cycle_of f x :=
+(same_cycle_apply.mpr (same_cycle.refl _ _)).symm.cycle_of_eq
+
+@[simp] lemma cycle_of_self_apply_pow [fintype α] (f : perm α) (n : ℕ) (x : α) :
+  cycle_of f ((f ^ n) x) = cycle_of f x :=
+(same_cycle_pow_left_iff.mpr (same_cycle.refl _ _)).cycle_of_eq
+
+@[simp] lemma cycle_of_self_apply_gpow [fintype α] (f : perm α) (n : ℤ) (x : α) :
+  cycle_of f ((f ^ n) x) = cycle_of f x :=
+(same_cycle_gpow_left_iff.mpr (same_cycle.refl _ _)).cycle_of_eq
+
 lemma is_cycle.cycle_of [fintype α] {f : perm α} (hf : is_cycle f) {x : α} :
   cycle_of f x = if f x = x then 1 else f :=
 begin
@@ -637,6 +667,22 @@ have cycle_of f x x ≠ x, by rwa [(same_cycle.refl _ _).cycle_of_apply],
   ⟨i, by rw [cycle_of_gpow_apply_self, hi]⟩
   else by { rw [cycle_of_apply_of_not_same_cycle hxy] at h, exact (h rfl).elim }⟩
 
+@[simp] lemma two_le_card_support_cycle_of_iff [fintype α] {f : perm α} {x : α} :
+  2 ≤ card (cycle_of f x).support ↔ f x ≠ x :=
+begin
+  refine ⟨λ h, _, λ h, by simpa using (is_cycle_cycle_of _ h).two_le_card_support⟩,
+  contrapose! h,
+  rw ←cycle_of_eq_one_iff at h,
+  simp [h]
+end
+
+@[simp] lemma card_support_cycle_of_pos_iff [fintype α] {f : perm α} {x : α} :
+  0 < card (cycle_of f x).support ↔ f x ≠ x :=
+begin
+  rw [←two_le_card_support_cycle_of_iff, ←nat.succ_le_iff],
+  exact ⟨λ h, or.resolve_left h.eq_or_lt (card_support_ne_one _).symm, zero_lt_two.trans_le⟩
+end
+
 lemma pow_apply_eq_pow_mod_order_of_cycle_of_apply [fintype α] (f : perm α) (n : ℕ) (x : α) :
   (f ^ n) x = (f ^ (n % order_of (cycle_of f x))) x :=
 by rw [←cycle_of_pow_apply_self f, ←cycle_of_pow_apply_self f, pow_eq_mod_order_of]
@@ -668,6 +714,16 @@ lemma support_cycle_of_eq_nil_iff [fintype α] {f : perm α} {x : α} :
   (f.cycle_of x).support = ∅ ↔ x ∉ f.support :=
 by simp
 
+lemma support_cycle_of_le [fintype α] (f : perm α) (x : α) :
+  support (f.cycle_of x) ≤ support f :=
+begin
+  intros y hy,
+  rw [mem_support, cycle_of_apply] at hy,
+  split_ifs at hy,
+  { exact mem_support.mpr hy },
+  { exact absurd rfl hy }
+end
+
 lemma mem_support_cycle_of_iff [fintype α] {f : perm α} {x y : α} :
   y ∈ support (f.cycle_of x) ↔ same_cycle f x y ∧ x ∈ support f :=
 begin
@@ -683,6 +739,20 @@ begin
     { simpa [hx] using hy } }
 end
 
+lemma same_cycle.mem_support_iff [fintype α] {f : perm α} {x y : α} (h : same_cycle f x y) :
+  x ∈ support f ↔ y ∈ support f :=
+⟨λ hx, support_cycle_of_le f x (mem_support_cycle_of_iff.mpr ⟨h, hx⟩),
+ λ hy, support_cycle_of_le f y (mem_support_cycle_of_iff.mpr ⟨h.symm, hy⟩)⟩
+
+lemma pow_mod_card_support_cycle_of_self_apply [fintype α] (f : perm α) (n : ℕ) (x : α) :
+  (f ^ (n % (f.cycle_of x).support.card)) x = (f ^ n) x :=
+begin
+  by_cases hx : f x = x,
+  { rw [pow_apply_eq_self_of_apply_eq_self hx, pow_apply_eq_self_of_apply_eq_self hx] },
+  { rw [←cycle_of_pow_apply_self, ←cycle_of_pow_apply_self f,
+        ←order_of_is_cycle (is_cycle_cycle_of f hx), ←pow_eq_mod_order_of] }
+end
+
 /-!
 ### `cycle_factors`
 -/