Cyclic permutations

Main definitions

In the following, f : equiv.perm β.

equiv.perm.is_cycle: f.is_cycle when two nonfixed points of β are related by repeated application of f.
equiv.perm.same_cycle: f.same_cycle x y when x and y are in the same cycle 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.

`is_cycle`

source

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

f.is_cycle = ∃ (x : β), ⇑f x ≠ x ∧ ∀ (y : β), ⇑f y ≠ y → (∃ (i : ℤ), ⇑(f ^ i) x = y)

source

theorem equiv.perm.is_cycle.swap {α : Type u_1} [decidable_eq α] {x y : α} (hxy : x ≠ y) :

(equiv.swap x y).is_cycle

source

theorem equiv.perm.is_cycle.inv {β : Type u_2} {f : equiv.perm β} (hf : f.is_cycle) :

f⁻¹.is_cycle

source

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

source

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

source

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

source

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

source

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)

source

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

source

theorem equiv.perm.is_cycle.sign {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} (hf : f.is_cycle) :

⇑equiv.perm.sign f = -(-1) ^ f.support.card

`same_cycle`

source

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

f.same_cycle x y = ∃ (i : ℤ), ⇑(f ^ i) x = y

source

theorem equiv.perm.same_cycle.refl {β : Type u_2} (f : equiv.perm β) (x : β) :

f.same_cycle x x

source

theorem equiv.perm.same_cycle.symm {β : Type u_2} (f : equiv.perm β) {x y : β} :

f.same_cycle x y → f.same_cycle y x

source

theorem equiv.perm.same_cycle.trans {β : Type u_2} (f : equiv.perm β) {x y z : β} :

f.same_cycle x y → f.same_cycle y z → f.same_cycle x z

source

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)

source

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) :

f.same_cycle x y

source

@[instance]

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

decidable_rel f.same_cycle

Equations

equiv.perm.same_cycle.decidable_rel f = λ (x y : α), decidable_of_iff (∃ (n : ℕ) (H : n ∈ list.range (order_of f)), ⇑(f ^ n) x = y) _

source

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

source

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

source

theorem equiv.perm.same_cycle_inv {β : Type u_2} (f : equiv.perm β) {x y : β} :

f⁻¹.same_cycle x y ↔ f.same_cycle x y

source

theorem equiv.perm.same_cycle_inv_apply {β : Type u_2} {f : equiv.perm β} {x y : β} :

f.same_cycle x (⇑f⁻¹ y) ↔ f.same_cycle x y

`cycle_of`

source

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

equiv.perm α

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

Equations

f.cycle_of x = ⇑equiv.perm.of_subtype (f.subtype_perm _)

source

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

source

theorem equiv.perm.cycle_of_inv {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) :

(f.cycle_of x)⁻¹ = f⁻¹.cycle_of x

source

@[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

source

@[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

source

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

source

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

source

@[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

source

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

source

theorem equiv.perm.cycle_of_one {α : Type u_1} [decidable_eq α] [fintype α] (x : α) :

1.cycle_of x = 1

source

theorem equiv.perm.is_cycle_cycle_of {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) {x : α} (hx : ⇑f x ≠ x) :

(f.cycle_of x).is_cycle

`cycle_factors`

source

def equiv.perm.cycle_factors_aux {α : Type u_1} [decidable_eq α] [fintype α] (l : list α) (f : equiv.perm α) :

(∀ {x : α}, ⇑f x ≠ x → x ∈ 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

equiv.perm.cycle_factors_aux (x :: l) f h = dite (⇑f x = x) (λ (hx : ⇑f x = x), equiv.perm.cycle_factors_aux l f _) (λ (hx : ¬⇑f x = x), equiv.perm.cycle_factors_aux._match_1 x f hx (equiv.perm.cycle_factors_aux l ((f.cycle_of x)⁻¹ * f) _))
equiv.perm.cycle_factors_aux list.nil f h = ⟨list.nil (equiv.perm α), _⟩
equiv.perm.cycle_factors_aux._match_1 x f hx ⟨m, _⟩ = ⟨f.cycle_of x :: m, _⟩

source

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

f.cycle_factors = equiv.perm.cycle_factors_aux (finset.sort has_le.le finset.univ) f _

Fixed points

source

theorem equiv.perm.one_lt_nonfixed_point_card_of_ne_one {α : Type u_1} [decidable_eq α] [fintype α] {σ : equiv.perm α} (h : σ ≠ 1) :

1 < (finset.filter (λ (x : α), ⇑σ x ≠ x) finset.univ).card

source

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