mathlib3 documentation

group_theory.perm.list

Permutations from a list #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A list l : list α can be interpreted as a equiv.perm α where each element in the list is permuted to the next one, defined as form_perm. When we have that nodup l, we prove that equiv.perm.support (form_perm l) = l.to_finset, and that form_perm l is rotationally invariant, in form_perm_rotate.

When there are duplicate elements in l, how and in what arrangement with respect to the other elements they appear in the list determines the formed permutation. This is because list.form_perm is implemented as a product of equiv.swaps. That means that presence of a sublist of two adjacent duplicates like [..., x, x, ...] will produce the same permutation as if the adjacent duplicates were not present.

The list.form_perm definition is meant to primarily be used with nodup l, so that the resulting permutation is cyclic (if l has at least two elements). The presence of duplicates in a particular placement can lead list.form_perm to produce a nontrivial permutation that is noncyclic.

def list.form_perm {α : Type u_1} [decidable_eq α] (l : list α) :

A list l : list α can be interpreted as a equiv.perm α where each element in the list is permuted to the next one, defined as form_perm. When we have that nodup l, we prove that equiv.perm.support (form_perm l) = l.to_finset, and that form_perm l is rotationally invariant, in form_perm_rotate.

Equations

l.form_perm = (list.zip_with equiv.swap l l.tail).prod

@[simp]

theorem list.form_perm_nil {α : Type u_1} [decidable_eq α] :

list.nil.form_perm = 1

@[simp]

theorem list.form_perm_singleton {α : Type u_1} [decidable_eq α] (x : α) :

[x].form_perm = 1

@[simp]

theorem list.form_perm_cons_cons {α : Type u_1} [decidable_eq α] (x y : α) (l : list α) :

(x :: y :: l).form_perm = equiv.swap x y * (y :: l).form_perm

theorem list.form_perm_pair {α : Type u_1} [decidable_eq α] (x y : α) :

[x, y].form_perm = equiv.swap x y

theorem list.form_perm_apply_of_not_mem {α : Type u_1} [decidable_eq α] (x : α) (l : list α) (h : x ∉ l) :

⇑(l.form_perm) x = x

theorem list.mem_of_form_perm_apply_ne {α : Type u_1} [decidable_eq α] (x : α) (l : list α) :

⇑(l.form_perm) x ≠ x → x ∈ l

theorem list.form_perm_apply_mem_of_mem {α : Type u_1} [decidable_eq α] (x : α) (l : list α) (h : x ∈ l) :

⇑(l.form_perm) x ∈ l

theorem list.mem_of_form_perm_apply_mem {α : Type u_1} [decidable_eq α] (x : α) (l : list α) (h : ⇑(l.form_perm) x ∈ l) :

x ∈ l

theorem list.form_perm_mem_iff_mem {α : Type u_1} [decidable_eq α] {l : list α} {x : α} :

⇑(l.form_perm) x ∈ l ↔ x ∈ l

@[simp]

theorem list.form_perm_cons_concat_apply_last {α : Type u_1} [decidable_eq α] (x y : α) (xs : list α) :

⇑((x :: (xs ++ [y])).form_perm) y = x

@[simp]

theorem list.form_perm_apply_last {α : Type u_1} [decidable_eq α] (x : α) (xs : list α) :

⇑((x :: xs).form_perm) ((x :: xs).last _) = x

@[simp]

theorem list.form_perm_apply_nth_le_length {α : Type u_1} [decidable_eq α] (x : α) (xs : list α) :

⇑((x :: xs).form_perm) ((x :: xs).nth_le xs.length _) = x

theorem list.form_perm_apply_head {α : Type u_1} [decidable_eq α] (x y : α) (xs : list α) (h : (x :: y :: xs).nodup) :

⇑((x :: y :: xs).form_perm) x = y

theorem list.form_perm_apply_nth_le_zero {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (hl : 1 < l.length) :

⇑(l.form_perm) (l.nth_le 0 _) = l.nth_le 1 hl

theorem list.form_perm_eq_head_iff_eq_last {α : Type u_1} [decidable_eq α] (l : list α) (x y : α) :

⇑((y :: l).form_perm) x = y ↔ x = (y :: l).last _

theorem list.zip_with_swap_prod_support' {α : Type u_1} [decidable_eq α] (l l' : list α) :

