Definition 9.9.1 (Projective Tensor Product). Let $E, F$ be locally convex spaces over $K \in \RC$, then there exists a pair $(E \otimes_{\pi} F, \iota)$ such that:
$E \otimes_{\pi} F$ is a locally convex space over $K$.
$\iota \in L^{2}(E, F; E \otimes_{\pi} F)$ is a continuous bilinear map.
For any $(G, \lambda)$ satisfying (1) and (2), there exists a unique $\Lambda \in L(E \otimes_{\pi} F; G)$ such that the following diagram commutes:
\[\xymatrix{ E \times F \ar@{->}[rd]_{\lambda} \ar@{->}[r]^{\iota} & E \otimes F \ar@{->}[d]^{\Lambda} \\ & G }\]For any topology $\topo$ on $E \otimes_{\pi} F$ satisfying (1) and (2), $\topo$ is coarser than the topology on $E \otimes_{\pi} F$.
$E \otimes_{\pi} F$ is the linear span of $\iota(E \times F)$.
For any $U \subset E$ and $V \subset F$, let $U \otimes V = \bracs{u \otimes v|u \in U, v \in V}$, then the convex circled hulls
\[\fB = \bracsn{\Gamma(U \otimes V)| U \in \cn_E(0), V \in \cn_F(0)}\]is a fundamental system of neighbourhoods at $0$ for $E \otimes_{\pi} F$.
The space $E \otimes_{\pi} F$ is the projective tensor product of $E$ and $F$, and the mapping $\iota \in L^{2}(E, F; E \otimes_{\pi} F)$ is the canonical embedding.
The space $E \widetilde{\otimes}_{\pi} F$ denotes the Hausdorff completion of $E \otimes_{\pi} F$.
Proof. Let $E \otimes_{\pi} F = E \otimes F$ be the tensor product of $E$ and $F$ as vector spaces. Let $\mathscr{T}\subset 2^{2^X}$ be the collection of all locally convex topologies satisfying (1) and (2), and let $\mathcal{S}$ be the projective topology on $E \otimes_{\pi} F$ generated by $\mathscr{T}$.
(1): By Proposition 9.5.1, $\mathcal{S}$ is a locally convex topology on $E \otimes_{\tau} F$.
(2): Since $\iota: E \times F \to E \otimes_{\pi} F$ is continuous with respect to every topology in $\mathscr{T}$, it is also continuous with respect to $\mathcal{S}$.
(U2): Since $\mathcal{T}\in \mathscr{T}$, $\mathcal{S}\supset \mathcal{T}$.
(U1): By (U) of the tensor product, there exists a unique $\Lambda \in \hom(E \otimes_{\pi} F; G)$ such that the given diagram commutes. Since $\lambda$ is continuous, the projective topology generated by $\Lambda$ satisfies (1) and (2). By (U2), $\mathcal{S}$ contains the projective topology generated by $\Lambda$. Therefore $\Lambda \in L(E \otimes_{\pi}; F)$.
(5): By (4) of the tensor product.
(6): Let $U \in \cn_{E}(0)$ and $V \in \cn_{F}(0)$ be balanced. For any $\sum_{j = 1}^{n} x_{j} \otimes y_{j} \in E \otimes_{\pi} F$, then there exists $\lambda > 0$ such that $\seqf{x_j}\subset \lambda U$ and $\seqf{y_j}\subset \lambda V$. In which case, $\sum_{j = 1}^{n} x_{j} \otimes y_{j} \subset \lambda \Gamma (U \otimes V)$, so $\fB$ is a collection of convex, circled, and radial sets. Since $\fB$ defines a locally convex topology that satisfies (1) and (2), $\mathcal{S}$ contains the topology defined by $\fB$.
On the other hand, for any convex and circled set $W \in \cn_{E \otimes_\pi F}(0)$, there exists $U \in \cn_{E}(0)$ and $V \in \cn_{F}(0)$ such that $U \otimes V \subset W$. In which case, $W \supset \Gamma(U \otimes V)$, so $\fB$ is a fundamental system of neighbourhoods at $0$ for $E \otimes_{\pi} F$.$\square$