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 #

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
source
theorem equiv.perm.is_cycle.ne_one {β : Type u_2} {f : equiv.perm β} (h : f.is_cycle) :
f ≠ 1
source
theorem equiv.perm.is_cycle.two_le_card_support {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} (h : f.is_cycle) :
2 ≤ f.support.card
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_swap.is_cycle {α : Type u_1} [decidable_eq α] {f : equiv.perm α} (hf : f.is_swap) :
f.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.is_cycle_conj {β : Type u_2} {f g : equiv.perm β} (hf : f.is_cycle) :
((g * f) * g⁻¹).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
def equiv.perm.is_cycle.gpowers_equiv_support {α : Type u_1} [decidable_eq α] [fintype α] {σ : equiv.perm α} (hσ : σ.is_cycle) :
↥↑(subgroup.gpowers σ) ≃ ↥↑(σ.support)

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

Equations
source
@[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σ), _⟩
source
@[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, _⟩
source
theorem equiv.perm.order_of_is_cycle {α : Type u_1} [decidable_eq α] [fintype α] {σ : equiv.perm α} (hσ : σ.is_cycle) :
order_of σ = σ.support.card
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
source
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) :
σ.is_cycle
source
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) :
(g.extend_domain f).is_cycle

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
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
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
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
@[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
source
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
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
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
source
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
source
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_cycle → P σ) (induction_disjoint : ∀ (σ τ : equiv.perm β), σ.disjoint τ → σ.is_cycle → P σ → P τ → P (σ * τ)) :
P σ
source
theorem equiv.perm.closure_is_cycle {β : Type u_2} [fintype β] :
subgroup.closure {σ : equiv.perm β | σ.is_cycle} = ⊤
source
theorem equiv.perm.closure_cycle_adjacent_swap {α : Type u_1} [decidable_eq α] [fintype α] {σ : equiv.perm α} (h1 : σ.is_cycle) (h2 : σ.support = ⊤) (x : α) :
subgroup.closure {σ, equiv.swap x (⇑σ x)} = ⊤
source
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)} = ⊤
source
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) :
subgroup.closure {σ, τ} = ⊤
source
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 σ τ
source
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 σ τ
source
theorem equiv.perm.is_cycle.is_conj_iff {α : Type u_1} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} (hσ : σ.is_cycle) (hτ : τ.is_cycle) :
is_conj σ τ ↔ σ.support.card = τ.support.card
source
@[simp]
theorem equiv.perm.support_conj {α : Type u_1} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} :
((σ * τ) * σ⁻¹).support = finset.map (equiv.to_embedding σ) τ.support
source
theorem equiv.perm.card_support_conj {α : Type u_1} [decidable_eq α] [fintype α] {σ τ : equiv.perm α} :
((σ * τ) * σ⁻¹).support.card = τ.support.card
source
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 #

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