doc-next-gen

Mathlib.GroupTheory.Perm.Cycle.Factors

Module docstring

{"# Cycle factors of a permutation

Let β be a Fintype and f : Equiv.Perm β.

  • Equiv.Perm.cycleOf: f.cycleOf x is the cycle of f that x belongs to.
  • Equiv.Perm.cycleFactors: f.cycleFactors is a list of disjoint cyclic permutations that multiply to f. ","### cycleOf ","### cycleFactors "}
Equiv.Perm.cycleOf definition
(f : Perm α) [DecidableRel f.SameCycle] (x : α) : Perm α
Full source 
/-- `f.cycleOf x` is the cycle of the permutation `f` to which `x` belongs. -/
def cycleOf (f : Perm α) [DecidableRel f.SameCycle] (x : α) : Perm α :=
  ofSubtype (subtypePerm f fun _ => sameCycle_apply_right.symm : Perm { y // SameCycle f x y })
Cycle of a permutation containing a given element
Informal description
For a permutation \( f \) of a type \( \alpha \) with a decidable same cycle relation, and an element \( x \in \alpha \), the cycle \( f.\text{cycleOf } x \) is the restriction of \( f \) to the set of elements \( y \) that are in the same cycle as \( x \) under \( f \). More precisely, \( f.\text{cycleOf } x \) is defined as the permutation obtained by restricting \( f \) to the subtype \( \{ y \mid \text{SameCycle } f \, x \, y \} \), where \( \text{SameCycle } f \, x \, y \) holds if there exists an integer \( i \) such that \( f^i(x) = y \).
Equiv.Perm.cycleOf_apply theorem
(f : Perm α) [DecidableRel f.SameCycle] (x y : α) : cycleOf f x y = if SameCycle f x y then f y else y
Full source 
theorem cycleOf_apply (f : Perm α) [DecidableRel f.SameCycle] (x y : α) :
    cycleOf f x y = if SameCycle f x y then f y else y := by
  dsimp only [cycleOf]
  split_ifs with h
  · apply ofSubtype_apply_of_mem
    exact h
  · apply ofSubtype_apply_of_not_mem
    exact h
Application of Cycle Restriction in Permutation
Informal description
For a permutation $f$ of a type $\alpha$ with a decidable same cycle relation, and elements $x, y \in \alpha$, the application of the cycle containing $x$ to $y$ is given by: $$f.\text{cycleOf}(x)(y) = \begin{cases} f(y) & \text{if } y \text{ is in the same cycle as } x \text{ under } f \\ y & \text{otherwise} \end{cases}$$ where $y$ is in the same cycle as $x$ under $f$ if there exists an integer $i$ such that $f^i(x) = y$.
Equiv.Perm.cycleOf_inv theorem
(f : Perm α) [DecidableRel f.SameCycle] (x : α) : (cycleOf f x)⁻¹ = cycleOf f⁻¹ x
Full source 
theorem cycleOf_inv (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
    (cycleOf f x)⁻¹ = cycleOf f⁻¹ x :=
  Equiv.ext fun y => by
    rw [inv_eq_iff_eq, cycleOf_apply, cycleOf_apply]
    split_ifs <;> simp_all [sameCycle_inv, sameCycle_inv_apply_right]
Inverse of Cycle Restriction Equals Cycle Restriction of Inverse
Informal description
For any permutation $f$ of a type $\alpha$ with a decidable same cycle relation, and any element $x \in \alpha$, the inverse of the cycle containing $x$ in $f$ is equal to the cycle containing $x$ in the inverse permutation $f^{-1}$. That is, $$(f.\text{cycleOf } x)^{-1} = f^{-1}.\text{cycleOf } x.$$
Equiv.Perm.cycleOf_pow_apply_self theorem
(f : Perm α) [DecidableRel f.SameCycle] (x : α) : ∀ n : ℕ, (cycleOf f x ^ n) x = (f ^ n) x
Full source 
@[simp]
theorem cycleOf_pow_apply_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
    ∀ n : ℕ, (cycleOf f x ^ n) x = (f ^ n) x := by
  intro n
  induction n with
  | zero => rfl
  | succ n hn =>
    rw [pow_succ', mul_apply, cycleOf_apply, hn, if_pos, pow_succ', mul_apply]
    exact ⟨n, rfl⟩
Cycle Power Equals Permutation Power at Fixed Element
Informal description
For any permutation \( f \) of a type \( \alpha \) with a decidable same cycle relation, and any element \( x \in \alpha \), the \( n \)-th power of the cycle containing \( x \) applied to \( x \) equals the \( n \)-th power of \( f \) applied to \( x \). That is, for all natural numbers \( n \), we have: \[ (\text{cycleOf}_f(x))^n(x) = f^n(x) \]
Equiv.Perm.cycleOf_zpow_apply_self theorem
(f : Perm α) [DecidableRel f.SameCycle] (x : α) : ∀ n : ℤ, (cycleOf f x ^ n) x = (f ^ n) x
Full source 
@[simp]
theorem cycleOf_zpow_apply_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
    ∀ n : ℤ, (cycleOf f x ^ n) x = (f ^ n) x := by
  intro z
  cases z with
  | ofNat z => exact cycleOf_pow_apply_self f x z
  | negSucc z =>
    rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]
Cycle Power Equals Permutation Power at Fixed Element for Integer Exponents
Informal description
For any permutation $f$ of a type $\alpha$ with a decidable same cycle relation, and any element $x \in \alpha$, the $n$-th power (for any integer $n$) of the cycle containing $x$ in $f$ applied to $x$ equals the $n$-th power of $f$ applied to $x$. That is, for all integers $n$, we have: $$(f.\text{cycleOf } x)^n(x) = f^n(x).$$
Equiv.Perm.SameCycle.cycleOf_apply theorem
[DecidableRel f.SameCycle] : SameCycle f x y → cycleOf f x y = f y
Full source 
theorem SameCycle.cycleOf_apply [DecidableRel f.SameCycle] :
    SameCycle f x y → cycleOf f x y = f y :=
  ofSubtype_apply_of_mem _
Cycle of a Permutation Acts as Original on Same-Cycle Elements
Informal description
For a permutation $f$ of a type $\alpha$ with a decidable same cycle relation, if two elements $x$ and $y$ are in the same cycle of $f$, then the cycle of $f$ containing $x$ acts on $y$ in the same way as $f$ does, i.e., $\text{cycleOf}_f(x)(y) = f(y)$.
Equiv.Perm.cycleOf_apply_of_not_sameCycle theorem
[DecidableRel f.SameCycle] : ¬SameCycle f x y → cycleOf f x y = y
Full source 
theorem cycleOf_apply_of_not_sameCycle [DecidableRel f.SameCycle] :
    ¬SameCycle f x y → cycleOf f x y = y :=
  ofSubtype_apply_of_not_mem _
Cycle of a Permutation Fixes Elements Outside Its Cycle
Informal description
For a permutation \( f \) of a type \( \alpha \) with a decidable same cycle relation, if two elements \( x \) and \( y \) are not in the same cycle of \( f \), then the cycle of \( f \) containing \( x \) fixes \( y \), i.e., \( f.\text{cycleOf } x \, y = y \).
Equiv.Perm.SameCycle.cycleOf_eq theorem
[DecidableRel f.SameCycle] (h : SameCycle f x y) : cycleOf f x = cycleOf f y
Full source 
theorem SameCycle.cycleOf_eq [DecidableRel f.SameCycle] (h : SameCycle f x y) :
    cycleOf f x = cycleOf f y := by
  ext z
  rw [Equiv.Perm.cycleOf_apply]
  split_ifs with hz
  · exact (h.symm.trans hz).cycleOf_apply.symm
  · exact (cycleOf_apply_of_not_sameCycle (mt h.trans hz)).symm
Equality of Cycles for Elements in the Same Cycle of a Permutation
Informal description
For a permutation $f$ of a type $\alpha$ with a decidable same cycle relation, if two elements $x$ and $y$ are in the same cycle of $f$, then the cycle of $f$ containing $x$ is equal to the cycle of $f$ containing $y$.
Equiv.Perm.cycleOf_apply_apply_zpow_self theorem
(f : Perm α) [DecidableRel f.SameCycle] (x : α) (k : ℤ) : cycleOf f x ((f ^ k) x) = (f ^ (k + 1) : Perm α) x
Full source 
@[simp]
theorem cycleOf_apply_apply_zpow_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) (k : ℤ) :
    cycleOf f x ((f ^ k) x) = (f ^ (k + 1) : Perm α) x := by
  rw [SameCycle.cycleOf_apply]
  · rw [add_comm, zpow_add, zpow_one, mul_apply]
  · exact ⟨k, rfl⟩
Cycle Action on Integer Powers: $\text{cycleOf}_f(x)(f^k(x)) = f^{k+1}(x)$
Informal description
For a permutation $f$ of a type $\alpha$ with a decidable same cycle relation, and an element $x \in \alpha$, the cycle of $f$ containing $x$ satisfies $\text{cycleOf}_f(x)(f^k(x)) = f^{k+1}(x)$ for any integer $k$.
Equiv.Perm.cycleOf_apply_apply_pow_self theorem
(f : Perm α) [DecidableRel f.SameCycle] (x : α) (k : ℕ) : cycleOf f x ((f ^ k) x) = (f ^ (k + 1) : Perm α) x
Full source 
@[simp]
theorem cycleOf_apply_apply_pow_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) (k : ℕ) :
    cycleOf f x ((f ^ k) x) = (f ^ (k + 1) : Perm α) x := by
  convert cycleOf_apply_apply_zpow_self f x k using 1
Cycle Action on Natural Powers: $\text{cycleOf}_f(x)(f^k(x)) = f^{k+1}(x)$
Informal description
For a permutation $f$ of a type $\alpha$ with a decidable same cycle relation, and an element $x \in \alpha$, the cycle of $f$ containing $x$ satisfies $\text{cycleOf}_f(x)(f^k(x)) = f^{k+1}(x)$ for any natural number $k$.
Equiv.Perm.cycleOf_apply_apply_self theorem
(f : Perm α) [DecidableRel f.SameCycle] (x : α) : cycleOf f x (f x) = f (f x)
Full source 
@[simp]
theorem cycleOf_apply_apply_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
    cycleOf f x (f x) = f (f x) := by
  convert cycleOf_apply_apply_pow_self f x 1 using 1
Cycle Action on First Iterate: $\text{cycleOf}_f(x)(f(x)) = f^2(x)$
Informal description
For a permutation $f$ of a type $\alpha$ with a decidable same cycle relation, and an element $x \in \alpha$, the cycle of $f$ containing $x$ satisfies $\text{cycleOf}_f(x)(f(x)) = f(f(x))$.
Equiv.Perm.cycleOf_apply_self theorem
(f : Perm α) [DecidableRel f.SameCycle] (x : α) : cycleOf f x x = f x
Full source 
@[simp]
theorem cycleOf_apply_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) : cycleOf f x x = f x :=
  SameCycle.rfl.cycleOf_apply
Cycle of a Permutation Acts as Original on Its Base Element
Informal description
For a permutation $f$ of a type $\alpha$ with a decidable same cycle relation, and an element $x \in \alpha$, the cycle of $f$ containing $x$ acts on $x$ in the same way as $f$ does, i.e., $\text{cycleOf}_f(x)(x) = f(x)$.
Equiv.Perm.IsCycle.cycleOf_eq theorem
[DecidableRel f.SameCycle] (hf : IsCycle f) (hx : f x ≠ x) : cycleOf f x = f
Full source 
theorem IsCycle.cycleOf_eq [DecidableRel f.SameCycle]
    (hf : IsCycle f) (hx : f x ≠ x) : cycleOf f x = f :=
  Equiv.ext fun y =>
    if h : SameCycle f x y then by rw [h.cycleOf_apply]
    else by
      rw [cycleOf_apply_of_not_sameCycle h,
        Classical.not_not.1 (mt ((isCycle_iff_sameCycle hx).1 hf).2 h)]
Cycle of a Cycle Permutation is Itself
Informal description
For a permutation \( f \) of a type \( \alpha \) with a decidable same cycle relation, if \( f \) is a cycle and \( x \) is a non-fixed point of \( f \) (i.e., \( f(x) \neq x \)), then the cycle of \( f \) containing \( x \) is equal to \( f \) itself, i.e., \( \text{cycleOf}_f(x) = f \).
Equiv.Perm.cycleOf_eq_one_iff theorem
(f : Perm α) [DecidableRel f.SameCycle] : cycleOf f x = 1 ↔ f x = x
Full source 
@[simp]
theorem cycleOf_eq_one_iff (f : Perm α) [DecidableRel f.SameCycle] : cycleOfcycleOf f x = 1 ↔ f x = x := by
  simp_rw [Perm.ext_iff, cycleOf_apply, one_apply]
  refine ⟨fun h => (if_pos (SameCycle.refl f x)).symm.trans (h x), fun h y => ?_⟩
  by_cases hy : f y = y
  · rw [hy, ite_self]
  · exact if_neg (mt SameCycle.apply_eq_self_iff (by tauto))
