Permutations of vectors

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

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

open import foundation.cartesian-product-types
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equivalence-extensionality
open import foundation.equivalences
open import foundation.functions
open import foundation.functoriality-coproduct-types
open import foundation.identity-types
open import foundation.negation
open import foundation.unit-type
open import foundation.universe-levels

open import linear-algebra.functoriality-vectors
open import linear-algebra.vectors

open import lists.arrays
open import lists.lists

open import univalent-combinatorics.2-element-decidable-subtypes
open import univalent-combinatorics.standard-finite-types

Idea

Given an functional vector t of length n and a automorphism σ of Fin n, the permutation of t according to σ is the functional vector where the index are permuted by σ. Then, we can define what is a permutation of a vector of length n via the equivalence between functional vectors and vectors.

Definitions

module _
  {l : Level} {A : UU l}
  where

  permute-vec : (n : )  vec A n  Permutation n  vec A n
  permute-vec n v s =
    listed-vec-functional-vec n (functional-vec-vec n v  (map-equiv s))

The predicate that a function from vec to vec is just permuting vectors.

  is-permutation-vec : (n : )  (vec A n  vec A n)  UU l
  is-permutation-vec n f =
    (v : vec A n) 
    Σ ( Permutation n)
      ( λ t  f v  permute-vec n v t)

  permutation-is-permutation-vec :
    (n : )(f : vec A n  vec A n)  is-permutation-vec n f 
    (v : vec A n)  Permutation n
  permutation-is-permutation-vec n f P v = pr1 (P v)

  eq-permute-vec-permutation-is-permutation-vec :
    (n : ) (f : vec A n  vec A n)  (P : is-permutation-vec n f) 
    (v : vec A n) 
    (f v  permute-vec n v (permutation-is-permutation-vec n f P v))
  eq-permute-vec-permutation-is-permutation-vec n f P v = pr2 (P v)

Properties

Computational rules

  compute-permute-vec-id-equiv :
    (n : )
    (v : vec A n) 
    permute-vec n v id-equiv  v
  compute-permute-vec-id-equiv n v =
    ap  f  map-equiv f v) (right-inverse-law-equiv (compute-vec n))

  compute-composition-permute-vec :
    (n : )
    (v : vec A n) 
    (a b : Permutation n) 
    permute-vec n v (a ∘e b)  permute-vec n (permute-vec n v a) b
  compute-composition-permute-vec n v a b =
    ap
      ( λ f  listed-vec-functional-vec n (f  (map-equiv b)))
      ( inv
        ( isretr-functional-vec-vec n (functional-vec-vec n v  map-equiv a)))

  compute-swap-two-last-elements-transposition-Fin-permute-vec :
    (n : )
    (v : vec A n) 
    (x y : A) 
    permute-vec
      (succ-ℕ (succ-ℕ n))
      (x  y  v)
      (swap-two-last-elements-transposition-Fin n) 
    (y  x  v)
  compute-swap-two-last-elements-transposition-Fin-permute-vec n v x y =
    eq-Eq-vec
      ( succ-ℕ (succ-ℕ n))
      ( permute-vec
          ( succ-ℕ (succ-ℕ n))
          ( x  y  v)
          ( swap-two-last-elements-transposition-Fin n))
      ( y  x  v)
      ( refl ,
        refl ,
        Eq-eq-vec
          ( n)
          ( permute-vec n v id-equiv)
          ( v)
          ( compute-permute-vec-id-equiv n v))

  compute-equiv-coprod-permutation-id-equiv-permute-vec :
    (n : )
    (v : vec A n)
    (x : A)
    (t : Permutation n) 
    permute-vec (succ-ℕ n) (x  v) (equiv-coprod t id-equiv) 
    (x  permute-vec n v t)
  compute-equiv-coprod-permutation-id-equiv-permute-vec n v x t =
    eq-Eq-vec
      ( succ-ℕ n)
      ( permute-vec (succ-ℕ n) (x  v) (equiv-coprod t id-equiv))
      ( x  permute-vec n v t)
      ( refl ,
        ( Eq-eq-vec
          ( n)
          ( _)
          ( permute-vec n v t)
          ( refl)))

  ap-permute-vec :
    {n : }
    (a : Permutation n)
    {v w : vec A n} 
    v  w 
    permute-vec n v a  permute-vec n w a
  ap-permute-vec a refl = refl

