Cherednik costandards have orthogonality and the standard character

Write $H=H_{1,c}$, $X=S({\mathfrak{h}}^{\ast })$, $Y=S(\mathfrak{h})$, $D=X⋊\mathbb{C}W$, and $\mathrm{\Sigma }=\{a_F:F\in \mathrm{Irr}W\}$. Regard $E$ as a $D$-module with positive-degree $X$ acting by zero. The full coinduced module is $N(E)={\mathrm{Hom}}_D(H,E)$, with $(hf)(u)=f(uh)$. PBW identifies it with the product over $d\ge 0$ of ${\mathrm{Hom}}_{\mathbb{C}}(S^d\mathfrak{h},E)$. On the degree-$d$ piece, $\mathrm{e}\mathrm{u}$ acts by $a_E+d$: for $u\in S^d\mathfrak{h}$, one has $u\mathrm{e}\mathrm{u}=(\mathrm{e}\mathrm{u}+d)u$; evaluating a $D$-linear map kills the left $x_i$ in ${\sum }_i{x}_i{y}_i$ and evaluates the central $z$ on $E$ as $a_E$. These eigenvalues are distinct as $d$ varies. Therefore the Euler-locally-finite part is exactly their direct sum, denoted $\mathrm{\nabla }(E)$. It is $H$-stable: $y$ lowers degree, $x$ raises degree, and $W$ preserves degree. In particular $Y$ acts locally nilpotently. Its Euler-graded $W$-space in degree $a_E+d$ is ${\mathrm{Hom}}_{\mathbb{C}}(S^d\mathfrak{h},E)\cong S^d({\mathfrak{h}}^{\ast })\otimes E$, exactly that of $\mathrm{\Delta }(E)$.

We prove finite generation of $\mathrm{\nabla }(E)$. Any nonzero module with locally nilpotent $Y$ and locally finite Euler action has a singular irreducible $W$-submodule: start with a finite $Y$-orbit, take the common kernel of the commuting nilpotents, and then an irreducible $W$-submodule of its singular space by finite-group averaging. Its Euler scalar lies in $\mathrm{\Sigma }$. Consequently $d(M)={\sum }_{\beta \in \mathrm{\Sigma }}\dim M[\beta ]$ is positive on every nonzero subquotient with finite weight spaces, and is additive in exact sequences; generalized Euler spaces are exact by taking the appropriate finite eigencomponent of a preimage. This integer is finite for $\mathrm{\nabla }(E)$ by step 1.1. Thus every strict chain of its submodules has length at most $d(\mathrm{\nabla }(E))$; taking maximal or minimal proper submodules and iterating gives a finite composition series. Every simple subquotient is generated by a singular irreducible $W$-module, so is a quotient of some standard and belongs to ${\mathcal{O}}_c$. An extension of finite $X$-modules is finite: lift finitely many quotient generators and add finitely many submodule generators. Induction along this composition series proves that $\mathrm{\nabla }(E)$ is finite over $X$, so it belongs to ${\mathcal{O}}_c$.

The arbitrary-algebra coinduction adjunction is explicit: maps $M\to {\mathrm{Hom}}_D(H,F)$ correspond by evaluation at $1$ to $D$-maps $M\to F$, with inverse $m\mapsto (u\mapsto f(um))$. Compute Ext using the finite Koszul resolution $P_i=H{\otimes }_{\mathbb{C}W}({\mathrm{\Lambda }}^i\mathfrak{h}\otimes E)$, augmented onto $\mathrm{\Delta }(E)$, with differential $u\otimes (y_1\wedge \cdots \wedge y_i\otimes e)\mapsto {\sum }_j(-1{)}^{j-1}u{y}_j\otimes (y_1\wedge \cdots {\widehat{y}}_j\cdots \wedge y_i\otimes e)$. The commuting $y_j$ give differential square zero, and the formula is $W$-equivariant, so it is well-defined. Each ${\mathrm{\Lambda }}^i\mathfrak{h}\otimes E$ is a summand of a finite free $\mathbb{C}W$-module by averaging, so $P_i$ is a finite projective $H$-module. PBW identifies its restriction to $D$ with $D{\otimes }_{\mathbb{C}W}(Y\otimes {\mathrm{\Lambda }}^i\mathfrak{h}\otimes E)$, whose differential is the ordinary polynomial Koszul operator $d={\sum }_j{y}_j{\iota }_j$. On polynomial degree $p$ and exterior degree $i$ with $p+i>0$, the operator $h=({\sum }_j{\epsilon }_j{\mathrm{\partial }}_{y_j})\mathrm{/}(p+i)$ satisfies $dh+hd=1$, by the identities between exterior multiplication ${\epsilon }_j$ and contraction ${\iota }_j$. It is $W$-equivariant and extends $D$-linearly. In total degree zero, augmentation projects to $D{\otimes }_{\mathbb{C}W}E={\mathrm{Res}}_D\mathrm{\Delta }(E)$. Thus this augmented restricted complex is explicitly contractible, proving exactness of the finite $H$-projective resolution. Adjunction identifies its Hom complex into $N(F)$ with this $D$-Hom complex into $F$, so ${\mathrm{Hom}}_H(\mathrm{\Delta }(E),N(F))={\mathrm{Hom}}_W(E,F)={\delta }_{EF}\mathbb{C}$ and ${\mathrm{Ext}}_H^1(\mathrm{\Delta }(E),N(F))=0$. No infinite free module or arbitrary choice principle is used. Any map from an Euler-locally-finite module into $N(F)$ lands in $\mathrm{\nabla }(F)$ by step 1.1. For an extension $0\to \mathrm{\nabla }(F)\to U\to \mathrm{\Delta }(E)\to 0$ in ${\mathcal{O}}_c$, push out to $N(F)$. The vanishing gives a retraction $U\to N(F)$ extending the inclusion of $\mathrm{\nabla }(F)$; its image is Euler-locally-finite and hence lies in $\mathrm{\nabla }(F)$. This splits the original extension and proves the stated orthogonality in ${\mathcal{O}}_c$.

A simple submodule $L(F)$ of $\mathrm{\nabla }(E)$ gives a nonzero map $\mathrm{\Delta }(F)\to \mathrm{\nabla }(E)$, forcing $F=E$ by step 3.1. Finite length ensures a nonzero socle, and its multiplicity is at most $\dim \mathrm{Hom}(\mathrm{\Delta }(E),\mathrm{\nabla }(E))=1$. Thus its socle is $L(E)$ once. This argument uses neither a real reflection group nor a simple-preserving duality.

Euler-graded $W$-classes are additive on exact sequences, and step 1.1 gives identical such characters for $\mathrm{\Delta }(E)$ and $\mathrm{\nabla }(E)$. The simple characters are linearly independent: in a finite nonzero integral relation choose a label $F$ of minimal $\mathrm{Re}(a_F)$ among the nonzero coefficients. At Euler weight $a_F$, labels with larger real part cannot contribute, labels with the same real part but a different imaginary part have no such weight, and the remaining lowest spaces are the distinct irreducible $W$-modules. Their classes are independent because averaging splits finite $W$-modules into their irreducibles. Thus the coefficient of each such lowest label must be zero, a contradiction. It follows that $[\mathrm{\nabla }(E):L(F)]=[\mathrm{\Delta }(E):L(F)]$ for every $F$, and hence $[\mathrm{\nabla }(E)]=[\mathrm{\Delta }(E)]$ in $K_0({\mathcal{O}}_c)$. This asserts equality of composition multiplicities, not an isomorphism of these modules.