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

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

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

Equations

• Equiv.Perm.cycleOf f x = Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm f ⋯)

theorem Equiv.Perm.cycleOf_apply {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) (y : α) : (Equiv.Perm.cycleOf f x) y = if Equiv.Perm.SameCycle f x y then f y else y

theorem Equiv.Perm.cycleOf_inv {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) : (Equiv.Perm.cycleOf f x)⁻¹ = Equiv.Perm.cycleOf f⁻¹ x

@[simp]

theorem Equiv.Perm.cycleOf_pow_apply_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) (n : ℕ) : (Equiv.Perm.cycleOf f x ^ n) x = (f ^ n) x

@[simp]

theorem Equiv.Perm.cycleOf_zpow_apply_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) (n : ℤ) : (Equiv.Perm.cycleOf f x ^ n) x = (f ^ n) x

theorem Equiv.Perm.SameCycle.cycleOf_apply {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} : Equiv.Perm.SameCycle f x y → (Equiv.Perm.cycleOf f x) y = f y

theorem Equiv.Perm.cycleOf_apply_of_not_sameCycle {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} : ¬Equiv.Perm.SameCycle f x y → (Equiv.Perm.cycleOf f x) y = y

theorem Equiv.Perm.SameCycle.cycleOf_eq {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} (h : Equiv.Perm.SameCycle f x y) : Equiv.Perm.cycleOf f x = Equiv.Perm.cycleOf f y

@[simp]

theorem Equiv.Perm.cycleOf_apply_apply_zpow_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) (k : ℤ) : (Equiv.Perm.cycleOf f x) ((f ^ k) x) = (f ^ (k + 1)) x

@[simp]

theorem Equiv.Perm.cycleOf_apply_apply_pow_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) (k : ℕ) : (Equiv.Perm.cycleOf f x) ((f ^ k) x) = (f ^ (k + 1)) x

@[simp]

theorem Equiv.Perm.cycleOf_apply_apply_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) : (Equiv.Perm.cycleOf f x) (f x) = f (f x)

@[simp]

theorem Equiv.Perm.cycleOf_apply_self {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) : (Equiv.Perm.cycleOf f x) x = f x

theorem Equiv.Perm.IsCycle.cycleOf_eq {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} (hf : Equiv.Perm.IsCycle f) (hx : f x ≠ x) : Equiv.Perm.cycleOf f x = f

@[simp]

theorem Equiv.Perm.cycleOf_eq_one_iff {α : Type u_2} [DecidableEq α] [Fintype α] {x : α} (f : Equiv.Perm α) : Equiv.Perm.cycleOf f x = 1 ↔ f x = x

@[simp]

theorem Equiv.Perm.cycleOf_self_apply {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) : Equiv.Perm.cycleOf f (f x) = Equiv.Perm.cycleOf f x

@[simp]

theorem Equiv.Perm.cycleOf_self_apply_pow {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (n : ℕ) (x : α) : Equiv.Perm.cycleOf f ((f ^ n) x) = Equiv.Perm.cycleOf f x

@[simp]

theorem Equiv.Perm.cycleOf_self_apply_zpow {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (n : ℤ) (x : α) : Equiv.Perm.cycleOf f ((f ^ n) x) = Equiv.Perm.cycleOf f x

theorem Equiv.Perm.IsCycle.cycleOf {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} (hf : Equiv.Perm.IsCycle f) : Equiv.Perm.cycleOf f x = if f x = x then 1 else f

theorem Equiv.Perm.cycleOf_one {α : Type u_2} [DecidableEq α] [Fintype α] (x : α) : Equiv.Perm.cycleOf 1 x = 1

theorem Equiv.Perm.isCycle_cycleOf {α : Type u_2} [DecidableEq α] [Fintype α] {x : α} (f : Equiv.Perm α) (hx : f x ≠ x) : Equiv.Perm.IsCycle (Equiv.Perm.cycleOf f x)

@[simp]

theorem Equiv.Perm.two_le_card_support_cycleOf_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} : 2 ≤ (Equiv.Perm.support (Equiv.Perm.cycleOf f x)).card ↔ f x ≠ x

@[simp]

theorem Equiv.Perm.card_support_cycleOf_pos_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} : 0 < (Equiv.Perm.support (Equiv.Perm.cycleOf f x)).card ↔ f x ≠ x

theorem Equiv.Perm.pow_mod_orderOf_cycleOf_apply {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (n : ℕ) (x : α) : (f ^ (n % orderOf (Equiv.Perm.cycleOf f x))) x = (f ^ n) x

theorem Equiv.Perm.cycleOf_mul_of_apply_right_eq_self {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : Commute f g) (x : α) (hx : g x = x) : Equiv.Perm.cycleOf (f * g) x = Equiv.Perm.cycleOf f x

theorem Equiv.Perm.Disjoint.cycleOf_mul_distrib {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : Equiv.Perm.Disjoint f g) (x : α) : Equiv.Perm.cycleOf (f * g) x = Equiv.Perm.cycleOf f x * Equiv.Perm.cycleOf g x

theorem Equiv.Perm.support_cycleOf_eq_nil_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} : Equiv.Perm.support (Equiv.Perm.cycleOf f x) = ∅ ↔ x ∉ Equiv.Perm.support f

