Double contragredient of a grading-restricted generalized module

For every finite-dimensional generalized-weight block, evaluation identifies $M_{[h]}$ with $M_{[h]}^{\ast \ast }$. Taking their algebraic direct sum gives a bijection $e_M:M\to M^{\mathrm{\prime }\mathrm{\prime }}$, characterized by $⟨e_M(m),\lambda ⟩=⟨\lambda ,m⟩$. In the joint convention the same construction on $M_{[\lambda ]}$ is a bijection of joint-weight direct sums, by F1. No full algebraic dual of an infinite direct sum is substituted for this restricted dual.

For a single module F2 proves equivariance for this exact evaluation map. For a joint module, fix j and all the other joint eigenvalues $\beta$ as in F1's fibre construction. F2 applied to $M^{j,\beta }$ says that the restriction of $e_M$ commutes with every jth field. The direct-sum formula in step 1.1 is the same fibre evaluation for every j and $\beta$, so $e_M$ commutes with every component field; it is therefore a module isomorphism in the component convention too.

For a module map $f:M\to N$, commutation with each $L_j(0)$ means that f preserves each generalized or joint weight block. Thus its restricted transpose $f^{\mathrm{\prime }}:N^{\mathrm{\prime }}\to M^{\mathrm{\prime }}$ is defined, and its double transpose obeys $⟨f^{\mathrm{\prime }\mathrm{\prime }}{e}_M(m),\nu ⟩=⟨e_M(m),f^{\mathrm{\prime }}(\nu )⟩=⟨\nu ,f(m)⟩=⟨e_{N}f(m),\nu ⟩$ for every restricted functional $\nu$. Such functionals separate each weight block, hence $f^{\mathrm{\prime }\mathrm{\prime }}{e}_M=e_{N}f$. This proves naturality of the module isomorphism.