Permutations of lists

module lists.permutation-lists where
Imports
open import elementary-number-theory.natural-numbers

open import finite-group-theory.permutations-standard-finite-types

open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.functions
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
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-Σ
          ( isretr-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))
          ( isretr-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
          ( isretr-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
               ( isretr-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)
              ( issec-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)))))