# 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` #

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

`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

source
theorem Equiv.Perm.cycleOf_apply {α : Type u_2} (f : Perm α) [DecidableRel f.SameCycle] (x y : α) :
(f.cycleOf x) y = if f.SameCycle x y then f y else y
source
theorem Equiv.Perm.cycleOf_inv {α : Type u_2} (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
(f.cycleOf x)⁻¹ = f⁻¹.cycleOf x
source
@[simp]
theorem Equiv.Perm.cycleOf_pow_apply_self {α : Type u_2} (f : Perm α) [DecidableRel f.SameCycle] (x : α) (n : ℕ) :
(f.cycleOf x ^ n) x = (f ^ n) x
source
@[simp]
theorem Equiv.Perm.cycleOf_zpow_apply_self {α : Type u_2} (f : Perm α) [DecidableRel f.SameCycle] (x : α) (n : ℤ) :
(f.cycleOf x ^ n) x = (f ^ n) x
source
theorem Equiv.Perm.SameCycle.cycleOf_apply {α : Type u_2} {f : Perm α} {x y : α} [DecidableRel f.SameCycle] :
f.SameCycle x y → (f.cycleOf x) y = f y
source
theorem Equiv.Perm.cycleOf_apply_of_not_sameCycle {α : Type u_2} {f : Perm α} {x y : α} [DecidableRel f.SameCycle] :
¬f.SameCycle x y → (f.cycleOf x) y = y
source
theorem Equiv.Perm.SameCycle.cycleOf_eq {α : Type u_2} {f : Perm α} {x y : α} [DecidableRel f.SameCycle] (h : f.SameCycle x y) :
f.cycleOf x = f.cycleOf y
source
@[simp]
theorem Equiv.Perm.cycleOf_apply_apply_zpow_self {α : Type u_2} (f : Perm α) [DecidableRel f.SameCycle] (x : α) (k : ℤ) :
(f.cycleOf x) ((f ^ k) x) = (f ^ (k + 1)) x
source
@[simp]
theorem Equiv.Perm.cycleOf_apply_apply_pow_self {α : Type u_2} (f : Perm α) [DecidableRel f.SameCycle] (x : α) (k : ℕ) :
(f.cycleOf x) ((f ^ k) x) = (f ^ (k + 1)) x
source
@[simp]
theorem Equiv.Perm.cycleOf_apply_apply_self {α : Type u_2} (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
(f.cycleOf x) (f x) = f (f x)
source
@[simp]
theorem Equiv.Perm.cycleOf_apply_self {α : Type u_2} (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
(f.cycleOf x) x = f x
source
theorem Equiv.Perm.IsCycle.cycleOf_eq {α : Type u_2} {f : Perm α} {x : α} [DecidableRel f.SameCycle] (hf : f.IsCycle) (hx : f x ≠ x) :
f.cycleOf x = f
source
@[simp]
theorem Equiv.Perm.cycleOf_eq_one_iff {α : Type u_2} {x : α} (f : Perm α) [DecidableRel f.SameCycle] :
f.cycleOf x = 1 ↔ f x = x
source
@[simp]
theorem Equiv.Perm.cycleOf_self_apply {α : Type u_2} (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
f.cycleOf (f x) = f.cycleOf x
source
@[simp]
theorem Equiv.Perm.cycleOf_self_apply_pow {α : Type u_2} (f : Perm α) [DecidableRel f.SameCycle] (n : ℕ) (x : α) :
f.cycleOf ((f ^ n) x) = f.cycleOf x
source
@[simp]
theorem Equiv.Perm.cycleOf_self_apply_zpow {α : Type u_2} (f : Perm α) [DecidableRel f.SameCycle] (n : ℤ) (x : α) :
f.cycleOf ((f ^ n) x) = f.cycleOf x
source
theorem Equiv.Perm.IsCycle.cycleOf {α : Type u_2} {f : Perm α} {x : α} [DecidableRel f.SameCycle] [DecidableEq α] (hf : f.IsCycle) :
f.cycleOf x = if f x = x then 1 else f
source
theorem Equiv.Perm.cycleOf_one {α : Type u_2} [DecidableRel (SameCycle 1)] (x : α) :
cycleOf 1 x = 1
source
theorem Equiv.Perm.isCycle_cycleOf {α : Type u_2} {x : α} (f : Perm α) [DecidableRel f.SameCycle] (hx : f x ≠ x) :
(f.cycleOf x).IsCycle
source
theorem Equiv.Perm.pow_mod_orderOf_cycleOf_apply {α : Type u_2} (f : Perm α) [DecidableRel f.SameCycle] (n : ℕ) (x : α) :
(f ^ (n % orderOf (f.cycleOf x))) x = (f ^ n) x
source
theorem Equiv.Perm.cycleOf_mul_of_apply_right_eq_self {α : Type u_2} {f g : Perm α} [DecidableRel f.SameCycle] [DecidableRel (f * g).SameCycle] (h : Commute f g) (x : α) (hx : g x = x) :
(f * g).cycleOf x = f.cycleOf x
source
theorem Equiv.Perm.Disjoint.cycleOf_mul_distrib {α : Type u_2} {f g : Perm α} [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
source
theorem Equiv.Perm.isCycle_cycleOf_iff {α : Type u_2} {x : α} (f : Perm α) [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.

source
instance Equiv.Perm.instDecidableRelSameCycle {α : Type u_2} [DecidableEq α] [Fintype α] (f : Perm α) :
DecidableRel f.SameCycle
Equations

- f.instDecidableRelSameCycle x y = decidable_of_iff (y ∈ List.iterate (⇑f) x (Fintype.card α)) ⋯

source
@[simp]
theorem Equiv.Perm.two_le_card_support_cycleOf_iff {α : Type u_2} {f : Perm α} {x : α} [DecidableEq α] [Fintype α] :
2 ≤ (f.cycleOf x).support.card ↔ f x ≠ x
source
@[simp]
theorem Equiv.Perm.support_cycleOf_nonempty {α : Type u_2} {f : Perm α} {x : α} [DecidableEq α] [Fintype α] :
(f.cycleOf x).support.Nonempty ↔ f x ≠ x
source
theorem Equiv.Perm.mem_support_cycleOf_iff {α : Type u_2} {f : Perm α} {x y : α} [DecidableEq α] [Fintype α] :
y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support
source
theorem Equiv.Perm.mem_support_cycleOf_iff' {α : Type u_2} {f : Perm α} {x y : α} (hx : f x ≠ x) [DecidableEq α] [Fintype α] :
y ∈ (f.cycleOf x).support ↔ f.SameCycle x y
source
theorem Equiv.Perm.sameCycle_iff_cycleOf_eq_of_mem_support {α : Type u_2} [DecidableEq α] [Fintype α] {g : Perm α} {x y : α} (hx : x ∈ g.support) (hy : y ∈ g.support) :
g.SameCycle x y ↔ g.cycleOf x = g.cycleOf y
source
theorem Equiv.Perm.support_cycleOf_eq_nil_iff {α : Type u_2} {f : Perm α} {x : α} [DecidableEq α] [Fintype α] :
(f.cycleOf x).support = ∅ ↔ x ∉ f.support
source
theorem Equiv.Perm.isCycleOn_support_cycleOf {α : Type u_2} [DecidableEq α] [Fintype α] (f : Perm α) (x : α) :
f.IsCycleOn ↑(f.cycleOf x).support
source
theorem Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support {α : Type u_2} {x y : α} {f : Perm α} [DecidableEq α] [Fintype α] (h : f.SameCycle x y) (hx : x ∈ f.support) :
∃ i < (f.cycleOf x).support.card, (f ^ i) x = y
source
theorem Equiv.Perm.support_cycleOf_le {α : Type u_2} [DecidableEq α] [Fintype α] (f : Perm α) (x : α) :
(f.cycleOf x).support ≤ f.support
source
theorem Equiv.Perm.SameCycle.mem_support_iff {α : Type u_2} {x y : α} {f : Perm α} [DecidableEq α] [Fintype α] (h : f.SameCycle x y) :
x ∈ f.support ↔ y ∈ f.support
source
theorem Equiv.Perm.pow_mod_card_support_cycleOf_self_apply {α : Type u_2} [DecidableEq α] [Fintype α] (f : Perm α) (n : ℕ) (x : α) :
(f ^ (n % (f.cycleOf x).support.card)) x = (f ^ n) x
source
theorem Equiv.Perm.SameCycle.exists_pow_eq {α : Type u_2} {x y : α} [DecidableEq α] [Fintype α] (f : Perm α) (h : f.SameCycle x y) :
∃ (i : ℕ), 0 < i ∧ i ≤ (f.cycleOf x).support.card + 1 ∧ (f ^ i) x = y
source
theorem Equiv.Perm.zpow_eq_zpow_on_iff {α : Type u_2} [DecidableEq α] [Fintype α] (g : Perm α) {m n : ℤ} {x : α} (hx : g x ≠ x) :
(g ^ m) x = (g ^ n) x ↔ m % ↑(g.cycleOf x).support.card = n % ↑(g.cycleOf x).support.card

### `cycleFactors` #

source
def Equiv.Perm.cycleFactorsAux {α : Type u_2} [DecidableEq α] [Fintype α] (l : List α) (f : Perm α) (h : ∀ {x : α}, f x ≠ x → x ∈ l) :
{ pl : List (Perm α) // pl.prod = f ∧ (∀ g ∈ pl, g.IsCycle) ∧ List.Pairwise Disjoint pl }

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

Equations

- Equiv.Perm.cycleFactorsAux l f h = Equiv.Perm.cycleFactorsAux.go f l f ⋯ ⋯

Instances For

source
def Equiv.Perm.cycleFactorsAux.go {α : Type u_2} [DecidableEq α] [Fintype α] (f : Perm α) (l : List α) (g : Perm α) (hg : ∀ {x : α}, g x ≠ x → x ∈ l) (hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x) :
{ pl : List (Perm α) // pl.prod = g ∧ (∀ g' ∈ pl, g'.IsCycle) ∧ List.Pairwise Disjoint pl }

The auxiliary of `cycleFactorsAux`. This functions separates cycles from `f` instead of `g` to prevent the process of a cycle gets complex.

Equations

- One or more equations did not get rendered due to their size.
- Equiv.Perm.cycleFactorsAux.go f [] g hg_2 hfg = ⟨[], ⋯⟩

Instances For

source
theorem Equiv.Perm.mem_list_cycles_iff {α : Type u_4} [Finite α] {l : List (Perm α)} (h1 : ∀ σ ∈ l, σ.IsCycle) (h2 : List.Pairwise Disjoint l) {σ : Perm α} :
σ ∈ l ↔ σ.IsCycle ∧ ∀ (a : α), σ a ≠ a → σ a = l.prod a
source
theorem Equiv.Perm.list_cycles_perm_list_cycles {α : Type u_4} [Finite α] {l₁ l₂ : List (Perm α)} (h₀ : l₁.prod = l₂.prod) (h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle) (h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle) (h₂l₁ : List.Pairwise Disjoint l₁) (h₂l₂ : List.Pairwise Disjoint l₂) :
l₁.Perm l₂
source
def Equiv.Perm.cycleFactors {α : Type u_2} [Fintype α] [LinearOrder α] (f : Perm α) :
{ l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l }

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

Equations

- f.cycleFactors = Equiv.Perm.cycleFactorsAux (Finset.univ.sort fun (a b : α) => a ≤ b) f ⋯

Instances For

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

source
def Equiv.Perm.cycleFactorsFinset {α : Type u_2} [DecidableEq α] [Fintype α] (f : Perm α) :
Finset (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.

Instances For

source
theorem Equiv.Perm.cycleFactorsFinset_eq_list_toFinset {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Perm α} {l : List (Perm α)} (hn : l.Nodup) :
σ.cycleFactorsFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
source
theorem Equiv.Perm.cycleFactorsFinset_eq_finset {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Perm α} {s : Finset (Perm α)} :
σ.cycleFactorsFinset = s ↔ (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s).Pairwise Disjoint), s.noncommProd id ⋯ = σ
source
theorem Equiv.Perm.cycleFactorsFinset_pairwise_disjoint {α : Type u_2} [DecidableEq α] [Fintype α] (f : Perm α) :
(↑f.cycleFactorsFinset).Pairwise Disjoint
source
theorem Equiv.Perm.cycleFactorsFinset_mem_commute {α : Type u_2} [DecidableEq α] [Fintype α] (f : Perm α) :
(↑f.cycleFactorsFinset).Pairwise Commute

Two cycles of a permutation commute.

source
theorem Equiv.Perm.cycleFactorsFinset_mem_commute' {α : Type u_2} [DecidableEq α] [Fintype α] (f : Perm α) {g1 g2 : Perm α} (h1 : g1 ∈ f.cycleFactorsFinset) (h2 : g2 ∈ f.cycleFactorsFinset) :
Commute g1 g2

Two cycles of a permutation commute.

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

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

source
theorem Equiv.Perm.mem_cycleFactorsFinset_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f p : Perm α} :
p ∈ f.cycleFactorsFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
source
theorem Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Perm α} {x : α} :
f.cycleOf x ∈ f.cycleFactorsFinset ↔ x ∈ f.support
source
theorem Equiv.Perm.cycleOf_ne_one_iff_mem_cycleFactorsFinset {α : Type u_2} [DecidableEq α] [Fintype α] {g : Perm α} {x : α} :
g.cycleOf x ≠ 1 ↔ g.cycleOf x ∈ g.cycleFactorsFinset
source
theorem Equiv.Perm.mem_cycleFactorsFinset_support_le {α : Type u_2} [DecidableEq α] [Fintype α] {p f : Perm α} (h : p ∈ f.cycleFactorsFinset) :
p.support ≤ f.support
source
theorem Equiv.Perm.support_zpowers_of_mem_cycleFactorsFinset_le {α : Type u_2} [DecidableEq α] [Fintype α] {g : Perm α} {c : ↥g.cycleFactorsFinset} (v : ↥(Subgroup.zpowers ↑c)) :
(↑v).support ≤ g.support
source
theorem Equiv.Perm.pairwise_disjoint_of_mem_zpowers {α : Type u_2} [DecidableEq α] [Fintype α] (f : Perm α) :
Pairwise fun (i j : ↥f.cycleFactorsFinset) => ∀ (x y : Perm α), x ∈ Subgroup.zpowers ↑i → y ∈ Subgroup.zpowers ↑j → x.Disjoint y
source
theorem Equiv.Perm.pairwise_commute_of_mem_zpowers {α : Type u_2} [DecidableEq α] [Fintype α] (f : Perm α) :
Pairwise fun (i j : ↥f.cycleFactorsFinset) => ∀ (x y : Perm α), x ∈ Subgroup.zpowers ↑i → y ∈ Subgroup.zpowers ↑j → Commute x y
source
theorem Equiv.Perm.disjoint_ofSubtype_noncommPiCoprod {α : Type u_2} [DecidableEq α] [Fintype α] (f : Perm α) (u : Perm ↑(Function.fixedPoints ⇑f)) (v : (c : { x : Perm α // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)) :
(ofSubtype u).Disjoint ((Subgroup.noncommPiCoprod ⋯) v)
source
theorem Equiv.Perm.commute_ofSubtype_noncommPiCoprod {α : Type u_2} [DecidableEq α] [Fintype α] (f : Perm α) (u : Perm ↑(Function.fixedPoints ⇑f)) (v : (c : { x : Perm α // x ∈ f.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)) :
Commute (ofSubtype u) ((Subgroup.noncommPiCoprod ⋯) v)
source
theorem Equiv.Perm.mem_support_iff_mem_support_of_mem_cycleFactorsFinset {α : Type u_2} [DecidableEq α] [Fintype α] {g : Perm α} {x : α} :
x ∈ g.support ↔ ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support
source
theorem Equiv.Perm.cycleFactorsFinset_eq_empty_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Perm α} :
f.cycleFactorsFinset = ∅ ↔ f = 1
source
@[simp]
theorem Equiv.Perm.cycleFactorsFinset_one {α : Type u_2} [DecidableEq α] [Fintype α] :
cycleFactorsFinset 1 = ∅
source
@[simp]
theorem Equiv.Perm.cycleFactorsFinset_eq_singleton_self_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f : Perm α} :
f.cycleFactorsFinset = {f} ↔ f.IsCycle
source
theorem Equiv.Perm.IsCycle.cycleFactorsFinset_eq_singleton {α : Type u_2} [DecidableEq α] [Fintype α] {f : Perm α} (hf : f.IsCycle) :
f.cycleFactorsFinset = {f}
source
theorem Equiv.Perm.cycleFactorsFinset_eq_singleton_iff {α : Type u_2} [DecidableEq α] [Fintype α] {f g : Perm α} :
f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g
source
theorem Equiv.Perm.cycleFactorsFinset_injective {α : Type u_2} [DecidableEq α] [Fintype α] :
Function.Injective cycleFactorsFinset

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

source
theorem Equiv.Perm.Disjoint.disjoint_cycleFactorsFinset {α : Type u_2} [DecidableEq α] [Fintype α] {f g : Perm α} (h : f.Disjoint g) :
_root_.Disjoint f.cycleFactorsFinset g.cycleFactorsFinset
source
theorem Equiv.Perm.Disjoint.cycleFactorsFinset_mul_eq_union {α : Type u_2} [DecidableEq α] [Fintype α] {f g : Perm α} (h : f.Disjoint g) :
(f * g).cycleFactorsFinset = f.cycleFactorsFinset ∪ g.cycleFactorsFinset
source
theorem Equiv.Perm.disjoint_mul_inv_of_mem_cycleFactorsFinset {α : Type u_2} [DecidableEq α] [Fintype α] {f g : Perm α} (h : f ∈ g.cycleFactorsFinset) :
(g * f⁻¹).Disjoint f
source
theorem Equiv.Perm.cycle_is_cycleOf {α : Type u_2} [DecidableEq α] [Fintype α] {f c : Perm α} {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`