x is in a vector v iff it is in permute v t

  is-in-functional-vec-is-in-permute-functional-vec :
    (n : ) (v : Fin n  A) (t : Permutation n) (x : A) 
    in-functional-vec n x (v  map-equiv t)  in-functional-vec n x v
  is-in-functional-vec-is-in-permute-functional-vec n v t x (k , refl) =
    map-equiv t k , refl

  is-in-vec-is-in-permute-vec :
    (n : ) (v : vec A n) (t : Permutation n) (x : A) 
    x ∈-vec (permute-vec n v t)  x ∈-vec v
  is-in-vec-is-in-permute-vec n v t x I =
    is-in-vec-is-in-functional-vec
      ( n)
      ( v)
      ( x)
      ( is-in-functional-vec-is-in-permute-functional-vec
        ( n)
        ( functional-vec-vec n v)
        ( t)
        ( x)
        ( tr
          ( λ p  in-functional-vec n x p)
          ( isretr-functional-vec-vec n (functional-vec-vec n v  map-equiv t))
          ( is-in-functional-vec-is-in-vec n (permute-vec n v t) x I)))

  is-in-permute-functional-vec-is-in-functional-vec :
    (n : ) (v : Fin n  A) (t : Permutation n) (x : A) 
    in-functional-vec n x v  in-functional-vec n x (v  map-equiv t)
  is-in-permute-functional-vec-is-in-functional-vec n v t x (k , refl) =
    map-inv-equiv t k , ap v (inv (issec-map-inv-equiv t k))

  is-in-permute-vec-is-in-vec :
    (n : ) (v : vec A n) (t : Permutation n) (x : A) 
    x ∈-vec v  x ∈-vec (permute-vec n v t)
  is-in-permute-vec-is-in-vec n v t x I =
    is-in-vec-is-in-functional-vec
      ( n)
      ( permute-vec n v t)
      ( x)
      ( tr
        ( λ p  in-functional-vec n x p)
        ( inv
          ( isretr-functional-vec-vec n (functional-vec-vec n v  map-equiv t)))
        ( is-in-permute-functional-vec-is-in-functional-vec
          ( n)
          ( functional-vec-vec n v)
          ( t)
          ( x)
          ( is-in-functional-vec-is-in-vec n v x I)))

