mathlib3documentation

group_theory.perm.cycle.basic

Cyclic permutations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file develops the theory of cycles in permutations.

Main definitions #

In the following, `f : equiv.perm β`.

• `equiv.perm.same_cycle`: `f.same_cycle x y` when `x` and `y` are in the same cycle of `f`.
• `equiv.perm.is_cycle`: `f` is a cycle if any two nonfixed points of `f` are related by repeated applications of `f`, and `f` is not the identity.
• `equiv.perm.is_cycle_on`: `f` is a cycle on a set `s` when any two points of `s` are related by repeated applications of `f`.

The following two definitions require that `β` is a `fintype`:

• `equiv.perm.cycle_of`: `f.cycle_of x` is the cycle of `f` that `x` belongs to.
• `equiv.perm.cycle_factors`: `f.cycle_factors` is a list of disjoint cyclic permutations that multiply to `f`.

Main results #

• This file contains several closure results:
• `closure_is_cycle` : The symmetric group is generated by cycles
• `closure_cycle_adjacent_swap` : The symmetric group is generated by a cycle and an adjacent transposition
• `closure_cycle_coprime_swap` : The symmetric group is generated by a cycle and a coprime transposition
• `closure_prime_cycle_swap` : The symmetric group is generated by a prime cycle and a transposition

Notes #

`equiv.perm.is_cycle` and `equiv.perm.is_cycle_on` are different in three ways:

• `is_cycle` is about the entire type while `is_cycle_on` is restricted to a set.
• `is_cycle` forbids the identity while `is_cycle_on` allows it (if `s` is a subsingleton).
• `is_cycle_on` forbids fixed points on `s` (if `s` is nontrivial), while `is_cycle` allows them.

`same_cycle`#

def equiv.perm.same_cycle {α : Type u_2} (f : equiv.perm α) (x y : α) :
Prop

The equivalence relation indicating that two points are in the same cycle of a permutation.

Equations
Instances for `equiv.perm.same_cycle`
@[refl]
theorem equiv.perm.same_cycle.refl {α : Type u_2} (f : equiv.perm α) (x : α) :
theorem equiv.perm.same_cycle.rfl {α : Type u_2} {f : equiv.perm α} {x : α} :
@[protected]
theorem eq.same_cycle {α : Type u_2} {x y : α} (h : x = y) (f : equiv.perm α) :
@[symm]
theorem equiv.perm.same_cycle.symm {α : Type u_2} {f : equiv.perm α} {x y : α} :
theorem equiv.perm.same_cycle_comm {α : Type u_2} {f : equiv.perm α} {x y : α} :
@[trans]
theorem equiv.perm.same_cycle.trans {α : Type u_2} {f : equiv.perm α} {x y z : α} :
@[simp]
theorem equiv.perm.same_cycle_one {α : Type u_2} {x y : α} :
1.same_cycle x y x = y
@[simp]
theorem equiv.perm.same_cycle_inv {α : Type u_2} {f : equiv.perm α} {x y : α} :
theorem equiv.perm.same_cycle.of_inv {α : Type u_2} {f : equiv.perm α} {x y : α} :

Alias of the forward direction of `equiv.perm.same_cycle_inv`.

theorem equiv.perm.same_cycle.inv {α : Type u_2} {f : equiv.perm α} {x y : α} :

Alias of the reverse direction of `equiv.perm.same_cycle_inv`.