theorem Equiv.Perm.support_cycleOf_le {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) : Equiv.Perm.support (Equiv.Perm.cycleOf f x) ≤ Equiv.Perm.support f

theorem Equiv.Perm.mem_support_cycleOf_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} : y ∈ Equiv.Perm.support (Equiv.Perm.cycleOf f x) ↔ Equiv.Perm.SameCycle f x y ∧ x ∈ Equiv.Perm.support f

theorem Equiv.Perm.mem_support_cycleOf_iff' {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} (hx : f x ≠ x) : y ∈ Equiv.Perm.support (Equiv.Perm.cycleOf f x) ↔ Equiv.Perm.SameCycle f x y

theorem Equiv.Perm.SameCycle.mem_support_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} (h : Equiv.Perm.SameCycle f x y) : x ∈ Equiv.Perm.support f ↔ y ∈ Equiv.Perm.support f

theorem Equiv.Perm.pow_mod_card_support_cycleOf_self_apply {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (n : ℕ) (x : α) : (f ^ (n % (Equiv.Perm.support (Equiv.Perm.cycleOf f x)).card)) x = (f ^ n) x

theorem Equiv.Perm.isCycle_cycleOf_iff {α : Type u_2} [DecidableEq α] [Fintype α] {x : α} (f : Equiv.Perm α) : Equiv.Perm.IsCycle (Equiv.Perm.cycleOf f x) ↔ 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} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) : Equiv.Perm.IsCycleOn f ↑(Equiv.Perm.support (Equiv.Perm.cycleOf f x))

theorem Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} {y : α} (h : Equiv.Perm.SameCycle f x y) (hx : x ∈ Equiv.Perm.support f) : ∃ i < (Equiv.Perm.support (Equiv.Perm.cycleOf f x)).card, (f ^ i) x = y

theorem Equiv.Perm.SameCycle.exists_pow_eq {α : Type u_2} [DecidableEq α] [Fintype α] {x : α} {y : α} (f : Equiv.Perm α) (h : Equiv.Perm.SameCycle f x y) : ∃ (i : ℕ), 0 < i ∧ i ≤ (Equiv.Perm.support (Equiv.Perm.cycleOf f x)).card + 1 ∧ (f ^ i) x = y

cycleFactors

