The PBW theorem for rational Cherednik algebras

Put all $x_i$ before every group symbol and all group symbols before all $y_j$, and order the $x_i$ and $y_j$ within their respective blocks by index. Use the defining relations as reductions: sort inverted pairs of $x$'s and of $y$'s; replace $wx$ by $w(x)w$; replace $yw$ by $w{w}^{-1}(y)$; replace $yx$ by $xy+\kappa (y,x)$; and multiply adjacent group symbols. Each vector in $w(x)$ or $w^{-1}(y)$ is expanded in the chosen finite bases. The irreducible words for these rules are precisely the displayed ordered monomials.

The reductions terminate. Use the lexicographic measure (i) number of vector letters, (ii) number of inversions of letter types for $x<\text{group}<y$, ignoring basis indices, (iii) number of group symbols, and (iv) sum of index inversions among the $x$ letters and among the $y$ letters. A correction term $\kappa (y,x)$ strictly decreases (i). The main mixed swap and each group crossing strictly decrease (ii), although expanding the group action may change (iv). Multiplication of adjacent group symbols cannot increase (ii) and, when it preserves (ii), decreases (iii); delete an identity group symbol by the same measure. A same-side sorting rule preserves (i)–(iii) and strictly decreases (iv). Every reduction therefore decreases a well-founded measure on finite words, so no infinite reduction sequence exists.

All overlapping reductions have the following forms. Overlaps among two adjacent group multiplications or group-crossing rules agree because the action of $W$ is an action and group multiplication is associative. Overlaps among same-side sorting rules agree because the $x$'s commute with one another and the $y$'s commute with one another. The forks $w{x}_j{x}_i$ and $y_j{y}_{i}w$ also join: a linear action preserves these commutativity relations, so applying the action before or after sorting gives the same symmetric product. A mixed group overlap $ywx$ agrees along its two reductions exactly by $W$-equivariance of $\kappa$ in [F2]. The only remaining overlaps are triples of vector letters, with two $y$'s and one $x$, or one $y$ and two $x$'s; the difference between reducing the two adjacent mixed pairs is the cyclic Jacobi expression from [F2], hence is zero. Reductions at disjoint pairs commute by substitution. Thus every one-step fork joins.

Termination from step 2.1 and the joining property from step 2.2 imply unique normal forms: by induction on the well-founded measure, if two first reductions differ, their join has smaller measure and therefore has the same normal form along both paths. Hence every word reduces uniquely to a linear combination of irreducible words. The reduction rules are consequences of [F1], so these words span the quotient. Conversely, the normal-form map annihilates each defining relation and all its left and right multiples; if a linear combination of irreducible words belonged to the defining ideal, its normal form would be both that combination and zero, so every coefficient would vanish. The irreducible words are therefore linearly independent in the quotient.

The irreducible words identified in step 1.1 are exactly $x_1^{a_1}\cdots x_n^{a_n}w{y}_1^{b_1}\cdots y_n^{b_n}$. Step 3.1 proves they form a basis. The tensor-product map in the Statement sends the tensor-product monomial basis to this basis, so it is an isomorphism. No restriction on $t$ or $c$ was used beyond the data definitions.