Transporting list rotations

This file records how list rotations act on their finite index types and interact with filtering, and how the permutation formed by a list interacts with mapping by an equivalence.

These lemmas transport a cyclic order, and the successor permutation it induces, across a renaming of indices. They are needed when comparing a combinatorial construction built from a list with the same construction built from a cyclic rotation of that list: filtering both lists by the same predicate gives cyclically rotated sublists, which therefore form the same permutation, and renaming the entries by an equivalence conjugates that permutation. For example, TauCeti.KnotTheory.BraidWord.Cyclic uses them to identify the closures of cyclically rotated braid words.

Main results

• List.rotateIndexEquiv: identify the entries before and after rotating a list.
• List.formPerm_map_equiv: mapping a list by an equivalence conjugates its formed permutation.
• List.formPerm_map_apply: mapping a list by an injective function intertwines the formed permutations on the image.
• List.formPerm_append_apply_of_mem_right and List.formPerm_append_apply_getLast_left: the permutation formed by T ++ V on the entries of V, and on the last entry of T.
• List.IsRotated.filter: filtering preserves cyclic rotation of lists.

def List.rotateIndexEquiv {α : Type u_1} (l : List α) (k : ℕ) : Fin (l.rotate k).length ≃ Fin l.length

The equivalence which sends the index of an entry in l.rotate k to its original index in l. It is the cast along preservation of length followed by addition of k modulo the list length.

Equations

• l.rotateIndexEquiv k = (finCongr ⋯).trans (finRotate l.length ^ k)

theorem List.getElem_rotateIndexEquiv {α : Type u_1} (l : List α) (k : ℕ) (j : Fin (l.rotate k).length) : (l.rotate k)[↑j] = l[↑((l.rotateIndexEquiv k) j)]

Looking up an entry after rotation and translating its index gives the same entry in the original list.

theorem List.map_finRange_rotateIndexEquiv {α : Type u_1} (l : List α) (k : ℕ) : map (⇑(l.rotateIndexEquiv k)) (finRange (l.rotate k).length) = (finRange l.length).rotate k

Translating every index of a rotated list gives the correspondingly rotated list of the original indices.

theorem List.formPerm_map_equiv {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (l : List α) (e : α ≃ β) : (map (⇑e) l).formPerm = e.permCongr l.formPerm

Mapping a list by an equivalence conjugates the permutation formed by the list.

theorem List.formPerm_map_apply {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) (l : List α) (x : α) : (map f l).formPerm (f x) = f (l.formPerm x)

Mapping a list by an injective function intertwines the permutations formed by the two lists: on the image of f, the permutation formed by l.map f is l.formPerm transported along f.

theorem List.formPerm_append_apply_of_mem_right {α : Type u_1} [DecidableEq α] {T V : List α} {x : α} (h : (T ++ V).Nodup) (hx : x ∈ V) : (T ++ V).formPerm x = if V.formPerm x = V.head ⋯ then (T ++ V).head ⋯ else V.formPerm x

On an entry x of V, the permutation formed by T ++ V agrees with the one formed by V, except that the last entry of V, which V.formPerm sends back to the head of V, is sent to the head of T ++ V instead.

theorem List.formPerm_append_apply_getLast_left {α : Type u_1} [DecidableEq α] {T V : List α} (h : (T ++ V).Nodup) (hT : T ≠ []) : (T ++ V).formPerm (T.getLast hT) = (V ++ T).head ⋯

The permutation formed by T ++ V sends the last entry of T to the head of V, or to the head of T if V is empty.

theorem List.IsRotated.filter {α : Type u_1} {l l' : List α} (h : l ~r l') (p : α → Bool) : List.filter p l ~r List.filter p l'

Filtering cyclically rotated lists by the same Boolean predicate preserves their cyclic rotation.