The sign of a permutation of Fin n as the parity of its inversions

An inversion of σ : Equiv.Perm (Fin n) is a pair of indices i < j with σ j < σ i. The sign of σ is (-1) raised to the number of inversions. Mathlib exposes the sign as the product Equiv.Perm.sign_eq_prod_prod_Ioi; this file turns that product into the cardinality of the finite set of inversions, which is the form met by combinatorial permutation counts.

Main results

• TauCeti.sign_eq_neg_one_pow_card_inversion: the sign of a permutation of Fin n is (-1) to the number of its inversions.
• TauCeti.sign_finAddFlip_trans_finCongr: the block swap of Fin (m + n), which exchanges the first m indices with the last n, has sign (-1) ^ (m * n).

This result was first proved on the earlier Tau Ceti split branch at commit 05c2722248 and is adapted here to current main.

theorem TauCeti.sign_eq_neg_one_pow_card_inversion {n : ℕ} (σ : Equiv.Perm (Fin n)) : Equiv.Perm.sign σ = (-1) ^ {p : Fin n × Fin n | p.1 < p.2 ∧ σ p.2 < σ p.1}.card

The sign of a permutation of Fin n is (-1) raised to the number of its inversions, the pairs of columns i < j whose values are in the opposite order.

theorem TauCeti.sign_finAddFlip_trans_finCongr (m n : ℕ) : Equiv.Perm.sign (finAddFlip.trans (finCongr ⋯)) = (-1) ^ (m * n)

The block swap of Fin (m + n), exchanging the first m indices with the last n while preserving the order within each block, has sign (-1) ^ (m * n): its inversions are exactly the m * n pairs taken from different blocks.