source
theorem Equiv.Perm.isCycleOn_support_of_mem_cycleFactorsFinset {α : Type u_2} [DecidableEq α] [Fintype α] {g c : Perm α} (hc : c ∈ g.cycleFactorsFinset) :
g.IsCycleOn ↑c.support
source
theorem Equiv.Perm.eq_cycleOf_of_mem_cycleFactorsFinset_iff {α : Type u_2} [DecidableEq α] [Fintype α] (g c : Perm α) (hc : c ∈ g.cycleFactorsFinset) (x : α) :
c = g.cycleOf x ↔ x ∈ c.support
source
theorem Equiv.Perm.zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff {α : Type u_2} [DecidableEq α] [Fintype α] {g : Perm α} {x : α} {m : ℤ} {c : ↥g.cycleFactorsFinset} :
(g ^ m) x ∈ (↑c).support ↔ x ∈ (↑c).support
source
theorem Equiv.Perm.mem_cycleFactorsFinset_conj {α : Type u_2} [DecidableEq α] [Fintype α] (g k c : Perm α) :
k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset

A permutation `c` is a cycle of `g` iff `k * c * k⁻¹` is a cycle of `k * g * k⁻¹`

source
theorem Equiv.Perm.commute_of_mem_cycleFactorsFinset_commute {α : Type u_2} [DecidableEq α] [Fintype α] (k g : Perm α) (hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c) :
Commute k g

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`

source
theorem Equiv.Perm.self_mem_cycle_factors_commute {α : Type u_2} [DecidableEq α] [Fintype α] {g c : Perm α} (hc : c ∈ g.cycleFactorsFinset) :
Commute c g

The cycles of a permutation commute with it

source
theorem Equiv.Perm.mem_support_cycle_of_cycle {α : Type u_2} [DecidableEq α] [Fintype α] {g d c : Perm α} (hc : c ∈ g.cycleFactorsFinset) (hd : d ∈ g.cycleFactorsFinset) (x : α) :
d x ∈ c.support ↔ x ∈ c.support

If `c` and `d` are cycles of `g`, then `d` stabilizes the support of `c`

source
theorem Equiv.Perm.mem_cycleFactorsFinset_support {α : Type u_2} [DecidableEq α] [Fintype α] {g c : Perm α} (hc : c ∈ g.cycleFactorsFinset) (a : α) :
g a ∈ c.support ↔ a ∈ c.support

If a permutation is a cycle of `g`, then its support is invariant under `g`.

source
theorem Equiv.Perm.cycle_induction_on {β : Type u_3} [Finite β] (P : Perm β → Prop) (σ : Perm β) (base_one : P 1) (base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ) (induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)) :
P σ
source
theorem Equiv.Perm.cycleFactorsFinset_mul_inv_mem_eq_sdiff {α : Type u_2} [DecidableEq α] [Fintype α] {f g : Perm α} (h : f ∈ g.cycleFactorsFinset) :
(g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}
source
theorem Equiv.Perm.IsCycle.forall_commute_iff {α : Type u_2} [DecidableEq α] [Fintype α] (g z : Perm α) :
(∀ c ∈ g.cycleFactorsFinset, Commute z c) ↔ ∀ c ∈ g.cycleFactorsFinset, ∃ (hc : ∀ (x : α), z x ∈ c.support ↔ x ∈ c.support), ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers c
source
theorem Equiv.Perm.subtypePerm_on_cycleFactorsFinset {α : Type u_2} [DecidableEq α] [Fintype α] {g c : Perm α} (hc : c ∈ g.cycleFactorsFinset) :
g.subtypePerm ⋯ = c.subtypePermOfSupport

A permutation restricted to the support of a cycle factor is that cycle factor

source
theorem Equiv.Perm.commute_iff_of_mem_cycleFactorsFinset {α : Type u_2} [DecidableEq α] [Fintype α] {g k c : Perm α} (hc : c ∈ g.cycleFactorsFinset) :
Commute k c ↔ ∃ (hc' : ∀ (x : α), k x ∈ c.support ↔ x ∈ c.support), k.subtypePerm hc' ∈ Subgroup.zpowers (g.subtypePerm ⋯)