Permutation descents, Eulerian numbers, and the cd-index
A Rocq / MathComp formalization of Stanley EC1 §1.4 + §1.6

6.3 Inversions

Definition 6.7 Inversion at a pair
#

Position pair \((i, j)\) is an inversion of \(\sigma \) when \(i {\lt} j\) but \(\sigma (j) {\lt} \sigma (i)\) — i.e., the pair appears in the “wrong” order.

Definition 6.8 Inversion set and count
#

\(\mathrm{inv\_ set}(\sigma )\) is the set of inversion pairs; \(\mathrm{inv}(\sigma ) = |\mathrm{inv\_ set}(\sigma )|\) is their count. Stanley writes \(\mathrm{inv}(w)\).

Lemma 6.9 Identity has no inversions

\(\mathrm{inv}(\mathrm{id}) = 0\).

Lemma 6.10 Triangular counting

\(\# \{ (i, j) \in \{ 0, \dots , m-1\} ^2 : i {\lt} j\} = \binom {m}{2}\).

Lemma 6.11 Inversion bound

\(\mathrm{inv}(\sigma ) \leq \binom {n+1}{2}\). The maximum is achieved by the order-reversing permutation, which has every pair inverted.

Theorem 6.12 Inversion reversal symmetry

Let \(\rev _n \in \mathfrak {S}_{n+1}\) be the order-reversing permutation. Then

\[ \mathrm{inv}(\rev _n \cdot \sigma ) \; =\; \binom {n+1}{2} - \mathrm{inv}(\sigma ). \]

Each pair \((i, j)\) with \(i {\lt} j\) is either an inversion or a co-inversion of \(\sigma \) (exactly one), and the bijection \((i, j) \mapsto (\rev _n(j), \rev _n(i))\) swaps the two.