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} [DecidableEq α] {l : List α} {l' : List α} (hl : List.Nodup l) (hl' : List.Nodup l') (hn : 2 ≤ List.length l) (hn' : 2 ≤ List.length l') : Equiv.Perm.Disjoint (List.formPerm l) (List.formPerm l') ↔ List.Disjoint l l'

theorem List.isCycle_formPerm {α : Type u_1} [DecidableEq α] {l : List α} (hl : List.Nodup l) (hn : 2 ≤ List.length l) : Equiv.Perm.IsCycle (List.formPerm l)

theorem List.pairwise_sameCycle_formPerm {α : Type u_1} [DecidableEq α] {l : List α} (hl : List.Nodup l) (hn : 2 ≤ List.length l) : List.Pairwise (Equiv.Perm.SameCycle (List.formPerm l)) l

theorem List.cycleOf_formPerm {α : Type u_1} [DecidableEq α] {l : List α} (hl : List.Nodup l) (hn : 2 ≤ List.length l) (x : { x : α // x ∈ l }) : Equiv.Perm.cycleOf (List.formPerm (List.attach l)) x = List.formPerm (List.attach l)

theorem List.cycleType_formPerm {α : Type u_1} [DecidableEq α] {l : List α} (hl : List.Nodup l) (hn : 2 ≤ List.length l) : Equiv.Perm.cycleType (List.formPerm (List.attach l)) = {List.length l}

theorem List.formPerm_apply_mem_eq_next {α : Type u_1} [DecidableEq α] {l : List α} (hl : List.Nodup l) (x : α) (hx : x ∈ l) : (List.formPerm l) x = List.next l x hx

def Cycle.formPerm {α : Type u_1} [DecidableEq α] (s : Cycle α) : Cycle.Nodup s → Equiv.Perm α

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

• Cycle.formPerm s = Quotient.hrecOn (motive := fun (x : Cycle α) => Cycle.Nodup x → Equiv.Perm α) s (fun (l : List α) (x : Cycle.Nodup ⟦l⟧) => List.formPerm l) ⋯

@[simp]

theorem Cycle.formPerm_coe {α : Type u_1} [DecidableEq α] (l : List α) (hl : List.Nodup l) : Cycle.formPerm (↑l) hl = List.formPerm l

theorem Cycle.formPerm_subsingleton {α : Type u_1} [DecidableEq α] (s : Cycle α) (h : Cycle.Subsingleton s) : Cycle.formPerm s ⋯ = 1

theorem Cycle.isCycle_formPerm {α : Type u_1} [DecidableEq α] (s : Cycle α) (h : Cycle.Nodup s) (hn : Cycle.Nontrivial s) : Equiv.Perm.IsCycle (Cycle.formPerm s h)

theorem Cycle.support_formPerm {α : Type u_1} [DecidableEq α] [Fintype α] (s : Cycle α) (h : Cycle.Nodup s) (hn : Cycle.Nontrivial s) : Equiv.Perm.support (Cycle.formPerm s h) = Cycle.toFinset s

theorem Cycle.formPerm_eq_self_of_not_mem {α : Type u_1} [DecidableEq α] (s : Cycle α) (h : Cycle.Nodup s) (x : α) (hx : x ∉ s) : (Cycle.formPerm s h) x = x

theorem Cycle.formPerm_apply_mem_eq_next {α : Type u_1} [DecidableEq α] (s : Cycle α) (h : Cycle.Nodup s) (x : α) (hx : x ∈ s) : (Cycle.formPerm s h) x = Cycle.next s h x hx

theorem Cycle.formPerm_reverse {α : Type u_1} [DecidableEq α] (s : Cycle α) (h : Cycle.Nodup s) : Cycle.formPerm (Cycle.reverse s) ⋯ = (Cycle.formPerm s h)⁻¹

theorem Cycle.formPerm_eq_formPerm_iff {α : Type u_2} [DecidableEq α] {s : Cycle α} {s' : Cycle α} {hs : Cycle.Nodup s} {hs' : Cycle.Nodup s'} : Cycle.formPerm s hs = Cycle.formPerm s' hs' ↔ s = s' ∨ Cycle.Subsingleton s ∧ Cycle.Subsingleton s'

def Equiv.Perm.toList {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (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

• Equiv.Perm.toList p x = List.map (fun (k : ℕ) => (p ^ k) x) (List.range (Equiv.Perm.support (Equiv.Perm.cycleOf p x)).card)

@[simp]

theorem Equiv.Perm.toList_one {α : Type u_1} [Fintype α] [DecidableEq α] (x : α) : Equiv.Perm.toList 1 x = []

@[simp]

theorem Equiv.Perm.toList_eq_nil_iff {α : Type u_1} [Fintype α] [DecidableEq α] {p : Equiv.Perm α} {x : α} : Equiv.Perm.toList p x = [] ↔ x ∉ Equiv.Perm.support p

@[simp]

theorem Equiv.Perm.length_toList {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) : List.length (Equiv.Perm.toList p x) = (Equiv.Perm.support (Equiv.Perm.cycleOf p x)).card

theorem Equiv.Perm.toList_ne_singleton {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) (y : α) : Equiv.Perm.toList p x ≠ [y]

theorem Equiv.Perm.two_le_length_toList_iff_mem_support {α : Type u_1} [Fintype α] [DecidableEq α] {p : Equiv.Perm α} {x : α} : 2 ≤ List.length (Equiv.Perm.toList p x) ↔ x ∈ Equiv.Perm.support p

theorem Equiv.Perm.length_toList_pos_of_mem_support {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) (h : x ∈ Equiv.Perm.support p) : 0 < List.length (Equiv.Perm.toList p x)

theorem Equiv.Perm.nthLe_toList {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) (n : ℕ) (hn : n < List.length (Equiv.Perm.toList p x)) : List.nthLe (Equiv.Perm.toList p x) n hn = (p ^ n) x

theorem Equiv.Perm.toList_nthLe_zero {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) (h : x ∈ Equiv.Perm.support p) : List.nthLe (Equiv.Perm.toList p x) 0 ⋯ = x

theorem Equiv.Perm.mem_toList_iff {α : Type u_1} [Fintype α] [DecidableEq α] {p : Equiv.Perm α} {x : α} {y : α} : y ∈ Equiv.Perm.toList p x ↔ Equiv.Perm.SameCycle p x y ∧ x ∈ Equiv.Perm.support p

theorem Equiv.Perm.nodup_toList {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) : List.Nodup (Equiv.Perm.toList p x)

theorem Equiv.Perm.next_toList_eq_apply {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) (y : α) (hy : y ∈ Equiv.Perm.toList p x) : List.next (Equiv.Perm.toList p x) y hy = p y

theorem Equiv.Perm.toList_pow_apply_eq_rotate {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) (k : ℕ) : Equiv.Perm.toList p ((p ^ k) x) = List.rotate (Equiv.Perm.toList p x) k

theorem Equiv.Perm.SameCycle.toList_isRotated {α : Type u_1} [Fintype α] [DecidableEq α] {f : Equiv.Perm α} {x : α} {y : α} (h : Equiv.Perm.SameCycle f x y) : Equiv.Perm.toList f x ~r Equiv.Perm.toList f y

theorem Equiv.Perm.pow_apply_mem_toList_iff_mem_support {α : Type u_1} [Fintype α] [DecidableEq α] {p : Equiv.Perm α} {x : α} {n : ℕ} : (p ^ n) x ∈ Equiv.Perm.toList p x ↔ x ∈ Equiv.Perm.support p

theorem Equiv.Perm.toList_formPerm_nil {α : Type u_1} [Fintype α] [DecidableEq α] (x : α) : Equiv.Perm.toList (List.formPerm []) x = []

theorem Equiv.Perm.toList_formPerm_singleton {α : Type u_1} [Fintype α] [DecidableEq α] (x : α) (y : α) : Equiv.Perm.toList (List.formPerm [x]) y = []

theorem Equiv.Perm.toList_formPerm_nontrivial {α : Type u_1} [Fintype α] [DecidableEq α] (l : List α) (hl : 2 ≤ List.length l) (hn : List.Nodup l) : Equiv.Perm.toList (List.formPerm l) (List.get l { val := 0, isLt := ⋯ }) = l

theorem Equiv.Perm.toList_formPerm_isRotated_self {α : Type u_1} [Fintype α] [DecidableEq α] (l : List α) (hl : 2 ≤ List.length l) (hn : List.Nodup l) (x : α) (hx : x ∈ l) : Equiv.Perm.toList (List.formPerm l) x ~r l

theorem Equiv.Perm.formPerm_toList {α : Type u_1} [Fintype α] [DecidableEq α] (f : Equiv.Perm α) (x : α) : List.formPerm (Equiv.Perm.toList f x) = Equiv.Perm.cycleOf f x

def Equiv.Perm.toCycle {α : Type u_1} [Fintype α] [DecidableEq α] (f : Equiv.Perm α) (hf : Equiv.Perm.IsCycle f) : 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.toList f x.

Equations

• Equiv.Perm.toCycle f hf = Multiset.recOn Finset.univ.val (Quot.mk Setoid.r []) (fun (x : α) (x_1 : Multiset α) (l : Cycle α) => if f x = x then l else ↑(Equiv.Perm.toList f x)) ⋯

theorem Equiv.Perm.toCycle_eq_toList {α : Type u_1} [Fintype α] [DecidableEq α] (f : Equiv.Perm α) (hf : Equiv.Perm.IsCycle f) (x : α) (hx : f x ≠ x) : Equiv.Perm.toCycle f hf = ↑(Equiv.Perm.toList f x)

theorem Equiv.Perm.nodup_toCycle {α : Type u_1} [Fintype α] [DecidableEq α] (f : Equiv.Perm α) (hf : Equiv.Perm.IsCycle f) : Cycle.Nodup (Equiv.Perm.toCycle f hf)

theorem Equiv.Perm.nontrivial_toCycle {α : Type u_1} [Fintype α] [DecidableEq α] (f : Equiv.Perm α) (hf : Equiv.Perm.IsCycle f) : Cycle.Nontrivial (Equiv.Perm.toCycle f hf)

def Equiv.Perm.isoCycle {α : Type u_1} [Fintype α] [DecidableEq α] : { f : Equiv.Perm α // Equiv.Perm.IsCycle f } ≃ { s : Cycle α // Cycle.Nodup s ∧ Cycle.Nontrivial 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.

Equations

• One or more equations did not get rendered due to their size.

theorem Equiv.Perm.IsCycle.existsUnique_cycle {α : Type u_1} [Finite α] [DecidableEq α] {f : Equiv.Perm α} (hf : Equiv.Perm.IsCycle f) : ∃! s : Cycle α, ∃ (h : Cycle.Nodup s), Cycle.formPerm s h = f

theorem Equiv.Perm.IsCycle.existsUnique_cycle_subtype {α : Type u_1} [Finite α] [DecidableEq α] {f : Equiv.Perm α} (hf : Equiv.Perm.IsCycle f) : ∃! s : { s : Cycle α // Cycle.Nodup s }, Cycle.formPerm ↑s ⋯ = f

theorem Equiv.Perm.IsCycle.existsUnique_cycle_nontrivial_subtype {α : Type u_1} [Finite α] [DecidableEq α] {f : Equiv.Perm α} (hf : Equiv.Perm.IsCycle f) : ∃! s : { s : Cycle α // Cycle.Nodup s ∧ Cycle.Nontrivial s }, Cycle.formPerm ↑s ⋯ = f

def Equiv.Perm.isoCycle' {α : Type u_1} [Fintype α] [DecidableEq α] : { f : Equiv.Perm α // Equiv.Perm.IsCycle f } ≃ { s : Cycle α // Cycle.Nodup s ∧ Cycle.Nontrivial 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.

Equations

• One or more equations did not get rendered due to their size.

def Equiv.Perm.«termC[_,]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.