{x : α | ⇑((list.zip_with equiv.swap l l').prod) x ≠ x} ≤ ↑(l.to_finset) ⊔ ↑(l'.to_finset)

theorem list.zip_with_swap_prod_support {α : Type u_1} [decidable_eq α] [fintype α] (l l' : list α) :

(list.zip_with equiv.swap l l').prod.support ≤ l.to_finset ⊔ l'.to_finset

theorem list.support_form_perm_le' {α : Type u_1} [decidable_eq α] (l : list α) :

{x : α | ⇑(l.form_perm) x ≠ x} ≤ ↑(l.to_finset)

theorem list.support_form_perm_le {α : Type u_1} [decidable_eq α] (l : list α) [fintype α] :

l.form_perm.support ≤ l.to_finset

theorem list.form_perm_apply_lt {α : Type u_1} [decidable_eq α] (xs : list α) (h : xs.nodup) (n : ℕ) (hn : n + 1 < xs.length) :

⇑(xs.form_perm) (xs.nth_le n _) = xs.nth_le (n + 1) hn

theorem list.form_perm_apply_nth_le {α : Type u_1} [decidable_eq α] (xs : list α) (h : xs.nodup) (n : ℕ) (hn : n < xs.length) :

⇑(xs.form_perm) (xs.nth_le n hn) = xs.nth_le ((n + 1) % xs.length) _

theorem list.support_form_perm_of_nodup' {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (h' : ∀ (x : α), l ≠ [x]) :

{x : α | ⇑(l.form_perm) x ≠ x} = ↑(l.to_finset)

theorem list.support_form_perm_of_nodup {α : Type u_1} [decidable_eq α] [fintype α] (l : list α) (h : l.nodup) (h' : ∀ (x : α), l ≠ [x]) :

l.form_perm.support = l.to_finset

theorem list.form_perm_rotate_one {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) :

(l.rotate 1).form_perm = l.form_perm

theorem list.form_perm_rotate {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (n : ℕ) :

(l.rotate n).form_perm = l.form_perm

theorem list.form_perm_eq_of_is_rotated {α : Type u_1} [decidable_eq α] {l l' : list α} (hd : l.nodup) (h : l ~r l') :

l.form_perm = l'.form_perm

theorem list.form_perm_reverse {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) :

l.reverse.form_perm = (l.form_perm)⁻¹

theorem list.form_perm_pow_apply_nth_le {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (n k : ℕ) (hk : k < l.length) :

⇑(l.form_perm ^ n) (l.nth_le k hk) = l.nth_le ((k + n) % l.length) _

theorem list.form_perm_pow_apply_head {α : Type u_1} [decidable_eq α] (x : α) (l : list α) (h : (x :: l).nodup) (n : ℕ) :

⇑((x :: l).form_perm ^ n) x = (x :: l).nth_le (n % (x :: l).length) _

theorem list.form_perm_ext_iff {α : Type u_1} [decidable_eq α] {x y x' y' : α} {l l' : list α} (hd : (x :: y :: l).nodup) (hd' : (x' :: y' :: l').nodup) :

(x :: y :: l).form_perm = (x' :: y' :: l').form_perm ↔ (x :: y :: l) ~r (x' :: y' :: l')

theorem list.form_perm_apply_mem_eq_self_iff {α : Type u_1} [decidable_eq α] (l : list α) (hl : l.nodup) (x : α) (hx : x ∈ l) :

⇑(l.form_perm) x = x ↔ l.length ≤ 1

theorem list.form_perm_apply_mem_ne_self_iff {α : Type u_1} [decidable_eq α] (l : list α) (hl : l.nodup) (x : α) (hx : x ∈ l) :

⇑(l.form_perm) x ≠ x ↔ 2 ≤ l.length

theorem list.mem_of_form_perm_ne_self {α : Type u_1} [decidable_eq α] (l : list α) (x : α) (h : ⇑(l.form_perm) x ≠ x) :

x ∈ l

theorem list.form_perm_eq_self_of_not_mem {α : Type u_1} [decidable_eq α] (l : list α) (x : α) (h : x ∉ l) :

⇑(l.form_perm) x = x

theorem list.form_perm_eq_one_iff {α : Type u_1} [decidable_eq α] (l : list α) (hl : l.nodup) :

l.form_perm = 1 ↔ l.length ≤ 1

theorem list.form_perm_eq_form_perm_iff {α : Type u_1} [decidable_eq α] {l l' : list α} (hl : l.nodup) (hl' : l'.nodup) :

l.form_perm = l'.form_perm ↔ l ~r l' ∨ l.length ≤ 1 ∧ l'.length ≤ 1

theorem list.form_perm_zpow_apply_mem_imp_mem {α : Type u_1} [decidable_eq α] (l : list α) (x : α) (hx : x ∈ l) (n : ℤ) :

⇑(l.form_perm ^ n) x ∈ l

theorem list.form_perm_pow_length_eq_one_of_nodup {α : Type u_1} [decidable_eq α] (l : list α) (hl : l.nodup) :

l.form_perm ^ l.length = 1