# Documentation

Mathlib.GroupTheory.Perm.Cycle.Concrete

# 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 : ) (hl' : ) (hn : 2 ) (hn' : 2 ) :
theorem List.isCycle_formPerm {α : Type u_1} [] {l : List α} (hl : ) (hn : 2 ) :
theorem List.pairwise_sameCycle_formPerm {α : Type u_1} [] {l : List α} (hl : ) (hn : 2 ) :
theorem List.cycleOf_formPerm {α : Type u_1} [] {l : List α} (hl : ) (hn : 2 ) (x : { x // x l }) :
theorem List.cycleType_formPerm {α : Type u_1} [] {l : List α} (hl : ) (hn : 2 ) :
theorem List.formPerm_apply_mem_eq_next {α : Type u_1} [] {l : List α} (hl : ) (x : α) (hx : x l) :
↑() x = List.next l x hx
def Cycle.formPerm {α : Type u_1} [] (s : ) :

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.

Instances For
@[simp]
theorem Cycle.formPerm_coe {α : Type u_1} [] (l : List α) (hl : ) :
Cycle.formPerm (l) hl =
theorem Cycle.formPerm_subsingleton {α : Type u_1} [] (s : ) (h : ) :
Cycle.formPerm s (_ : ) = 1
theorem Cycle.isCycle_formPerm {α : Type u_1} [] (s : ) (h : ) (hn : ) :
theorem Cycle.support_formPerm {α : Type u_1} [] [] (s : ) (h : ) (hn : ) :
theorem Cycle.formPerm_eq_self_of_not_mem {α : Type u_1} [] (s : ) (h : ) (x : α) (hx : ¬x s) :
↑() x = x
theorem Cycle.formPerm_apply_mem_eq_next {α : Type u_1} [] (s : ) (h : ) (x : α) (hx : x s) :
↑() x = Cycle.next s h x hx
theorem Cycle.formPerm_reverse {α : Type u_1} [] (s : ) (h : ) :
Cycle.formPerm () (_ : ) = ()⁻¹
theorem Cycle.formPerm_eq_formPerm_iff {α : Type u_2} [] {s : } {s' : } {hs : } {hs' : } :
= Cycle.formPerm s' hs' s = s'
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 = [].

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 : α} :
= [] ¬
@[simp]
theorem Equiv.Perm.length_toList {α : Type u_1} [] [] (p : ) (x : α) :
theorem Equiv.Perm.toList_ne_singleton {α : Type u_1} [] [] (p : ) (x : α) (y : α) :
[y]
theorem Equiv.Perm.two_le_length_toList_iff_mem_support {α : Type u_1} [] [] {p : } {x : α} :
2
theorem Equiv.Perm.length_toList_pos_of_mem_support {α : Type u_1} [] [] (p : ) (x : α) (h : ) :
0 <
theorem Equiv.Perm.nthLe_toList {α : Type u_1} [] [] (p : ) (x : α) (n : ) (hn : n < ) :
List.nthLe () n hn = ↑(p ^ n) x
theorem Equiv.Perm.toList_nthLe_zero {α : Type u_1} [] [] (p : ) (x : α) (h : ) :
List.nthLe () 0 (_ : 0 < ) = x
theorem Equiv.Perm.mem_toList_iff {α : Type u_1} [] [] {p : } {x : α} {y : α} :
theorem Equiv.Perm.nodup_toList {α : Type u_1} [] [] (p : ) (x : α) :
theorem Equiv.Perm.next_toList_eq_apply {α : Type u_1} [] [] (p : ) (x : α) (y : α) (hy : y ) :
List.next () y hy = p y
theorem Equiv.Perm.toList_pow_apply_eq_rotate {α : Type u_1} [] [] (p : ) (x : α) (k : ) :
Equiv.Perm.toList p (↑(p ^ k) x) = List.rotate () k
theorem Equiv.Perm.SameCycle.toList_isRotated {α : Type u_1} [] [] {f : } {x : α} {y : α} (h : ) :
theorem Equiv.Perm.pow_apply_mem_toList_iff_mem_support {α : Type u_1} [] [] {p : } {x : α} {n : } :
↑(p ^ n) x
theorem Equiv.Perm.toList_formPerm_nil {α : Type u_1} [] [] (x : α) :
= []
theorem Equiv.Perm.toList_formPerm_singleton {α : Type u_1} [] [] (x : α) (y : α) :
= []
theorem Equiv.Perm.toList_formPerm_nontrivial {α : Type u_1} [] [] (l : List α) (hl : 2 ) (hn : ) :
Equiv.Perm.toList () (List.nthLe l 0 (_ : 0 < )) = l
theorem Equiv.Perm.toList_formPerm_isRotated_self {α : Type u_1} [] [] (l : List α) (hl : 2 ) (hn : ) (x : α) (hx : x l) :
~r l
theorem Equiv.Perm.formPerm_toList {α : Type u_1} [] [] (f : ) (x : α) :
def Equiv.Perm.toCycle {α : Type u_1} [] [] (f : ) (hf : ) :

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.

Instances For
theorem Equiv.Perm.toCycle_eq_toList {α : Type u_1} [] [] (f : ) (hf : ) (x : α) (hx : f x x) :
= ↑()
theorem Equiv.Perm.nodup_toCycle {α : Type u_1} [] [] (f : ) (hf : ) :
theorem Equiv.Perm.nontrivial_toCycle {α : Type u_1} [] [] (f : ) (hf : ) :
def Equiv.Perm.isoCycle {α : Type u_1} [] [] :
{ f // } { s // }

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.

Instances For
theorem Equiv.Perm.IsCycle.existsUnique_cycle {α : Type u_1} [] [] {f : } (hf : ) :
∃! s, h, = f
theorem Equiv.Perm.IsCycle.existsUnique_cycle_subtype {α : Type u_1} [] [] {f : } (hf : ) :
∃! s, Cycle.formPerm s (_ : ) = f
theorem Equiv.Perm.IsCycle.existsUnique_cycle_nontrivial_subtype {α : Type u_1} [] [] {f : } (hf : ) :
∃! s, Cycle.formPerm s (_ : ) = f
def Equiv.Perm.isoCycle' {α : Type u_1} [] [] :
{ f // } { s // }

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.

Instances For
Instances For
Instances For
unsafe instance Equiv.Perm.repr_perm {α : Type u_1} [] [] [Repr α] :
Repr ()