PBW basis of the universal affine vacuum module

Fix a finite ordered basis $e_1,\dots ,e_d$ of $\mathfrak{g}$ and the countable basis $e_{i,n}=e_i\otimes t^n$ of the loop modes, together with $K$. Fix a total order on this basis that places every mode with $n<0$ before every basis element of $\mathfrak{p}$; within each part use any fixed enumeration. For basis letters $b_j>b_i$, apply the defining rewrite $b_j{b}_i\mapsto b_i{b}_j+[b_j,b_i]$. Order words by length and then inversion number. The swapped word has one fewer inversion and every bracket term has smaller length; each bracket is a finite linear combination of basis letters. Thus every reduction tree is finitely branching and strictly decreases this well-founded pair, so it terminates in a finite linear combination of ordered words.

Reductions at disjoint adjacent pairs commute. The only overlapping reductions occur in a descending triple $xyz$ of basis letters with $x>y>z$. Reducing the left pair first and then swapping the remaining inversions gives $xyz⟶zyx+[y,z]x+y[x,z]+[x,y]z,$ whereas reducing the right pair first gives $xyz⟶zyx+z[x,y]+[x,z]y+x[y,z]\mathrm{.}$ Their difference is $([y,z]x-x[y,z])+(y[x,z]-[x,z]y)+([x,y]z-z[x,y])$. By bilinearity, the two-letter defining relations reduce these three differences respectively to $[[y,z],x]$, $[y,[x,z]]$, and $[[x,y],z]$; their sum is zero by Jacobi. Each bracket expands into finitely many basis letters, and every comparison term has smaller word length than the original triple. Induction on (length, inversion number) therefore joins every overlapping reduction, also inside any fixed left and right word context, so all reduction paths from each word agree.

The resulting linear normal-form map fixes every ordered word and sends each contextual relation $u(b_j{b}_i-b_i{b}_j-[b_j,b_i])v$ to zero, by the uniqueness in step 1.2. This checks all basis pairs: a reversed pair is the negative of its oriented relation by antisymmetry, and an equal pair has bracket zero. Bilinearity then gives the same for arbitrary $x,y\in \widehat{\mathfrak{g}}$, so the map kills the full two-sided ideal $I$ of [F2]. Conversely each reduction changes a word by an element of $I$. Hence ordered monomials span the quotient, and a linear combination of distinct ordered monomials in $I$ would be fixed by the normal-form map and also sent to zero; it must be zero. Ordered monomials are therefore a basis of $U(\widehat{\mathfrak{g}})$.

The negative-mode span ${\mathfrak{n}}_{-}:=\mathfrak{g}\otimes t^{-1}\mathbb{C}[t^{-1}]$ is a Lie subalgebra because sums of two negative indices stay negative and [F1] has no central term for them. The subalgebra $\mathfrak{p}=\mathfrak{g}[t]\oplus \mathbb{C}K$ is established in [F4]. With the order fixed in step 1.1, each PBW word is a negative-mode monomial followed by a $U(\mathfrak{p})$-monomial. Thus multiplication identifies $U({\mathfrak{n}}_{-})\otimes U(\mathfrak{p})$ with $U(\widehat{\mathfrak{g}})$ as a vector space and as a right $U(\mathfrak{p})$-module.

Tensor the right-module decomposition in step 3.1 over $U(\mathfrak{p})$ with ${\mathbb{C}}_k$. It identifies [F3] with $U({\mathfrak{n}}_{-})\otimes {\mathbb{C}}_k$; the negative-mode PBW monomials tensor the nonzero generator of ${\mathbb{C}}_k$ to a basis. The empty monomial is nonzero, proving the claimed basis and vacuum assertion.