Sorting signs under a permutation of positions

Reordering a duplicate-free tuple multiplies the sorting sign of the list it spells by the sign of the reordering. The proof reduces to adjacent transpositions, where the two lists differ by one swap and the sorting signs by one factor of −1.

Splitting List.ofFn v at two adjacent positions

ofFn (v ∘ adjTrans i) is the swapped split

The swap step

The word lemma: induction on an adjacent-transposition word

Sign of adjacent transposition words

Main theorem

theorem RS.sortSign_ofFn_comp_perm {α : Type} [LinearOrder α] {n : ℕ} (v : Fin n → α) (hinj : Function.Injective v) (τ : Equiv.Perm (Fin n)) : sortSign (List.ofFn fun (i : Fin n) => v (τ i)) = ↑(Equiv.Perm.sign τ) * sortSign (List.ofFn v)

Permuting a duplicate-free tuple multiplies its sorting sign by the permutation's sign.