Cycle is Identity if and only if Element is Fixed
Informal description
For a permutation $f$ of a type $\alpha$ with a decidable same cycle relation, the cycle of $f$ containing $x$ is the identity permutation if and only if $f$ fixes $x$, i.e., $\text{cycleOf}_f(x) = 1 \leftrightarrow f(x) = x$.
Equiv.Perm.cycleOf_self_apply theorem
(f : Perm α) [DecidableRel f.SameCycle] (x : α) : cycleOf f (f x) = cycleOf f x
Full source 
@[simp]
theorem cycleOf_self_apply (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
    cycleOf f (f x) = cycleOf f x :=
  (sameCycle_apply_right.2 SameCycle.rfl).symm.cycleOf_eq
Cycle Preservation under Permutation Application: $\text{cycleOf}_f(f(x)) = \text{cycleOf}_f(x)$
Informal description
For a permutation $f$ of a type $\alpha$ with a decidable same cycle relation, and for any element $x \in \alpha$, the cycle of $f$ containing $f(x)$ is equal to the cycle of $f$ containing $x$. That is, $\text{cycleOf}_f(f(x)) = \text{cycleOf}_f(x)$.
Equiv.Perm.cycleOf_self_apply_pow theorem
(f : Perm α) [DecidableRel f.SameCycle] (n : ℕ) (x : α) : cycleOf f ((f ^ n) x) = cycleOf f x
Full source 
@[simp]
theorem cycleOf_self_apply_pow (f : Perm α) [DecidableRel f.SameCycle] (n : ℕ) (x : α) :
    cycleOf f ((f ^ n) x) = cycleOf f x :=
  SameCycle.rfl.pow_left.cycleOf_eq
Cycle Preservation under Iterated Permutation: $\text{cycleOf } f (f^n(x)) = \text{cycleOf } f x$
Informal description
For a permutation $f$ of a type $\alpha$ with a decidable same cycle relation, and for any natural number $n$ and element $x \in \alpha$, the cycle of $f$ containing $f^n(x)$ is equal to the cycle of $f$ containing $x$. That is, $\text{cycleOf } f (f^n(x)) = \text{cycleOf } f x$.
Equiv.Perm.cycleOf_self_apply_zpow theorem
(f : Perm α) [DecidableRel f.SameCycle] (n : ℤ) (x : α) : cycleOf f ((f ^ n) x) = cycleOf f x
Full source 
@[simp]
theorem cycleOf_self_apply_zpow (f : Perm α) [DecidableRel f.SameCycle] (n : ℤ) (x : α) :
    cycleOf f ((f ^ n) x) = cycleOf f x :=
  SameCycle.rfl.zpow_left.cycleOf_eq
Cycle Preservation under Integer Powers of a Permutation
Informal description
For any permutation $f$ of a type $\alpha$ with a decidable same cycle relation, any integer $n \in \mathbb{Z}$, and any element $x \in \alpha$, the cycle of $f$ containing $f^n(x)$ is equal to the cycle of $f$ containing $x$. In other words, $\text{cycleOf } f (f^n(x)) = \text{cycleOf } f (x)$.
Equiv.Perm.IsCycle.cycleOf theorem
[DecidableRel f.SameCycle] [DecidableEq α] (hf : IsCycle f) : cycleOf f x = if f x = x then 1 else f
Full source 
protected theorem IsCycle.cycleOf [DecidableRel f.SameCycle] [DecidableEq α]
    (hf : IsCycle f) : cycleOf f x = if f x = x then 1 else f := by
  by_cases hx : f x = x
  · rwa [if_pos hx, cycleOf_eq_one_iff]
  · rwa [if_neg hx, hf.cycleOf_eq]
Cycle of a Cycle Permutation Equals Itself or Identity
Informal description
For a cycle permutation $f$ of a type $\alpha$ with decidable same cycle relation and decidable equality, the cycle of $f$ containing an element $x$ is equal to $f$ if $x$ is not fixed by $f$ (i.e., $f(x) \neq x$), and is the identity permutation otherwise. In other words: \[ \text{cycleOf}_f(x) = \begin{cases} f & \text{if } f(x) \neq x, \\ 1 & \text{if } f(x) = x. \end{cases} \]
Equiv.Perm.cycleOf_one theorem
[DecidableRel (1 : Perm α).SameCycle] (x : α) : cycleOf 1 x = 1
Full source 
theorem cycleOf_one [DecidableRel (1 : Perm α).SameCycle] (x : α) :
    cycleOf 1 x = 1 := (cycleOf_eq_one_iff 1).mpr rfl
Cycle of Identity Permutation is Identity
Informal description
For any element $x$ of a type $\alpha$, the cycle of the identity permutation $1$ containing $x$ is equal to the identity permutation itself, i.e., $\text{cycleOf}_1(x) = 1$.
Equiv.Perm.isCycle_cycleOf theorem
(f : Perm α) [DecidableRel f.SameCycle] (hx : f x ≠ x) : IsCycle (cycleOf f x)
Full source 
theorem isCycle_cycleOf (f : Perm α) [DecidableRel f.SameCycle] (hx : f x ≠ x) :
    IsCycle (cycleOf f x) :=
  have : cycleOfcycleOf f x x ≠ x := by rwa [SameCycle.rfl.cycleOf_apply]
  (isCycle_iff_sameCycle this).2 @fun y =>
    ⟨fun h => mt h.apply_eq_self_iff.2 this, fun h =>
      if hxy : SameCycle f x y then
        let ⟨i, hi⟩ := hxy
        ⟨i, by rw [cycleOf_zpow_apply_self, hi]⟩
      else by
        rw [cycleOf_apply_of_not_sameCycle hxy] at h
        exact (h rfl).elim⟩
Cycle of a Non-Fixed Point is a Cycle Permutation
Informal description
For a permutation $f$ of a type $\alpha$ with a decidable same cycle relation, if an element $x \in \alpha$ is not fixed by $f$ (i.e., $f(x) \neq x$), then the cycle of $f$ containing $x$ is itself a cycle permutation.
Equiv.Perm.pow_mod_orderOf_cycleOf_apply theorem
(f : Perm α) [DecidableRel f.SameCycle] (n : ℕ) (x : α) : (f ^ (n % orderOf (cycleOf f x))) x = (f ^ n) x
Full source 
theorem pow_mod_orderOf_cycleOf_apply (f : Perm α) [DecidableRel f.SameCycle] (n : ℕ) (x : α) :
    (f ^ (n % orderOf (cycleOf f x))) x = (f ^ n) x := by
  rw [← cycleOf_pow_apply_self f, ← cycleOf_pow_apply_self f, pow_mod_orderOf]
Cycle Power Reduction: $f^{n \bmod \text{ord}(C_x)}x = f^n x$ where $C_x$ is the cycle containing $x$
Informal description
For any permutation $f$ of a type $\alpha$ with a decidable same cycle relation, any natural number $n$, and any element $x \in \alpha$, we have: \[ (f^{n \bmod \text{orderOf}(f.\text{cycleOf } x)})x = f^n x \] where $\text{orderOf}(f.\text{cycleOf } x)$ is the order of the cycle containing $x$ in $f$.
Equiv.Perm.cycleOf_mul_of_apply_right_eq_self theorem
[DecidableRel f.SameCycle] [DecidableRel (f * g).SameCycle] (h : Commute f g) (x : α) (hx : g x = x) : (f * g).cycleOf x = f.cycleOf x
Full source 
theorem cycleOf_mul_of_apply_right_eq_self [DecidableRel f.SameCycle]
    [DecidableRel (f * g).SameCycle]
    (h : Commute f g) (x : α) (hx : g x = x) : (f * g).cycleOf x = f.cycleOf x := by
  ext y
  by_cases hxy : (f * g).SameCycle x y
  · obtain ⟨z, rfl⟩ := hxy
    rw [cycleOf_apply_apply_zpow_self]
    simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]
  · rw [cycleOf_apply_of_not_sameCycle hxy, cycleOf_apply_of_not_sameCycle]
    contrapose! hxy
    obtain ⟨z, rfl⟩ := hxy
    refine ⟨z, ?_⟩
    simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]
