mathlib3 documentation

group_theory.perm.cycle.concrete

Properties of cyclic permutations constructed from lists/cycles #

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

In the following, {α : Type*} [fintype α] [decidable_eq α].

Main definitions #

cycle.form_perm: the cyclic permutation created by looping over a cycle α
equiv.perm.to_list: the list formed by iterating application of a permutation
equiv.perm.to_cycle: the cycle formed by iterating application of a permutation
equiv.perm.iso_cycle: the equivalence between cyclic permutations f : perm α and the terms of cycle α that correspond to them
equiv.perm.iso_cycle': the same equivalence as equiv.perm.iso_cycle but with evaluation via choosing over fintypes
The notation c[1, 2, 3] to emulate notation of cyclic permutations (1 2 3)
A has_repr instance for any perm α, by representing the finset of cycle α that correspond to the cycle factors.

Main results #

list.is_cycle_form_perm: a nontrivial list without duplicates, when interpreted as a permutation, is cyclic
equiv.perm.is_cycle.exists_unique_cycle: there is only one nontrivial cycle α corresponding to each cyclic f : perm α

Implementation details #

The forward direction of equiv.perm.iso_cycle' uses fintype.choose of the uniqueness result, relying on the fintype instance of a cycle.nodup subtype. It is unclear if this works faster than the equiv.perm.to_cycle, which relies on recursion over finset.univ. Running #eval on even a simple noncyclic permutation c[(1 : fin 7), 2, 3] * c[0, 5] to show it takes a long time. TODO: is this because computing the cycle factors is slow?

