# Transpositions of standard finite types

Content created by Fredrik Bakke, Egbert Rijke, Victor Blanchi, Julian KG, fernabnor and louismntnu.

Created on 2023-05-03.

{-# OPTIONS --lossy-unification #-}

module finite-group-theory.transpositions-standard-finite-types 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 foundation.action-on-identifications-functions
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equivalence-extensionality
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-coproduct-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.negated-equality
open import foundation.negation
open import foundation.propositions
open import foundation.unit-type
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import lists.functoriality-lists
open import lists.lists

open import univalent-combinatorics.equality-standard-finite-types
open import univalent-combinatorics.standard-finite-types


## Idea

Given i and j in Fin n, the transposition associated to i and j swap these two elements.

## Definitions

### Transpositions on Fin n

This definition uses the standard-transposition in finite-group-theory.transposition.

module _
(n : ℕ) (i j : Fin n) (neq : i ≠ j)
where

transposition-Fin : Permutation n
transposition-Fin = standard-transposition (has-decidable-equality-Fin n) neq

map-transposition-Fin : Fin n → Fin n
map-transposition-Fin =
map-standard-transposition (has-decidable-equality-Fin n) neq

left-computation-transposition-Fin :
map-standard-transposition (has-decidable-equality-Fin n) neq i ＝ j
left-computation-transposition-Fin =
left-computation-standard-transposition (has-decidable-equality-Fin n) neq

right-computation-transposition-Fin :
map-standard-transposition (has-decidable-equality-Fin n) neq j ＝ i
right-computation-transposition-Fin =
right-computation-standard-transposition (has-decidable-equality-Fin n) neq

is-fixed-point-transposition-Fin :
(z : Fin n) →
i ≠ z →
j ≠ z →
map-standard-transposition (has-decidable-equality-Fin n) neq z ＝ z
is-fixed-point-transposition-Fin =
is-fixed-point-standard-transposition (has-decidable-equality-Fin n) neq


### The transposition that swaps the two last elements of Fin (succ-ℕ (succ-ℕ n))

We define directly the transposition of Fin (succ-ℕ (succ-ℕ n)) that exchanges the two elements associated to n and succ-ℕ n.

module _
(n : ℕ)
where

map-swap-two-last-elements-transposition-Fin :
Fin (succ-ℕ (succ-ℕ n)) → Fin (succ-ℕ (succ-ℕ n))
map-swap-two-last-elements-transposition-Fin (inl (inl x)) = inl (inl x)
map-swap-two-last-elements-transposition-Fin (inl (inr star)) = inr star
map-swap-two-last-elements-transposition-Fin (inr star) = inl (inr star)

is-involution-map-swap-two-last-elements-transposition-Fin :
( map-swap-two-last-elements-transposition-Fin ∘
map-swap-two-last-elements-transposition-Fin) ~
id
is-involution-map-swap-two-last-elements-transposition-Fin (inl (inl x)) =
refl
is-involution-map-swap-two-last-elements-transposition-Fin (inl (inr star)) =
refl
is-involution-map-swap-two-last-elements-transposition-Fin (inr star) = refl

swap-two-last-elements-transposition-Fin : Permutation (succ-ℕ (succ-ℕ n))
pr1 swap-two-last-elements-transposition-Fin =
map-swap-two-last-elements-transposition-Fin
pr2 swap-two-last-elements-transposition-Fin =
is-equiv-is-invertible
map-swap-two-last-elements-transposition-Fin
is-involution-map-swap-two-last-elements-transposition-Fin
is-involution-map-swap-two-last-elements-transposition-Fin


We show that this definiton is an instance of the previous one.

  cases-htpy-swap-two-last-elements-transposition-Fin :
(x : Fin (succ-ℕ (succ-ℕ n))) →
(x ＝ neg-one-Fin (succ-ℕ n)) + (x ≠ neg-one-Fin (succ-ℕ n)) →
(x ＝ neg-two-Fin (succ-ℕ n)) + (x ≠ neg-two-Fin (succ-ℕ n)) →
map-swap-two-last-elements-transposition-Fin x ＝
map-transposition-Fin
( succ-ℕ (succ-ℕ n))
( neg-two-Fin (succ-ℕ n))
( neg-one-Fin (succ-ℕ n))
( neq-inl-inr)
( x)
cases-htpy-swap-two-last-elements-transposition-Fin _ (inl refl) _ =
inv
( right-computation-transposition-Fin
( succ-ℕ (succ-ℕ n))
( neg-two-Fin (succ-ℕ n))
( neg-one-Fin (succ-ℕ n))
( neq-inl-inr))
cases-htpy-swap-two-last-elements-transposition-Fin _ (inr p) (inl refl) =
inv
( left-computation-transposition-Fin
( succ-ℕ (succ-ℕ n))
( neg-two-Fin (succ-ℕ n))
( neg-one-Fin (succ-ℕ n))
( neq-inl-inr))
cases-htpy-swap-two-last-elements-transposition-Fin
( inl (inl x))
( inr p)
( inr q) =
inv
( is-fixed-point-transposition-Fin
( succ-ℕ (succ-ℕ n))
( neg-two-Fin (succ-ℕ n))
( neg-one-Fin (succ-ℕ n))
( neq-inl-inr)
( inl (inl x))
( q ∘ inv)
( p ∘ inv))
cases-htpy-swap-two-last-elements-transposition-Fin
( inl (inr star))
( inr p)
( inr q) = ex-falso (q refl)
cases-htpy-swap-two-last-elements-transposition-Fin
( inr star)
( inr p)
( inr q) = ex-falso (p refl)

htpy-swap-two-last-elements-transposition-Fin :
htpy-equiv
( swap-two-last-elements-transposition-Fin)
( transposition-Fin
( succ-ℕ (succ-ℕ n))
( neg-two-Fin (succ-ℕ n))
( neg-one-Fin (succ-ℕ n))
( neq-inl-inr))
htpy-swap-two-last-elements-transposition-Fin x =
cases-htpy-swap-two-last-elements-transposition-Fin
( x)
( has-decidable-equality-Fin
( succ-ℕ (succ-ℕ n))
( x)
( neg-one-Fin (succ-ℕ n)))
( has-decidable-equality-Fin
( succ-ℕ (succ-ℕ n))
( x)
( neg-two-Fin (succ-ℕ n)))


### Transpositions of a pair of adjacent elements in Fin (succ-ℕ n)

#### Definition using swap-two-last-elements-transposition-Fin

adjacent-transposition-Fin :
(n : ℕ) → (k : Fin n) →
Permutation (succ-ℕ n)
adjacent-transposition-Fin (succ-ℕ n) (inl x) =
adjacent-transposition-Fin (succ-ℕ n) (inr x) =
swap-two-last-elements-transposition-Fin n

(n : ℕ) → (k : Fin n) →
(Fin (succ-ℕ n) → Fin (succ-ℕ n))


#### adjacent-transposition-Fin is an instance of the definiton transposition-Fin

cases-htpy-map-coproduct-map-transposition-id-Fin :
(n : ℕ) → (k l : Fin n) → (neq : k ≠ l) →
(x : Fin (succ-ℕ n)) →
(x ＝ inl-Fin n k) + (x ≠ inl-Fin n k) →
(x ＝ inl-Fin n l) + (x ≠ inl-Fin n l) →
map-coproduct (map-transposition-Fin n k l neq) id x ＝
map-transposition-Fin
( succ-ℕ n)
( inl-Fin n k)
( inl-Fin n l)
( neq ∘ is-injective-inl-Fin n)
( x)
cases-htpy-map-coproduct-map-transposition-id-Fin n k l neq x (inl refl) _ =
( ( ap
( inl-Fin n)
( left-computation-transposition-Fin n k l neq)) ∙
( inv
( left-computation-transposition-Fin
( succ-ℕ n)
( inl-Fin n k)
( inl-Fin n l)
( neq ∘ is-injective-inl-Fin n))))
cases-htpy-map-coproduct-map-transposition-id-Fin
( n)
( k)
( l)
( neq)
( x)
( inr _)
( inl refl) =
( ( ap
( inl-Fin n)
( right-computation-transposition-Fin n k l neq)) ∙
( inv
( right-computation-transposition-Fin
( succ-ℕ n)
( inl-Fin n k)
( inl-Fin n l)
( neq ∘ is-injective-inl-Fin n))))
cases-htpy-map-coproduct-map-transposition-id-Fin
( n)
( k)
( l)
( neq)
( inl x)
( inr neqk)
( inr neql) =
( ( ap
( inl-Fin n)
( is-fixed-point-transposition-Fin
( n)
( k)
( l)
( neq)
( x)
( neqk ∘ (inv ∘ ap (inl-Fin n)))
( neql ∘ (inv ∘ ap (inl-Fin n))))) ∙
( inv
( is-fixed-point-transposition-Fin
( succ-ℕ n)
( inl-Fin n k)
( inl-Fin n l)
( neq ∘ is-injective-inl-Fin n)
( inl x)
( neqk ∘ inv)
( neql ∘ inv))))
cases-htpy-map-coproduct-map-transposition-id-Fin
( n)
( k)
( l)
( neq)
( inr star)
( inr neqk)
( inr neql) =
inv
( is-fixed-point-transposition-Fin
( succ-ℕ n)
( inl-Fin n k)
( inl-Fin n l)
( neq ∘ is-injective-inl-Fin n)
( inr star)
( neqk ∘ inv)
( neql ∘ inv))

htpy-map-coproduct-map-transposition-id-Fin :
(n : ℕ) → (k l : Fin n) → (neq : k ≠ l) →
htpy-equiv
( equiv-coproduct (transposition-Fin n k l neq) id-equiv)
( transposition-Fin
( succ-ℕ n)
( inl-Fin n k)
( inl-Fin n l)
( neq ∘ is-injective-inl-Fin n))
htpy-map-coproduct-map-transposition-id-Fin n k l neq x =
cases-htpy-map-coproduct-map-transposition-id-Fin
( n)
( k)
( l)
( neq)
( x)
( has-decidable-equality-Fin (succ-ℕ n) x (inl-Fin n k))
( has-decidable-equality-Fin (succ-ℕ n) x (inl-Fin n l))

helper-htpy-same-transposition-Fin :
(n : ℕ) (k l : Fin n) (neq1 : k ≠ l) (neq2 : k ≠ l) →
(neq1 ＝ neq2) →
htpy-equiv
( transposition-Fin n k l neq1)
( transposition-Fin n k l neq2)
helper-htpy-same-transposition-Fin n k l neq1 .neq1 refl = refl-htpy

htpy-same-transposition-Fin :
{n : ℕ} {k l : Fin n} {neq1 : k ≠ l} {neq2 : k ≠ l} →
htpy-equiv
( transposition-Fin n k l neq1)
( transposition-Fin n k l neq2)
htpy-same-transposition-Fin {n} {k} {l} {neq1} {neq2} =
helper-htpy-same-transposition-Fin n k l neq1 neq2 (eq-is-prop is-prop-neg)

(n : ℕ) → (k : Fin n) →
htpy-equiv
( transposition-Fin
( succ-ℕ n)
( inl-Fin n k)
( inr-Fin n k)
( neq-inl-Fin-inr-Fin n k))
htpy-adjacent-transposition-Fin (succ-ℕ n) (inl x) =
( ( htpy-map-coproduct (htpy-adjacent-transposition-Fin n x) refl-htpy) ∙h
( ( htpy-map-coproduct-map-transposition-id-Fin
( succ-ℕ n)
( inl-Fin n x)
( inr-Fin n x)
( neq-inl-Fin-inr-Fin n x)) ∙h
( htpy-same-transposition-Fin)))
htpy-adjacent-transposition-Fin (succ-ℕ n) (inr star) =
htpy-swap-two-last-elements-transposition-Fin n


## Properties

### The transposition associated to i and j is homotopic to the one associated with j and i

cases-htpy-transposition-Fin-transposition-swap-Fin :
(n : ℕ) → (i j : Fin n) → (neq : i ≠ j) → (x : Fin n) →
(x ＝ i) + (x ≠ i) →
(x ＝ j) + (x ≠ j) →
map-transposition-Fin n i j neq x ＝
map-transposition-Fin n j i (neq ∘ inv) x
cases-htpy-transposition-Fin-transposition-swap-Fin
( n)
( i)
( j)
( neq)
( .i)
( inl refl) _ =
left-computation-transposition-Fin n i j neq ∙
inv (right-computation-transposition-Fin n j i (neq ∘ inv))
cases-htpy-transposition-Fin-transposition-swap-Fin
( n)
( i)
( j)
( neq)
( .j)
( inr _)
( inl refl) =
right-computation-transposition-Fin n i j neq ∙
inv (left-computation-transposition-Fin n j i (neq ∘ inv))
cases-htpy-transposition-Fin-transposition-swap-Fin
( n)
( i)
( j)
( neq)
( x)
( inr neqi)
( inr neqj) =
is-fixed-point-transposition-Fin
( n)
( i)
( j)
( neq)
( x)
( neqi ∘ inv)
( neqj ∘ inv) ∙
inv
(is-fixed-point-transposition-Fin
( n)
( j)
( i)
( neq ∘ inv)
( x)
( neqj ∘ inv)
( neqi ∘ inv))

htpy-transposition-Fin-transposition-swap-Fin :
(n : ℕ) → (i j : Fin n) → (neq : i ≠ j) →
htpy-equiv
( transposition-Fin n i j neq)
( transposition-Fin n j i (neq ∘ inv))
htpy-transposition-Fin-transposition-swap-Fin n i j neq x =
cases-htpy-transposition-Fin-transposition-swap-Fin
( n)
( i)
( j)
( neq)
( x)
( has-decidable-equality-Fin n x i)
( has-decidable-equality-Fin n x j)


### The conjugate of a transposition is also a transposition

htpy-conjugate-transposition-Fin :
(n : ℕ) (x y z : Fin n)
(neqxy : x ≠ y)
(neqyz : y ≠ z)
(neqxz : x ≠ z) →
htpy-equiv
( transposition-Fin n y z neqyz ∘e
( transposition-Fin n x y neqxy ∘e
transposition-Fin n y z neqyz))
( transposition-Fin n x z neqxz)
htpy-conjugate-transposition-Fin n x y z neqxy neqyz neqxz =
htpy-conjugate-transposition
( has-decidable-equality-Fin n)
( neqxy)
( neqyz)
( neqxz)

private
htpy-whisker-conjugate :
{l1 : Level} {A : UU l1} {f f' : A → A} (g : A → A) →
(f ~ f') → (f ∘ (g ∘ f)) ~ (f' ∘ (g ∘ f'))
htpy-whisker-conjugate {f = f} {f' = f'} g H x =
H (g ( f x)) ∙ ap (f' ∘ g) (H x)

htpy-conjugate-transposition-swap-two-last-elements-transposition-Fin :
(n : ℕ) (x : Fin (succ-ℕ n)) (neq : x ≠ neg-one-Fin n) →
htpy-equiv
( swap-two-last-elements-transposition-Fin n ∘e
( transposition-Fin
( succ-ℕ (succ-ℕ n))
( inl-Fin (succ-ℕ n) x)
( neg-two-Fin (succ-ℕ n))
( neq ∘ is-injective-inl-Fin (succ-ℕ n)) ∘e
swap-two-last-elements-transposition-Fin n))
( transposition-Fin
( succ-ℕ (succ-ℕ n))
( inl-Fin (succ-ℕ n) x)
( neg-one-Fin (succ-ℕ n))
( neq-inl-inr))
htpy-conjugate-transposition-swap-two-last-elements-transposition-Fin n x neq =
( ( htpy-whisker-conjugate
( map-transposition-Fin
( succ-ℕ (succ-ℕ n))
( inl-Fin (succ-ℕ n) x)
( neg-two-Fin (succ-ℕ n))
( neq ∘ is-injective-inl-Fin (succ-ℕ n)))
( htpy-swap-two-last-elements-transposition-Fin n)) ∙h
( ( htpy-conjugate-transposition-Fin
( succ-ℕ (succ-ℕ n))
( inl-Fin (succ-ℕ n) x)
( neg-two-Fin (succ-ℕ n))
( neg-one-Fin (succ-ℕ n))
( neq ∘ is-injective-inl-Fin (succ-ℕ n))
( neq-inl-inr)
( neq-inl-inr))))

htpy-conjugate-transposition-swap-two-last-elements-transposition-Fin' :
(n : ℕ) (x : Fin (succ-ℕ n)) (neq : x ≠ neg-one-Fin n) →
htpy-equiv
( swap-two-last-elements-transposition-Fin n ∘e
( transposition-Fin
( succ-ℕ (succ-ℕ n))
( neg-two-Fin (succ-ℕ n))
( inl-Fin (succ-ℕ n) x)
( neq ∘ (is-injective-inl-Fin (succ-ℕ n) ∘ inv)) ∘e
swap-two-last-elements-transposition-Fin n))
( transposition-Fin
( succ-ℕ (succ-ℕ n))
( neg-one-Fin (succ-ℕ n))
( inl-Fin (succ-ℕ n) x)
( neq-inr-inl))
htpy-conjugate-transposition-swap-two-last-elements-transposition-Fin' n x neq =
( ( double-whisker-comp
( map-swap-two-last-elements-transposition-Fin n)
( ( htpy-transposition-Fin-transposition-swap-Fin
( succ-ℕ (succ-ℕ n))
( neg-two-Fin (succ-ℕ n))
( inl-Fin (succ-ℕ n) x)
( neq ∘ (is-injective-inl-Fin (succ-ℕ n) ∘ inv))) ∙h
htpy-same-transposition-Fin)
( map-swap-two-last-elements-transposition-Fin n)) ∙h
( ( htpy-conjugate-transposition-swap-two-last-elements-transposition-Fin
( n)
( x)
( neq) ∙h
( ( htpy-transposition-Fin-transposition-swap-Fin
( succ-ℕ (succ-ℕ n))
( inl-Fin (succ-ℕ n) x)
( neg-one-Fin (succ-ℕ n))
( neq-inl-inr)) ∙h
htpy-same-transposition-Fin))))


### Every transposition is the composition of a list of adjacent transpositions

list-adjacent-transpositions-transposition-Fin :
(n : ℕ) → (i j : Fin (succ-ℕ n)) →
list (Fin n)
list-adjacent-transpositions-transposition-Fin n (inr _) (inr _) = nil
list-adjacent-transpositions-transposition-Fin 0 (inl _) (inr _) = nil
list-adjacent-transpositions-transposition-Fin 0 (inl _) (inl _) = nil
list-adjacent-transpositions-transposition-Fin 0 (inr _) (inl _) = nil
( succ-ℕ n)
( inl i)
( inl j) =
map-list (inl-Fin n) (list-adjacent-transpositions-transposition-Fin n i j)
( succ-ℕ n)
( inl (inr star))
( inr star) = cons (inr star) nil
( succ-ℕ n)
( inl (inl i))
( inr star) =
snoc
( cons
( inr star)
( map-list
( inl-Fin n)
( list-adjacent-transpositions-transposition-Fin n (inl i) (inr star))))
( inr star)
( succ-ℕ n)
( inr star)
( inl (inl j)) =
snoc
( cons
( inr star)
( map-list
( inl-Fin n)
( list-adjacent-transpositions-transposition-Fin n (inr star) (inl j))))
( inr star)
( succ-ℕ n)
( inr star)
( inl (inr star)) = cons (inr star) nil

(n : ℕ) → list (Fin n) → Permutation (succ-ℕ n)
permutation-list-adjacent-transpositions n (cons x l) =

(n : ℕ) → list (Fin n) → Fin (succ-ℕ n) → Fin (succ-ℕ n)

(n : ℕ) → (l : list (Fin n)) →
htpy-equiv
( succ-ℕ n)
( map-list (inl-Fin n) l))
( equiv-coproduct
( id-equiv))
inv-htpy (id-map-coproduct (Fin (succ-ℕ n)) unit)
htpy-permutation-inl-list-adjacent-transpositions n (cons x l) =
( map-coproduct (map-adjacent-transposition-Fin n x) id ·l
( inv-htpy
( preserves-comp-map-coproduct
( id)
( id)))

(n : ℕ) (l : list (Fin n)) (x : Fin n) →
htpy-equiv
( permutation-list-adjacent-transpositions n (snoc l x))
htpy-permutation-snoc-list-adjacent-transpositions n nil x = refl-htpy
htpy-permutation-snoc-list-adjacent-transpositions n (cons y l) x =

(n : ℕ) (i j : Fin (succ-ℕ n)) (neq : i ≠ j) →
htpy-equiv
( n)
( transposition-Fin (succ-ℕ n) i j neq)
( 0)
( inr star)
( inr star)
( neq) = ex-falso (neq refl)
( succ-ℕ n)
( inl i)
( inl j)
( neq) =
( n)
( list-adjacent-transpositions-transposition-Fin n i j)) ∙h
( ( htpy-map-coproduct
( n)
( i)
( j)
( neq ∘ (ap (inl-Fin (succ-ℕ n)))))
( refl-htpy)) ∙h
( ( htpy-map-coproduct-map-transposition-id-Fin
( succ-ℕ n)
( i)
( j)
( neq ∘ ap (inl-Fin (succ-ℕ n)))) ∙h
( htpy-same-transposition-Fin))))
( succ-ℕ n)
( inl (inl i))
( inr star)
( neq) =
( ( map-swap-two-last-elements-transposition-Fin n ·l
( succ-ℕ n)
( map-list
( inl-Fin n)
( n)
( inl i)
( inr star)))
( inr star)) ∙h
( ( double-whisker-comp
( map-swap-two-last-elements-transposition-Fin n)
( n)
( n)
( inl i)
( inr star))) ∙h
( htpy-map-coproduct
( n)
( inl i)
( inr star)
( neq-inl-inr))
( refl-htpy) ∙h
htpy-map-coproduct-map-transposition-id-Fin
( succ-ℕ n)
( inl i)
( inr star)
( neq-inl-inr)))
( map-swap-two-last-elements-transposition-Fin n)) ∙h
( htpy-conjugate-transposition-swap-two-last-elements-transposition-Fin
( n)
( inl i)
( neq-inl-inr) ∙h
htpy-same-transposition-Fin)))
( succ-ℕ n)
( inl (inr star))
( inr star)
( neq) =
htpy-swap-two-last-elements-transposition-Fin n ∙h
htpy-same-transposition-Fin
( succ-ℕ n)
( inr star)
( inl (inl j))
( neq) =
( ( map-swap-two-last-elements-transposition-Fin n ·l
( succ-ℕ n)
( map-list
( inl-Fin n)
( n)
( inr star)
( inl j)))
( inr star)) ∙h
( ( double-whisker-comp
( map-swap-two-last-elements-transposition-Fin n)
( n)
( n)
( inr star)
( inl j))) ∙h
( ( htpy-map-coproduct
( n)
( inr star)
( inl j)
( neq-inr-inl))
( refl-htpy)) ∙h
( ( htpy-map-coproduct-map-transposition-id-Fin
( succ-ℕ n)
( inr star)
( inl j)
( neq-inr-inl)) ∙h
( htpy-same-transposition-Fin))))
( map-swap-two-last-elements-transposition-Fin n)) ∙h
( ( htpy-conjugate-transposition-swap-two-last-elements-transposition-Fin'
( n)
( inl j)
( neq-inl-inr)) ∙h
htpy-same-transposition-Fin)))
( succ-ℕ n)
( inr star)
( inl (inr star))
( neq) =
htpy-swap-two-last-elements-transposition-Fin n ∙h
( ( htpy-transposition-Fin-transposition-swap-Fin
( succ-ℕ (succ-ℕ n))
( neg-two-Fin (succ-ℕ n))
( neg-one-Fin (succ-ℕ n))
( neq-inl-inr)) ∙h
htpy-same-transposition-Fin)