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

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

theorem List.cycleOf_formPerm {α : Type u_1} [DecidableEq α] {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} [DecidableEq α] {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} [DecidableEq α] {l : List α} (hl : l.Nodup) (x : α) (hx : x ∈ l) : l.formPerm x = l.next x hx

def Cycle.formPerm {α : Type u_1} [DecidableEq α] (s : Cycle α) : s.Nodup → 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

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

@[simp]

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

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

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

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

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

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

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

theorem Cycle.formPerm_eq_formPerm_iff {α : Type u_2} [DecidableEq α] {s : Cycle α} {s' : Cycle α} {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} [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

• p.toList x = List.map (fun (k : ℕ) => (p ^ k) x) (List.range (p.cycleOf x).support.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 : α} : p.toList x = [] ↔ x ∉ p.support

@[simp]

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

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

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

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

theorem Equiv.Perm.get_toList {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (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} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) (h : x ∈ p.support) : (p.toList x).get ⟨0, ⋯⟩ = x

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

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

theorem Equiv.Perm.next_toList_eq_apply {α : Type u_1} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (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} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (x : α) (k : ℕ) : p.toList ((p ^ k) x) = (p.toList x).rotate k

theorem Equiv.Perm.SameCycle.toList_isRotated {α : Type u_1} [Fintype α] [DecidableEq α] {f : Equiv.Perm α} {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} [Fintype α] [DecidableEq α] {p : Equiv.Perm α} {x : α} {n : ℕ} : (p ^ n) x ∈ p.toList x ↔ x ∈ p.support

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

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

theorem Equiv.Perm.toList_formPerm_nontrivial {α : Type u_1} [Fintype α] [DecidableEq α] (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} [Fintype α] [DecidableEq α] (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} [Fintype α] [DecidableEq α] (f : Equiv.Perm α) (x : α) : (f.toList x).formPerm = f.cycleOf x

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

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

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

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

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

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

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

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

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

def Equiv.Perm.isoCycle' {α : Type u_1} [Fintype α] [DecidableEq α] : { f : Equiv.Perm α // f.IsCycle } ≃ { s : Cycle α // 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' = { toFun := Fintype.bijInv ⋯, invFun := fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) => ⟨(↑s).formPerm ⋯, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

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 α)