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