Finite tensor products of smooth vector bundles

In local frames $e_{j,a}$ with dual frames ${ϵ}_j^a$, any multilinear functional $T$ has the expansion $T={\sum }_{a_1,\dots ,a_k}T({ϵ}_1^{a_1},\dots ,{ϵ}_k^{a_k})e_{1,a_1}\otimes \cdots \otimes e_{k,a_k}$. Indeed write each argument ${\alpha }_j={\sum }_a{\alpha }_j(e_{j,a}){ϵ}_j^a$ and expand multilinearly. Evaluation at every tuple of dual basis vectors also proves uniqueness of these coefficients. Hence the elementary product tensors form a basis; they need not individually exhaust all tensors.

Successive currying identifies the multilinear model with the iterated bundle $\mathrm{Hom}(E_1^{\ast },\mathrm{Hom}(E_2^{\ast },\dots ,\mathrm{Hom}(E_k^{\ast },M\times \mathbb{R}))\dots ))$: send $T$ to ${\alpha }_1\mapsto ({\alpha }_2\mapsto \cdots T({\alpha }_1,\dots ,{\alpha }_k))$, and reverse by evaluation. Each arrow is linear in its displayed argument exactly because $T$ is multilinear. Transport the smooth bundle structure supplied by repeated applications of [F1] through this bijection. In these Hom charts the coordinates are exactly those of step 1.1. A frame change $e_j^{\mathrm{\prime }}=e_j{A}_j$ changes the product frame by entries ${\prod }_j(A_j{)}_{a_j{b}_j}$, by expanding the elementary tensors. These smooth matrices have inverse obtained from the inverse matrices and satisfy the cocycle law by finite matrix multiplication. Thus the product-frame charts are precisely the canonical smooth atlas just constructed. No countable family of frames is selected.

In the resulting atlas smoothness is exactly smoothness of the finite coefficient list. For $k=0$ the single empty tensor is $1$ in the scalar line; for $k=1$ evaluation identifies the model with $E_1$ by step 1.1. A zero-rank factor for $k>0$ makes every multilinear functional zero. Empty base and zero-dimensional base have the same local chart interpretation. All identifications are uniquely determined by evaluations, so this construction needs no AC.