Cycle Preservation in Product of Commuting Permutations with Fixed Point
Informal description
Let $f$ and $g$ be commuting permutations of a finite type $\alpha$ with decidable same cycle relations. If $g$ fixes an element $x \in \alpha$ (i.e., $g(x) = x$), then the cycle of the product permutation $f \circ g$ containing $x$ is equal to the cycle of $f$ containing $x$, i.e., $(f \circ g).\text{cycleOf } x = f.\text{cycleOf } x$.
Equiv.Perm.Disjoint.cycleOf_mul_distrib theorem
[DecidableRel f.SameCycle] [DecidableRel g.SameCycle] [DecidableRel (f * g).SameCycle] [DecidableRel (g * f).SameCycle] (h : f.Disjoint g) (x : α) : (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
Full source 
theorem Disjoint.cycleOf_mul_distrib [DecidableRel f.SameCycle] [DecidableRel g.SameCycle]
    [DecidableRel (f * g).SameCycle] [DecidableRel (g * f).SameCycle] (h : f.Disjoint g) (x : α) :
    (f * g).cycleOf x = f.cycleOf x * g.cycleOf x := by
  rcases (disjoint_iff_eq_or_eq.mp h) x with hfx | hgx
  · simp [h.commute.eq, cycleOf_mul_of_apply_right_eq_self h.symm.commute, hfx]
  · simp [cycleOf_mul_of_apply_right_eq_self h.commute, hgx]
Distributivity of Cycle Construction over Composition for Disjoint Permutations
Informal description
Let $f$ and $g$ be disjoint permutations of a finite type $\alpha$ with decidable same cycle relations. Then for any element $x \in \alpha$, the cycle of the product permutation $f \circ g$ containing $x$ is equal to the product of the cycles of $f$ and $g$ containing $x$, i.e., \[ (f \circ g).\text{cycleOf } x = f.\text{cycleOf } x \circ g.\text{cycleOf } x. \]
Equiv.Perm.isCycle_cycleOf_iff theorem
(f : Perm α) [DecidableRel f.SameCycle] : IsCycle (cycleOf f x) ↔ f x ≠ x
Full source 
/-- `x` is in the support of `f` iff `Equiv.Perm.cycle_of f x` is a cycle. -/
theorem isCycle_cycleOf_iff (f : Perm α) [DecidableRel f.SameCycle] :
    IsCycleIsCycle (cycleOf f x) ↔ f x ≠ x := by
  refine ⟨fun hx => ?_, f.isCycle_cycleOf⟩
  rw [Ne, ← cycleOf_eq_one_iff f]
  exact hx.ne_one
Cycle of a Permutation is a Cycle if and only if Element is Not Fixed
Informal description
For a permutation $f$ of a type $\alpha$ with a decidable same cycle relation, the cycle of $f$ containing $x$ is a cycle permutation if and only if $x$ is not a fixed point of $f$, i.e., $\text{IsCycle}(\text{cycleOf}_f(x)) \leftrightarrow f(x) \neq x$.
Equiv.Perm.instDecidableRelSameCycle instance
[DecidableEq α] [Fintype α] (f : Perm α) : DecidableRel (SameCycle f)
Full source 
instance instDecidableRelSameCycle [DecidableEq α] [Fintype α] (f : Perm α) :
    DecidableRel (SameCycle f) := fun x y =>
  decidable_of_iff (y ∈ List.iterate f x (Fintype.card α)) <| by
    simp only [List.mem_iterate, iterate_eq_pow, eq_comm (a := y)]
    constructor
    · rintro ⟨n, _, hn⟩
      exact ⟨n, hn⟩
    · intro hxy
      by_cases hx : x ∈ f.support
      case pos =>
        -- we can't invoke the aux lemmas above without obtaining the decidable instance we are
        -- already building; but now we've left the data, so we can do this non-constructively
        -- without sacrificing computability.
        let _inst (f : Perm α) : DecidableRel (SameCycle f) := Classical.decRel _
        rcases hxy.exists_pow_eq_of_mem_support_aux hx with ⟨i, hixy, hi⟩
        refine ⟨i, lt_of_lt_of_le hixy (card_le_univ _), hi⟩
      case neg =>
        haveI : Nonempty α := ⟨x⟩
        rw [not_mem_support] at hx
        exact ⟨0, Fintype.card_pos, hxy.eq_of_left hx⟩
Decidability of the Same Cycle Relation for Permutations on Finite Types
Informal description
For any finite type $\alpha$ with decidable equality and permutation $f$ of $\alpha$, the relation $\text{SameCycle } f$ is decidable. That is, for any two elements $x$ and $y$ in $\alpha$, it is decidable whether there exists an integer $i$ such that $f^i(x) = y$.
Equiv.Perm.two_le_card_support_cycleOf_iff theorem
[DecidableEq α] [Fintype α] : 2 ≤ #(cycleOf f x).support ↔ f x ≠ x
Full source 
@[simp]
theorem two_le_card_support_cycleOf_iff [DecidableEq α] [Fintype α] :
    2 ≤ #(cycleOf f x).support ↔ f x ≠ x := by
  refine ⟨fun h => ?_, fun h => by simpa using (isCycle_cycleOf _ h).two_le_card_support⟩
  contrapose! h
  rw [← cycleOf_eq_one_iff] at h
  simp [h]
Cycle Support Size Condition for Non-Fixed Points
Informal description
For a permutation $f$ of a finite type $\alpha$ with decidable equality, the support of the cycle containing $x$ has cardinality at least 2 if and only if $x$ is not a fixed point of $f$, i.e., $2 \leq \#\text{supp}(f.\text{cycleOf } x) \leftrightarrow f(x) \neq x$.
Equiv.Perm.support_cycleOf_nonempty theorem
[DecidableEq α] [Fintype α] : (cycleOf f x).support.Nonempty ↔ f x ≠ x
Full source 
@[simp] lemma support_cycleOf_nonempty [DecidableEq α] [Fintype α] :
    (cycleOf f x).support.Nonempty ↔ f x ≠ x := by
  rw [← two_le_card_support_cycleOf_iff, ← card_pos, ← Nat.succ_le_iff]
  exact ⟨fun h => Or.resolve_left h.eq_or_lt (card_support_ne_one _).symm, zero_lt_two.trans_le⟩
Nonempty Support of Cycle in Permutation Characterizes Non-Fixed Points
Informal description
For a permutation $f$ of a finite type $\alpha$ with decidable equality, the support of the cycle containing $x$ is nonempty if and only if $x$ is not a fixed point of $f$, i.e., $\text{supp}(f.\text{cycleOf } x) \neq \emptyset \leftrightarrow f(x) \neq x$.
Equiv.Perm.mem_support_cycleOf_iff theorem
[DecidableEq α] [Fintype α] : y ∈ support (f.cycleOf x) ↔ SameCycle f x y ∧ x ∈ support f
Full source 
theorem mem_support_cycleOf_iff [DecidableEq α] [Fintype α] :
    y ∈ support (f.cycleOf x)y ∈ support (f.cycleOf x) ↔ SameCycle f x y ∧ x ∈ support f :=
  mem_support_cycleOf_iff_aux
Characterization of Membership in the Support of a Permutation Cycle
Informal description
For a permutation $f$ of a finite type $\alpha$ with decidable equality, an element $y$ is in the support of the cycle containing $x$ (i.e., $y \in \text{support}(f.\text{cycleOf } x)$) if and only if $y$ is in the same cycle as $x$ under $f$ and $x$ is a non-fixed point of $f$ (i.e., $f(x) \neq x$).
Equiv.Perm.mem_support_cycleOf_iff' theorem
(hx : f x ≠ x) [DecidableEq α] [Fintype α] : y ∈ support (f.cycleOf x) ↔ SameCycle f x y
Full source 
theorem mem_support_cycleOf_iff' (hx : f x ≠ x) [DecidableEq α] [Fintype α] :
    y ∈ support (f.cycleOf x)y ∈ support (f.cycleOf x) ↔ SameCycle f x y :=
  mem_support_cycleOf_iff'_aux hx
Characterization of Support Membership in a Permutation Cycle for Non-Fixed Points
Informal description
For a permutation $f$ of a finite type $\alpha$ with decidable equality, if $x$ is a non-fixed point of $f$ (i.e., $f(x) \neq x$), then an element $y$ belongs to the support of the cycle containing $x$ (i.e., $y \in \text{support}(f.\text{cycleOf } x)$) if and only if $y$ is in the same cycle as $x$ under $f$ (i.e., $\text{SameCycle } f \, x \, y$ holds).
Equiv.Perm.sameCycle_iff_cycleOf_eq_of_mem_support theorem
[DecidableEq α] [Fintype α] {g : Perm α} {x y : α} (hx : x ∈ g.support) (hy : y ∈ g.support) : g.SameCycle x y ↔ g.cycleOf x = g.cycleOf y
Full source 
theorem sameCycle_iff_cycleOf_eq_of_mem_support [DecidableEq α] [Fintype α]
    {g : Perm α} {x y : α} (hx : x ∈ g.support) (hy : y ∈ g.support) :
    g.SameCycle x y ↔ g.cycleOf x = g.cycleOf y := by
  refine ⟨SameCycle.cycleOf_eq, fun h ↦ ?_⟩
  rw [← mem_support_cycleOf_iff' (mem_support.mp hx), h,
    mem_support_cycleOf_iff' (mem_support.mp hy)]
Characterization of Same Cycle Relation via Cycle Equality for Non-Fixed Points
Informal description
Let $\alpha$ be a finite type with decidable equality, and let $g$ be a permutation of $\alpha$. For any elements $x, y \in \alpha$ that are non-fixed points of $g$ (i.e., $x \in \text{support}(g)$ and $y \in \text{support}(g)$), the following are equivalent: 1. $x$ and $y$ are in the same cycle of $g$ (i.e., $\text{SameCycle } g \, x \, y$ holds). 2. The cycle of $g$ containing $x$ is equal to the cycle of $g$ containing $y$ (i.e., $g.\text{cycleOf } x = g.\text{cycleOf } y$).
Equiv.Perm.support_cycleOf_eq_nil_iff theorem
[DecidableEq α] [Fintype α] : (f.cycleOf x).support = ∅ ↔ x ∉ f.support
Full source 
theorem support_cycleOf_eq_nil_iff [DecidableEq α] [Fintype α] :
    (f.cycleOf x).support = ∅ ↔ x ∉ f.support := by simp
Empty Support of Cycle in Permutation iff Element Not in Support
Informal description
For a permutation $f$ of a finite type $\alpha$ with decidable equality, the support of the cycle of $f$ containing $x$ is empty if and only if $x$ is not in the support of $f$. That is, $\text{support}(f.\text{cycleOf } x) = \emptyset \leftrightarrow x \notin \text{support}(f)$.
Equiv.Perm.isCycleOn_support_cycleOf theorem
[DecidableEq α] [Fintype α] (f : Perm α) (x : α) : f.IsCycleOn (f.cycleOf x).support
Full source 
theorem isCycleOn_support_cycleOf [DecidableEq α] [Fintype α] (f : Perm α) (x : α) :
    f.IsCycleOn (f.cycleOf x).support :=
  isCycleOn_support_cycleOf_aux f x
Permutation Acts Cyclically on Support of Its Cycle Containing an Element
Informal description
For a permutation $f$ of a finite type $\alpha$ with decidable equality and any element $x \in \alpha$, the permutation $f$ is a cycle on the support of its cycle containing $x$ (i.e., $f$ acts cyclically on $\text{support}(f.\text{cycleOf } x)$).
Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support theorem
{f} [DecidableEq α] [Fintype α] (h : SameCycle f x y) (hx : x ∈ f.support) : ∃ i < #(f.cycleOf x).support, (f ^ i) x = y
Full source 
theorem SameCycle.exists_pow_eq_of_mem_support {f} [DecidableEq α] [Fintype α] (h : SameCycle f x y)
    (hx : x ∈ f.support) : ∃ i < #(f.cycleOf x).support, (f ^ i) x = y :=
  h.exists_pow_eq_of_mem_support_aux hx
Existence of Power Mapping Elements in Same Cycle with Bounded Exponent
Informal description
Let $f$ be a permutation of a finite type $\alpha$ with decidable equality, and let $x, y \in \alpha$ be elements in the same cycle of $f$ (i.e., $\text{SameCycle } f \, x \, y$ holds). If $x$ is in the support of $f$, then there exists an integer $i$ such that $i$ is less than the size of the support of the cycle containing $x$ and $f^i(x) = y$.
Equiv.Perm.support_cycleOf_le theorem
[DecidableEq α] [Fintype α] (f : Perm α) (x : α) : support (f.cycleOf x) ≤ support f
Full source 
theorem support_cycleOf_le [DecidableEq α] [Fintype α] (f : Perm α) (x : α) :
    support (f.cycleOf x) ≤ support f := by
  intro y hy
  rw [mem_support, cycleOf_apply] at hy
  split_ifs at hy
  · exact mem_support.mpr hy
  · exact absurd rfl hy
Support of Cycle Containing an Element is Subset of Permutation Support
Informal description
For a permutation $f$ of a finite type $\alpha$ with decidable equality and any element $x \in \alpha$, the support of the cycle containing $x$ is a subset of the support of $f$. In other words, $\text{support}(f.\text{cycleOf } x) \subseteq \text{support}(f)$.
Equiv.Perm.SameCycle.mem_support_iff theorem
{f} [DecidableEq α] [Fintype α] (h : SameCycle f x y) : x ∈ support f ↔ y ∈ support f
Full source 
theorem SameCycle.mem_support_iff {f} [DecidableEq α] [Fintype α] (h : SameCycle f x y) :
    x ∈ support fx ∈ support f ↔ y ∈ support f :=
  ⟨fun hx => support_cycleOf_le f x (mem_support_cycleOf_iff.mpr ⟨h, hx⟩), fun hy =>
    support_cycleOf_le f y (mem_support_cycleOf_iff.mpr ⟨h.symm, hy⟩)⟩
Support Membership Equivalence for Elements in the Same Cycle of a Permutation
Informal description
For a permutation $f$ of a finite type $\alpha$ with decidable equality, if two elements $x$ and $y$ are in the same cycle of $f$ (i.e., $\text{SameCycle } f \, x \, y$ holds), then $x$ is in the support of $f$ if and only if $y$ is in the support of $f$.
Equiv.Perm.pow_mod_card_support_cycleOf_self_apply theorem
[DecidableEq α] [Fintype α] (f : Perm α) (n : ℕ) (x : α) : (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x
Full source 
theorem pow_mod_card_support_cycleOf_self_apply [DecidableEq α] [Fintype α]
    (f : Perm α) (n : ℕ) (x : α) : (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x := by
  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 [← cycleOf_pow_apply_self, ← cycleOf_pow_apply_self f, ← (isCycle_cycleOf f hx).orderOf,
      pow_mod_orderOf]
Periodicity of Permutation Powers Modulo Cycle Support Size
Informal description
Let $\alpha$ be a finite type with decidable equality, $f$ be a permutation of $\alpha$, $n$ be a natural number, and $x$ be an element of $\alpha$. Then the action of $f$ raised to the power $(n \mod \#\text{support}(f.\text{cycleOf } x))$ on $x$ equals the action of $f$ raised to the power $n$ on $x$. That is: \[ (f^{n \mod \#\text{support}(f.\text{cycleOf } x)}) x = f^n x \]
Equiv.Perm.SameCycle.exists_pow_eq theorem
[DecidableEq α] [Fintype α] (f : Perm α) (h : SameCycle f x y) : ∃ i : ℕ, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y
Full source 
theorem SameCycle.exists_pow_eq [DecidableEq α] [Fintype α] (f : Perm α) (h : SameCycle f x y) :
    ∃ i : ℕ, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y := by
  by_cases hx : x ∈ f.support
  · obtain ⟨k, hk, hk'⟩ := h.exists_pow_eq_of_mem_support hx
    rcases k with - | k
    · refine ⟨#(f.cycleOf x).support, ?_, self_le_add_right _ _, ?_⟩
      · refine zero_lt_one.trans (one_lt_card_support_of_ne_one ?_)
        simpa using hx
      · simp only [pow_zero, coe_one, id_eq] at hk'
        subst hk'
        rw [← (isCycle_cycleOf _ <| mem_support.1 hx).orderOf, ← cycleOf_pow_apply_self,
          pow_orderOf_eq_one, one_apply]
    · exact ⟨k + 1, by simp, Nat.le_succ_of_le hk.le, hk'⟩
  · refine ⟨1, zero_lt_one, by simp, ?_⟩
    obtain ⟨k, rfl⟩ := h
    rw [not_mem_support] at hx
    rw [pow_apply_eq_self_of_apply_eq_self hx, zpow_apply_eq_self_of_apply_eq_self hx]
Existence of Power Mapping Elements in Same Cycle with Bounded Exponent
Informal description
Let $\alpha$ be a finite type with decidable equality, and let $f$ be a permutation of $\alpha$. If two elements $x$ and $y$ are in the same cycle of $f$ (i.e., $\text{SameCycle } f \, x \, y$ holds), then there exists a positive integer $i$ such that: 1. $i \leq \#\text{support}(f.\text{cycleOf } x) + 1$, 2. $f^i(x) = y$. Here, $\text{support}(f.\text{cycleOf } x)$ denotes the set of elements not fixed by the cycle of $f$ containing $x$.
Equiv.Perm.zpow_eq_zpow_on_iff theorem
[DecidableEq α] [Fintype α] (g : Perm α) {m n : ℤ} {x : α} (hx : g x ≠ x) : (g ^ m) x = (g ^ n) x ↔ m % #(g.cycleOf x).support = n % #(g.cycleOf x).support
Full source 
theorem zpow_eq_zpow_on_iff [DecidableEq α] [Fintype α]
    (g : Perm α) {m n : ℤ} {x : α} (hx : g x ≠ x) :
    (g ^ m) x = (g ^ n) x ↔ m % #(g.cycleOf x).support = n % #(g.cycleOf x).support := by
  rw [Int.emod_eq_emod_iff_emod_sub_eq_zero]
  conv_lhs => rw [← Int.sub_add_cancel m n, Int.add_comm, zpow_add]
  simp only [coe_mul, Function.comp_apply, EmbeddingLike.apply_eq_iff_eq]
  rw [← Int.dvd_iff_emod_eq_zero]
  rw [← cycleOf_zpow_apply_self g x, cycle_zpow_mem_support_iff]
  · rw [← Int.dvd_iff_emod_eq_zero]
  · exact isCycle_cycleOf g hx
  · simp only [mem_support, cycleOf_apply_self]; exact hx
Cycle Permutation Powers Agree on Element iff Exponents are Congruent Modulo Cycle Support Size
Informal description
Let $\alpha$ be a finite type with decidable equality, $g$ be a permutation of $\alpha$, and $x \in \alpha$ be an element not fixed by $g$ (i.e., $g(x) \neq x$). Then for any integers $m$ and $n$, the following are equivalent: 1. The action of $g^m$ on $x$ equals the action of $g^n$ on $x$, i.e., $g^m(x) = g^n(x)$. 2. The integers $m$ and $n$ are congruent modulo the size of the support of the cycle containing $x$ in $g$, i.e., $m \equiv n \pmod{\#\text{supp}(g.\text{cycleOf } x)}$. In symbols: $$g^m(x) = g^n(x) \leftrightarrow m \equiv n \pmod{\#\text{supp}(g.\text{cycleOf } x)}.$$
Equiv.Perm.cycleFactorsAux definition
[DecidableEq α] [Fintype α] (l : List α) (f : Perm α) (h : ∀ {x}, f x ≠ x → x ∈ l) : { pl : List (Perm α) // pl.prod = f ∧ (∀ g ∈ pl, IsCycle g) ∧ pl.Pairwise Disjoint }
Full source 
/-- Given a list `l : List α` and a permutation `f : Perm α` whose nonfixed points are all in `l`,
  recursively factors `f` into cycles. -/
def cycleFactorsAux [DecidableEq α] [Fintype α]
    (l : List α) (f : Perm α) (h : ∀ {x}, f x ≠ x → x ∈ l) :
    { pl : List (Perm α) // pl.prod = f ∧ (∀ g ∈ pl, IsCycle g) ∧ pl.Pairwise Disjoint } :=
  go l f h (fun _ => rfl)
where
  /-- The auxiliary of `cycleFactorsAux`. This functions separates cycles from `f` instead of `g`
  to prevent the process of a cycle gets complex. -/
  go (l : List α) (g : Perm α) (hg : ∀ {x}, g x ≠ x → x ∈ l)
    (hfg : ∀ {x}, g x ≠ x → cycleOf f x = cycleOf g x) :
    { pl : List (Perm α) // pl.prod = g ∧ (∀ g' ∈ pl, IsCycle g') ∧ pl.Pairwise Disjoint } :=
  match l with
  | [] => ⟨[], by
      { simp only [imp_false, List.Pairwise.nil, List.not_mem_nil, forall_const, and_true,
          forall_prop_of_false, Classical.not_not, not_false_iff, List.prod_nil] at *
        ext
        simp [*]}⟩
  | x :: l =>
    if hx : g x = x then go l g (by
        intro y hy; exact List.mem_of_ne_of_mem (fun h => hy (by rwa [h])) (hg hy)) hfg
    else
      let ⟨m, hm₁, hm₂, hm₃⟩ :=
        go l ((cycleOf f x)⁻¹ * g) (by
            rw [hfg hx]
            intro y hy
            exact List.mem_of_ne_of_mem
              (fun h : y = x => by
                rw [h, mul_apply, Ne, inv_eq_iff_eq, cycleOf_apply_self] at hy
                exact hy rfl)
              (hg fun h : g y = y => by
                rw [mul_apply, h, Ne, inv_eq_iff_eq, cycleOf_apply] at hy
                split_ifs at hy <;> tauto))
          (by
            rw [hfg hx]
            intro y hy
            simp [inv_eq_iff_eq, cycleOf_apply, eq_comm (a := g y)] at hy
            rw [hfg (Ne.symm hy.right), ← mul_inv_eq_one (a := g.cycleOf y), cycleOf_inv]
            simp_rw [mul_inv_rev]
            rw [inv_inv, cycleOf_mul_of_apply_right_eq_self, ← cycleOf_inv, mul_inv_eq_one]
            · rw [Commute.inv_left_iff, commute_iff_eq]
              ext z; by_cases hz : SameCycle g x z
              · simp [cycleOf_apply, hz]
              · simp [cycleOf_apply_of_not_sameCycle, hz]
            · exact cycleOf_apply_of_not_sameCycle hy.left)
      ⟨cycleOf f x :: m, by
        rw [hfg hx] at hm₁ ⊢
        constructor
        · rw [List.prod_cons, hm₁]
          simp
        · exact
            ⟨fun g' hg' =>
              ((List.mem_cons).1 hg').elim (fun hg' => hg'.symm ▸ isCycle_cycleOf _ hx) (hm₂ g'),
              List.pairwise_cons.2
                ⟨fun g' hg' y =>
                  or_iff_not_imp_left.2 fun hgy =>
                    have hxy : SameCycle g x y :=
                      Classical.not_not.1 (mt cycleOf_apply_of_not_sameCycle hgy)
                    have hg'm : (g' :: m.erase g') ~ m :=
                      List.cons_perm_iff_perm_erase.2 ⟨hg', List.Perm.refl _⟩
                    have : ∀ h ∈ m.erase g', Disjoint g' h :=
                      (List.pairwise_cons.1 ((hg'm.pairwise_iff Disjoint.symm).2 hm₃)).1
                    by_cases id fun hg'y : g' y ≠ y =>
                      (disjoint_prod_right _ this y).resolve_right <| by
                        have hsc : SameCycle g⁻¹ x (g y) := by
                          rwa [sameCycle_inv, sameCycle_apply_right]
                        rw [disjoint_prod_perm hm₃ hg'm.symm, List.prod_cons,
                            ← eq_inv_mul_iff_mul_eq] at hm₁
                        rwa [hm₁, mul_apply, mul_apply, cycleOf_inv, hsc.cycleOf_apply,
                          inv_apply_self, inv_eq_iff_eq, eq_comm],
                  hm₃⟩⟩⟩
Cycle factorization of a permutation with respect to a list of elements
Informal description
Given a finite type $\alpha$ with decidable equality, a list $l$ of elements of $\alpha$, and a permutation $f$ of $\alpha$ such that every non-fixed point of $f$ is in $l$, the function `cycleFactorsAux` recursively factors $f$ into a list of disjoint cyclic permutations whose product is $f$. More precisely, `cycleFactorsAux l f h` returns a list $[g_1, \ldots, g_n]$ of permutations such that: 1. The product $g_1 \cdots g_n = f$, 2. Each $g_i$ is a cycle (i.e., satisfies `IsCycle`), 3. The cycles $g_i$ are pairwise disjoint.
Equiv.Perm.mem_list_cycles_iff theorem
{α : Type*} [Finite α] {l : List (Perm α)} (h1 : ∀ σ : Perm α, σ ∈ l → σ.IsCycle) (h2 : l.Pairwise Disjoint) {σ : Perm α} : σ ∈ l ↔ σ.IsCycle ∧ ∀ a, σ a ≠ a → σ a = l.prod a
Full source 
theorem mem_list_cycles_iff {α : Type*} [Finite α] {l : List (Perm α)}
    (h1 : ∀ σ : Perm α, σ ∈ l → σ.IsCycle) (h2 : l.Pairwise Disjoint) {σ : Perm α} :
    σ ∈ lσ ∈ l ↔ σ.IsCycle ∧ ∀ a, σ a ≠ a → σ a = l.prod a := by
  suffices σ.IsCycle → (σ ∈ lσ ∈ l ↔ ∀ a, σ a ≠ a → σ a = l.prod a) by
    exact ⟨fun hσ => ⟨h1 σ hσ, (this (h1 σ hσ)).mp hσ⟩, fun hσ => (this hσ.1).mpr hσ.2⟩
  intro h3
  classical
    cases nonempty_fintype α
    constructor
    · intro h a ha
      exact eq_on_support_mem_disjoint h h2 _ (mem_support.mpr ha)
    · intro h
      have hσl : σ.support ⊆ l.prod.support := by
        intro x hx
        rw [mem_support] at hx
        rwa [mem_support, ← h _ hx]
      obtain ⟨a, ha, -⟩ := id h3
      rw [← mem_support] at ha
      obtain ⟨τ, hτ, hτa⟩ := exists_mem_support_of_mem_support_prod (hσl ha)
      have hτl : ∀ x ∈ τ.support, τ x = l.prod x := eq_on_support_mem_disjoint hτ h2
      have key : ∀ x ∈ σ.support ∩ τ.support, σ x = τ x := by
        intro x hx
        rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]
      convert hτ
      refine h3.eq_on_support_inter_nonempty_congr (h1 _ hτ) key ?_ ha
      exact key a (mem_inter_of_mem ha hτa)
Characterization of Permutations in a List of Disjoint Cycles
Informal description
Let $\alpha$ be a finite type, and let $l$ be a list of permutations of $\alpha$ such that: 1. Every permutation in $l$ is a cycle (i.e., satisfies $\text{IsCycle}$). 2. The permutations in $l$ are pairwise disjoint. Then for any permutation $\sigma$ of $\alpha$, $\sigma$ is in the list $l$ if and only if: 1. $\sigma$ is a cycle, and 2. For every element $a \in \alpha$ such that $\sigma(a) \neq a$, we have $\sigma(a) = \prod_{g \in l} g(a)$.
Equiv.Perm.list_cycles_perm_list_cycles theorem
{α : Type*} [Finite α] {l₁ l₂ : List (Perm α)} (h₀ : l₁.prod = l₂.prod) (h₁l₁ : ∀ σ : Perm α, σ ∈ l₁ → σ.IsCycle) (h₁l₂ : ∀ σ : Perm α, σ ∈ l₂ → σ.IsCycle) (h₂l₁ : l₁.Pairwise Disjoint) (h₂l₂ : l₂.Pairwise Disjoint) : l₁ ~ l₂
Full source 
theorem list_cycles_perm_list_cycles {α : Type*} [Finite α] {l₁ l₂ : List (Perm α)}
    (h₀ : l₁.prod = l₂.prod) (h₁l₁ : ∀ σ : Perm α, σ ∈ l₁ → σ.IsCycle)
    (h₁l₂ : ∀ σ : Perm α, σ ∈ l₂ → σ.IsCycle) (h₂l₁ : l₁.Pairwise Disjoint)
    (h₂l₂ : l₂.Pairwise Disjoint) : l₁ ~ l₂ := by
  classical
    refine
      (List.perm_ext_iff_of_nodup (nodup_of_pairwise_disjoint_cycles h₁l₁ h₂l₁)
            (nodup_of_pairwise_disjoint_cycles h₁l₂ h₂l₂)).mpr
        fun σ => ?_
    by_cases hσ : σ.IsCycle
    · obtain _ := not_forall.mp (mt ext hσ.ne_one)
      rw [mem_list_cycles_iff h₁l₁ h₂l₁, mem_list_cycles_iff h₁l₂ h₂l₂, h₀]
    · exact iff_of_false (mt (h₁l₁ σ) hσ) (mt (h₁l₂ σ) hσ)
Uniqueness of Cycle Factorization up to Permutation
Informal description
Let $\alpha$ be a finite type, and let $l_1$ and $l_2$ be two lists of permutations of $\alpha$ such that: 1. The product of the permutations in $l_1$ equals the product of the permutations in $l_2$ (i.e., $\prod_{g \in l_1} g = \prod_{h \in l_2} h$), 2. Every permutation in $l_1$ and $l_2$ is a cycle (i.e., satisfies $\text{IsCycle}$), 3. The permutations in $l_1$ are pairwise disjoint, 4. The permutations in $l_2$ are pairwise disjoint. Then $l_1$ and $l_2$ are permutations of each other (i.e., $l_1 \sim l_2$).
Equiv.Perm.cycleFactors definition
[Fintype α] [LinearOrder α] (f : Perm α) : { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint }
Full source 
/-- Factors a permutation `f` into a list of disjoint cyclic permutations that multiply to `f`. -/
def cycleFactors [Fintype α] [LinearOrder α] (f : Perm α) :
    { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } :=
  cycleFactorsAux (sort (α := α) (· ≤ ·) univ) f (fun {_ _} ↦ (mem_sort _).2 (mem_univ _))
Cycle factorization of a permutation
Informal description
Given a finite type $\alpha$ with a linear order and a permutation $f$ of $\alpha$, the function `cycleFactors` returns a list of disjoint cyclic permutations whose product is $f$. More precisely, `cycleFactors f` returns a list $[g_1, \ldots, g_n]$ of permutations such that: 1. The product $g_1 \cdots g_n = f$, 2. Each $g_i$ is a cycle (i.e., satisfies `IsCycle`), 3. The cycles $g_i$ are pairwise disjoint.
Equiv.Perm.truncCycleFactors definition
[DecidableEq α] [Fintype α] (f : Perm α) : Trunc { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint }
Full source 
/-- Factors a permutation `f` into a list of disjoint cyclic permutations that multiply to `f`,
  without a linear order. -/
def truncCycleFactors [DecidableEq α] [Fintype α] (f : Perm α) :
    Trunc { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } :=
  Quotient.recOnSubsingleton (@univ α _).1 (fun l h => Trunc.mk (cycleFactorsAux l f (h _)))
    (show ∀ x, f x ≠ x → x ∈ (@univ α _).1 from fun _ _ => mem_univ _)
Truncated cycle factorization of a permutation
Informal description
Given a finite type $\alpha$ with decidable equality and a permutation $f$ of $\alpha$, the function `truncCycleFactors` returns a truncated list of disjoint cyclic permutations whose product is $f$. More precisely, `truncCycleFactors f` produces a list $[g_1, \ldots, g_n]$ (up to truncation) such that: 1. The product $g_1 \cdots g_n = f$, 2. Each $g_i$ is a cycle (i.e., satisfies `IsCycle`), 3. The cycles $g_i$ are pairwise disjoint.
Equiv.Perm.cycleFactorsFinset definition
: Finset (Perm α)
Full source 
/-- Factors a permutation `f` into a `Finset` of disjoint cyclic permutations that multiply to `f`.
-/
def cycleFactorsFinset : Finset (Perm α) :=
  (truncCycleFactors f).lift
    (fun l : { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } =>
      l.val.toFinset)
    fun ⟨_, hl⟩ ⟨_, hl'⟩ =>
    List.toFinset_eq_of_perm _ _
      (list_cycles_perm_list_cycles (hl'.left.symm ▸ hl.left) hl.right.left hl'.right.left
        hl.right.right hl'.right.right)
Finite set of cycle factors of a permutation
Informal description
Given a finite type $\alpha$ and a permutation $f$ of $\alpha$, the function `cycleFactorsFinset` returns a finite set of disjoint cyclic permutations whose product is $f$. More precisely, `cycleFactorsFinset f` produces a finite set $\{g_1, \ldots, g_n\}$ such that: 1. The product $g_1 \cdots g_n = f$, 2. Each $g_i$ is a cycle (i.e., satisfies `IsCycle`), 3. The cycles $g_i$ are pairwise disjoint.
Equiv.Perm.cycleFactorsFinset_eq_list_toFinset theorem
{σ : Perm α} {l : List (Perm α)} (hn : l.Nodup) : σ.cycleFactorsFinset = l.toFinset ↔ (∀ f : Perm α, f ∈ l → f.IsCycle) ∧ l.Pairwise Disjoint ∧ l.prod = σ
Full source 
theorem cycleFactorsFinset_eq_list_toFinset {σ : Perm α} {l : List (Perm α)} (hn : l.Nodup) :
    σ.cycleFactorsFinset = l.toFinset ↔
      (∀ f : Perm α, f ∈ l → f.IsCycle) ∧ l.Pairwise Disjoint ∧ l.prod = σ := by
  obtain ⟨⟨l', hp', hc', hd'⟩, hl⟩ := Trunc.exists_rep σ.truncCycleFactors
  have ht : cycleFactorsFinset σ = l'.toFinset := by
    rw [cycleFactorsFinset, ← hl, Trunc.lift_mk]
  rw [ht]
  constructor
  · intro h
    have hn' : l'.Nodup := nodup_of_pairwise_disjoint_cycles hc' hd'
    have hperm : l ~ l' := List.perm_of_nodup_nodup_toFinset_eq hn hn' h.symm
    refine ⟨?_, ?_, ?_⟩
    · exact fun _ h => hc' _ (hperm.subset h)
    · have := List.Perm.pairwise_iff (@Disjoint.symmetric _) hperm
      rwa [this]
    · rw [← hp', hperm.symm.prod_eq']
      refine hd'.imp ?_
      exact Disjoint.commute
  · rintro ⟨hc, hd, hp⟩
    refine List.toFinset_eq_of_perm _ _ ?_
    refine list_cycles_perm_list_cycles ?_ hc' hc hd' hd
    rw [hp, hp']
Characterization of Cycle Factors Finset via List Conditions
Informal description
Let $\alpha$ be a finite type with decidable equality, $\sigma$ a permutation of $\alpha$, and $l$ a list of permutations of $\alpha$ with no duplicates. Then the cycle factors finset of $\sigma$ equals the finset constructed from $l$ if and only if: 1. Every permutation in $l$ is a cycle, 2. The permutations in $l$ are pairwise disjoint, and 3. The product of the permutations in $l$ equals $\sigma$. In other words, $\sigma.\text{cycleFactorsFinset} = l.\text{toFinset}$ holds precisely when $l$ consists of pairwise disjoint cycles whose product is $\sigma$ and has no duplicate elements.
Equiv.Perm.cycleFactorsFinset_eq_finset theorem
{σ : Perm α} {s : Finset (Perm α)} : σ.cycleFactorsFinset = s ↔ (∀ f : Perm α, f ∈ s → f.IsCycle) ∧ ∃ h : (s : Set (Perm α)).Pairwise Disjoint, s.noncommProd id (h.mono' fun _ _ => Disjoint.commute) = σ
Full source 
theorem cycleFactorsFinset_eq_finset {σ : Perm α} {s : Finset (Perm α)} :
    σ.cycleFactorsFinset = s ↔
      (∀ f : Perm α, f ∈ s → f.IsCycle) ∧
        ∃ h : (s : Set (Perm α)).Pairwise Disjoint,
          s.noncommProd id (h.mono' fun _ _ => Disjoint.commute) = σ := by
  obtain ⟨l, hl, rfl⟩ := s.exists_list_nodup_eq
  simp [cycleFactorsFinset_eq_list_toFinset, hl]
Characterization of Cycle Factors of a Permutation via Finite Set Equality
Informal description
For a permutation $\sigma$ of a finite type $\alpha$ and a finite set $s$ of permutations of $\alpha$, the following are equivalent: 1. The set of cycle factors of $\sigma$ is equal to $s$. 2. Every permutation in $s$ is a cycle, and there exists a pairwise disjointness condition on $s$ such that the noncommutative product of the permutations in $s$ (with respect to the identity function) equals $\sigma$.
Equiv.Perm.cycleFactorsFinset_pairwise_disjoint theorem
: (cycleFactorsFinset f : Set (Perm α)).Pairwise Disjoint
Full source 
theorem cycleFactorsFinset_pairwise_disjoint :
    (cycleFactorsFinset f : Set (Perm α)).Pairwise Disjoint :=
  (cycleFactorsFinset_eq_finset.mp rfl).2.choose
Pairwise Disjointness of Cycle Factors in a Permutation
Informal description
For any permutation $f$ of a finite type $\alpha$, the cycles in the finite set of cycle factors of $f$ are pairwise disjoint. That is, for any two distinct cycles $g_1$ and $g_2$ in $\text{cycleFactorsFinset}(f)$, the supports of $g_1$ and $g_2$ are disjoint.
Equiv.Perm.cycleFactorsFinset_mem_commute theorem
: (cycleFactorsFinset f : Set (Perm α)).Pairwise Commute
Full source 
/-- Two cycles of a permutation commute. -/
theorem cycleFactorsFinset_mem_commute : (cycleFactorsFinset f : Set (Perm α)).Pairwise Commute :=
  (cycleFactorsFinset_pairwise_disjoint _).mono' fun _ _ => Disjoint.commute
Commutation of Cycle Factors in a Permutation
Informal description
For any permutation $f$ of a finite type $\alpha$, the cycles in the finite set of cycle factors of $f$ pairwise commute. That is, for any two distinct cycles $g_1$ and $g_2$ in $\text{cycleFactorsFinset}(f)$, we have $g_1 \circ g_2 = g_2 \circ g_1$.
Equiv.Perm.cycleFactorsFinset_mem_commute' theorem
{g1 g2 : Perm α} (h1 : g1 ∈ f.cycleFactorsFinset) (h2 : g2 ∈ f.cycleFactorsFinset) : Commute g1 g2
Full source 
/-- Two cycles of a permutation commute. -/
theorem cycleFactorsFinset_mem_commute' {g1 g2 : Perm α}
    (h1 : g1 ∈ f.cycleFactorsFinset) (h2 : g2 ∈ f.cycleFactorsFinset) :
    Commute g1 g2 := by
  rcases eq_or_ne g1 g2 with rfl | h
  · apply Commute.refl
  · exact Equiv.Perm.cycleFactorsFinset_mem_commute f h1 h2 h
Commutation of Distinct Cycles in a Permutation's Decomposition
Informal description
For any permutation $f$ of a finite type $\alpha$, if $g_1$ and $g_2$ are two distinct cycles in the cycle decomposition of $f$, then $g_1$ and $g_2$ commute, i.e., $g_1 \circ g_2 = g_2 \circ g_1$.
Equiv.Perm.mem_cycleFactorsFinset_iff theorem
{f p : Perm α} : p ∈ cycleFactorsFinset f ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
Full source 
theorem mem_cycleFactorsFinset_iff {f p : Perm α} :
    p ∈ cycleFactorsFinset fp ∈ cycleFactorsFinset f ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a := by
  obtain ⟨l, hl, hl'⟩ := f.cycleFactorsFinset.exists_list_nodup_eq
  rw [← hl']
  rw [eq_comm, cycleFactorsFinset_eq_list_toFinset hl] at hl'
  simpa [List.mem_toFinset, Ne, ← hl'.right.right] using
    mem_list_cycles_iff hl'.left hl'.right.left
Characterization of Cycle Factors in a Permutation
Informal description
Let $\alpha$ be a finite type and $f, p$ be permutations of $\alpha$. Then $p$ belongs to the cycle factors finset of $f$ if and only if: 1. $p$ is a cycle, and 2. For every element $a$ in the support of $p$, we have $p(a) = f(a)$.
Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff theorem
{f : Perm α} {x : α} : cycleOf f x ∈ cycleFactorsFinset f ↔ x ∈ f.support
Full source 
theorem cycleOf_mem_cycleFactorsFinset_iff {f : Perm α} {x : α} :
    cycleOfcycleOf f x ∈ cycleFactorsFinset fcycleOf f x ∈ cycleFactorsFinset f ↔ x ∈ f.support := by
  rw [mem_cycleFactorsFinset_iff]
  constructor
  · rintro ⟨hc, _⟩
    contrapose! hc
    rw [not_mem_support, ← cycleOf_eq_one_iff] at hc
    simp [hc]
  · intro hx
    refine ⟨isCycle_cycleOf _ (mem_support.mp hx), ?_⟩
    intro y hy
    rw [mem_support] at hy
    rw [cycleOf_apply]
    split_ifs with H
    · rfl
    · rw [cycleOf_apply_of_not_sameCycle H] at hy
      contradiction
Cycle Factor Membership Criterion: $f.\text{cycleOf}(x) \in \text{cycleFactorsFinset}(f) \leftrightarrow x \in \text{support}(f)$
Informal description
For a permutation $f$ of a finite type $\alpha$ and an element $x \in \alpha$, the cycle of $f$ containing $x$ is a factor in the cycle decomposition of $f$ if and only if $x$ is in the support of $f$ (i.e., $f(x) \neq x$).
Equiv.Perm.cycleOf_ne_one_iff_mem_cycleFactorsFinset theorem
{g : Equiv.Perm α} {x : α} : g.cycleOf x ≠ 1 ↔ g.cycleOf x ∈ g.cycleFactorsFinset
Full source 
lemma cycleOf_ne_one_iff_mem_cycleFactorsFinset {g : Equiv.Perm α} {x : α} :
    g.cycleOf x ≠ 1g.cycleOf x ≠ 1 ↔ g.cycleOf x ∈ g.cycleFactorsFinset := by
  rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support, ne_eq, cycleOf_eq_one_iff]
Cycle Non-triviality Criterion: $g.\text{cycleOf}(x) \neq 1 \leftrightarrow g.\text{cycleOf}(x) \in \text{cycleFactorsFinset}(g)$
Informal description
For a permutation $g$ of a finite type $\alpha$ and an element $x \in \alpha$, the cycle of $g$ containing $x$ is non-trivial (i.e., not the identity permutation) if and only if it belongs to the cycle factors finset of $g$.
Equiv.Perm.mem_cycleFactorsFinset_support_le theorem
{p f : Perm α} (h : p ∈ cycleFactorsFinset f) : p.support ≤ f.support
Full source 
theorem mem_cycleFactorsFinset_support_le {p f : Perm α} (h : p ∈ cycleFactorsFinset f) :
    p.support ≤ f.support := by
  rw [mem_cycleFactorsFinset_iff] at h
  intro x hx
  rwa [mem_support, ← h.right x hx, ← mem_support]
Support of Cycle Factor is Contained in Support of Permutation
Informal description
For any permutations $p$ and $f$ of a finite type $\alpha$, if $p$ is a cycle factor of $f$ (i.e., $p \in \text{cycleFactorsFinset}(f)$), then the support of $p$ is a subset of the support of $f$.
Equiv.Perm.support_zpowers_of_mem_cycleFactorsFinset_le theorem
{g : Perm α} {c : g.cycleFactorsFinset} (v : Subgroup.zpowers (c : Perm α)) : (v : Perm α).support ≤ g.support
Full source 
lemma support_zpowers_of_mem_cycleFactorsFinset_le {g : Perm α}
    {c : g.cycleFactorsFinset} (v : Subgroup.zpowers (c : Perm α)) :
    (v : Perm α).support ≤ g.support := by
  obtain ⟨m, hm⟩ := v.prop
  simp only [← hm]
  exact le_trans (support_zpow_le _ _) (mem_cycleFactorsFinset_support_le c.prop)
Support of Powers of Cycle Factor is Contained in Support of Permutation
Informal description
For any permutation $g$ of a finite type $\alpha$ and any cycle factor $c$ in the finite set of cycle factors of $g$, the support of any element $v$ in the subgroup generated by $c$ is contained in the support of $g$. In other words, if $v$ is a power of $c$, then $\text{supp}(v) \subseteq \text{supp}(g)$.
Equiv.Perm.pairwise_disjoint_of_mem_zpowers theorem
: Pairwise fun (i j : f.cycleFactorsFinset) ↦ ∀ (x y : Perm α), x ∈ Subgroup.zpowers ↑i → y ∈ Subgroup.zpowers ↑j → Disjoint x y
Full source 
theorem pairwise_disjoint_of_mem_zpowers :
    Pairwise fun (i j : f.cycleFactorsFinset) ↦
      ∀ (x y : Perm α), x ∈ Subgroup.zpowers ↑i → y ∈ Subgroup.zpowers ↑j → Disjoint x y :=
  fun c d  hcd ↦ fun x y hx hy ↦ by
  obtain ⟨m, hm⟩ := hx; obtain ⟨n, hn⟩ := hy
  simp only [← hm, ← hn]
  apply Disjoint.zpow_disjoint_zpow
  exact f.cycleFactorsFinset_pairwise_disjoint c.prop d.prop (Subtype.coe_ne_coe.mpr hcd)
Pairwise Disjointness of Subgroups Generated by Cycle Factors
Informal description
For any permutation $f$ of a finite type $\alpha$, the cycles in the finite set of cycle factors of $f$ are pairwise disjoint in the following sense: for any two distinct cycles $i$ and $j$ in $\text{cycleFactorsFinset}(f)$, and for any elements $x$ in the subgroup generated by $i$ and $y$ in the subgroup generated by $j$, the permutations $x$ and $y$ have disjoint supports.
Equiv.Perm.pairwise_commute_of_mem_zpowers theorem
: Pairwise fun (i j : f.cycleFactorsFinset) ↦ ∀ (x y : Perm α), x ∈ Subgroup.zpowers ↑i → y ∈ Subgroup.zpowers ↑j → Commute x y
Full source 
lemma pairwise_commute_of_mem_zpowers :
    Pairwise fun (i j : f.cycleFactorsFinset) ↦
      ∀ (x y : Perm α), x ∈ Subgroup.zpowers ↑i → y ∈ Subgroup.zpowers ↑j → Commute x y :=
  f.pairwise_disjoint_of_mem_zpowers.mono
    (fun _ _ ↦ forall₂_imp (fun _ _ h hx hy ↦ (h hx hy).commute))
Pairwise Commutativity of Subgroups Generated by Cycle Factors
Informal description
For any permutation $f$ of a finite type $\alpha$, the cycles in the finite set of cycle factors of $f$ are pairwise commuting in the following sense: for any two distinct cycles $i$ and $j$ in $\text{cycleFactorsFinset}(f)$, and for any elements $x$ in the subgroup generated by $i$ and $y$ in the subgroup generated by $j$, the permutations $x$ and $y$ commute.
Equiv.Perm.disjoint_ofSubtype_noncommPiCoprod theorem
(u : Perm (Function.fixedPoints f)) (v : (c : { x // x ∈ f.cycleFactorsFinset }) → (Subgroup.zpowers (c : Perm α))) : Disjoint (ofSubtype u) ((Subgroup.noncommPiCoprod f.pairwise_commute_of_mem_zpowers) v)
Full source 
lemma disjoint_ofSubtype_noncommPiCoprod (u : Perm (Function.fixedPoints f))
    (v : (c : { x // x ∈ f.cycleFactorsFinset }) → (Subgroup.zpowers (c : Perm α))) :
    Disjoint (ofSubtype u) ((Subgroup.noncommPiCoprod f.pairwise_commute_of_mem_zpowers) v) := by
  apply Finset.noncommProd_induction
  · intro a _ b _ h
    apply f.pairwise_commute_of_mem_zpowers h <;> simp only [Subgroup.coe_subtype, SetLike.coe_mem]
  · intro x y
    exact Disjoint.mul_right
  · exact disjoint_one_right _
  · intro c _
    simp only [Subgroup.coe_subtype]
    exact Disjoint.mono (disjoint_ofSubtype_of_memFixedPoints_self u)
      le_rfl (support_zpowers_of_mem_cycleFactorsFinset_le (v c))
Disjointness of Fixed Point Permutation and Cycle Factor Product
Informal description
Let $f$ be a permutation of a finite type $\alpha$, and let $u$ be a permutation of the fixed points of $f$. For any family of permutations $v$ where each $v(c)$ is in the subgroup generated by a cycle factor $c$ of $f$, the permutation $u$ (lifted to a permutation of $\alpha$) is disjoint from the product of the permutations $v(c)$ over all cycle factors $c$ of $f$.
Equiv.Perm.commute_ofSubtype_noncommPiCoprod theorem
(u : Perm (Function.fixedPoints f)) (v : (c : { x // x ∈ f.cycleFactorsFinset }) → (Subgroup.zpowers (c : Perm α))) : Commute (ofSubtype u) ((Subgroup.noncommPiCoprod f.pairwise_commute_of_mem_zpowers) v)
Full source 
lemma commute_ofSubtype_noncommPiCoprod (u : Perm (Function.fixedPoints f))
    (v : (c : { x // x ∈ f.cycleFactorsFinset }) → (Subgroup.zpowers (c : Perm α))) :
    Commute (ofSubtype u) ((Subgroup.noncommPiCoprod f.pairwise_commute_of_mem_zpowers) v) :=
  Disjoint.commute (f.disjoint_ofSubtype_noncommPiCoprod u v)
Commutativity of Fixed Point Permutation with Cycle Factor Product
Informal description
Let $f$ be a permutation of a finite type $\alpha$, and let $u$ be a permutation of the fixed points of $f$. For any family of permutations $v$ where each $v(c)$ is in the subgroup generated by a cycle factor $c$ of $f$, the permutation $u$ (lifted to a permutation of $\alpha$) commutes with the product of the permutations $v(c)$ over all cycle factors $c$ of $f$.
Equiv.Perm.mem_support_iff_mem_support_of_mem_cycleFactorsFinset theorem
{g : Equiv.Perm α} {x : α} : x ∈ g.support ↔ ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support
Full source 
theorem mem_support_iff_mem_support_of_mem_cycleFactorsFinset {g : Equiv.Perm α} {x : α} :
    x ∈ g.supportx ∈ g.support ↔ ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support := by
  constructor
  · intro h
    use g.cycleOf x, cycleOf_mem_cycleFactorsFinset_iff.mpr h
    rw [mem_support_cycleOf_iff]
    exact ⟨SameCycle.refl g x, h⟩
  · rintro ⟨c, hc, hx⟩
    exact mem_cycleFactorsFinset_support_le hc hx
Support Membership Criterion via Cycle Factors: $x \in \text{supp}(g) \leftrightarrow \exists c \in \text{cycleFactorsFinset}(g), x \in \text{supp}(c)$
Informal description
For a permutation $g$ of a finite type $\alpha$ and an element $x \in \alpha$, $x$ is in the support of $g$ (i.e., $g(x) \neq x$) if and only if there exists a cycle factor $c$ in the cycle decomposition of $g$ (i.e., $c \in g.\text{cycleFactorsFinset}$) such that $x$ is in the support of $c$.
Equiv.Perm.cycleFactorsFinset_eq_empty_iff theorem
{f : Perm α} : cycleFactorsFinset f = ∅ ↔ f = 1
Full source 
theorem cycleFactorsFinset_eq_empty_iff {f : Perm α} : cycleFactorsFinsetcycleFactorsFinset f = ∅ ↔ f = 1 := by
  simpa [cycleFactorsFinset_eq_finset] using eq_comm
Empty Cycle Factors Set Characterizes Identity Permutation
Informal description
For any permutation $f$ of a finite type $\alpha$, the set of cycle factors of $f$ is empty if and only if $f$ is the identity permutation.
Equiv.Perm.cycleFactorsFinset_one theorem
: cycleFactorsFinset (1 : Perm α) = ∅
Full source 
@[simp]
theorem cycleFactorsFinset_one : cycleFactorsFinset (1 : Perm α) = ∅ := by
  simp [cycleFactorsFinset_eq_empty_iff]
Cycle factors of the identity permutation are empty
Informal description
The cycle factors of the identity permutation on a finite type $\alpha$ is the empty set, i.e., $\text{cycleFactorsFinset}(1) = \emptyset$.
Equiv.Perm.cycleFactorsFinset_eq_singleton_self_iff theorem
{f : Perm α} : f.cycleFactorsFinset = { f } ↔ f.IsCycle
Full source 
@[simp]
theorem cycleFactorsFinset_eq_singleton_self_iff {f : Perm α} :
    f.cycleFactorsFinset = {f} ↔ f.IsCycle := by simp [cycleFactorsFinset_eq_finset]
Cycle factors are singleton $\{f\}$ iff $f$ is a cycle
Informal description
For any permutation $f$ of a finite type $\alpha$, the set of cycle factors of $f$ is the singleton $\{f\}$ if and only if $f$ is a cycle.
Equiv.Perm.cycleFactorsFinset_eq_singleton_iff theorem
{f g : Perm α} : f.cycleFactorsFinset = { g } ↔ f.IsCycle ∧ f = g
Full source 
theorem cycleFactorsFinset_eq_singleton_iff {f g : Perm α} :
    f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g := by
  suffices f = g → (g.IsCycle ↔ f.IsCycle) by
    rw [cycleFactorsFinset_eq_finset]
    simpa [eq_comm]
  rintro rfl
  exact Iff.rfl
Cycle factors are singleton $\{g\}$ iff $f$ is a cycle equal to $g$
Informal description
For any permutations $f$ and $g$ of a finite type $\alpha$, the set of cycle factors of $f$ is the singleton $\{g\}$ if and only if $f$ is a cycle and $f = g$.
Equiv.Perm.cycleFactorsFinset_injective theorem
: Function.Injective (@cycleFactorsFinset α _ _)
Full source 
/-- Two permutations `f g : Perm α` have the same cycle factors iff they are the same. -/
theorem cycleFactorsFinset_injective : Function.Injective (@cycleFactorsFinset α _ _) := by
  intro f g h
  rw [← cycleFactorsFinset_noncommProd f]
  simpa [h] using cycleFactorsFinset_noncommProd g
Injectivity of Cycle Factors Function for Permutations
Informal description
The function that maps a permutation $f$ of a finite type $\alpha$ to its finite set of cycle factors is injective. That is, if two permutations $f$ and $g$ have the same cycle factors, then $f = g$.
Equiv.Perm.Disjoint.disjoint_cycleFactorsFinset theorem
{f g : Perm α} (h : Disjoint f g) : _root_.Disjoint (cycleFactorsFinset f) (cycleFactorsFinset g)
Full source 
theorem Disjoint.disjoint_cycleFactorsFinset {f g : Perm α} (h : Disjoint f g) :
    _root_.Disjoint (cycleFactorsFinset f) (cycleFactorsFinset g) := by
  rw [disjoint_iff_disjoint_support] at h
  rw [Finset.disjoint_left]
  intro x hx hy
  simp only [mem_cycleFactorsFinset_iff, mem_support] at hx hy
  obtain ⟨⟨⟨a, ha, -⟩, hf⟩, -, hg⟩ := hx, hy
  have := h.le_bot (by simp [ha, ← hf a ha, ← hg a ha] : a ∈ f.support ∩ g.support)
  tauto
Disjoint Permutations Have Disjoint Cycle Factor Sets
Informal description
For any two permutations $f$ and $g$ of a finite type $\alpha$, if $f$ and $g$ are disjoint (i.e., they have no common non-fixed points), then their cycle factor finite sets are also disjoint. In other words, if $\text{Disjoint}(f, g)$ holds, then $\text{cycleFactorsFinset}(f) \cap \text{cycleFactorsFinset}(g) = \emptyset$.
Equiv.Perm.Disjoint.cycleFactorsFinset_mul_eq_union theorem
{f g : Perm α} (h : Disjoint f g) : cycleFactorsFinset (f * g) = cycleFactorsFinset f ∪ cycleFactorsFinset g
Full source 
theorem Disjoint.cycleFactorsFinset_mul_eq_union {f g : Perm α} (h : Disjoint f g) :
    cycleFactorsFinset (f * g) = cycleFactorsFinsetcycleFactorsFinset f ∪ cycleFactorsFinset g := by
  rw [cycleFactorsFinset_eq_finset]
  refine ⟨?_, ?_, ?_⟩
  · simp [or_imp, mem_cycleFactorsFinset_iff, forall_swap]
  · rw [coe_union, Set.pairwise_union_of_symmetric Disjoint.symmetric]
    exact
      ⟨cycleFactorsFinset_pairwise_disjoint _, cycleFactorsFinset_pairwise_disjoint _,
        fun x hx y hy _ =>
        h.mono (mem_cycleFactorsFinset_support_le hx) (mem_cycleFactorsFinset_support_le hy)⟩
  · rw [noncommProd_union_of_disjoint h.disjoint_cycleFactorsFinset]
    rw [cycleFactorsFinset_noncommProd, cycleFactorsFinset_noncommProd]
Cycle Factors of Composition of Disjoint Permutations Equals Union of Cycle Factors
Informal description
For any two disjoint permutations $f$ and $g$ of a finite type $\alpha$, the finite set of cycle factors of their composition $f \circ g$ is equal to the union of the cycle factor sets of $f$ and $g$. That is, $\text{cycleFactorsFinset}(f \circ g) = \text{cycleFactorsFinset}(f) \cup \text{cycleFactorsFinset}(g)$.
Equiv.Perm.disjoint_mul_inv_of_mem_cycleFactorsFinset theorem
{f g : Perm α} (h : f ∈ cycleFactorsFinset g) : Disjoint (g * f⁻¹) f
Full source 
theorem disjoint_mul_inv_of_mem_cycleFactorsFinset {f g : Perm α} (h : f ∈ cycleFactorsFinset g) :
    Disjoint (g * f⁻¹) f := by
  rw [mem_cycleFactorsFinset_iff] at h
  intro x
  by_cases hx : f x = x
  · exact Or.inr hx
  · refine Or.inl ?_
    rw [mul_apply, ← h.right, apply_inv_self]
    rwa [← support_inv, apply_mem_support, support_inv, mem_support]
Disjointness of Permutation Composition with Inverse Cycle Factor
Informal description
For any permutations $f$ and $g$ of a finite type $\alpha$, if $f$ belongs to the cycle factors finset of $g$, then the permutation $g \circ f^{-1}$ is disjoint from $f$. That is, $g \circ f^{-1}$ and $f$ have no common non-fixed points.
Equiv.Perm.cycle_is_cycleOf theorem
{f c : Equiv.Perm α} {a : α} (ha : a ∈ c.support) (hc : c ∈ f.cycleFactorsFinset) : c = f.cycleOf a
Full source 
/-- If c is a cycle, a ∈ c.support and c is a cycle of f, then `c = f.cycleOf a` -/
theorem cycle_is_cycleOf {f c : Equiv.Perm α} {a : α} (ha : a ∈ c.support)
    (hc : c ∈ f.cycleFactorsFinset) : c = f.cycleOf a := by
  suffices f.cycleOf a = c.cycleOf a by
    rw [this]
    apply symm
    exact
      Equiv.Perm.IsCycle.cycleOf_eq (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).left
        (Equiv.Perm.mem_support.mp ha)
  let hfc := (Equiv.Perm.disjoint_mul_inv_of_mem_cycleFactorsFinset hc).symm
  let hfc2 := Perm.Disjoint.commute hfc
  rw [← Equiv.Perm.cycleOf_mul_of_apply_right_eq_self hfc2]
  · simp only [hfc2.eq, inv_mul_cancel_right]
  -- `a` is in the support of `c`, hence it is not in the support of `g c⁻¹`
  exact
    Equiv.Perm.not_mem_support.mp
      (Finset.disjoint_left.mp (Equiv.Perm.Disjoint.disjoint_support hfc) ha)
Cycle Factor Equals Cycle of Contained Element
Informal description
Let $f$ and $c$ be permutations of a finite type $\alpha$, and let $a \in \alpha$ be an element in the support of $c$ (i.e., $c(a) \neq a$). If $c$ is a cycle factor of $f$ (i.e., $c \in f.\text{cycleFactorsFinset}$), then $c$ is equal to the cycle of $f$ containing $a$, i.e., $c = f.\text{cycleOf } a$.
Equiv.Perm.isCycleOn_support_of_mem_cycleFactorsFinset theorem
{g c : Equiv.Perm α} (hc : c ∈ g.cycleFactorsFinset) : IsCycleOn g c.support
Full source 
theorem isCycleOn_support_of_mem_cycleFactorsFinset {g c : Equiv.Perm α}
    (hc : c ∈ g.cycleFactorsFinset) :
    IsCycleOn g c.support := by
  obtain ⟨x, hx⟩ := IsCycle.nonempty_support (mem_cycleFactorsFinset_iff.mp hc).1
  rw [cycle_is_cycleOf hx hc]
  exact isCycleOn_support_cycleOf g x
Cyclic Action on Support of Cycle Factors
Informal description
For any permutations $g$ and $c$ of a finite type $\alpha$, if $c$ is a cycle factor of $g$ (i.e., $c \in g.\text{cycleFactorsFinset}$), then $g$ acts cyclically on the support of $c$. That is, for any two elements $x, y$ in the support of $c$, there exists an integer $i$ such that $g^i(x) = y$.
Equiv.Perm.zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff theorem
{g : Perm α} {x : α} {m : ℤ} {c : g.cycleFactorsFinset} : (g ^ m) x ∈ (c : Perm α).support ↔ x ∈ (c : Perm α).support
Full source 
theorem zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff {g : Perm α}
    {x : α} {m : ℤ} {c : g.cycleFactorsFinset} :
    (g ^ m) x ∈ (c : Perm α).support(g ^ m) x ∈ (c : Perm α).support ↔ x ∈ (c : Perm α).support := by
  rw [← g.eq_cycleOf_of_mem_cycleFactorsFinset_iff _ c.prop, cycleOf_self_apply_zpow,
    eq_cycleOf_of_mem_cycleFactorsFinset_iff _ _ c.prop]
Support Membership Preservation under Powers of a Permutation Cycle Factor
Informal description
For a permutation $g$ of a finite type $\alpha$, an element $x \in \alpha$, an integer $m \in \mathbb{Z}$, and a cycle factor $c$ in the cycle factorization of $g$, the element $g^m(x)$ belongs to the support of $c$ if and only if $x$ belongs to the support of $c$.
Equiv.Perm.mem_cycleFactorsFinset_conj theorem
(g k c : Perm α) : k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset
Full source 
/-- A permutation `c` is a cycle of `g` iff `k * c * k⁻¹` is a cycle of `k * g * k⁻¹` -/
theorem mem_cycleFactorsFinset_conj (g k c : Perm α) :
    k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinsetk * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset := by
  suffices imp_lemma : ∀ {g k c : Perm α},
      c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset by
    refine ⟨fun h ↦ ?_, imp_lemma⟩
    have aux : ∀ h : Perm α, h = k⁻¹ * (k * h * k⁻¹) * k := fun _ ↦ by group
    rw [aux g, aux c]
    exact imp_lemma h
  intro g k c
  simp only [mem_cycleFactorsFinset_iff]
  apply And.imp IsCycle.conj
  intro hc a ha
  simp only [coe_mul, Function.comp_apply, EmbeddingLike.apply_eq_iff_eq]
  apply hc
  rw [mem_support] at ha ⊢
  contrapose! ha
  simp only [mul_smul, ← Perm.smul_def] at ha ⊢
  rw [ha]
  simp only [Perm.smul_def, apply_inv_self]
Conjugation Invariance of Cycle Factors: $k c k^{-1} \in \text{cycleFactors}(k g k^{-1}) \leftrightarrow c \in \text{cycleFactors}(g)$
Informal description
Let $g$, $k$, and $c$ be permutations of a finite type $\alpha$. The conjugate permutation $k c k^{-1}$ belongs to the cycle factors of the conjugate permutation $k g k^{-1}$ if and only if $c$ belongs to the cycle factors of $g$.
Equiv.Perm.commute_of_mem_cycleFactorsFinset_commute theorem
(k g : Perm α) (hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c) : Commute k g
Full source 
/-- If a permutation commutes with every cycle of `g`, then it commutes with `g`

NB. The converse is false. Commuting with every cycle of `g` means that we belong
to the kernel of the action of `Equiv.Perm α` on `g.cycleFactorsFinset` -/
theorem commute_of_mem_cycleFactorsFinset_commute (k g : Perm α)
    (hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c) :
    Commute k g := by
  rw [← cycleFactorsFinset_noncommProd g (cycleFactorsFinset_mem_commute g)]
  apply Finset.noncommProd_commute
  simpa only [id_eq] using hk
Commutation with Cycle Factors Implies Commutation with Permutation
Informal description
Let $\alpha$ be a finite type and let $k$ and $g$ be permutations of $\alpha$. If $k$ commutes with every cycle in the cycle decomposition of $g$ (i.e., for every cycle $c$ in $\text{cycleFactorsFinset}(g)$, we have $k \circ c = c \circ k$), then $k$ commutes with $g$ itself (i.e., $k \circ g = g \circ k$).
Equiv.Perm.self_mem_cycle_factors_commute theorem
{g c : Perm α} (hc : c ∈ g.cycleFactorsFinset) : Commute c g
Full source 
/-- The cycles of a permutation commute with it -/
theorem self_mem_cycle_factors_commute {g c : Perm α}
    (hc : c ∈ g.cycleFactorsFinset) : Commute c g := by
  apply commute_of_mem_cycleFactorsFinset_commute
  intro c' hc'
  by_cases hcc' : c = c'
  · rw [hcc']
  · apply g.cycleFactorsFinset_mem_commute hc hc'; exact hcc'
Commutation of Cycle Factors with Permutation
Informal description
Let $\alpha$ be a finite type and let $g$ be a permutation of $\alpha$. For any cycle $c$ in the cycle decomposition of $g$ (i.e., $c \in \text{cycleFactorsFinset}(g)$), the cycle $c$ commutes with $g$ (i.e., $c \circ g = g \circ c$).
Equiv.Perm.mem_support_cycle_of_cycle theorem
{g d c : Perm α} (hc : c ∈ g.cycleFactorsFinset) (hd : d ∈ g.cycleFactorsFinset) : ∀ x : α, x ∈ c.support ↔ d x ∈ c.support
Full source 
/-- If `c` and `d` are cycles of `g`, then `d` stabilizes the support of `c` -/
theorem mem_support_cycle_of_cycle {g d c : Perm α}
    (hc : c ∈ g.cycleFactorsFinset) (hd : d ∈ g.cycleFactorsFinset) :
    ∀ x : α, x ∈ c.supportx ∈ c.support ↔ d x ∈ c.support := by
  intro x
  simp only [mem_support, not_iff_not]
  by_cases h : c = d
  · rw [← h, EmbeddingLike.apply_eq_iff_eq]
  · rw [← Perm.mul_apply,
      Commute.eq (cycleFactorsFinset_mem_commute g hc hd h),
      mul_apply, EmbeddingLike.apply_eq_iff_eq]
Cycle Support Invariance under Other Cycles in a Permutation
Informal description
Let $\alpha$ be a finite type and $g$ a permutation of $\alpha$. For any two cycles $c$ and $d$ in the cycle decomposition of $g$ (i.e., $c, d \in \text{cycleFactorsFinset}(g)$), and for any element $x \in \alpha$, we have that $x$ is in the support of $c$ if and only if $d(x)$ is in the support of $c$.
Equiv.Perm.mem_cycleFactorsFinset_support theorem
{g c : Perm α} (hc : c ∈ g.cycleFactorsFinset) (a : α) : a ∈ c.support ↔ g a ∈ c.support
Full source 
/-- If a permutation is a cycle of `g`, then its support is invariant under `g`. -/
theorem mem_cycleFactorsFinset_support {g c : Perm α} (hc : c ∈ g.cycleFactorsFinset) (a : α) :
    a ∈ c.supporta ∈ c.support ↔ g a ∈ c.support :=
  mem_support_iff_of_commute (self_mem_cycle_factors_commute hc).symm a
Support Invariance under Permutation Action for Cycle Factors
Informal description
Let $\alpha$ be a finite type and let $g$ be a permutation of $\alpha$. For any cycle $c$ in the cycle decomposition of $g$ (i.e., $c \in \text{cycleFactorsFinset}(g)$) and any element $a \in \alpha$, we have that $a$ belongs to the support of $c$ if and only if $g(a)$ belongs to the support of $c$.
Equiv.Perm.cycle_induction_on theorem
[Finite β] (P : Perm β → Prop) (σ : Perm β) (base_one : P 1) (base_cycles : ∀ σ : Perm β, σ.IsCycle → P σ) (induction_disjoint : ∀ σ τ : Perm β, Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)) : P σ
Full source 
@[elab_as_elim]
theorem cycle_induction_on [Finite β] (P : Perm β → Prop) (σ : Perm β) (base_one : P 1)
    (base_cycles : ∀ σ : Perm β, σ.IsCycle → P σ)
    (induction_disjoint : ∀ σ τ : Perm β,
      Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)) : P σ := by
  cases nonempty_fintype β
  suffices ∀ l : List (Perm β),
      (∀ τ : Perm β, τ ∈ l → τ.IsCycle) → l.Pairwise Disjoint → P l.prod by
    classical
      let x := σ.truncCycleFactors.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 fun _ _ => base_one
  · intro h1 h2
    rw [List.prod_cons]
    exact
      induction_disjoint σ l.prod (disjoint_prod_right _ (List.pairwise_cons.mp h2).1)
        (h1 _ List.mem_cons_self) (base_cycles σ (h1 σ List.mem_cons_self))
        (ih (fun τ hτ => h1 τ (List.mem_cons_of_mem σ hτ)) h2.of_cons)
Induction Principle for Permutations via Cycle Decomposition
Informal description
Let $β$ be a finite type and $P$ a property of permutations of $β$. To prove that $P(σ)$ holds for all permutations $σ$ of $β$, it suffices to: 1. Show that $P$ holds for the identity permutation (base case for 1) 2. Show that $P$ holds for all cyclic permutations (base case for cycles) 3. Show that if $σ$ and $τ$ are disjoint permutations where $σ$ is cyclic and $P(σ)$ and $P(τ)$ both hold, then $P(σ * τ)$ also holds (inductive step)
Equiv.Perm.cycleFactorsFinset_mul_inv_mem_eq_sdiff theorem
[DecidableEq α] [Fintype α] {f g : Perm α} (h : f ∈ cycleFactorsFinset g) : cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ { f }
Full source 
theorem cycleFactorsFinset_mul_inv_mem_eq_sdiff [DecidableEq α] [Fintype α] {f g : Perm α}
    (h : f ∈ cycleFactorsFinset g) : cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinsetcycleFactorsFinset g \ {f} := by
  revert f
  refine
    cycle_induction_on (P := fun {g : Perm α} ↦
      ∀ {f}, (f ∈ cycleFactorsFinset g)
        → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinsetcycleFactorsFinset g \ {f}) _ ?_ ?_ ?_
  · simp
  · intro σ hσ f hf
    simp only [cycleFactorsFinset_eq_singleton_self_iff.mpr hσ, mem_singleton] at hf ⊢
    simp [hf]
  · intro σ τ hd _ hσ hτ f
    simp_rw [hd.cycleFactorsFinset_mul_eq_union, mem_union]
    -- if only `wlog` could work here...
    rintro (hf | hf)
    · rw [hd.commute.eq, union_comm, union_sdiff_distrib, sdiff_singleton_eq_erase,
        erase_eq_of_not_mem, mul_assoc, Disjoint.cycleFactorsFinset_mul_eq_union, hσ hf]
      · rw [mem_cycleFactorsFinset_iff] at hf
        intro x
        rcases hd.symm x with hx | hx
        · exact Or.inl hx
        · refine Or.inr ?_
          by_cases hfx : f x = x
          · rw [← hfx]
            simpa [hx] using hfx.symm
          · rw [mul_apply]
            rw [← hf.right _ (mem_support.mpr hfx)] at hx
            contradiction
      · exact fun H =>
        not_mem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem hf H))
    · rw [union_sdiff_distrib, sdiff_singleton_eq_erase, erase_eq_of_not_mem, mul_assoc,
        Disjoint.cycleFactorsFinset_mul_eq_union, hτ hf]
      · rw [mem_cycleFactorsFinset_iff] at hf
        intro x
        rcases hd x with hx | hx
        · exact Or.inl hx
        · refine Or.inr ?_
          by_cases hfx : f x = x
          · rw [← hfx]
            simpa [hx] using hfx.symm
          · rw [mul_apply]
            rw [← hf.right _ (mem_support.mpr hfx)] at hx
            contradiction
      · exact fun H =>
        not_mem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem H hf))
Cycle Factor Removal: $\text{cycleFactorsFinset}(g \circ f^{-1}) = \text{cycleFactorsFinset}(g) \setminus \{f\}$ for $f \in \text{cycleFactorsFinset}(g)$
Informal description
Let $\alpha$ be a finite type with decidable equality, and let $f$ and $g$ be permutations of $\alpha$. If $f$ is a cycle factor of $g$ (i.e., $f \in \text{cycleFactorsFinset}(g)$), then the cycle factors of the composition $g \circ f^{-1}$ are exactly the cycle factors of $g$ with $f$ removed. That is, \[ \text{cycleFactorsFinset}(g \circ f^{-1}) = \text{cycleFactorsFinset}(g) \setminus \{f\}. \]
Equiv.Perm.IsCycle.forall_commute_iff theorem
[DecidableEq α] [Fintype α] (g z : Perm α) : (∀ c ∈ g.cycleFactorsFinset, Commute z c) ↔ ∀ c ∈ g.cycleFactorsFinset, ∃ (hc : ∀ x : α, x ∈ c.support ↔ z x ∈ c.support), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c
Full source 
theorem IsCycle.forall_commute_iff [DecidableEq α] [Fintype α] (g z : Perm α) :
    (∀ c ∈ g.cycleFactorsFinset, Commute z c) ↔
      ∀ c ∈ g.cycleFactorsFinset,
      ∃ (hc : ∀ x : α, x ∈ c.support ↔ z x ∈ c.support),
        ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c := by
  apply forall_congr'
  intro c
  apply imp_congr_right
  intro hc
  exact IsCycle.commute_iff (mem_cycleFactorsFinset_iff.mp hc).1
Characterization of Commuting Permutations via Cycle Factors: $z$ Commutes with All Cycle Factors of $g$ iff $z$ Preserves Supports and Acts as Powers on Each Cycle
Informal description
Let $\alpha$ be a finite type with decidable equality, and let $g$ and $z$ be permutations of $\alpha$. Then the following are equivalent: 1. For every cycle $c$ in the cycle factors finset of $g$, the permutations $z$ and $c$ commute. 2. For every cycle $c$ in the cycle factors finset of $g$, there exists a condition $hc$ stating that for any $x \in \alpha$, $x$ is in the support of $c$ if and only if $z(x)$ is in the support of $c$, and the restriction of $z$ to the support of $c$ (under condition $hc$) is an integer power of $c$.
Equiv.Perm.subtypePerm_on_cycleFactorsFinset theorem
[DecidableEq α] [Fintype α] {g c : Perm α} (hc : c ∈ g.cycleFactorsFinset) : g.subtypePerm (mem_cycleFactorsFinset_support hc) = c.subtypePermOfSupport
Full source 
/-- A permutation restricted to the support of a cycle factor is that cycle factor -/
theorem subtypePerm_on_cycleFactorsFinset [DecidableEq α] [Fintype α]
    {g c : Perm α} (hc : c ∈ g.cycleFactorsFinset) :
    g.subtypePerm (mem_cycleFactorsFinset_support hc) = c.subtypePermOfSupport := by
  ext ⟨x, hx⟩
  simp only [subtypePerm_apply, Subtype.coe_mk, subtypePermOfSupport]
  exact ((mem_cycleFactorsFinset_iff.mp hc).2 x hx).symm
Restriction of Permutation to Cycle Factor Support Equals Cycle Factor
Informal description
Let $\alpha$ be a finite type with decidable equality, and let $g$ and $c$ be permutations of $\alpha$ such that $c$ is a cycle factor of $g$ (i.e., $c \in \text{cycleFactorsFinset}(g)$). Then the restriction of $g$ to the support of $c$ is equal to the restriction of $c$ to its own support. More precisely, if we denote by $g|_{c.\text{support}}$ the restriction of $g$ to the support of $c$ (under the condition that $x \in c.\text{support} \leftrightarrow g(x) \in c.\text{support}$), and by $c|_{\text{support}}$ the restriction of $c$ to its support, then: \[ g|_{c.\text{support}} = c|_{\text{support}}. \]
Equiv.Perm.commute_iff_of_mem_cycleFactorsFinset theorem
[DecidableEq α] [Fintype α] {g k c : Equiv.Perm α} (hc : c ∈ g.cycleFactorsFinset) : Commute k c ↔ ∃ hc' : ∀ x : α, x ∈ c.support ↔ k x ∈ c.support, k.subtypePerm hc' ∈ Subgroup.zpowers (g.subtypePerm (mem_cycleFactorsFinset_support hc))
Full source 
theorem commute_iff_of_mem_cycleFactorsFinset [DecidableEq α] [Fintype α] {g k c : Equiv.Perm α}
    (hc : c ∈ g.cycleFactorsFinset) :
    CommuteCommute k c ↔
      ∃ hc' : ∀ x : α, x ∈ c.support ↔ k x ∈ c.support,
        k.subtypePerm hc' ∈ Subgroup.zpowers
          (g.subtypePerm (mem_cycleFactorsFinset_support hc)) := by
  rw [IsCycle.commute_iff' (mem_cycleFactorsFinset_iff.mp hc).1]
  apply exists_congr
  intro hc'
  simp only [Subgroup.mem_zpowers_iff]
  apply exists_congr
  intro n
  rw [Equiv.Perm.subtypePerm_on_cycleFactorsFinset hc]
Characterization of Commuting Permutations for Cycle Factors: $k$ Commutes with Cycle Factor $c$ of $g$ iff $k$ Preserves Support and is a Power of $g$ on Support
Informal description
Let $\alpha$ be a finite type with decidable equality, and let $g$, $k$, and $c$ be permutations of $\alpha$ such that $c$ is a cycle factor of $g$ (i.e., $c \in \text{cycleFactorsFinset}(g)$). Then $k$ commutes with $c$ if and only if there exists a condition $hc'$ stating that for any $x \in \alpha$, $x$ is in the support of $c$ if and only if $k(x)$ is in the support of $c$, and the restriction of $k$ to the support of $c$ (under condition $hc'$) is an integer power of the restriction of $g$ to the support of $c$. More precisely, the following are equivalent: 1. The permutations $k$ and $c$ commute, i.e., $k \circ c = c \circ k$. 2. There exists a condition $hc'$ such that for all $x \in \alpha$, $x \in \text{support}(c) \leftrightarrow k(x) \in \text{support}(c)$, and the restriction $k|_{\text{support}(c)}$ (defined via $hc'$) is in the subgroup generated by $g|_{\text{support}(c)}$.