The tensor product of two vector spaces V,W over \mathbb{F} is a vector space V \otimes W over \mathbb{F} together with a bilinear map V \times W \stackrel{\otimes}{\rightarrow} V \otimes W with the property that when­ever \mathcal{B}_V, \mathcal{B}_W are bases for V,W respectively, the set \{ v_i \otimes w_j \mid v_i \in \mathcal{B}_V, w_j \in \mathcal{B}_W \} gives a basis for V \otimes W.

The following theorem shows that the property in the definition need not be checked for all pairs of bases; just one pair is sufficient.

Theorem: Let Y be a vector space and \phi : V \times W \rightarrow Y be bilinear. Suppose there are bases \mathcal{B}_V, \mathcal{B}_W for V,W respectively, such that \phi(v \times w) is a basis for Y. Then the same holds for any pair of bases.

Let V, W be vector spaces over \mathbb{F}. Following (Zakharevich 2015), our goal is to construct a vector space V \otimes W such that for any vector space Z,

\mathcal{L}(V \otimes W, Z) \cong \big\{ \substack{\text{bilinear maps}\\{V \times W \rightarrow Z}} \big\}

Let A = \mathrm{Free}(V \times W) be the free vector space over \mathbb{F} on the product V \times W. We will demonstrate that

\mathcal{L}(A,Z) \cong \big\{ \substack{\text{functions}\\{V \times W \rightarrow Z}} \big\}

For v \in V, w \in W, define the notation v \otimes w \equiv \mathbb{1}_{(v,w)} \in A. A typical vector has the form f = \sum_{k=1}^n \alpha_k (v_k \otimes w_k) \in A. By linearity, observe that each T \in \mathcal{L}(A,Z) is determined uniquely by its values on the standard basis, exposing a bijection between \mathcal{L}(A,Z) and (nonlinear) functions V \times W \rightarrow Z.

T f = T \left( \sum_{k=1}^n \alpha_k (v_k \otimes w_k) \right) = \sum_{k=1}^n \alpha_k T (v_k \otimes w_k)

Step 2: Since \mathcal{L}(A,Z) represents arbitrary functions, we will construct V \oplus W by shrinking A so that \mathcal{L}(V \times W, Z) represents only the bilinear maps V \times W \rightarrow Z. For example, if T \in \mathcal{L}(V \otimes W, Z) is a linear map, the following proof of bilinearity in the first argument

\begin{aligned} T( (v_1 + v_2) \otimes w ) &= T( (v_1 \otimes w) + (v_2 \otimes w) ) \\ &= T(v_1 \otimes w) + T(v_2 \otimes w) \end{aligned}

requires that (v_1 + v_2) \otimes w and (v_1 \otimes w) + (v_2 \otimes w) refer to the same element in V \otimes W. Starting from A, we can enforce this equivalence implicitly by defining V \otimes W to be the quotient space A / A_0, where

A_0 = \mathrm{Span}\left\{ \begin{aligned}[c] (v_1 + v_2) \otimes w - (v_1 \otimes w) - (v_2 \otimes w) \\ v \otimes (w_1 + w_2) - (v \otimes w_1) - (v \otimes w_2) \\ (\alpha v) \otimes w - \alpha (v \otimes w) \\ v \otimes (\alpha w) - \alpha (v \otimes w) \end{aligned} \;\middle\vert\; \begin{array}{l} \alpha \in F \\ v \in V, w \in W \end{array} \right\}

This choice was made so that each linear map T \in \mathcal{L}(V \otimes W, Z) will satisfy

\begin{aligned}
T( (v_1 + v_2) \otimes w) &= T(v_1 \otimes w) + T(v_2 \otimes w) \\ T( v \otimes (w_1 + w_2)) &= T(v \otimes w_1) + T(v \otimes w_2) \\ T( (\alpha v) \otimes w ) &= T( \alpha ( v \otimes w) ) \\ T( v \otimes (\alpha w) ) &= T( \alpha ( v \otimes w) ) \end{aligned}

(Technically, (v \otimes w) \in V \otimes W stands for the equivalence class of v \otimes w = \mathbb{1}_{(v,w)} \in A.)

As pointed out by Purbhoo 2012, since A = \mathrm{Free}(V \times W) is the space of formal linear combinations of (v,w) pairs, A_0 is the space of those linear combinations that can be simplified to the zero vector using bilinearity. Accordingly, A / A_0 reduces A to a space where two expressions are equal iff one can be simplified to the other using bilinearity.