mathlib documentation

group_theory.perm.cycles

Cyclic permutations #

Main definitions #

In the following, f : equiv.perm β.

The following two definitions require that β is a fintype:

Main results #

is_cycle #

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

A permutation is a cycle when 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} :
theorem equiv.perm.is_cycle.two_le_card_support {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} (h : f.is_cycle) :
theorem equiv.perm.is_cycle_swap {α : Type u_1} [decidable_eq α] {x y : α} (hxy : x y) :
theorem equiv.perm.is_swap.is_cycle {α : Type u_1} [decidable_eq α] {f : equiv.perm α} (hf : f.is_swap) :
theorem equiv.perm.is_cycle.inv {β : Type u_2} {f : equiv.perm β} (hf : f.is_cycle) :
theorem equiv.perm.is_cycle.is_cycle_conj {β : Type u_2} {f g : equiv.perm β} (hf : f.is_cycle) :
((g * f) * g⁻¹).is_cycle
theorem equiv.perm.is_cycle.exists_gpow_eq {β : Type u_2} {f : equiv.perm β} (hf : f.is_cycle) {x y : β} (hx : f x x) (hy : f y y) :
∃ (i : ), (f ^ i) x = y
theorem equiv.perm.is_cycle.exists_pow_eq {β : Type u_2} [fintype β] {f : equiv.perm β} (hf : f.is_cycle) {x y : β} (hx : f x x) (hy : f y y) :
∃ (i : ), (f ^ i) x = y
theorem equiv.perm.is_cycle.exists_pow_eq_one {β : Type u_2} [fintype β] {f : equiv.perm β} (hf : f.is_cycle) :
∃ (k : ) (hk : 1 < k), f ^ k = 1

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

