Pointwise representation of one-forms by vector-field functionals (source code)

= Pointwise representation of one-forms by vector-field functionals
{title2=$\theta(\omega)(X)=\omega(X)$}

Let $W$ consist of real-linear maps $\alpha$ from smooth <vector fields> to smooth functions such that $X_p=0$ implies $\alpha(X)(p)=0$. These are exactly evaluations by smooth <differential one-forms>. Define $\omega_p(v)=\alpha(X)(p)$ using any global field with $X_p=v$; the vanishing condition makes it well-defined. Bump-extended local frame vectors make its coefficients smooth. Also $\alpha(fX)(p)=f(p)\alpha(X)(p)$, so real linearity and pointwise vanishing automatically give $C^\infty$-linearity. The evaluation correspondence is a natural module isomorphism.