# Permutations of lists

Content created by Fredrik Bakke, Egbert Rijke and Victor Blanchi.

Created on 2023-05-03.

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)

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