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

1.1 Descents of a permutation

Definition 1.1 Descent and descent set
#

Let \(\sigma \in \mathfrak {S}_{n+1}\). Position \(i \in \{ 0, \dots , n-1\} \) is a descent of \(\sigma \) when \(\sigma (i+1) {\lt} \sigma (i)\). The descent set is

\[ D(\sigma ) = \{ i : \sigma (i+1) {\lt} \sigma (i) \} \subseteq \{ 0, \dots , n-1\} . \]
Definition 1.2 Descent and ascent counts
#

Set \(\operatorname {des}(\sigma ) = |D(\sigma )|\) and \(\operatorname {asc}(\sigma ) = n - \operatorname {des}(\sigma )\).

Lemma 1.3 Identity has no descents
#

\(\operatorname {des}(\mathrm{id}_{\mathfrak {S}_{n+1}}) = 0\).

Lemma 1.4 Reversal flips descents

Let \(\rev _n \in \mathfrak {S}_{n+1}\) be the order-reversing permutation \(i \mapsto n - i\). Position \(i\) is a descent of \(\sigma \) if and only if \(i\) is not a descent of \(\rev _n \cdot \sigma \), hence \(\operatorname {des}(\rev _n \cdot \sigma ) = n - \operatorname {des}(\sigma )\). In particular \(\operatorname {des}(\rev _n) = n\).