mathlib documentation

group_theory.perm.cycles

def equiv.perm.same_cycle {β : Type u_2} :
equiv.perm ββ → β → 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.apply_eq_self_iff_of_same_cycle {β : Type u_2} {f : equiv.perm β} {x y : β} :
f.same_cycle x y(f x = x f y = y)

theorem equiv.perm.same_cycle_of_is_cycle {β : Type u_2} {f : equiv.perm β} (hf : f.is_cycle) {x y : β} :
f x xf y yf.same_cycle x y

@[instance]
def equiv.perm.decidable_rel {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) :

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 : β} :
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 : β} :

def equiv.perm.cycle_of {α : Type u_1} [decidable_eq α] [fintype α] :
equiv.perm αα → equiv.perm α

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.cycle_of_apply_of_same_cycle {α : Type u_1} [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_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} :
¬f.same_cycle x y(f.cycle_of x) y = y

@[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.cycle_of_cycle {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} (hf : f.is_cycle) {x : α} :
f x xf.cycle_of x = 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 : α} :
f x x(f.cycle_of x).is_cycle

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
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
theorem equiv.perm.one_lt_nonfixed_point_card_of_ne_one {α : Type u_1} [decidable_eq α] [fintype α] {σ : equiv.perm α} :
σ 11 < (finset.filter (λ (x : α), σ x x) finset.univ).card

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