This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.
Permutations of lists
module lists.permutation-lists where
Imports
open import elementary-number-theory.equality-natural-numbers open import elementary-number-theory.natural-numbers open import finite-group-theory.permutations-standard-finite-types open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.equality-dependent-pair-types open import foundation.identity-types open import foundation.propositions open import foundation.transport-along-identifications open import foundation.universe-levels open import linear-algebra.functoriality-vectors open import linear-algebra.vectors open import lists.arrays open import lists.functoriality-lists open import lists.lists open import lists.permutation-vectors
Idea
Given an array t of length n and a automorphism σ of Fin n, the
permutation of t according to σ is the array where the index are permuted by
σ. Then, we can define what is a permutation of a list of length n via the
equivalence between arrays and lists.
Definition
module _ {l : Level} {A : UU l} where permute-list : (l : list A) → Permutation (length-list l) → list A permute-list l s = list-vec ( length-list l) ( permute-vec (length-list l) (vec-list l) s)
The predicate that a function from list to list is permuting lists
is-permutation-list : (list A → list A) → UU l is-permutation-list f = (l : list A) → Σ ( Permutation (length-list l)) ( λ t → f l ＝ permute-list l t) permutation-is-permutation-list : (f : list A → list A) → is-permutation-list f → ((l : list A) → Permutation (length-list l)) permutation-is-permutation-list f P l = pr1 (P l) eq-permute-list-permutation-is-permutation-list : (f : list A → list A) → (P : is-permutation-list f) → (l : list A) → (f l ＝ permute-list l (permutation-is-permutation-list f P l)) eq-permute-list-permutation-is-permutation-list f P l = pr2 (P l)
Properties
The length of a permuted list
length-permute-list : (l : list A) (t : Permutation (length-list l)) → length-list (permute-list l t) ＝ (length-list l) length-permute-list l t = compute-length-list-list-vec ( length-list l) ( permute-vec (length-list l) (vec-list l) t)
Link between permute-list and permute-vec
eq-vec-list-permute-list : (l : list A) (f : Permutation (length-list l)) → permute-vec (length-list l) (vec-list l) f ＝ tr ( vec A) ( _) ( vec-list ( permute-list l f)) eq-vec-list-permute-list l f = inv ( pr2 ( pair-eq-Σ ( is-retraction-vec-list ( (length-list l , permute-vec (length-list l) (vec-list l) f)))))
If a function f from vec to vec is a permutation of vectors then list-vec ∘ f ∘ vec-list is a permutation of lists
is-permutation-list-is-permutation-vec : (f : (n : ℕ) → vec A n → vec A n) → ((n : ℕ) → is-permutation-vec n (f n)) → is-permutation-list ( λ l → list-vec (length-list l) (f (length-list l) (vec-list l))) pr1 (is-permutation-list-is-permutation-vec f T l) = pr1 (T (length-list l) (vec-list l)) pr2 (is-permutation-list-is-permutation-vec f T l) = ap (λ p → list-vec (length-list l) p) (pr2 (T (length-list l) (vec-list l)))
If x is in permute-list l t then x is in l
is-in-list-is-in-permute-list : (l : list A) (t : Permutation (length-list l)) (x : A) → x ∈-list (permute-list l t) → x ∈-list l is-in-list-is-in-permute-list l t x I = is-in-list-is-in-vec-list ( l) ( x) ( is-in-vec-is-in-permute-vec ( length-list l) ( vec-list l) ( t) ( x) ( tr ( λ p → x ∈-vec (pr2 p)) ( is-retraction-vec-list ( length-list l , permute-vec (length-list l) (vec-list l) t)) ( is-in-vec-list-is-in-list ( list-vec ( length-list l) ( permute-vec (length-list l) (vec-list l) t)) ( x) ( I)))) is-in-permute-list-is-in-list : (l : list A) (t : Permutation (length-list l)) (x : A) → x ∈-list l → x ∈-list (permute-list l t) is-in-permute-list-is-in-list l t x I = is-in-list-is-in-vec-list ( permute-list l t) ( x) ( tr ( λ p → x ∈-vec (pr2 p)) ( inv ( is-retraction-vec-list ( length-list l , permute-vec (length-list l) (vec-list l) t))) ( is-in-permute-vec-is-in-vec ( length-list l) ( vec-list l) ( t) ( x) ( is-in-vec-list-is-in-list l x I)))
If μ : A → (B → B) satisfies a commutativity property, then fold-list b μ is invariant under permutation for every b : B
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} (b : B) (μ : A → (B → B)) (C : commutative-fold-vec μ) where invariant-fold-vec-tr : {n m : ℕ} (v : vec A n) (eq : n ＝ m) → fold-vec b μ (tr (vec A) eq v) ＝ fold-vec b μ v invariant-fold-vec-tr v refl = refl invariant-permutation-fold-list : (l : list A) → (f : Permutation (length-list l)) → fold-list b μ l ＝ fold-list b μ (permute-list l f) invariant-permutation-fold-list l f = ( inv (htpy-fold-list-fold-vec b μ l) ∙ ( invariant-permutation-fold-vec b μ C (vec-list l) f ∙ ( ap (fold-vec b μ) (eq-vec-list-permute-list l f) ∙ ( ( invariant-fold-vec-tr { m = length-list l} ( vec-list (permute-list l f)) ( _)) ∙ ( htpy-fold-list-fold-vec b μ (permute-list l f))))))
map-list of the permutation of a list
compute-tr-permute-vec : {l : Level} {A : UU l} {n m : ℕ} (e : n ＝ m) (v : vec A n) (t : Permutation m) → tr ( vec A) ( e) ( permute-vec ( n) ( v) ( tr Permutation (inv e) t)) ＝ permute-vec ( m) ( tr (vec A) e v) ( t) compute-tr-permute-vec refl v t = refl compute-tr-map-vec : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) {n m : ℕ} (p : n ＝ m) (v : vec A n) → tr (vec B) p (map-vec f v) ＝ map-vec f (tr (vec A) p v) compute-tr-map-vec f refl v = refl helper-compute-list-vec-map-vec-permute-vec-vec-list : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (p : list A) (t : Permutation (length-list p)) → tr ( vec B) ( inv (length-permute-list p t)) ( map-vec f (permute-vec (length-list p) (vec-list p) t)) ＝ map-vec f (vec-list (permute-list p t)) helper-compute-list-vec-map-vec-permute-vec-vec-list f p t = ( ( compute-tr-map-vec ( f) ( inv (length-permute-list p t)) ( permute-vec (length-list p) (vec-list p) t)) ∙ ( ( ap ( λ P → map-vec ( f) ( tr (vec _) P (permute-vec (length-list p) (vec-list p) t))) ( eq-is-prop (is-set-ℕ _ _))) ∙ ( ap ( map-vec f) ( pr2 ( pair-eq-Σ ( inv ( is-retraction-vec-list ( length-list p , permute-vec (length-list p) (vec-list p) t)))))))) compute-list-vec-map-vec-permute-vec-vec-list : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (p : list A) (t : Permutation (length-list p)) → list-vec ( length-list p) ( map-vec f (permute-vec (length-list p) (vec-list p) t)) ＝ list-vec ( length-list (permute-list p t)) ( map-vec f (vec-list (permute-list p t))) compute-list-vec-map-vec-permute-vec-vec-list f p t = ap ( λ p → list-vec (pr1 p) (pr2 p)) ( eq-pair-Σ ( inv (length-permute-list p t)) ( ( helper-compute-list-vec-map-vec-permute-vec-vec-list f p t))) eq-map-list-permute-list : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (p : list A) (t : Permutation (length-list p)) → permute-list (map-list f p) (tr Permutation (inv (length-map-list f p)) t) ＝ map-list f (permute-list p t) eq-map-list-permute-list {B = B} f p t = ( ( ap ( λ (n , p) → list-vec n p) ( eq-pair-Σ ( length-map-list f p) ( ( ap ( λ x → tr ( vec B) ( length-map-list f p) ( permute-vec ( length-list (map-list f p)) ( x) ( tr Permutation (inv (length-map-list f p)) t))) ( vec-list-map-list-map-vec-list' f p)) ∙ ( ( compute-tr-permute-vec ( length-map-list f p) ( tr (vec B) (inv (length-map-list f p)) (map-vec f (vec-list p))) ( t)) ∙ ( ap ( λ v → permute-vec (length-list p) v t) ( is-section-inv-tr ( vec B) ( length-map-list f p) ( map-vec f (vec-list p)))))))) ∙ ( ( ap ( list-vec (length-list p)) ( eq-map-vec-permute-vec f (vec-list p) t)) ∙ ( compute-list-vec-map-vec-permute-vec-vec-list f p t ∙ ( map-list-map-vec-list f (permute-list p t)))))