@[simp]
theorem equiv.perm.same_cycle_conj {α : Type u_2} {f g : equiv.perm α} {x y : α} :
theorem equiv.perm.same_cycle.conj {α : Type u_2} {f g : equiv.perm α} {x y : α} :
f.same_cycle x y (g * f * g⁻¹).same_cycle (g x) (g y)
theorem equiv.perm.same_cycle.apply_eq_self_iff {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle x y (f x = x f y = y)
theorem equiv.perm.same_cycle.eq_of_left {α : Type u_2} {f : equiv.perm α} {x y : α} (h : f.same_cycle x y) (hx : x) :
x = y
theorem equiv.perm.same_cycle.eq_of_right {α : Type u_2} {f : equiv.perm α} {x y : α} (h : f.same_cycle x y) (hy : y) :
x = y
@[simp]
theorem equiv.perm.same_cycle_apply_left {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle (f x) y f.same_cycle x y
@[simp]
theorem equiv.perm.same_cycle_apply_right {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle x (f y) f.same_cycle x y
@[simp]
theorem equiv.perm.same_cycle_inv_apply_left {α : Type u_2} {f : equiv.perm α} {x y : α} :
@[simp]
theorem equiv.perm.same_cycle_inv_apply_right {α : Type u_2} {f : equiv.perm α} {x y : α} :
@[simp]
theorem equiv.perm.same_cycle_zpow_left {α : Type u_2} {f : equiv.perm α} {x y : α} {n : } :
f.same_cycle ((f ^ n) x) y f.same_cycle x y
@[simp]
theorem equiv.perm.same_cycle_zpow_right {α : Type u_2} {f : equiv.perm α} {x y : α} {n : } :
f.same_cycle x ((f ^ n) y) f.same_cycle x y
@[simp]
theorem equiv.perm.same_cycle_pow_left {α : Type u_2} {f : equiv.perm α} {x y : α} {n : } :
f.same_cycle ((f ^ n) x) y f.same_cycle x y
@[simp]
theorem equiv.perm.same_cycle_pow_right {α : Type u_2} {f : equiv.perm α} {x y : α} {n : } :
f.same_cycle x ((f ^ n) y) f.same_cycle x y
theorem equiv.perm.same_cycle.of_apply_left {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle (f x) y f.same_cycle x y

Alias of the forward direction of `equiv.perm.same_cycle_apply_left`.

theorem equiv.perm.same_cycle.apply_left {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle x y f.same_cycle (f x) y

Alias of the reverse direction of `equiv.perm.same_cycle_apply_left`.

theorem equiv.perm.same_cycle.of_apply_right {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle x (f y) f.same_cycle x y

Alias of the forward direction of `equiv.perm.same_cycle_apply_right`.

theorem equiv.perm.same_cycle.apply_right {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.same_cycle x y f.same_cycle x (f y)

Alias of the reverse direction of `equiv.perm.same_cycle_apply_right`.

theorem equiv.perm.same_cycle.inv_apply_left {α : Type u_2} {f : equiv.perm α} {x y : α} :

Alias of the reverse direction of `equiv.perm.same_cycle_inv_apply_left`.

theorem equiv.perm.same_cycle.of_inv_apply_left {α : Type u_2} {f : equiv.perm α} {x y : α} :

Alias of the forward direction of `equiv.perm.same_cycle_inv_apply_left`.

theorem equiv.perm.same_cycle.inv_apply_right {α : Type u_2} {f : equiv.perm α} {x y : α} :

Alias of the reverse direction of `equiv.perm.same_cycle_inv_apply_right`.

theorem equiv.perm.same_cycle.of_inv_apply_right {α : Type u_2} {f : equiv.perm α} {x y : α} :

Alias of the forward direction of `equiv.perm.same_cycle_inv_apply_right`.

theorem equiv.perm.same_cycle.of_pow_left {α : Type u_2} {f : equiv.perm α} {x y : α} {n : } :
f.same_cycle ((f ^ n) x) y f.same_cycle x y

Alias of the forward direction of `equiv.perm.same_cycle_pow_left`.

theorem equiv.perm.same_cycle.pow_left {α : Type u_2} {f : equiv.perm α} {x y : α} {n : } :
f.same_cycle x y f.same_cycle ((f ^ n) x) y

Alias of the reverse direction of `equiv.perm.same_cycle_pow_left`.

theorem equiv.perm.same_cycle.pow_right {α : Type u_2} {f : equiv.perm α} {x y : α} {n : } :
f.same_cycle x y f.same_cycle x ((f ^ n) y)

Alias of the reverse direction of `equiv.perm.same_cycle_pow_right`.

theorem equiv.perm.same_cycle.of_pow_right {α : Type u_2} {f : equiv.perm α} {x y : α} {n : } :
f.same_cycle x ((f ^ n) y) f.same_cycle x y

Alias of the forward direction of `equiv.perm.same_cycle_pow_right`.

theorem equiv.perm.same_cycle.zpow_left {α : Type u_2} {f : equiv.perm α} {x y : α} {n : } :
f.same_cycle x y f.same_cycle ((f ^ n) x) y

Alias of the reverse direction of `equiv.perm.same_cycle_zpow_left`.

theorem equiv.perm.same_cycle.of_zpow_left {α : Type u_2} {f : equiv.perm α} {x y : α} {n : } :
f.same_cycle ((f ^ n) x) y f.same_cycle x y

Alias of the forward direction of `equiv.perm.same_cycle_zpow_left`.

theorem equiv.perm.same_cycle.zpow_right {α : Type u_2} {f : equiv.perm α} {x y : α} {n : } :
f.same_cycle x y f.same_cycle x ((f ^ n) y)

Alias of the reverse direction of `equiv.perm.same_cycle_zpow_right`.

theorem equiv.perm.same_cycle.of_zpow_right {α : Type u_2} {f : equiv.perm α} {x y : α} {n : } :
f.same_cycle x ((f ^ n) y) f.same_cycle x y

Alias of the forward direction of `equiv.perm.same_cycle_zpow_right`.

theorem equiv.perm.same_cycle.of_pow {α : Type u_2} {f : equiv.perm α} {x y : α} {n : } :
(f ^ n).same_cycle x y f.same_cycle x y
theorem equiv.perm.same_cycle.of_zpow {α : Type u_2} {f : equiv.perm α} {x y : α} {n : } :
(f ^ n).same_cycle x y f.same_cycle x y
@[simp]
theorem equiv.perm.same_cycle_subtype_perm {α : Type u_2} {f : equiv.perm α} {p : α Prop} {h : (x : α), p x p (f x)} {x y : {x // p x}} :
theorem equiv.perm.same_cycle.subtype_perm {α : Type u_2} {f : equiv.perm α} {p : α Prop} {h : (x : α), p x p (f x)} {x y : {x // p x}} :

Alias of the reverse direction of `equiv.perm.same_cycle_subtype_perm`.

@[simp]
theorem equiv.perm.same_cycle_extend_domain {α : Type u_2} {β : Type u_3} {g : equiv.perm α} {x y : α} {p : β Prop} {f : α } :
theorem equiv.perm.same_cycle.extend_domain {α : Type u_2} {β : Type u_3} {g : equiv.perm α} {x y : α} {p : β Prop} {f : α } :

Alias of the reverse direction of `equiv.perm.same_cycle_extend_domain`.

theorem equiv.perm.same_cycle.exists_pow_eq' {α : Type u_2} {f : equiv.perm α} {x y : α} [finite α] :
f.same_cycle x y ( (i : ) (H : i < order_of f), (f ^ i) x = y)
theorem equiv.perm.same_cycle.exists_pow_eq'' {α : Type u_2} {f : equiv.perm α} {x y : α} [finite α] (h : f.same_cycle x y) :
(i : ) (hpos : 0 < i) (h : i order_of f), (f ^ i) x = y
@[protected, instance]
Equations

`is_cycle`#

def equiv.perm.is_cycle {α : Type u_2} (f : equiv.perm α) :
Prop

A cycle is a non identity permutation where any two nonfixed points of the permutation are related by repeated application of the permutation.

Equations
theorem equiv.perm.is_cycle.ne_one {α : Type u_2} {f : equiv.perm α} (h : f.is_cycle) :
f 1
@[simp]
theorem equiv.perm.not_is_cycle_one {α : Type u_2} :
@[protected]
theorem equiv.perm.is_cycle.same_cycle {α : Type u_2} {f : equiv.perm α} {x y : α} (hf : f.is_cycle) (hx : f x x) (hy : f y y) :
theorem equiv.perm.is_cycle.exists_zpow_eq {α : Type u_2} {f : equiv.perm α} {x y : α} :
f.is_cycle f x x f y y ( (i : ), (f ^ i) x = y)
theorem equiv.perm.is_cycle.inv {α : Type u_2} {f : equiv.perm α} (hf : f.is_cycle) :
@[simp]
theorem equiv.perm.is_cycle_inv {α : Type u_2} {f : equiv.perm α} :
theorem equiv.perm.is_cycle.conj {α : Type u_2} {f g : equiv.perm α} :
@[protected]
theorem equiv.perm.is_cycle.extend_domain {α : Type u_2} {β : Type u_3} {g : equiv.perm α} {p : β Prop} (f : α ) :
theorem equiv.perm.is_cycle_iff_same_cycle {α : Type u_2} {f : equiv.perm α} {x : α} (hx : f x x) :
f.is_cycle {y : α}, f.same_cycle x y f y y
theorem equiv.perm.is_cycle.exists_pow_eq {α : Type u_2} {f : equiv.perm α} {x y : α} [finite α] (hf : f.is_cycle) (hx : f x x) (hy : f y y) :
(i : ), (f ^ i) x = y
theorem equiv.perm.is_cycle_swap {α : Type u_2} {x y : α} [decidable_eq α] (hxy : x y) :
@[protected]
theorem equiv.perm.is_swap.is_cycle {α : Type u_2} {f : equiv.perm α} [decidable_eq α] :
theorem equiv.perm.is_cycle.exists_pow_eq_one {β : Type u_3} [finite β] {f : equiv.perm β} (hf : f.is_cycle) :
(k : ) (hk : 1 < k), f ^ k = 1
noncomputable def equiv.perm.is_cycle.zpowers_equiv_support {α : Type u_2} [decidable_eq α] [fintype α] {σ : equiv.perm α} (hσ : σ.is_cycle) :

The subgroup generated by a cycle is in bijection with its support

Equations
@[simp]
theorem equiv.perm.is_cycle.zpowers_equiv_support_apply {α : Type u_2} [decidable_eq α] [fintype α] {σ : equiv.perm α} (hσ : σ.is_cycle) {n : } :
(hσ.zpowers_equiv_support) σ ^ n, _⟩ = ^ n) (classical.some hσ), _⟩
@[simp]
theorem equiv.perm.is_cycle.zpowers_equiv_support_symm_apply {α : Type u_2} [decidable_eq α] [fintype α] {σ : equiv.perm α} (hσ : σ.is_cycle) (n : ) :
(hσ.zpowers_equiv_support.symm) ^ n) (classical.some hσ), _⟩ = σ ^ n, _⟩
@[protected]
theorem equiv.perm.is_cycle.order_of {α : Type u_2} {f : equiv.perm α} [decidable_eq α] [fintype α] (hf : f.is_cycle) :
theorem equiv.perm.is_cycle_swap_mul_aux₁ {α : Type u_1} [decidable_eq α] (n : ) {b x : α} {f : equiv.perm α} (hb : (f x) * f) b b) (h : (f ^ n) (f x) = b) :
(i : ), ((equiv.swap x (f x) * f) ^ i) (f x) = b
theorem equiv.perm.is_cycle_swap_mul_aux₂ {α : Type u_1} [decidable_eq α] (n : ) {b x : α} {f : equiv.perm α} (hb : (f x) * f) b b) (h : (f ^ n) (f x) = b) :
(i : ), ((equiv.swap x (f x) * f) ^ i) (f x) = b
theorem equiv.perm.is_cycle.eq_swap_of_apply_apply_eq_self {α : Type u_1} [decidable_eq α] {f : equiv.perm α} (hf : f.is_cycle) {x : α} (hfx : f x x) (hffx : f (f x) = x) :
f = (f x)
theorem equiv.perm.is_cycle.swap_mul {α : Type u_1} [decidable_eq α] {f : equiv.perm α} (hf : f.is_cycle) {x : α} (hx : f x x) (hffx : f (f x) x) :
(f x) * f).is_cycle
theorem equiv.perm.is_cycle.sign {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} (hf : f.is_cycle) :
= -(-1) ^ f.support.card
theorem equiv.perm.is_cycle.of_pow {α : Type u_2} {f : equiv.perm α} [decidable_eq α] [fintype α] {n : } (h1 : (f ^ n).is_cycle) (h2 : f.support (f ^ n).support) :
theorem equiv.perm.is_cycle.of_zpow {α : Type u_2} {f : equiv.perm α} [decidable_eq α] [fintype α] {n : } (h1 : (f ^ n).is_cycle) (h2 : f.support (f ^ n).support) :
theorem equiv.perm.nodup_of_pairwise_disjoint_cycles {β : Type u_3} {l : list (equiv.perm β)} (h1 : (f : , f l f.is_cycle) (h2 : l) :
theorem equiv.perm.is_cycle.support_congr {α : Type u_2} {f g : equiv.perm α} [decidable_eq α] [fintype α] (hf : f.is_cycle) (hg : g.is_cycle) (h : f.support g.support) (h' : (x : α), x f.support f x = g x) :
f = g

Unlike `support_congr`, which assumes that `∀ (x ∈ g.support), f x = g x)`, here we have the weaker assumption that `∀ (x ∈ f.support), f x = g x`.

theorem equiv.perm.is_cycle.eq_on_support_inter_nonempty_congr {α : Type u_2} {f g : equiv.perm α} {x : α} [decidable_eq α] [fintype α] (hf : f.is_cycle) (hg : g.is_cycle) (h : (x : α), x f.support g.support f x = g x) (hx : f x = g x) (hx' : x f.support) :
f = g

If two cyclic permutations agree on all terms in their intersection, and that intersection is not empty, then the two cyclic permutations must be equal.

theorem equiv.perm.is_cycle.support_pow_eq_iff {α : Type u_2} {f : equiv.perm α} [decidable_eq α] [fintype α] (hf : f.is_cycle) {n : } :
(f ^ n).support = f.support ¬ n
theorem equiv.perm.is_cycle.support_pow_of_pos_of_lt_order_of {α : Type u_2} {f : equiv.perm α} [decidable_eq α] [fintype α] (hf : f.is_cycle) {n : } (npos : 0 < n) (hn : n < ) :
(f ^ n).support = f.support
theorem equiv.perm.is_cycle.pow_iff {β : Type u_3} [finite β] {f : equiv.perm β} (hf : f.is_cycle) {n : } :
theorem equiv.perm.is_cycle.pow_eq_one_iff {β : Type u_3} [finite β] {f : equiv.perm β} (hf : f.is_cycle) {n : } :
f ^ n = 1 (x : β), f x x (f ^ n) x = x
theorem equiv.perm.is_cycle.pow_eq_one_iff' {β : Type u_3} [finite β] {f : equiv.perm β} (hf : f.is_cycle) {n : } {x : β} (hx : f x x) :
f ^ n = 1 (f ^ n) x = x
theorem equiv.perm.is_cycle.pow_eq_one_iff'' {β : Type u_3} [finite β] {f : equiv.perm β} (hf : f.is_cycle) {n : } :
f ^ n = 1 (x : β), f x x (f ^ n) x = x
theorem equiv.perm.is_cycle.pow_eq_pow_iff {β : Type u_3} [finite β] {f : equiv.perm β} (hf : f.is_cycle) {a b : } :
f ^ a = f ^ b (x : β), f x x (f ^ a) x = (f ^ b) x
theorem equiv.perm.is_cycle.is_cycle_pow_pos_of_lt_prime_order {β : Type u_3} [finite β] {f : equiv.perm β} (hf : f.is_cycle) (hf' : nat.prime (order_of f)) (n : ) (hn : 0 < n) (hn' : n < ) :
(f ^ n).is_cycle

`is_cycle_on`#

def equiv.perm.is_cycle_on {α : Type u_2} (f : equiv.perm α) (s : set α) :
Prop

A permutation is a cycle on `s` when any two points of `s` are related by repeated application of the permutation. Note that this means the identity is a cycle of subsingleton sets.

Equations
@[simp]
theorem equiv.perm.is_cycle_on_empty {α : Type u_2} {f : equiv.perm α} :
@[simp]
theorem equiv.perm.is_cycle_on_one {α : Type u_2} {s : set α} :
theorem set.subsingleton.is_cycle_on_one {α : Type u_2} {s : set α} :

Alias of the reverse direction of `equiv.perm.is_cycle_on_one`.

Alias of the forward direction of `equiv.perm.is_cycle_on_one`.

@[simp]
theorem equiv.perm.is_cycle_on_singleton {α : Type u_2} {f : equiv.perm α} {a : α} :
f.is_cycle_on {a} f a = a
theorem equiv.perm.is_cycle_on_of_subsingleton {α : Type u_2} [subsingleton α] (f : equiv.perm α) (s : set α) :
@[simp]
theorem equiv.perm.is_cycle_on_inv {α : Type u_2} {f : equiv.perm α} {s : set α} :
theorem equiv.perm.is_cycle_on.of_inv {α : Type u_2} {f : equiv.perm α} {s : set α} :

Alias of the forward direction of `equiv.perm.is_cycle_on_inv`.

theorem equiv.perm.is_cycle_on.inv {α : Type u_2} {f : equiv.perm α} {s : set α} :

Alias of the reverse direction of `equiv.perm.is_cycle_on_inv`.

theorem equiv.perm.is_cycle_on.conj {α : Type u_2} {f g : equiv.perm α} {s : set α} (h : f.is_cycle_on s) :
(g * f * g⁻¹).is_cycle_on (g '' s)
theorem equiv.perm.is_cycle_on_swap {α : Type u_2} {a b : α} [decidable_eq α] (hab : a b) :
b).is_cycle_on {a, b}
@[protected]
theorem equiv.perm.is_cycle_on.apply_ne {α : Type u_2} {f : equiv.perm α} {s : set α} {a : α} (hf : f.is_cycle_on s) (hs : s.nontrivial) (ha : a s) :
f a a
@[protected]
theorem equiv.perm.is_cycle.is_cycle_on {α : Type u_2} {f : equiv.perm α} (hf : f.is_cycle) :
f.is_cycle_on {x : α | f x x}
theorem equiv.perm.is_cycle_iff_exists_is_cycle_on {α : Type u_2} {f : equiv.perm α} :
f.is_cycle (s : set α), s.nontrivial f.is_cycle_on s ⦃x : α⦄, x s

This lemma demonstrates the relation between `equiv.perm.is_cycle` and `equiv.perm.is_cycle_on` in non-degenerate cases.

theorem equiv.perm.is_cycle_on.apply_mem_iff {α : Type u_2} {f : equiv.perm α} {s : set α} {x : α} (hf : f.is_cycle_on s) :
f x s x s
theorem equiv.perm.is_cycle_on.is_cycle_subtype_perm {α : Type u_2} {f : equiv.perm α} {s : set α} (hf : f.is_cycle_on s) (hs : s.nontrivial) :

Note that the identity satisfies `is_cycle_on` for any subsingleton set, but not `is_cycle`.

@[protected]
theorem equiv.perm.is_cycle_on.subtype_perm {α : Type u_2} {f : equiv.perm α} {s : set α} (hf : f.is_cycle_on s) :

Note that the identity is a cycle on any subsingleton set, but not a cycle.

theorem equiv.perm.is_cycle_on.pow_apply_eq {α : Type u_2} {f : equiv.perm α} {a : α} {s : finset α} (hf : f.is_cycle_on s) (ha : a s) {n : } :
(f ^ n) a = a s.card n
theorem equiv.perm.is_cycle_on.zpow_apply_eq {α : Type u_2} {f : equiv.perm α} {a : α} {s : finset α} (hf : f.is_cycle_on s) (ha : a s) {n : } :
(f ^ n) a = a (s.card) n
theorem equiv.perm.is_cycle_on.pow_apply_eq_pow_apply {α : Type u_2} {f : equiv.perm α} {a : α} {s : finset α} (hf : f.is_cycle_on s) (ha : a s) {m n : } :
(f ^ m) a = (f ^ n) a m n [MOD s.card]
theorem equiv.perm.is_cycle_on.zpow_apply_eq_zpow_apply {α : Type u_2} {f : equiv.perm α} {a : α} {s : finset α} (hf : f.is_cycle_on s) (ha : a s) {m n : } :
(f ^ m) a = (f ^ n) a m n [ZMOD (s.card)]
theorem equiv.perm.is_cycle_on.pow_card_apply {α : Type u_2} {f : equiv.perm α} {a : α} {s : finset α} (hf : f.is_cycle_on s) (ha : a s) :
(f ^ s.card) a = a
theorem equiv.perm.is_cycle_on.exists_pow_eq {α : Type u_2} {f : equiv.perm α} {a b : α} {s : finset α} (hf : f.is_cycle_on s) (ha : a s) (hb : b s) :
(n : ) (H : n < s.card), (f ^ n) a = b
theorem equiv.perm.is_cycle_on.exists_pow_eq' {α : Type u_2} {f : equiv.perm α} {s : set α} {a b : α} (hs : s.finite) (hf : f.is_cycle_on s) (ha : a s) (hb : b s) :
(n : ), (f ^ n) a = b
theorem equiv.perm.is_cycle_on.range_pow {α : Type u_2} {f : equiv.perm α} {s : set α} {a : α} (hs : s.finite) (h : f.is_cycle_on s) (ha : a s) :
set.range (λ (n : ), (f ^ n) a) = s
theorem equiv.perm.is_cycle_on.range_zpow {α : Type u_2} {f : equiv.perm α} {s : set α} {a : α} (h : f.is_cycle_on s) (ha : a s) :
set.range (λ (n : ), (f ^ n) a) = s
theorem equiv.perm.is_cycle_on.of_pow {α : Type u_2} {f : equiv.perm α} {s : set α} {n : } (hf : (f ^ n).is_cycle_on s) (h : s s) :
theorem equiv.perm.is_cycle_on.of_zpow {α : Type u_2} {f : equiv.perm α} {s : set α} {n : } (hf : (f ^ n).is_cycle_on s) (h : s s) :
theorem equiv.perm.is_cycle_on.extend_domain {α : Type u_2} {β : Type u_3} {g : equiv.perm α} {s : set α} {p : β Prop} (f : α ) (h : g.is_cycle_on s) :
@[protected]
theorem equiv.perm.is_cycle_on.countable {α : Type u_2} {f : equiv.perm α} {s : set α} (hs : f.is_cycle_on s) :

`cycle_of`#

def equiv.perm.cycle_of {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) :

`f.cycle_of x` is the cycle of the permutation `f` to which `x` belongs.

Equations
theorem equiv.perm.cycle_of_apply {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x y : α) :
(f.cycle_of x) y = ite (f.same_cycle x y) (f y) y
theorem equiv.perm.cycle_of_inv {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) :
@[simp]
theorem equiv.perm.cycle_of_pow_apply_self {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) (n : ) :
(f.cycle_of x ^ n) x = (f ^ n) x
@[simp]
theorem equiv.perm.cycle_of_zpow_apply_self {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) (n : ) :
(f.cycle_of x ^ n) x = (f ^ n) x
theorem equiv.perm.same_cycle.cycle_of_apply {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} :
f.same_cycle x y (f.cycle_of x) y = f y
theorem equiv.perm.cycle_of_apply_of_not_same_cycle {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} :
¬f.same_cycle x y (f.cycle_of x) y = y
theorem equiv.perm.same_cycle.cycle_of_eq {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} (h : f.same_cycle x y) :
@[simp]
theorem equiv.perm.cycle_of_apply_apply_zpow_self {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) (k : ) :
(f.cycle_of x) ((f ^ k) x) = (f ^ (k + 1)) x
@[simp]
theorem equiv.perm.cycle_of_apply_apply_pow_self {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) (k : ) :
(f.cycle_of x) ((f ^ k) x) = (f ^ (k + 1)) x
@[simp]
theorem equiv.perm.cycle_of_apply_apply_self {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) :
(f.cycle_of x) (f x) = f (f x)
@[simp]
theorem equiv.perm.cycle_of_apply_self {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) :
(f.cycle_of x) x = f x
theorem equiv.perm.is_cycle.cycle_of_eq {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} (hf : f.is_cycle) (hx : f x x) :
f.cycle_of x = f
@[simp]
theorem equiv.perm.cycle_of_eq_one_iff {α : Type u_2} [decidable_eq α] [fintype α] {x : α} (f : equiv.perm α) :
f.cycle_of x = 1 f x = x
@[simp]
theorem equiv.perm.cycle_of_self_apply {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) :
f.cycle_of (f x) = f.cycle_of x
@[simp]
theorem equiv.perm.cycle_of_self_apply_pow {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (n : ) (x : α) :
f.cycle_of ((f ^ n) x) = f.cycle_of x
@[simp]
theorem equiv.perm.cycle_of_self_apply_zpow {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (n : ) (x : α) :
f.cycle_of ((f ^ n) x) = f.cycle_of x
@[protected]
theorem equiv.perm.is_cycle.cycle_of {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} (hf : f.is_cycle) :
f.cycle_of x = ite (f x = x) 1 f
theorem equiv.perm.cycle_of_one {α : Type u_2} [decidable_eq α] [fintype α] (x : α) :
1.cycle_of x = 1
theorem equiv.perm.is_cycle_cycle_of {α : Type u_2} [decidable_eq α] [fintype α] {x : α} (f : equiv.perm α) (hx : f x x) :
@[simp]
theorem equiv.perm.two_le_card_support_cycle_of_iff {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
@[simp]
theorem equiv.perm.card_support_cycle_of_pos_iff {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
theorem equiv.perm.pow_apply_eq_pow_mod_order_of_cycle_of_apply {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (n : ) (x : α) :
(f ^ n) x = (f ^ (n % order_of (f.cycle_of x))) x
theorem equiv.perm.cycle_of_mul_of_apply_right_eq_self {α : Type u_2} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : g) (x : α) (hx : g x = x) :
(f * g).cycle_of x = f.cycle_of x
theorem equiv.perm.disjoint.cycle_of_mul_distrib {α : Type u_2} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f.disjoint g) (x : α) :
(f * g).cycle_of x = f.cycle_of x * g.cycle_of x
theorem equiv.perm.support_cycle_of_eq_nil_iff {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
theorem equiv.perm.support_cycle_of_le {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) :
theorem equiv.perm.mem_support_cycle_of_iff {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} :
theorem equiv.perm.mem_support_cycle_of_iff' {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} (hx : f x x) :
theorem equiv.perm.same_cycle.mem_support_iff {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} (h : f.same_cycle x y) :
theorem equiv.perm.pow_mod_card_support_cycle_of_self_apply {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (n : ) (x : α) :
(f ^ (n % (f.cycle_of x).support.card)) x = (f ^ n) x
theorem equiv.perm.is_cycle_cycle_of_iff {α : Type u_2} [decidable_eq α] [fintype α] {x : α} (f : equiv.perm α) :

`x` is in the support of `f` iff `equiv.perm.cycle_of f x` is a cycle.

theorem equiv.perm.same_cycle.exists_pow_eq_of_mem_support {α : Type u_2} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} (h : f.same_cycle x y) (hx : x f.support) :
(i : ) (hi' : i < (f.cycle_of x).support.card), (f ^ i) x = y
theorem equiv.perm.same_cycle.exists_pow_eq {α : Type u_2} [decidable_eq α] [fintype α] {x y : α} (f : equiv.perm α) (h : f.same_cycle x y) :
(i : ) (hi : 0 < i) (hi' : i (f.cycle_of x).support.card + 1), (f ^ i) x = y

`cycle_factors`#

def equiv.perm.cycle_factors_aux {α : Type u_2} [decidable_eq α] [fintype α] (l : list α) (f : equiv.perm α) :
( {x : α}, f x x x l) {l // l.prod = f ( (g : , g l g.is_cycle)

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

Equations
theorem equiv.perm.mem_list_cycles_iff {α : Type u_1} [finite α] {l : list (equiv.perm α)} (h1 : (σ : , σ l σ.is_cycle) (h2 : l) {σ : equiv.perm α} :
σ l σ.is_cycle (a : α), σ a a σ a = (l.prod) a
theorem equiv.perm.list_cycles_perm_list_cycles {α : Type u_1} [finite α] {l₁ l₂ : list (equiv.perm α)} (h₀ : l₁.prod = l₂.prod) (h₁l₁ : (σ : , σ l₁ σ.is_cycle) (h₁l₂ : (σ : , σ l₂ σ.is_cycle) (h₂l₁ : l₁) (h₂l₂ : l₂) :
l₁ ~ l₂
def equiv.perm.cycle_factors {α : Type u_2} [decidable_eq α] [fintype α] [linear_order α] (f : equiv.perm α) :
{l // l.prod = f ( (g : , g l g.is_cycle)

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

Equations
def equiv.perm.trunc_cycle_factors {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) :
trunc {l // l.prod = f ( (g : , g l g.is_cycle)

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

Equations

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

Equations
theorem equiv.perm.cycle_factors_finset_eq_list_to_finset {α : Type u_2} [decidable_eq α] [fintype α] {σ : equiv.perm α} {l : list (equiv.perm α)} (hn : l.nodup) :
( (f : , f l f.is_cycle)
theorem equiv.perm.cycle_factors_finset_eq_finset {α : Type u_2} [decidable_eq α] [fintype α] {σ : equiv.perm α} {s : finset (equiv.perm α)} :
( (f : , f s f.is_cycle) (h : , _ = σ
theorem equiv.perm.cycle_factors_finset_noncomm_prod {α : Type u_2} [decidable_eq α] [fintype α] (f : equiv.perm α) (comm : := _) :
= f

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

theorem equiv.perm.mem_cycle_factors_finset_iff {α : Type u_2} [decidable_eq α] [fintype α] {f p : equiv.perm α} :
p.is_cycle (a : α), a p.support p a = f a
@[simp]

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

theorem equiv.perm.cycle_is_cycle_of {α : Type u_2} [decidable_eq α] [fintype α] {f c : equiv.perm α} {a : α} (ha : a c.support) (hc : c f.cycle_factors_finset) :
c = f.cycle_of a

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

theorem equiv.perm.cycle_induction_on {β : Type u_3} [finite β] (P : Prop) (σ : equiv.perm β) (base_one : P 1) (base_cycles : (σ : , σ.is_cycle P σ) (induction_disjoint : (σ τ : , σ.disjoint τ σ.is_cycle P σ P τ P * τ)) :
P σ
theorem equiv.perm.closure_is_cycle {β : Type u_3} [finite β] :
theorem equiv.perm.closure_cycle_adjacent_swap {α : Type u_2} [decidable_eq α] [fintype α] {σ : equiv.perm α} (h1 : σ.is_cycle) (h2 : σ.support = ) (x : α) :
theorem equiv.perm.closure_cycle_coprime_swap {α : Type u_2} [decidable_eq α] [fintype α] {n : } {σ : equiv.perm α} (h0 : n.coprime (fintype.card α)) (h1 : σ.is_cycle) (h2 : σ.support = finset.univ) (x : α) :
subgroup.closure {σ, (^ n) x)} =
theorem equiv.perm.closure_prime_cycle_swap {α : Type u_2} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} (h0 : nat.prime (fintype.card α)) (h1 : σ.is_cycle) (h2 : σ.support = finset.univ) (h3 : τ.is_swap) :
theorem equiv.perm.is_conj_of_support_equiv {α : Type u_2} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} (f : {x // x (σ.support)} {x // x (τ.support)}) (hf : (x : α) (hx : x (σ.support)), (f σ x, _⟩) = τ (f x, hx⟩)) :
τ
theorem equiv.perm.is_cycle.is_conj {α : Type u_2} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} (hσ : σ.is_cycle) (hτ : τ.is_cycle) (h : σ.support.card = τ.support.card) :
τ
theorem equiv.perm.is_cycle.is_conj_iff {α : Type u_2} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} (hσ : σ.is_cycle) (hτ : τ.is_cycle) :
@[simp]
theorem equiv.perm.support_conj {α : Type u_2} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} :
* τ * σ⁻¹).support =
theorem equiv.perm.card_support_conj {α : Type u_2} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} :
* τ * σ⁻¹).support.card = τ.support.card
theorem equiv.perm.disjoint.is_conj_mul {α : Type u_1} [finite α] {σ τ π ρ : equiv.perm α} (hc1 : π) (hc2 : ρ) (hd1 : σ.disjoint τ) (hd2 : π.disjoint ρ) :
is_conj * τ) * ρ)

Fixed points #

theorem equiv.perm.fixed_point_card_lt_of_ne_one {α : Type u_2} [decidable_eq α] [fintype α] {σ : equiv.perm α} (h : σ 1) :
(finset.filter (λ (x : α), σ x = x) finset.univ).card <
theorem list.nodup.is_cycle_on_form_perm {α : Type u_2} [decidable_eq α] {l : list α} (h : l.nodup) :
l.form_perm.is_cycle_on {a : α | a l}
theorem finset.exists_cycle_on {α : Type u_2} [decidable_eq α] [fintype α] (s : finset α) :
theorem set.countable.exists_cycle_on {α : Type u_2} {s : set α} (hs : s.countable) :
(f : , f.is_cycle_on s {x : α | f x x} s
theorem set.prod_self_eq_Union_perm {α : Type u_2} {f : equiv.perm α} {s : set α} (hf : f.is_cycle_on s) :
s ×ˢ s = (n : ), (λ (a : α), (a, (f ^ n) a)) '' s
theorem finset.product_self_eq_disj_Union_perm_aux {α : Type u_2} {f : equiv.perm α} {s : finset α} (hf : f.is_cycle_on s) :
(λ (k : ), finset.map {to_fun := λ (i : α), (i, (f ^ k) i), inj' := _} s)
theorem finset.product_self_eq_disj_Union_perm {α : Type u_2} {f : equiv.perm α} {s : finset α} (hf : f.is_cycle_on s) :
s ×ˢ s = (λ (k : ), finset.map {to_fun := λ (i : α), (i, (f ^ k) i), inj' := _} s) _

We can partition the square `s ×ˢ s` into shifted diagonals as such:

``````01234
40123
34012
23401
12340
``````

The diagonals are given by the cycle `f`.

theorem finset.sum_smul_sum_eq_sum_perm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [semiring α] [ β] {s : finset ι} {σ : equiv.perm ι} (hσ : σ.is_cycle_on s) (f : ι α) (g : ι β) :
s.sum (λ (i : ι), f i) s.sum (λ (i : ι), g i) = (finset.range s.card).sum (λ (k : ), s.sum (λ (i : ι), f i g (^ k) i)))
theorem finset.sum_mul_sum_eq_sum_perm {ι : Type u_1} {α : Type u_2} [semiring α] {s : finset ι} {σ : equiv.perm ι} (hσ : σ.is_cycle_on s) (f g : ι α) :
s.sum (λ (i : ι), f i) * s.sum (λ (i : ι), g i) = (finset.range s.card).sum (λ (k : ), s.sum (λ (i : ι), f i * g (^ k) i)))