Contragredient construction preserves generalized VOA modules

In the single-module clause all hypotheses of F1 are exactly those in the Statement and Grading-restricted generalized module. The formula in F3 is the formula proved in F1. Thus F1 supplies lower truncation, vacuum, module Jacobi and the grading-restricted generalized-weight decomposition, without an additional unproved formal-adjoint input. This proves the single-module clause.

Fix a component j and a tuple $\beta$ of eigenvalues for all components other than j. Let $M^{j,\beta }={⨁}_{h\in \mathbb{C}}{M}_{[(\beta ,h{)}_j]}$, where $(\beta ,h{)}_j$ denotes the joint tuple with h in position j. Every mode of the jth action commutes with $L_i(0)$ for $i\mathrm{\ne }j$, hence preserves their generalized eigenspaces and this subspace. The restriction is a V-module, since its truncation, vacuum and Jacobi identities restrict from the jth component action. Its generalized $L_j(0)$-eigenspace at h is exactly $M_{[(\beta ,h{)}_j]}$: on any other generalized eigenspace the operator $L_j(0)-h$ is invertible, and each vector has finite support. F2 gives finite-dimensionality of this block and the lower bound $B_j$. Thus $M^{j,\beta }$ is an actual grading-restricted generalized V-module even when M is not grading restricted for the sum ${\sum }_i{L}_i(0)$.

Apply F1 to every fibre in step 1.2. For fixed j the joint restricted dual has the algebraic identification $M^{\mathrm{\prime }}={⨁}_{\beta }(M^{j,\beta }{)}^{\mathrm{\prime }}$, since both sides consist of finite sums of functionals on the same joint blocks. The fibre contragredient action is exactly F3's jth formula and preserves the other dual labels $\beta$. Therefore it defines a component action on M'. For any vector of M', only finitely many fibres and weight blocks occur; taking the maximum of their truncation bounds proves lower truncation on that vector. Vacuum and Jacobi hold on each fibre, hence on their algebraic direct sum.

For distinct components i and j, all original component modes commute. Each opposite mode is a finite sum of modes of that same component, because the state-side exponential is finite. The opposite modes of distinct components therefore commute, and their transposes commute too: pairing their commutator against any m gives the negative of the original opposite-mode commutator, zero. Hence the dual component actions commute. On the finite joint block $M_{[\lambda ]}^{\ast }$ each dual $L_j(0)$ is the transpose of the original $L_j(0)$, so $L_j(0)-{\lambda }_j$ remains nilpotent there. Finite-dimensionality, finite support and every coordinate lower bound are unchanged, and the displayed direct sum is its joint generalized-weight decomposition. These are precisely F2's component-module axioms for $V^{\otimes k}$, proving the full tensor-component clause.

For a module map $f:M\to N$, commutation with the component conformal fields implies that f preserves joint generalized weights. Its restricted transpose $f^{\mathrm{\prime }}:N^{\mathrm{\prime }}\to M^{\mathrm{\prime }}$ is therefore defined. Pairing with m gives $⟨f^{\mathrm{\prime }}{Y}_{N^{\mathrm{\prime }}}(u,z)\nu ,m⟩=⟨\nu ,Y_N^o(u,z)f(m)⟩=⟨\nu ,f{Y}_M^o(u,z)m⟩=⟨Y_{M^{\mathrm{\prime }}}(u,z)f^{\mathrm{\prime }}(\nu ),m⟩$, component by component. The middle equality uses only f commuting with the original modes and their finite opposite-state combinations. The separating restricted pairings prove that f' is a module map. The same pairing gives $(g\circ f{)}^{\mathrm{\prime }}=f^{\mathrm{\prime }}\circ g^{\mathrm{\prime }}$ and ${\mathrm{i}\mathrm{d}}^{\mathrm{\prime }}=\mathrm{i}\mathrm{d}$, so the constructed contragredient acts contravariantly on module maps as well.