mathlib3documentation

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) :
theorem list.is_cycle_form_perm {α : Type u_1} [decidable_eq α] {l : list α} (hl : l.nodup) (hn : 2 l.length) :
theorem list.pairwise_same_cycle_form_perm {α : Type u_1} [decidable_eq α] {l : list α} (hl : l.nodup) (hn : 2 l.length) :
theorem list.cycle_of_form_perm {α : Type u_1} [decidable_eq α] {l : list α} (hl : l.nodup) (hn : 2 l.length) (x : {x // x l}) :
theorem list.cycle_type_form_perm {α : Type u_1} [decidable_eq α] {l : list α} (hl : l.nodup) (hn : 2 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
@[simp]
theorem cycle.form_perm_coe {α : Type u_1} [decidable_eq α] (l : list α) (hl : l.nodup) :
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) :
theorem cycle.support_form_perm {α : Type u_1} [decidable_eq α] [fintype α] (s : cycle α) (h : s.nodup) (hn : s.nontrivial) :
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) :
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'
def equiv.perm.to_list {α : Type u_1} [fintype α] [decidable_eq α] (p : equiv.perm α) (x : α) :
list α

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
@[simp]
theorem equiv.perm.to_list_one {α : Type u_1} [fintype α] [decidable_eq α] (x : α) :
@[simp]
theorem equiv.perm.to_list_eq_nil_iff {α : Type u_1} [fintype α] [decidable_eq α] {p : equiv.perm α} {x : α} :
@[simp]
theorem equiv.perm.length_to_list {α : Type u_1} [fintype α] [decidable_eq α] (p : equiv.perm α) (x : α) :
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.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 : α} :
theorem equiv.perm.nodup_to_list {α : Type u_1} [fintype α] [decidable_eq α] (p : equiv.perm α) (x : α) :
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) :
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 : α) :
theorem equiv.perm.to_list_form_perm_singleton {α : Type u_1} [fintype α] [decidable_eq α] (x y : α) :
theorem equiv.perm.to_list_form_perm_nontrivial {α : Type u_1} [fintype α] [decidable_eq α] (l : list α) (hl : 2 l.length) (hn : l.nodup) :
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) :
theorem equiv.perm.form_perm_to_list {α : Type u_1} [fintype α] [decidable_eq α] (f : equiv.perm α) (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
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) :
theorem equiv.perm.nontrivial_to_cycle {α : Type u_1} [fintype α] [decidable_eq α] (f : equiv.perm α) (hf : f.is_cycle) :
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
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
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
@[protected, instance]
meta def equiv.perm.repr_perm {α : Type u_1} [fintype α] [decidable_eq α] [has_repr α] :