Tensor product of Hilbert Spaces I am following this link under "definitions" 
I need to see why the suggested inner product on the pre-Hilbert space $H_1$ tensor $H_2$ is well defined.  Recall that the fundamental tensors are a spanning set, but not a linearly independent one, hence not free in the category of vector spaces.  How do I know that this definition is consistent no matter what representation of an element of the tensor space I give?
 A: As was pointed out in a comment, probably the simplest way to handle the technical details is to do everything in terms of chosen orthonormal bases for $H_1$ and $H_2$ (to lessen the number of subscripts, I will write $H$ and $K$ instead of $H_1$ and $H_2$ from now on).
But there are other ways to do it, as there are other ways to handle the details of the purely algebraic vector space tensor product (which I will denote by $\otimes_a$, to distinguish it from the Hilbert space tensor product).
One construction of $H \otimes_a K$ is as a quotient $V/W$, where $V$ is the free vector space with basis $H \times K$ and the subspace $W$ the span of an explicit set of vectors (including, e.g. all vectors of the form $(h_1 + h_2, k) - (h_1, k) - (h_2, k)$ with $h_1$ and $h_2$ in $H$ and $k$ in $K$).  In this realization, the "elementary tensor" $h \otimes k$ is simply the image of $(h,k)$ in the quotient $V/W$, and the problem of defining an inner product on $H \otimes_a K$ is a special case of the problem of defining a positive definite Hermitian sesquilinear form on a quotient vector space $V/W$ in terms of something on $V$.  So one can do this as a special case of a more general  algebraic problem.
Suppose $S: V \times V \to \mathbb{C}$ is a positive (not necessarily positive definite) Hermitian sesquilinear form on a complex vector space $V$.  Define
$$
N = \{x \in V: S(x,y) = 0 \text{ for all } y \in V\}.
$$
Note that $N$ is obviously a subspace of $V$.
Fix any subspace $W$ of $V$, and let $q: V \to V/W$ denote the quotient map.  It is easy to verify that


*

*Then there is a positive Hermitian sesquilinear form $S'$ on $V/W$ satisfying 
$$
S'(q(x), q(y)) = S(x,y), \qquad x, y \in V,
$$
if and only if $W \subseteq N$.

*In the case that $W \subseteq N$, the form $S'$ on $V/W$ from part 1. is positive definite if and only if $W = N$.
[In proving 2. it helps to recall that the Cauchy-Schwarz inequality for $S$ (which requires only positivity, not definiteness, of $S$) gives the alternate description $N = \{x \in V: S(x,x) = 0\}$ of $N$.]
So we have a general program to follow in the application of interest.
We take $V$ to be the free vector space on $H \times K$ and $W$ the subspace spanned by the elements representing the relations one wants in the tensor product.


*

*It is clear (from freeness) that the recipe 
$$
S((\xi_1,\eta_1), (\xi_2,\eta_2)) = \langle\xi_1,\xi_2\rangle_H \langle\eta_1,\eta_2\rangle_K, \qquad \xi_1, \xi_2 \in H, \quad \eta_1, \eta_2 \in K,
$$
gives rise to a well-defined sesquilinear form on all of $V$.  

*To know that $S$ is positive on $V$, one must know that for all $n$ and all $\xi_1, \dots, \xi_n \in H$ and $\eta_1, \dots, \eta_n$ the number
$$
\sum_{i,j=1}^n \langle\xi_i,\xi_j\rangle_H \langle\eta_i,\eta_j\rangle_K
$$
is nonnegative.  One way to do this is to recall that the "Gram matrix" $m = (\langle\xi_i,\xi_j\rangle_H)_{i,j=1}^n \in M_n(\mathbb{C})$ of any finite sequence of $n$ vectors in a Hilbert space is positive semidefinite.  So there is $b = (b_{kl})_{k,l=1}^n \in M_n(\mathbb{C})$ with $b^* b = m$, and hence
$$
\sum_{i,j=1}^n \langle\xi_i,\xi_j\rangle_H \langle\eta_i,\eta_j\rangle_K = \sum_{i,j,p=1}^n \overline{b_{pi}} b_{pj} \langle\eta_i, \eta_j\rangle_K = \sum_{p=1}^n \left\|\sum_{k=1}^n \overline{b_{pk}} \eta_k\right\|_K^2 \geq 0.
$$

*It clear that the subspace $W$ one quotients with to get $H \otimes_a K$ is contained in the space "$N$" of the form (just check that each generator of $W$ is in $N$, which is immediate from the sesquilinearity of the inner products on $H$ and $K$).  
So the recipe does give, for rather general reasons, a well defined positive sesquilinear form $S'$ on $H \otimes_a K$.  
The detail that is not immediately clear in this realization is why the form $S'$ is definite--- ie, why if $x \in V$ satisfies $S(x,x) = 0$, then $x \in W$.  There are several ways to verify this.  One is to note that (since any fixed $x \in V$ is a finite sum $\sum_{j=1}^n (s_j, t_j)$) it suffices to prove this assertion for $H$ and $K$ finite dimensional.  In this case, letting $h = \dim H$ and $k = \dim K$ one can use orthonormal bases of $H$ and $K$ to observe that the quotient $V/N$ contains $hk$ mutually orthogonal vectors and hence has dimension at least $hk$.  Since for purely linear algebraic reasons one knows that $V/W = H \otimes_a K$ has dimension $hk$, it follows that $\dim(N) \leq \dim(W)$, and hence $N = W$ as desired.  (I think you can also tweak the above proof of positivity of $S$ into a proof of definiteness, if you understand the matrix algebraic consequences of an element of $V$ being $0$ in the tensor product.)