Equations
@[simp]
theorem equiv.perm.is_cycle.gpowers_equiv_support_apply {α : Type u_1} [decidable_eq α] [fintype α] {σ : equiv.perm α} (hσ : σ.is_cycle) {n : } :
(hσ.gpowers_equiv_support) σ ^ n, _⟩ = ^ n) (classical.some hσ), _⟩
@[simp]
theorem equiv.perm.is_cycle.gpowers_equiv_support_symm_apply {α : Type u_1} [decidable_eq α] [fintype α] {σ : equiv.perm α} (hσ : σ.is_cycle) (n : ) :
(hσ.gpowers_equiv_support.symm) ^ n) (classical.some hσ), _⟩ = σ ^ n, _⟩
theorem equiv.perm.order_of_is_cycle {α : Type u_1} [decidable_eq α] [fintype α] {σ : equiv.perm α} (hσ : σ.is_cycle) :
theorem equiv.perm.is_cycle_swap_mul_aux₁ {α : Type u_1} [decidable_eq α] (n : ) {b x : α} {f : equiv.perm α} (hb : ((equiv.swap x (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 : ((equiv.swap x (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 = equiv.swap x (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) :
((equiv.swap x (f x)) * f).is_cycle
theorem equiv.perm.is_cycle.sign {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} (hf : f.is_cycle) :
theorem equiv.perm.is_cycle_of_is_cycle_pow {α : Type u_1} [decidable_eq α] [fintype α] {σ : equiv.perm α} {n : } (h1 : ^ n).is_cycle) (h2 : σ.support ^ n).support) :
theorem equiv.perm.is_cycle_of_is_cycle_gpow {α : Type u_1} [decidable_eq α] [fintype α] {σ : equiv.perm α} {n : } (h1 : ^ n).is_cycle) (h2 : σ.support ^ n).support) :
theorem equiv.perm.is_cycle.extend_domain {β : Type u_2} {α : Type u_1} {p : β → Prop} [decidable_pred p] (f : α subtype p) {g : equiv.perm α} (h : g.is_cycle) :
theorem equiv.perm.nodup_of_pairwise_disjoint_cycles {β : Type u_2} {l : list (equiv.perm β)} (h1 : ∀ (f : equiv.perm β), f l → f.is_cycle) (h2 : list.pairwise equiv.perm.disjoint l) :

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
theorem equiv.perm.same_cycle.refl {β : Type u_2} (f : equiv.perm β) (x : β) :
theorem equiv.perm.same_cycle.symm {β : Type u_2} {f : equiv.perm β} {x y : β} :
f.same_cycle x yf.same_cycle y x
theorem equiv.perm.same_cycle.trans {β : Type u_2} {f : equiv.perm β} {x y z : β} :
f.same_cycle x yf.same_cycle y zf.same_cycle x z
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.is_cycle.same_cycle {β : Type u_2} {f : equiv.perm β} (hf : f.is_cycle) {x y : β} (hx : f x x) (hy : f y y) :
theorem equiv.perm.same_cycle.nat' {β : Type u_2} [fintype β] {f : equiv.perm β} {x y : β} (h : f.same_cycle x y) :
∃ (i : ) (h : i < order_of f), (f ^ i) x = y
theorem equiv.perm.same_cycle.nat'' {β : Type u_2} [fintype β] {f : equiv.perm β} {x y : β} (h : f.same_cycle x y) :
∃ (i : ) (hpos : 0 < i) (h : i order_of f), (f ^ i) x = y
@[instance]
Equations
theorem equiv.perm.same_cycle_apply {β : Type u_2} {f : equiv.perm β} {x y : β} :
f.same_cycle x (f y) f.same_cycle x y
theorem equiv.perm.same_cycle_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.same_cycle_inv {β : Type u_2} (f : equiv.perm β) {x y : β} :
theorem equiv.perm.same_cycle_inv_apply {β : Type u_2} {f : equiv.perm β} {x y : β} :
@[simp]
theorem equiv.perm.same_cycle_pow_left_iff {β : 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_gpow_left_iff {β : Type u_2} {f : equiv.perm β} {x y : β} {n : } :
f.same_cycle ((f ^ n) x) y f.same_cycle x y
theorem equiv.perm.is_cycle.support_congr {α : Type u_1} [decidable_eq α] [fintype α] {f g : equiv.perm α} (hf : f.is_cycle) (hg : g.is_cycle) (h : f.support g.support) (h' : ∀ (x : α), x f.supportf 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_1} [decidable_eq α] [fintype α] {f g : equiv.perm α} (hf : f.is_cycle) (hg : g.is_cycle) (h : ∀ (x : α), x f.support g.supportf x = g x) {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_1} [decidable_eq α] [fintype α] {f : equiv.perm α} (hf : f.is_cycle) {n : } :
theorem equiv.perm.is_cycle.pow_iff {β : Type u_2} [fintype β] {f : equiv.perm β} (hf : f.is_cycle) {n : } :
theorem equiv.perm.is_cycle.pow_eq_one_iff {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} (hf : f.is_cycle) {n : } :
f ^ n = 1 ∃ (x : α) (H : x f.support), (f ^ n) x = x
theorem equiv.perm.is_cycle.mem_support_pos_pow_iff_of_lt_order_of {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} (hf : f.is_cycle) {n : } (npos : 0 < n) (hn : n < order_of f) {x : α} :
x (f ^ n).support x f.support
theorem equiv.perm.is_cycle.is_cycle_pow_pos_of_lt_prime_order {β : Type u_2} [fintype β] {f : equiv.perm β} (hf : f.is_cycle) (hf' : nat.prime (order_of f)) (n : ) (hn : 0 < n) (hn' : n < order_of f) :
(f ^ n).is_cycle

cycle_of #

def equiv.perm.cycle_of {α : Type u_1} [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_1} [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_1} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) :
@[simp]
theorem equiv.perm.cycle_of_pow_apply_self {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) (n : ) :
(f.cycle_of x ^ n) x = (f ^ n) x
@[simp]
theorem equiv.perm.cycle_of_gpow_apply_self {α : Type u_1} [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_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} (h : f.same_cycle x y) :
(f.cycle_of x) y = f y
theorem equiv.perm.cycle_of_apply_of_not_same_cycle {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} (h : ¬f.same_cycle x y) :
(f.cycle_of x) y = y
theorem equiv.perm.same_cycle.cycle_of_eq {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} (h : f.same_cycle x y) :
@[simp]
theorem equiv.perm.cycle_of_apply_apply_gpow_self {α : Type u_1} [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_1} [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_1} [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_1} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) :
(f.cycle_of x) x = f x
theorem equiv.perm.is_cycle.cycle_of_eq {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} (hf : f.is_cycle) {x : α} (hx : f x x) :
f.cycle_of x = f
@[simp]
theorem equiv.perm.cycle_of_eq_one_iff {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) {x : α} :
f.cycle_of x = 1 f x = x
@[simp]
theorem equiv.perm.cycle_of_self_apply {α : Type u_1} [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_1} [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_gpow {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) (n : ) (x : α) :
f.cycle_of ((f ^ n) x) = f.cycle_of x
theorem equiv.perm.is_cycle.cycle_of {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} (hf : f.is_cycle) {x : α} :
f.cycle_of x = ite (f x = x) 1 f
theorem equiv.perm.cycle_of_one {α : Type u_1} [decidable_eq α] [fintype α] (x : α) :
1.cycle_of x = 1
theorem equiv.perm.is_cycle_cycle_of {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) {x : α} (hx : f x x) :
@[simp]
theorem equiv.perm.two_le_card_support_cycle_of_iff {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
@[simp]
theorem equiv.perm.card_support_cycle_of_pos_iff {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
theorem equiv.perm.pow_apply_eq_pow_mod_order_of_cycle_of_apply {α : Type u_1} [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_1} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : commute f 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_1} [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_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
theorem equiv.perm.support_cycle_of_le {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) :
theorem equiv.perm.mem_support_cycle_of_iff {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} :
theorem equiv.perm.same_cycle.mem_support_iff {α : Type u_1} [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_1} [decidable_eq α] [fintype α] (f : equiv.perm α) (n : ) (x : α) :
(f ^ (n % (f.cycle_of x).support.card)) x = (f ^ n) x

cycle_factors #

def equiv.perm.cycle_factors_aux {α : Type u_1} [decidable_eq α] [fintype α] (l : list α) (f : equiv.perm α) :
(∀ {x : α}, f x xx l){l // l.prod = f (∀ (g : equiv.perm α), g l → g.is_cycle) 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
theorem equiv.perm.mem_list_cycles_iff {α : Type u_1} [fintype α] {l : list (equiv.perm α)} (h1 : ∀ (σ : equiv.perm α), σ l → σ.is_cycle) (h2 : list.pairwise equiv.perm.disjoint l) {σ : equiv.perm α} :
σ l σ.is_cycle ∀ (a : α), σ a aσ a = (l.prod) a
theorem equiv.perm.list_cycles_perm_list_cycles {α : Type u_1} [fintype α] {l₁ l₂ : list (equiv.perm α)} (h₀ : l₁.prod = l₂.prod) (h₁l₁ : ∀ (σ : equiv.perm α), σ l₁ → σ.is_cycle) (h₁l₂ : ∀ (σ : equiv.perm α), σ l₂ → σ.is_cycle) (h₂l₁ : list.pairwise equiv.perm.disjoint l₁) (h₂l₂ : list.pairwise equiv.perm.disjoint l₂) :
l₁ ~ l₂
def equiv.perm.cycle_factors {α : Type u_1} [decidable_eq α] [fintype α] [linear_order α] (f : equiv.perm α) :
{l // l.prod = f (∀ (g : equiv.perm α), g l → g.is_cycle) list.pairwise equiv.perm.disjoint l}

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

Equations
def equiv.perm.trunc_cycle_factors {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) :
trunc {l // l.prod = f (∀ (g : equiv.perm α), g l → g.is_cycle) 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
def equiv.perm.cycle_factors_finset {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) :

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

Equations
theorem equiv.perm.cycle_factors_finset_eq_finset {α : Type u_1} [decidable_eq α] [fintype α] {σ : equiv.perm α} {s : finset (equiv.perm α)} :
σ.cycle_factors_finset = s (∀ (f : equiv.perm α), f s → f.is_cycle) ∃ (h : ∀ (a : equiv.perm α), a s∀ (b : equiv.perm α), b sa ba.disjoint b), s.noncomm_prod id _ = σ
theorem equiv.perm.cycle_factors_finset_pairwise_disjoint {α : Type u_1} [decidable_eq α] [fintype α] (f p : equiv.perm α) (hp : p f.cycle_factors_finset) (q : equiv.perm α) (hq : q f.cycle_factors_finset) (h : p q) :
theorem equiv.perm.cycle_factors_finset_mem_commute {α : Type u_1} [decidable_eq α] [fintype α] (f p : equiv.perm α) (hp : p f.cycle_factors_finset) (q : equiv.perm α) (hq : q f.cycle_factors_finset) :
theorem equiv.perm.cycle_factors_finset_noncomm_prod {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) (comm : (∀ (g : equiv.perm α), g f.cycle_factors_finset∀ (h : equiv.perm α), h f.cycle_factors_finsetcommute (id g) (id h)) := _) :

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

theorem equiv.perm.mem_cycle_factors_finset_iff {α : Type u_1} [decidable_eq α] [fintype α] {f p : equiv.perm α} :
p f.cycle_factors_finset p.is_cycle ∀ (a : α), a p.supportp a = f a

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

theorem equiv.perm.cycle_induction_on {β : Type u_2} [fintype β] (P : equiv.perm β → Prop) (σ : equiv.perm β) (base_one : P 1) (base_cycles : ∀ (σ : equiv.perm β), σ.is_cycleP σ) (induction_disjoint : ∀ (σ τ : equiv.perm β), σ.disjoint τσ.is_cycleP σP τP * τ)) :
P σ
theorem equiv.perm.same_cycle.nat_of_mem_support {α : Type u_1} [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.nat {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) {x y : α} (h : f.same_cycle x y) :
∃ (i : ) (hi : 0 < i) (hi' : i (f.cycle_of x).support.card + 1), (f ^ i) x = y
theorem equiv.perm.closure_is_cycle {β : Type u_2} [fintype β] :
theorem equiv.perm.closure_cycle_adjacent_swap {α : Type u_1} [decidable_eq α] [fintype α] {σ : equiv.perm α} (h1 : σ.is_cycle) (h2 : σ.support = ) (x : α) :
theorem equiv.perm.closure_cycle_coprime_swap {α : Type u_1} [decidable_eq α] [fintype α] {n : } {σ : equiv.perm α} (h0 : n.coprime (fintype.card α)) (h1 : σ.is_cycle) (h2 : σ.support = finset.univ) (x : α) :
subgroup.closure {σ, equiv.swap x (^ n) x)} =
theorem equiv.perm.closure_prime_cycle_swap {α : Type u_1} [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_1} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} (f : {x // x (σ.support)} {x // x (τ.support)}) (hf : ∀ (x : α) (hx : x (σ.support)), (f σ x, _⟩) = τ (f x, hx⟩)) :
is_conj σ τ
theorem equiv.perm.is_cycle.is_conj {α : Type u_1} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} (hσ : σ.is_cycle) (hτ : τ.is_cycle) (h : σ.support.card = τ.support.card) :
is_conj σ τ
theorem equiv.perm.is_cycle.is_conj_iff {α : Type u_1} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} (hσ : σ.is_cycle) (hτ : τ.is_cycle) :
@[simp]
theorem equiv.perm.support_conj {α : Type u_1} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} :
theorem equiv.perm.card_support_conj {α : Type u_1} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} :
((σ * τ) * σ⁻¹).support.card = τ.support.card
theorem equiv.perm.disjoint.is_conj_mul {α : Type u_1} [fintype α] {σ τ π ρ : equiv.perm α} (hc1 : is_conj σ «π») (hc2 : is_conj τ ρ) (hd1 : σ.disjoint τ) (hd2 : «π».disjoint ρ) :
is_conj * τ) («π» * ρ)

Fixed points #

theorem equiv.perm.fixed_point_card_lt_of_ne_one {α : Type u_1} [decidable_eq α] [fintype α] {σ : equiv.perm α} (h : σ 1) :
(finset.filter (λ (x : α), σ x = x) finset.univ).card < fintype.card α - 1