The Weyl denominator identity

Given: The Axiom of Choice, the finite root system with positive system ${\mathrm{\Phi }}^{+}$, Weyl group $W$, length $\mathrm{\ell }$ and Weyl vector $\rho$, the completed character ring $\mathcal{R}$, and the alternants $A(\nu )$.

The Axiom of Choice is assumed; it enters through the BGG Euler identity of [F1] and the classification of [F2] (The Axiom of Choice).

For every $\lambda \in {\mathrm{\Lambda }}^{+}$ the BGG Euler identity gives $\mathrm{ch}L(\lambda )={\sum }_{w\in W}(-1{)}^{\mathrm{\ell }(w)}{e}^{w\circ \lambda }{\prod }_{\alpha \in {\mathrm{\Phi }}^{+}}(1-e^{-\alpha }{)}^{-1}$ in $\mathcal{R}$, where the dot action is $w\circ \lambda =w(\lambda +\rho )-\rho$; in particular $w\circ 0=w\rho -\rho$ (The Euler-character identity for a finite-dimensional simple module, The Grothendieck group and character of O).

$L(0)$ is the trivial one-dimensional module: the module $\mathbb{C}$ with zero action is finite-dimensional, irreducible and of highest weight $0$, so by the classification it is $L(0)$, and $\mathrm{ch}\mathbb{C}=e^0=1$ (Highest-weight classification, The highest-weight space is one-dimensional, Representations of Lie algebras, The formal character of a finite-dimensional weight module).

The product $e^{\rho }{\prod }_{\alpha \in {\mathrm{\Phi }}^{+}}(1-e^{-\alpha })$ is invertible in $\mathcal{R}$, with inverse $e^{-\rho }{\prod }_{\alpha \in {\mathrm{\Phi }}^{+}}(1-e^{-\alpha }{)}^{-1}$ (Geometric series are invertible in the completed character ring).

$\rho \in P$: the pairings $⟨\rho ,{\beta }^{\vee }⟩$ are positive integers for every positive root $\beta$ (Positive coroot pairings of a dominant integral weight, Integral, dominant, and strictly dominant weights), and $W$ preserves the weight lattice $P$, so every $w\rho$ and every exponent $\rho -{\sum }_{\alpha \in S}\alpha$ occurring in the expansion of the finite product lies in $P$ (Finite Weyl positive roots and simple reflections, Finite Weyl root system, lattice and chamber conventions).

$A(\rho )={\sum }_{w\in W}(-1{)}^{\mathrm{\ell }(w)}{e}^{w\rho }$ is the finite alternant of The Weyl alternation operator, and monomials satisfy $e^{\mu }{e}^{\nu }=e^{\mu +\nu }$, so $e^{\alpha \mathrm{/}2}-e^{-\alpha \mathrm{/}2}=e^{-\alpha \mathrm{/}2}(e^{\alpha }-1)$ and ${\prod }_{\alpha \in {\mathrm{\Phi }}^{+}}{e}^{\pm \alpha \mathrm{/}2}=e^{\pm \rho }$ in $\mathcal{R}$ (The completed formal character ring).