def Equiv.Perm.cycleFactorsAux {α : Type u_2} [DecidableEq α] [Fintype α] (l : List α) (f : Equiv.Perm α) : (∀ {x : α}, f x ≠ x → x ∈ l) → { l : List (Equiv.Perm α) // List.prod l = f ∧ (∀ g ∈ l, Equiv.Perm.IsCycle g) ∧ 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.
• Equiv.Perm.cycleFactorsAux [] f h_2 = { val := [], property := ⋯ }

theorem Equiv.Perm.mem_list_cycles_iff {α : Type u_4} [Finite α] {l : List (Equiv.Perm α)} (h1 : ∀ σ ∈ l, Equiv.Perm.IsCycle σ) (h2 : List.Pairwise Equiv.Perm.Disjoint l) {σ : Equiv.Perm α} : σ ∈ l ↔ Equiv.Perm.IsCycle σ ∧ ∀ (a : α), σ a ≠ a → σ a = (List.prod l) a

theorem Equiv.Perm.list_cycles_perm_list_cycles {α : Type u_4} [Finite α] {l₁ : List (Equiv.Perm α)} {l₂ : List (Equiv.Perm α)} (h₀ : List.prod l₁ = List.prod l₂) (h₁l₁ : ∀ σ ∈ l₁, Equiv.Perm.IsCycle σ) (h₁l₂ : ∀ σ ∈ l₂, Equiv.Perm.IsCycle σ) (h₂l₁ : List.Pairwise Equiv.Perm.Disjoint l₁) (h₂l₂ : List.Pairwise Equiv.Perm.Disjoint l₂) : List.Perm l₁ l₂

def Equiv.Perm.cycleFactors {α : Type u_2} [Fintype α] [LinearOrder α] (f : Equiv.Perm α) : { l : List (Equiv.Perm α) // List.prod l = f ∧ (∀ g ∈ l, Equiv.Perm.IsCycle g) ∧ List.Pairwise Equiv.Perm.Disjoint l }

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

Equations

• Equiv.Perm.cycleFactors f = Equiv.Perm.cycleFactorsAux (Finset.sort (fun (x x_1 : α) => x ≤ x_1) Finset.univ) f ⋯

def Equiv.Perm.truncCycleFactors {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) : Trunc { l : List (Equiv.Perm α) // List.prod l = f ∧ (∀ g ∈ l, Equiv.Perm.IsCycle g) ∧ 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.

def Equiv.Perm.cycleFactorsFinset {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) : Finset (Equiv.Perm α)

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.

theorem Equiv.Perm.cycleFactorsFinset_eq_list_toFinset {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {l : List (Equiv.Perm α)} (hn : List.Nodup l) : Equiv.Perm.cycleFactorsFinset σ = List.toFinset l ↔ (∀ f ∈ l, Equiv.Perm.IsCycle f) ∧ List.Pairwise Equiv.Perm.Disjoint l ∧ List.prod l = σ

theorem Equiv.Perm.cycleFactorsFinset_eq_finset {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {s : Finset (Equiv.Perm α)} : Equiv.Perm.cycleFactorsFinset σ = s ↔ (∀ f ∈ s, Equiv.Perm.IsCycle f) ∧ ∃ (h : Set.Pairwise (↑s) Equiv.Perm.Disjoint), Finset.noncommProd s id ⋯ = σ

theorem Equiv.Perm.cycleFactorsFinset_pairwise_disjoint {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) : Set.Pairwise (↑(Equiv.Perm.cycleFactorsFinset f)) Equiv.Perm.Disjoint

theorem Equiv.Perm.cycleFactorsFinset_mem_commute {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) : Set.Pairwise (↑(Equiv.Perm.cycleFactorsFinset f)) Commute

theorem Equiv.Perm.cycleFactorsFinset_noncommProd {α : Type u_2} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (comm : optParam (Set.Pairwise (↑(Equiv.Perm.cycleFactorsFinset f)) Commute) ⋯) : Finset.noncommProd (Equiv.Perm.cycleFactorsFinset f) id comm = f

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

theorem Equiv.Perm.mem_cycleFactorsFinset_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {p : Equiv.Perm α} : p ∈ Equiv.Perm.cycleFactorsFinset f ↔ Equiv.Perm.IsCycle p ∧ ∀ a ∈ Equiv.Perm.support p, p a = f a

theorem Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} : Equiv.Perm.cycleOf f x ∈ Equiv.Perm.cycleFactorsFinset f ↔ x ∈ Equiv.Perm.support f

theorem Equiv.Perm.mem_cycleFactorsFinset_support_le {α : Type u_2} [DecidableEq α] [Fintype α] {p : Equiv.Perm α} {f : Equiv.Perm α} (h : p ∈ Equiv.Perm.cycleFactorsFinset f) : Equiv.Perm.support p ≤ Equiv.Perm.support f

theorem Equiv.Perm.cycleFactorsFinset_eq_empty_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} : Equiv.Perm.cycleFactorsFinset f = ∅ ↔ f = 1

@[simp]

theorem Equiv.Perm.cycleFactorsFinset_one {α : Type u_2} [DecidableEq α] [Fintype α] : Equiv.Perm.cycleFactorsFinset 1 = ∅

@[simp]

theorem Equiv.Perm.cycleFactorsFinset_eq_singleton_self_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} : Equiv.Perm.cycleFactorsFinset f = {f} ↔ Equiv.Perm.IsCycle f

theorem Equiv.Perm.IsCycle.cycleFactorsFinset_eq_singleton {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} (hf : Equiv.Perm.IsCycle f) : Equiv.Perm.cycleFactorsFinset f = {f}

theorem Equiv.Perm.cycleFactorsFinset_eq_singleton_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} : Equiv.Perm.cycleFactorsFinset f = {g} ↔ Equiv.Perm.IsCycle f ∧ f = g

theorem Equiv.Perm.cycleFactorsFinset_injective {α : Type u_2} [DecidableEq α] [Fintype α] : 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} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : Equiv.Perm.Disjoint f g) : Disjoint (Equiv.Perm.cycleFactorsFinset f) (Equiv.Perm.cycleFactorsFinset g)

theorem Equiv.Perm.Disjoint.cycleFactorsFinset_mul_eq_union {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : Equiv.Perm.Disjoint f g) : Equiv.Perm.cycleFactorsFinset (f * g) = Equiv.Perm.cycleFactorsFinset f ∪ Equiv.Perm.cycleFactorsFinset g

theorem Equiv.Perm.disjoint_mul_inv_of_mem_cycleFactorsFinset {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : f ∈ Equiv.Perm.cycleFactorsFinset g) : Equiv.Perm.Disjoint (g * f⁻¹) f

theorem Equiv.Perm.cycle_is_cycleOf {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {c : Equiv.Perm α} {a : α} (ha : a ∈ Equiv.Perm.support c) (hc : c ∈ Equiv.Perm.cycleFactorsFinset f) : c = Equiv.Perm.cycleOf f 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} [Finite β] (P : Equiv.Perm β → Prop) (σ : Equiv.Perm β) (base_one : P 1) (base_cycles : ∀ (σ : Equiv.Perm β), Equiv.Perm.IsCycle σ → P σ) (induction_disjoint : ∀ (σ τ : Equiv.Perm β), Equiv.Perm.Disjoint σ τ → Equiv.Perm.IsCycle σ → P σ → P τ → P (σ * τ)) : P σ

theorem Equiv.Perm.cycleFactorsFinset_mul_inv_mem_eq_sdiff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : f ∈ Equiv.Perm.cycleFactorsFinset g) : Equiv.Perm.cycleFactorsFinset (g * f⁻¹) = Equiv.Perm.cycleFactorsFinset g \ {f}