6.5 Foata’s first fundamental bijection and MacMahon’s equidistribution
Foata’s first fundamental bijection \(\varphi : \mathfrak {S}_{n+1} \to \mathfrak {S}_{n+1}\) is defined recursively on the seq representation: read \(w = w_1 w_2 \dots w_{n+1}\) left-to-right and at each step splice the new letter into a current word via a cyclic-rotation rule on maximal blocks. Implemented as seq_to_perm \(\circ \) foata \(\circ \) perm_to_seq.
For every \(\sigma \in \mathfrak {S}_{n+1}\),
This is the load-bearing identity of the bijection. It is proved via the seq-level invariant foata_inv_eq_maj: \(\mathrm{inv\_ seq}(\mathrm{foata}(w)) = \mathrm{maj\_ seq}(w)\), which in turn is proved by reverse induction on \(w\) using the per-step invariant foata_step_inv (a tally of cyclic-rotation effects on the inversion count).
\(\varphi \) is injective (hence bijective on the finite group \(\mathfrak {S}_{n+1}\)). Proof: explicit construction of the inverse \(\varphi ^{-1}\) on seqs (cuts at \(P\)-elements rather than after them, undoing the cyclic rotation block-wise) plus a cancellation lemma \(\varphi ^{-1}(\varphi (w)) = w\).
Stanley EC1 Theorem 1.3.4 (MacMahon). For every \(n, k \in \mathbb {N}\),
The proof is a direct consequence of 6.18 and 6.19: \(\varphi \) is a bijection of \(\mathfrak {S}_{n+1}\) that maps \(\{ \sigma : \mathrm{maj}(\sigma ) = k\} \) onto \(\{ \sigma : \mathrm{inv}(\sigma ) = k\} \) for every \(k\). The closed form for both distributions is the \(q\)-factorial (6.22 and 6.23).