# Cycle factors of a permutation #

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

### cycleOf#

def Equiv.Perm.cycleOf {α : Type u_2} (f : ) [DecidableRel f.SameCycle] (x : α) :

f.cycleOf x is the cycle of the permutation f to which x belongs.

Equations
• f.cycleOf x = Equiv.Perm.ofSubtype (f.subtypePerm )
Instances For
theorem Equiv.Perm.cycleOf_apply {α : Type u_2} (f : ) [DecidableRel f.SameCycle] (x : α) (y : α) :
(f.cycleOf x) y = if f.SameCycle x y then f y else y
theorem Equiv.Perm.cycleOf_inv {α : Type u_2} (f : ) [DecidableRel f.SameCycle] (x : α) :
(f.cycleOf x)⁻¹ = f⁻¹.cycleOf x
@[simp]
theorem Equiv.Perm.cycleOf_pow_apply_self {α : Type u_2} (f : ) [DecidableRel f.SameCycle] (x : α) (n : ) :
(f.cycleOf x ^ n) x = (f ^ n) x
@[simp]
theorem Equiv.Perm.cycleOf_zpow_apply_self {α : Type u_2} (f : ) [DecidableRel f.SameCycle] (x : α) (n : ) :
(f.cycleOf x ^ n) x = (f ^ n) x
theorem Equiv.Perm.SameCycle.cycleOf_apply {α : Type u_2} {f : } {x : α} {y : α} [DecidableRel f.SameCycle] :
f.SameCycle x y(f.cycleOf x) y = f y
theorem Equiv.Perm.cycleOf_apply_of_not_sameCycle {α : Type u_2} {f : } {x : α} {y : α} [DecidableRel f.SameCycle] :
¬f.SameCycle x y(f.cycleOf x) y = y
theorem Equiv.Perm.SameCycle.cycleOf_eq {α : Type u_2} {f : } {x : α} {y : α} [DecidableRel f.SameCycle] (h : f.SameCycle x y) :
f.cycleOf x = f.cycleOf y
@[simp]
theorem Equiv.Perm.cycleOf_apply_apply_zpow_self {α : Type u_2} (f : ) [DecidableRel f.SameCycle] (x : α) (k : ) :
(f.cycleOf x) ((f ^ k) x) = (f ^ (k + 1)) x
@[simp]
theorem Equiv.Perm.cycleOf_apply_apply_pow_self {α : Type u_2} (f : ) [DecidableRel f.SameCycle] (x : α) (k : ) :
(f.cycleOf x) ((f ^ k) x) = (f ^ (k + 1)) x
@[simp]
theorem Equiv.Perm.cycleOf_apply_apply_self {α : Type u_2} (f : ) [DecidableRel f.SameCycle] (x : α) :
(f.cycleOf x) (f x) = f (f x)
@[simp]
theorem Equiv.Perm.cycleOf_apply_self {α : Type u_2} (f : ) [DecidableRel f.SameCycle] (x : α) :
(f.cycleOf x) x = f x
theorem Equiv.Perm.IsCycle.cycleOf_eq {α : Type u_2} {f : } {x : α} [DecidableRel f.SameCycle] (hf : f.IsCycle) (hx : f x x) :
f.cycleOf x = f
@[simp]
theorem Equiv.Perm.cycleOf_eq_one_iff {α : Type u_2} {x : α} (f : ) [DecidableRel f.SameCycle] :
f.cycleOf x = 1 f x = x
@[simp]
theorem Equiv.Perm.cycleOf_self_apply {α : Type u_2} (f : ) [DecidableRel f.SameCycle] (x : α) :
f.cycleOf (f x) = f.cycleOf x
@[simp]
theorem Equiv.Perm.cycleOf_self_apply_pow {α : Type u_2} (f : ) [DecidableRel f.SameCycle] (n : ) (x : α) :
f.cycleOf ((f ^ n) x) = f.cycleOf x
@[simp]
theorem Equiv.Perm.cycleOf_self_apply_zpow {α : Type u_2} (f : ) [DecidableRel f.SameCycle] (n : ) (x : α) :
f.cycleOf ((f ^ n) x) = f.cycleOf x
theorem Equiv.Perm.IsCycle.cycleOf {α : Type u_2} {f : } {x : α} [DecidableRel f.SameCycle] [] (hf : f.IsCycle) :
f.cycleOf x = if f x = x then 1 else f
theorem Equiv.Perm.cycleOf_one {α : Type u_2} (x : α) :
= 1
theorem Equiv.Perm.isCycle_cycleOf {α : Type u_2} {x : α} (f : ) [DecidableRel f.SameCycle] (hx : f x x) :
(f.cycleOf x).IsCycle
@[simp]
theorem Equiv.Perm.two_le_card_support_cycleOf_iff {α : Type u_2} {f : } {x : α} [DecidableRel f.SameCycle] [] [] :
2 (f.cycleOf x).support.card f x x
@[simp]
theorem Equiv.Perm.support_cycleOf_nonempty {α : Type u_2} {f : } {x : α} [DecidableRel f.SameCycle] [] [] :
(f.cycleOf x).support.Nonempty f x x
@[deprecated Equiv.Perm.support_cycleOf_nonempty]
theorem Equiv.Perm.card_support_cycleOf_pos_iff {α : Type u_2} {f : } {x : α} [DecidableRel f.SameCycle] [] [] :
0 < (f.cycleOf x).support.card f x x
theorem Equiv.Perm.pow_mod_orderOf_cycleOf_apply {α : Type u_2} (f : ) [DecidableRel f.SameCycle] (n : ) (x : α) :
(f ^ (n % orderOf (f.cycleOf x))) x = (f ^ n) x
theorem Equiv.Perm.cycleOf_mul_of_apply_right_eq_self {α : Type u_2} {f : } {g : } [DecidableRel f.SameCycle] [DecidableRel (f * g).SameCycle] (h : Commute f g) (x : α) (hx : g x = x) :
(f * g).cycleOf x = f.cycleOf x
theorem Equiv.Perm.Disjoint.cycleOf_mul_distrib {α : Type u_2} {f : } {g : } [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
theorem Equiv.Perm.support_cycleOf_eq_nil_iff {α : Type u_2} {f : } {x : α} [DecidableRel f.SameCycle] [] [] :
(f.cycleOf x).support = xf.support
theorem Equiv.Perm.support_cycleOf_le {α : Type u_2} [] [] (f : ) (x : α) :
(f.cycleOf x).support f.support
theorem Equiv.Perm.mem_support_cycleOf_iff {α : Type u_2} {f : } {x : α} {y : α} [DecidableRel f.SameCycle] [] [] :
y (f.cycleOf x).support f.SameCycle x y x f.support
theorem Equiv.Perm.mem_support_cycleOf_iff' {α : Type u_2} {f : } {x : α} {y : α} [DecidableRel f.SameCycle] (hx : f x x) [] [] :
y (f.cycleOf x).support f.SameCycle x y
theorem Equiv.Perm.SameCycle.mem_support_iff {α : Type u_2} {x : α} {y : α} {f : } [] [] (h : f.SameCycle x y) :
x f.support y f.support
theorem Equiv.Perm.pow_mod_card_support_cycleOf_self_apply {α : Type u_2} [] [] (f : ) (n : ) (x : α) :
(f ^ (n % (f.cycleOf x).support.card)) x = (f ^ n) x
theorem Equiv.Perm.isCycle_cycleOf_iff {α : Type u_2} {x : α} (f : ) [DecidableRel f.SameCycle] :
(f.cycleOf x).IsCycle f x x

x is in the support of f iff Equiv.Perm.cycle_of f x is a cycle.

theorem Equiv.Perm.isCycleOn_support_cycleOf {α : Type u_2} [] [] (f : ) (x : α) :
f.IsCycleOn (f.cycleOf x).support
theorem Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support {α : Type u_2} {x : α} {y : α} {f : } [] [] (h : f.SameCycle x y) (hx : x f.support) :
i < (f.cycleOf x).support.card, (f ^ i) x = y
theorem Equiv.Perm.SameCycle.exists_pow_eq {α : Type u_2} {x : α} {y : α} [] [] (f : ) (h : f.SameCycle x y) :
∃ (i : ), 0 < i i (f.cycleOf x).support.card + 1 (f ^ i) x = y

### cycleFactors#

def Equiv.Perm.cycleFactorsAux {α : Type u_2} [] [] (l : List α) (f : ) :
(∀ {x : α}, f x xx l){ l : List () // l.prod = f (gl, g.IsCycle) List.Pairwise Equiv.Perm.Disjoint l }

Given a list l : List α and a permutation f : Perm α whose nonfixed points are all in l, recursively factors f into cycles.

Equations
• One or more equations did not get rendered due to their size.
• = [],
Instances For
theorem Equiv.Perm.mem_list_cycles_iff {α : Type u_4} [] {l : List ()} (h1 : σl, σ.IsCycle) (h2 : List.Pairwise Equiv.Perm.Disjoint l) {σ : } :
σ l σ.IsCycle ∀ (a : α), σ a aσ a = l.prod a
theorem Equiv.Perm.list_cycles_perm_list_cycles {α : Type u_4} [] {l₁ : List ()} {l₂ : List ()} (h₀ : l₁.prod = l₂.prod) (h₁l₁ : σl₁, σ.IsCycle) (h₁l₂ : σl₂, σ.IsCycle) (h₂l₁ : List.Pairwise Equiv.Perm.Disjoint l₁) (h₂l₂ : List.Pairwise Equiv.Perm.Disjoint l₂) :
l₁.Perm l₂
def Equiv.Perm.cycleFactors {α : Type u_2} [] [] (f : ) :
{ l : List () // l.prod = f (gl, g.IsCycle) List.Pairwise Equiv.Perm.Disjoint l }

Factors a permutation f into a list of disjoint cyclic permutations that multiply to f.

Equations
Instances For
def Equiv.Perm.truncCycleFactors {α : Type u_2} [] [] (f : ) :
Trunc { l : List () // l.prod = f (gl, g.IsCycle) List.Pairwise Equiv.Perm.Disjoint l }

Factors a permutation f into a list of disjoint cyclic permutations that multiply to f, without a linear order.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Equiv.Perm.cycleFactorsFinset {α : Type u_2} [] [] (f : ) :

Factors a permutation f into a Finset of disjoint cyclic permutations that multiply to f.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Equiv.Perm.cycleFactorsFinset_eq_list_toFinset {α : Type u_2} [] [] {σ : } {l : List ()} (hn : l.Nodup) :
σ.cycleFactorsFinset = l.toFinset (fl, f.IsCycle) List.Pairwise Equiv.Perm.Disjoint l l.prod = σ
theorem Equiv.Perm.cycleFactorsFinset_eq_finset {α : Type u_2} [] [] {σ : } {s : Finset ()} :
σ.cycleFactorsFinset = s (fs, f.IsCycle) ∃ (h : (s).Pairwise Equiv.Perm.Disjoint), s.noncommProd id = σ
theorem Equiv.Perm.cycleFactorsFinset_pairwise_disjoint {α : Type u_2} [] [] (f : ) :
(f.cycleFactorsFinset).Pairwise Equiv.Perm.Disjoint
theorem Equiv.Perm.cycleFactorsFinset_mem_commute {α : Type u_2} [] [] (f : ) :
(f.cycleFactorsFinset).Pairwise Commute
theorem Equiv.Perm.cycleFactorsFinset_noncommProd {α : Type u_2} [] [] (f : ) (comm : optParam ((f.cycleFactorsFinset).Pairwise Commute) ) :
f.cycleFactorsFinset.noncommProd id comm = f

The product of cycle factors is equal to the original f : perm α.

theorem Equiv.Perm.mem_cycleFactorsFinset_iff {α : Type u_2} [] [] {f : } {p : } :
p f.cycleFactorsFinset p.IsCycle ap.support, p a = f a
theorem Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff {α : Type u_2} [] [] {f : } {x : α} :
f.cycleOf x f.cycleFactorsFinset x f.support
theorem Equiv.Perm.mem_cycleFactorsFinset_support_le {α : Type u_2} [] [] {p : } {f : } (h : p f.cycleFactorsFinset) :
p.support f.support
theorem Equiv.Perm.cycleFactorsFinset_eq_empty_iff {α : Type u_2} [] [] {f : } :
f.cycleFactorsFinset = f = 1
@[simp]
theorem Equiv.Perm.cycleFactorsFinset_one {α : Type u_2} [] [] :
@[simp]
theorem Equiv.Perm.cycleFactorsFinset_eq_singleton_self_iff {α : Type u_2} [] [] {f : } :
f.cycleFactorsFinset = {f} f.IsCycle
theorem Equiv.Perm.IsCycle.cycleFactorsFinset_eq_singleton {α : Type u_2} [] [] {f : } (hf : f.IsCycle) :
f.cycleFactorsFinset = {f}
theorem Equiv.Perm.cycleFactorsFinset_eq_singleton_iff {α : Type u_2} [] [] {f : } {g : } :
f.cycleFactorsFinset = {g} f.IsCycle f = g
theorem Equiv.Perm.cycleFactorsFinset_injective {α : Type u_2} [] [] :
Function.Injective Equiv.Perm.cycleFactorsFinset

Two permutations f g : Perm α have the same cycle factors iff they are the same.

theorem Equiv.Perm.Disjoint.disjoint_cycleFactorsFinset {α : Type u_2} [] [] {f : } {g : } (h : f.Disjoint g) :
Disjoint f.cycleFactorsFinset g.cycleFactorsFinset
theorem Equiv.Perm.Disjoint.cycleFactorsFinset_mul_eq_union {α : Type u_2} [] [] {f : } {g : } (h : f.Disjoint g) :
(f * g).cycleFactorsFinset = f.cycleFactorsFinset g.cycleFactorsFinset
theorem Equiv.Perm.disjoint_mul_inv_of_mem_cycleFactorsFinset {α : Type u_2} [] [] {f : } {g : } (h : f g.cycleFactorsFinset) :
(g * f⁻¹).Disjoint f
theorem Equiv.Perm.cycle_is_cycleOf {α : Type u_2} [] [] {f : } {c : } {a : α} (ha : a c.support) (hc : c f.cycleFactorsFinset) :
c = f.cycleOf a

If c is a cycle, a ∈ c.support and c is a cycle of f, then c = f.cycleOf a

theorem Equiv.Perm.cycle_induction_on {β : Type u_3} [] (P : ) (σ : ) (base_one : P 1) (base_cycles : ∀ (σ : ), σ.IsCycleP σ) (induction_disjoint : ∀ (σ τ : ), σ.Disjoint τσ.IsCycleP σP τP (σ * τ)) :
P σ
theorem Equiv.Perm.cycleFactorsFinset_mul_inv_mem_eq_sdiff {α : Type u_2} [] [] {f : } {g : } (h : f g.cycleFactorsFinset) :
(g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}