theorem list.form_perm_disjoint_iff {α : Type u_1} [decidable_eq α] {l l' : list α} (hl : l.nodup) (hl' : l'.nodup) (hn : 2 ≤ l.length) (hn' : 2 ≤ l'.length) :

l.form_perm.disjoint l'.form_perm ↔ l.disjoint l'

theorem list.is_cycle_form_perm {α : Type u_1} [decidable_eq α] {l : list α} (hl : l.nodup) (hn : 2 ≤ l.length) :

l.form_perm.is_cycle

theorem list.pairwise_same_cycle_form_perm {α : Type u_1} [decidable_eq α] {l : list α} (hl : l.nodup) (hn : 2 ≤ l.length) :

list.pairwise l.form_perm.same_cycle l

theorem list.cycle_of_form_perm {α : Type u_1} [decidable_eq α] {l : list α} (hl : l.nodup) (hn : 2 ≤ l.length) (x : {x // x ∈ l}) :

l.attach.form_perm.cycle_of x = l.attach.form_perm

theorem list.cycle_type_form_perm {α : Type u_1} [decidable_eq α] {l : list α} (hl : l.nodup) (hn : 2 ≤ l.length) :

l.attach.form_perm.cycle_type = {l.length}

theorem list.form_perm_apply_mem_eq_next {α : Type u_1} [decidable_eq α] {l : list α} (hl : l.nodup) (x : α) (hx : x ∈ l) :

⇑(l.form_perm) x = l.next x hx

def cycle.form_perm {α : Type u_1} [decidable_eq α] (s : cycle α) (h : s.nodup) :

A cycle s : cycle α , given nodup s can be interpreted as a equiv.perm α where each element in the list is permuted to the next one, defined as form_perm.

Equations

cycle.form_perm = λ (s : cycle α), quot.hrec_on s (λ (l : list α) (h : cycle.nodup (quot.mk setoid.r l)), l.form_perm) cycle.form_perm._proof_1

@[simp]

theorem cycle.form_perm_coe {α : Type u_1} [decidable_eq α] (l : list α) (hl : l.nodup) :

↑l.form_perm hl = l.form_perm

theorem cycle.form_perm_subsingleton {α : Type u_1} [decidable_eq α] (s : cycle α) (h : s.subsingleton) :

s.form_perm _ = 1

theorem cycle.is_cycle_form_perm {α : Type u_1} [decidable_eq α] (s : cycle α) (h : s.nodup) (hn : s.nontrivial) :

(s.form_perm h).is_cycle

theorem cycle.support_form_perm {α : Type u_1} [decidable_eq α] [fintype α] (s : cycle α) (h : s.nodup) (hn : s.nontrivial) :

(s.form_perm h).support = s.to_finset

theorem cycle.form_perm_eq_self_of_not_mem {α : Type u_1} [decidable_eq α] (s : cycle α) (h : s.nodup) (x : α) (hx : x ∉ s) :

⇑(s.form_perm h) x = x

theorem cycle.form_perm_apply_mem_eq_next {α : Type u_1} [decidable_eq α] (s : cycle α) (h : s.nodup) (x : α) (hx : x ∈ s) :

⇑(s.form_perm h) x = s.next h x hx

theorem cycle.form_perm_reverse {α : Type u_1} [decidable_eq α] (s : cycle α) (h : s.nodup) :

s.reverse.form_perm _ = (s.form_perm h)⁻¹

theorem cycle.form_perm_eq_form_perm_iff {α : Type u_1} [decidable_eq α] {s s' : cycle α} {hs : s.nodup} {hs' : s'.nodup} :

s.form_perm hs = s'.form_perm hs' ↔ s = s' ∨ s.subsingleton ∧ s'.subsingleton

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

equiv.perm.to_list (f : perm α) (x : α) generates the list [x, f x, f (f x), ...] until looping. That means when f x = x, to_list f x = [].

Equations

p.to_list x = list.map (λ (k : ℕ), ⇑(p ^ k) x) (list.range (p.cycle_of x).support.card)

@[simp]

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

1.to_list x = list.nil

@[simp]

theorem equiv.perm.to_list_eq_nil_iff {α : Type u_1} [fintype α] [decidable_eq α] {p : equiv.perm α} {x : α} :

p.to_list x = list.nil ↔ x ∉ p.support

@[simp]

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

(p.to_list x).length = (p.cycle_of x).support.card

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

p.to_list x ≠ [y]

theorem equiv.perm.two_le_length_to_list_iff_mem_support {α : Type u_1} [fintype α] [decidable_eq α] {p : equiv.perm α} {x : α} :

2 ≤ (p.to_list x).length ↔ x ∈ p.support

theorem equiv.perm.length_to_list_pos_of_mem_support {α : Type u_1} [fintype α] [decidable_eq α] (p : equiv.perm α) (x : α) (h : x ∈ p.support) :

0 < (p.to_list x).length

theorem equiv.perm.nth_le_to_list {α : Type u_1} [fintype α] [decidable_eq α] (p : equiv.perm α) (x : α) (n : ℕ) (hn : n < (p.to_list x).length) :

(p.to_list x).nth_le n hn = ⇑(p ^ n) x

theorem equiv.perm.to_list_nth_le_zero {α : Type u_1} [fintype α] [decidable_eq α] (p : equiv.perm α) (x : α) (h : x ∈ p.support) :

(p.to_list x).nth_le 0 _ = x

theorem equiv.perm.mem_to_list_iff {α : Type u_1} [fintype α] [decidable_eq α] {p : equiv.perm α} {x y : α} :

y ∈ p.to_list x ↔ p.same_cycle x y ∧ x ∈ p.support

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

(p.to_list x).nodup

theorem equiv.perm.next_to_list_eq_apply {α : Type u_1} [fintype α] [decidable_eq α] (p : equiv.perm α) (x y : α) (hy : y ∈ p.to_list x) :

(p.to_list x).next y hy = ⇑p y

theorem equiv.perm.to_list_pow_apply_eq_rotate {α : Type u_1} [fintype α] [decidable_eq α] (p : equiv.perm α) (x : α) (k : ℕ) :

p.to_list (⇑(p ^ k) x) = (p.to_list x).rotate k

theorem equiv.perm.same_cycle.to_list_is_rotated {α : Type u_1} [fintype α] [decidable_eq α] {f : equiv.perm α} {x y : α} (h : f.same_cycle x y) :

f.to_list x ~r f.to_list y

theorem equiv.perm.pow_apply_mem_to_list_iff_mem_support {α : Type u_1} [fintype α] [decidable_eq α] {p : equiv.perm α} {x : α} {n : ℕ} :

⇑(p ^ n) x ∈ p.to_list x ↔ x ∈ p.support

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

list.nil.form_perm.to_list x = list.nil

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

[x].form_perm.to_list y = list.nil

theorem equiv.perm.to_list_form_perm_nontrivial {α : Type u_1} [fintype α] [decidable_eq α] (l : list α) (hl : 2 ≤ l.length) (hn : l.nodup) :

l.form_perm.to_list (l.nth_le 0 _) = l

theorem equiv.perm.to_list_form_perm_is_rotated_self {α : Type u_1} [fintype α] [decidable_eq α] (l : list α) (hl : 2 ≤ l.length) (hn : l.nodup) (x : α) (hx : x ∈ l) :

l.form_perm.to_list x ~r l

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

(f.to_list x).form_perm = f.cycle_of x

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

Given a cyclic f : perm α, generate the cycle α in the order of application of f. Implemented by finding an element x : α in the support of f in finset.univ, and iterating on using equiv.perm.to_list f x.

Equations

f.to_cycle hf = finset.univ.val.rec_on (quot.mk setoid.r list.nil) (λ (x : α) (s : multiset α) (l : cycle α), ite (⇑f x = x) l ↑(f.to_list x)) _

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

f.to_cycle hf = ↑(f.to_list x)

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

(f.to_cycle hf).nodup

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

(f.to_cycle hf).nontrivial

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

{f // f.is_cycle} ≃ {s // s.nodup ∧ s.nontrivial}

Any cyclic f : perm α is isomorphic to the nontrivial cycle α that corresponds to repeated application of f. The forward direction is implemented by equiv.perm.to_cycle.

Equations

equiv.perm.iso_cycle = {to_fun := λ (f : {f // f.is_cycle}), ⟨↑f.to_cycle _, _⟩, inv_fun := λ (s : {s // s.nodup ∧ s.nontrivial}), ⟨↑s.form_perm _, _⟩, left_inv := _, right_inv := _}

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

∃! (s : cycle α), ∃ (h : s.nodup), s.form_perm h = f

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

∃! (s : {s // s.nodup}), ↑s.form_perm _ = f

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

∃! (s : {s // s.nodup ∧ s.nontrivial}), ↑s.form_perm _ = f

def equiv.perm.iso_cycle' {α : Type u_1} [fintype α] [decidable_eq α] :

{f // f.is_cycle} ≃ {s // s.nodup ∧ s.nontrivial}

Any cyclic f : perm α is isomorphic to the nontrivial cycle α that corresponds to repeated application of f. The forward direction is implemented by finding this cycle α using fintype.choose.

Equations

equiv.perm.iso_cycle' = {to_fun := λ (f : {f // f.is_cycle}), fintype.choose (λ (a : {s // s.nodup ∧ s.nontrivial}), ↑a.form_perm _ = ↑f) _, inv_fun := λ (s : {s // s.nodup ∧ s.nontrivial}), ⟨↑s.form_perm _, _⟩, left_inv := _, right_inv := _}

@[protected, instance]

meta def equiv.perm.repr_perm {α : Type u_1} [fintype α] [decidable_eq α] [has_repr α] :

has_repr (equiv.perm α)