# Properties of cyclic permutations constructed from lists/cycles #

In the following, {α : Type*} [Fintype α] [DecidableEq α].

## Main definitions #

• Cycle.formPerm: the cyclic permutation created by looping over a Cycle α
• Equiv.Perm.toList: the list formed by iterating application of a permutation
• Equiv.Perm.toCycle: the cycle formed by iterating application of a permutation
• Equiv.Perm.isoCycle: the equivalence between cyclic permutations f : Perm α and the terms of Cycle α that correspond to them
• Equiv.Perm.isoCycle': the same equivalence as Equiv.Perm.isoCycle but with evaluation via choosing over fintypes
• The notation c[1, 2, 3] to emulate notation of cyclic permutations (1 2 3)
• A Repr instance for any Perm α, by representing the Finset of Cycle α that correspond to the cycle factors.

## Main results #

• List.isCycle_formPerm: a nontrivial list without duplicates, when interpreted as a permutation, is cyclic
• Equiv.Perm.IsCycle.existsUnique_cycle: there is only one nontrivial Cycle α corresponding to each cyclic f : Perm α

## Implementation details #

The forward direction of Equiv.Perm.isoCycle' 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.toCycle, 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.formPerm_disjoint_iff {α : Type u_1} [] {l : List α} {l' : List α} (hl : l.Nodup) (hl' : l'.Nodup) (hn : 2 l.length) (hn' : 2 l'.length) :
l.formPerm.Disjoint l'.formPerm l.Disjoint l'
theorem List.isCycle_formPerm {α : Type u_1} [] {l : List α} (hl : l.Nodup) (hn : 2 l.length) :
l.formPerm.IsCycle
theorem List.pairwise_sameCycle_formPerm {α : Type u_1} [] {l : List α} (hl : l.Nodup) (hn : 2 l.length) :
List.Pairwise l.formPerm.SameCycle l
theorem List.cycleOf_formPerm {α : Type u_1} [] {l : List α} (hl : l.Nodup) (hn : 2 l.length) (x : { x : α // x l }) :
l.attach.formPerm.cycleOf x = l.attach.formPerm
theorem List.cycleType_formPerm {α : Type u_1} [] {l : List α} (hl : l.Nodup) (hn : 2 l.length) :
l.attach.formPerm.cycleType = {l.length}
theorem List.formPerm_apply_mem_eq_next {α : Type u_1} [] {l : List α} (hl : l.Nodup) (x : α) (hx : x l) :
l.formPerm x = l.next x hx
def Cycle.formPerm {α : Type u_1} [] (s : ) :
s.Nodup

A cycle s : Cycle α, given Nodup s can be interpreted as an Equiv.Perm α where each element in the list is permuted to the next one, defined as formPerm.

Equations
Instances For
@[simp]
theorem Cycle.formPerm_coe {α : Type u_1} [] (l : List α) (hl : l.Nodup) :
(l).formPerm hl = l.formPerm
theorem Cycle.formPerm_subsingleton {α : Type u_1} [] (s : ) (h : s.Subsingleton) :
s.formPerm = 1
theorem Cycle.isCycle_formPerm {α : Type u_1} [] (s : ) (h : s.Nodup) (hn : s.Nontrivial) :
(s.formPerm h).IsCycle
theorem Cycle.support_formPerm {α : Type u_1} [] [] (s : ) (h : s.Nodup) (hn : s.Nontrivial) :
(s.formPerm h).support = s.toFinset
theorem Cycle.formPerm_eq_self_of_not_mem {α : Type u_1} [] (s : ) (h : s.Nodup) (x : α) (hx : xs) :
(s.formPerm h) x = x
theorem Cycle.formPerm_apply_mem_eq_next {α : Type u_1} [] (s : ) (h : s.Nodup) (x : α) (hx : x s) :
(s.formPerm h) x = s.next h x hx
theorem Cycle.formPerm_reverse {α : Type u_1} [] (s : ) (h : s.Nodup) :
s.reverse.formPerm = (s.formPerm h)⁻¹
theorem Cycle.formPerm_eq_formPerm_iff {α : Type u_2} [] {s : } {s' : } {hs : s.Nodup} {hs' : s'.Nodup} :
s.formPerm hs = s'.formPerm hs' s = s' s.Subsingleton s'.Subsingleton
def Equiv.Perm.toList {α : Type u_1} [] [] (p : ) (x : α) :
List α

Equiv.Perm.toList (f : Perm α) (x : α) generates the list [x, f x, f (f x), ...] until looping. That means when f x = x, toList f x = [].

Equations
Instances For
@[simp]
theorem Equiv.Perm.toList_one {α : Type u_1} [] [] (x : α) :
= []
@[simp]
theorem Equiv.Perm.toList_eq_nil_iff {α : Type u_1} [] [] {p : } {x : α} :
p.toList x = [] xp.support
@[simp]
theorem Equiv.Perm.length_toList {α : Type u_1} [] [] (p : ) (x : α) :
(p.toList x).length = (p.cycleOf x).support.card
theorem Equiv.Perm.toList_ne_singleton {α : Type u_1} [] [] (p : ) (x : α) (y : α) :
p.toList x [y]
theorem Equiv.Perm.two_le_length_toList_iff_mem_support {α : Type u_1} [] [] {p : } {x : α} :
2 (p.toList x).length x p.support
theorem Equiv.Perm.length_toList_pos_of_mem_support {α : Type u_1} [] [] (p : ) (x : α) (h : x p.support) :
0 < (p.toList x).length
theorem Equiv.Perm.get_toList {α : Type u_1} [] [] (p : ) (x : α) (n : ) (hn : n < (p.toList x).length) :
(p.toList x).get n, hn = (p ^ n) x
theorem Equiv.Perm.toList_get_zero {α : Type u_1} [] [] (p : ) (x : α) (h : x p.support) :
(p.toList x).get 0, = x
@[deprecated Equiv.Perm.get_toList]
theorem Equiv.Perm.nthLe_toList {α : Type u_1} [] [] (p : ) (x : α) (n : ) (hn : n < (p.toList x).length) :
(p.toList x).nthLe n hn = (p ^ n) x
@[deprecated Equiv.Perm.toList_get_zero]
theorem Equiv.Perm.toList_nthLe_zero {α : Type u_1} [] [] (p : ) (x : α) (h : x p.support) :
(p.toList x).nthLe 0 = x
theorem Equiv.Perm.mem_toList_iff {α : Type u_1} [] [] {p : } {x : α} {y : α} :
y p.toList x p.SameCycle x y x p.support
theorem Equiv.Perm.nodup_toList {α : Type u_1} [] [] (p : ) (x : α) :
(p.toList x).Nodup
theorem Equiv.Perm.next_toList_eq_apply {α : Type u_1} [] [] (p : ) (x : α) (y : α) (hy : y p.toList x) :
(p.toList x).next y hy = p y
theorem Equiv.Perm.toList_pow_apply_eq_rotate {α : Type u_1} [] [] (p : ) (x : α) (k : ) :
p.toList ((p ^ k) x) = (p.toList x).rotate k
theorem Equiv.Perm.SameCycle.toList_isRotated {α : Type u_1} [] [] {f : } {x : α} {y : α} (h : f.SameCycle x y) :
f.toList x ~r f.toList y
theorem Equiv.Perm.pow_apply_mem_toList_iff_mem_support {α : Type u_1} [] [] {p : } {x : α} {n : } :
(p ^ n) x p.toList x x p.support
theorem Equiv.Perm.toList_formPerm_nil {α : Type u_1} [] [] (x : α) :
[].formPerm.toList x = []
theorem Equiv.Perm.toList_formPerm_singleton {α : Type u_1} [] [] (x : α) (y : α) :
[x].formPerm.toList y = []
theorem Equiv.Perm.toList_formPerm_nontrivial {α : Type u_1} [] [] (l : List α) (hl : 2 l.length) (hn : l.Nodup) :
l.formPerm.toList (l.get 0, ) = l
theorem Equiv.Perm.toList_formPerm_isRotated_self {α : Type u_1} [] [] (l : List α) (hl : 2 l.length) (hn : l.Nodup) (x : α) (hx : x l) :
l.formPerm.toList x ~r l
theorem Equiv.Perm.formPerm_toList {α : Type u_1} [] [] (f : ) (x : α) :
(f.toList x).formPerm = f.cycleOf x
def Equiv.Perm.toCycle {α : Type u_1} [] [] (f : ) (hf : f.IsCycle) :

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.toList f x.

Equations
• f.toCycle hf = Finset.univ.val.recOn (Quot.mk Setoid.r []) (fun (x : α) (x_1 : ) (l : ) => if f x = x then l else (f.toList x))
Instances For
theorem Equiv.Perm.toCycle_eq_toList {α : Type u_1} [] [] (f : ) (hf : f.IsCycle) (x : α) (hx : f x x) :
f.toCycle hf = (f.toList x)
theorem Equiv.Perm.nodup_toCycle {α : Type u_1} [] [] (f : ) (hf : f.IsCycle) :
(f.toCycle hf).Nodup
theorem Equiv.Perm.nontrivial_toCycle {α : Type u_1} [] [] (f : ) (hf : f.IsCycle) :
(f.toCycle hf).Nontrivial
def Equiv.Perm.isoCycle {α : Type u_1} [] [] :
{ f : // f.IsCycle } { 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.toCycle.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Equiv.Perm.IsCycle.existsUnique_cycle {α : Type u_1} [] [] {f : } (hf : f.IsCycle) :
∃! s : , ∃ (h : s.Nodup), s.formPerm h = f
theorem Equiv.Perm.IsCycle.existsUnique_cycle_subtype {α : Type u_1} [] [] {f : } (hf : f.IsCycle) :
∃! s : { s : // s.Nodup }, (s).formPerm = f
theorem Equiv.Perm.IsCycle.existsUnique_cycle_nontrivial_subtype {α : Type u_1} [] [] {f : } (hf : f.IsCycle) :
∃! s : { s : // s.Nodup s.Nontrivial }, (s).formPerm = f
def Equiv.Perm.isoCycle' {α : Type u_1} [] [] :
{ f : // f.IsCycle } { 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.isoCycle' = let f := fun (s : { s : // s.Nodup s.Nontrivial }) => (s).formPerm , ; { toFun := , invFun := f, left_inv := , right_inv := }
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
unsafe instance Equiv.Perm.repr_perm {α : Type u_1} [] [] [Repr α] :
Repr ()
Equations
• One or more equations did not get rendered due to their size.