Is the tensor product of linear maps defined to be linear or provably linear? Suppose $S:V\rightarrow X$ and $T:W\rightarrow Y$ are two linear maps between vector spaces. One then defines $S \otimes T:V\otimes W \rightarrow X \otimes Y$ by $(S\otimes T)(v\otimes w) = S(v) \otimes T(w)$ for $v \in V, w \in W$.  But is the further fact that $S\otimes T$ is linear something that needs to be asserted about $S\otimes T$, so that the definition extends to all of $V\otimes W$, or is this fact something that can somehow be proven?
 A: It depends.
You can obtain $S\otimes T$ by invoking the universal property of the tensor product $V\otimes W$: we have a bilinear map $V\times W\to X\otimes Y$ given by $(v,w)\mapsto S(v)\otimes T(w)$. That this is bilinear follows because it is the composition of the linear map $V\times W\to X\times Y$ given by $S\times T$, followed by the bilinear universal map $u\colon X\times Y\to X\otimes Y$ given by $u(x,y)=x\otimes y$.
By the universal property of the tensor product, this bilinear map induces a (unique) linear map $V\otimes W\to X\otimes Y$ given by $v\otimes w\mapsto S(v)\otimes T(w)$, giving that the map you have is necessarily linear.
However, this is technically not a definition of $S\otimes T$, but rather a derivation of that map; if you simply try to define $S\otimes T$ by the given formula and then attempt to extend it linearly, then you need to show that it is well defined (note that the vectors $v\otimes w$ span $V\otimes W$, but are not a basis, since there are linear relations between them). Once you know it is well defined, you will probably get linearity out of it. But in general proving a map is well-defined on $V\otimes W$ devolves into invoking the universal property above, so you are better off using that directly.