If μ : A → (B → B) satisfies a commutativity property, then fold-vec b μ is invariant under permutation for every b : B

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (μ : A  (B  B))
  where

  commutative-fold-vec : UU (l1  l2)
  commutative-fold-vec = (a1 a2 : A) (b : B)  μ a1 (μ a2 b)  μ a2 (μ a1 b)

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  (b : B)
  (μ : A  (B  B))
  (C : commutative-fold-vec μ)
  where

  invariant-swap-two-last-elements-transposition-fold-vec :
    {n : }  (v : vec A (succ-ℕ (succ-ℕ n))) 
    fold-vec b μ v 
    fold-vec
      ( b)
      ( μ)
      ( permute-vec (succ-ℕ (succ-ℕ n))
      ( v)
      ( swap-two-last-elements-transposition-Fin n))
  invariant-swap-two-last-elements-transposition-fold-vec {n} (y  z  v) =
    C y z (fold-vec b μ v) 
    inv
      ( ap
        ( fold-vec b μ)
        ( compute-swap-two-last-elements-transposition-Fin-permute-vec
          ( n)
          ( v)
          ( y)
          ( z)))

  invariant-adjacent-transposition-fold-vec :
    {n : }  (v : vec A (succ-ℕ n))  (k : Fin n) 
    fold-vec b μ v 
    fold-vec b μ (permute-vec (succ-ℕ n) v (adjacent-transposition-Fin n k))
  invariant-adjacent-transposition-fold-vec {succ-ℕ n} (x  v) (inl k) =
     ap
       ( μ x)
       ( invariant-adjacent-transposition-fold-vec v k) 
     inv
       ( ap
         ( fold-vec b μ)
         ( compute-equiv-coprod-permutation-id-equiv-permute-vec
           ( succ-ℕ n)
           ( v)
           ( x)
           ( adjacent-transposition-Fin n k)))
  invariant-adjacent-transposition-fold-vec {succ-ℕ n} (x  v) (inr _) =
    invariant-swap-two-last-elements-transposition-fold-vec (x  v)

  invariant-list-adjacent-transpositions-fold-vec :
    {n : } (v : vec A (succ-ℕ n)) (l : list (Fin n)) 
    fold-vec b μ v 
    fold-vec
      ( b)
      ( μ)
      ( permute-vec
        ( succ-ℕ n)
        ( v)
        ( permutation-list-adjacent-transpositions n l))
  invariant-list-adjacent-transpositions-fold-vec {n} v nil =
    ap (fold-vec b μ) (inv (compute-permute-vec-id-equiv (succ-ℕ n) v))
  invariant-list-adjacent-transpositions-fold-vec {n} v (cons x l) =
    ( invariant-adjacent-transposition-fold-vec v x 
      ( ( invariant-list-adjacent-transpositions-fold-vec
          ( permute-vec (succ-ℕ n) v (adjacent-transposition-Fin n x))
          ( l)) 
        ( ap
          ( fold-vec b μ)
          ( inv
            ( compute-composition-permute-vec
              ( succ-ℕ n)
              ( v)
              ( adjacent-transposition-Fin n x)
              ( permutation-list-adjacent-transpositions n l))))))

  invariant-transposition-fold-vec :
    {n : } (v : vec A (succ-ℕ n)) (i j : Fin (succ-ℕ n)) (neq : ¬ (i  j)) 
    fold-vec b μ v 
    fold-vec
      ( b)
      ( μ)
      ( permute-vec (succ-ℕ n) v (transposition-Fin (succ-ℕ n) i j neq))
  invariant-transposition-fold-vec {n} v i j neq =
    ( ( invariant-list-adjacent-transpositions-fold-vec
        ( v)
        ( list-adjacent-transpositions-transposition-Fin n i j))
      ( ap
        ( λ t  fold-vec b μ (permute-vec (succ-ℕ n) v t))
        ( eq-htpy-equiv
          {e = permutation-list-adjacent-transpositions
                 ( n)
                 ( list-adjacent-transpositions-transposition-Fin n i j)}
          {e' = transposition-Fin (succ-ℕ n) i j neq}
          ( htpy-permutation-list-adjacent-transpositions-transposition-Fin
            ( n)
            ( i)
            ( j)
            ( neq)))))

  invariant-list-transpositions-fold-vec :
    {n : }
    (v : vec A n)
    (l : list (Σ (Fin n × Fin n)
                 ( λ (i , j)  ¬ (i  j)))) 
    fold-vec b μ v 
    fold-vec
      ( b)
      ( μ)
      ( permute-vec
        ( n)
        ( v)
        ( permutation-list-standard-transpositions-Fin n l))
  invariant-list-transpositions-fold-vec {n} v nil =
    ap
      ( fold-vec b μ)
      ( inv ( compute-permute-vec-id-equiv n v))
  invariant-list-transpositions-fold-vec {0} v (cons _ _) = refl
  invariant-list-transpositions-fold-vec {succ-ℕ n} v (cons ((i , j) , neq) l) =
    ( invariant-transposition-fold-vec v i j neq 
      ( ( invariant-list-transpositions-fold-vec
          ( permute-vec (succ-ℕ n) v (transposition-Fin (succ-ℕ n) i j neq))
          ( l)) 
        ( ap
          ( fold-vec b μ)
          ( inv
            ( compute-composition-permute-vec
              ( succ-ℕ n)
              ( v)
              ( transposition-Fin (succ-ℕ n) i j neq)
              ( permutation-list-standard-transpositions-Fin (succ-ℕ n) l))))))

  invariant-permutation-fold-vec :
    {n : }  (v : vec A n)  (f : Permutation n) 
    fold-vec b μ v  fold-vec b μ (permute-vec n v f)
  invariant-permutation-fold-vec {n} v f =
    ( ( invariant-list-transpositions-fold-vec
        ( v)
        ( list-standard-transpositions-permutation-Fin n f)) 
      ( ap
        ( λ f  fold-vec b μ (permute-vec n v f))
        ( eq-htpy-equiv
          {e =
            permutation-list-standard-transpositions-Fin
              ( n)
              ( list-standard-transpositions-permutation-Fin n f)}
          {e' = f}
          ( retr-permutation-list-standard-transpositions-Fin n f))))

map-vec of the permutation of a vector

eq-map-vec-permute-vec :
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  (f : A  B) {n : } (v : vec A n) (t : Permutation n) 
  permute-vec n (map-vec f v) t 
  map-vec f (permute-vec n v t)
eq-map-vec-permute-vec f {n} v t =
  ( ( ap
      ( λ w 
        ( listed-vec-functional-vec
          ( n)
          ( functional-vec-vec n w  (map-equiv t)))))
      ( inv (map-vec-map-functional-vec f n v)) 
    ( ( ap
        ( λ p 
          listed-vec-functional-vec
            ( n)
            ( p  map-equiv t))
        ( isretr-functional-vec-vec
          ( n)
          ( map-functional-vec n f (functional-vec-vec n v)))) 
      ( ( ap
          ( listed-vec-functional-vec n  map-functional-vec n f)
          ( inv
            ( isretr-functional-vec-vec
              ( n)
              ( λ z  functional-vec-vec n v (map-equiv t z))))) 
        ( map-vec-map-functional-vec f n (permute-vec n v t)))))