Added the injective tensor product.

src/topology/main/c0.tex

@@ -64,4 +64,43 @@ For details regarding the complex-valued cased, in particular its properties as
 
 \end{proof}
 
+\begin{theorem}
+\label{theorem:c0-beq-tensor}
+    Let $X$ be a LCH space and $E$ be a complete locally convex space over $K \in \RC$, then the canonical map
+    \[
+    C_0(X; K) \otimes_\eps E \to C_0(X; E) \quad \sum_{j = 1}^n f_j \otimes y_j \mapsto \sum_{j = 1}^n y_j \cdot f_j
+    \]
+
+    extends into an isomorphism between $C_0(X; K) \wh{\otimes}_\eps E$ and $C_0(X; E)$. Moreover, if $E$ is a Banach space, then the isomorphism is an isometry. 
+\end{theorem}
+\begin{proof}
+    To see that the canonical map is continuous, let $\rho: E \to [0, \infty)$ be a continuous seminorm on $E$. By the \hyperref[Hahn-Banach Theorem]{proposition:hahn-banach-utility}, there exists an equicontinuous family $T \subset E^*$ such that for each $y \in E$, $\rho(y) = \sup_{\phi \in T}|\dpn{y, \phi}{E}|$. 
+
+    Let $\lambda = \sum_{j = 1}^n f_j \otimes y_j \in C_0(X; K) \otimes_\eps E$, then
+    \[
+    \sup_{x \in X}\rho(\lambda(x)) = \sup_{x \in X}\sup_{\phi \in T}|\dpn{\lambda(x), \phi}{E}| = \sup_{x \in X}\sup_{\phi \in T}\abs{\sum_{j = 1}^n f_j(x) \dpn{y_j, \phi}{E}}
+    \]
+
+    Since the evaluation maps $\bracsn{\pi_x: C_0(X; K) \to K|x \in X}$ are equicontinuous, the uniform seminorm on $C_0(X; E)$ with respect to $\rho$ is bounded above by a cross seminorm of the injective tensor product. Thus the inclusion is continuous. 
+
+    On the other hand, let $T \subset E^*$ be equicontinuous, then there exists a continuous seminorm $\rho: E \to [0, \infty)$ such that $|\phi| \le \rho$ for all $\phi \in T$. In which case, for any $\lambda = \sum_{j = 1}^n f_j \otimes y_j \in C_0(X; K) \otimes_\eps E$, $I \in C_0(X; K)^*$, and $\phi \in T$, 
+    \begin{align*}
+        \abs{\sum_{j = 1}^n \dpn{f_j, I}{C_0(X; K)}\dpn{y_j, \phi}{E}} &= \abs{\angles{\sum_{j = 1}^nf_j\dpn{y_j, \phi}{E}, I}_{C_0(X; K)}} \\
+        &\le \norm{I}_{C_0(X; K)} \cdot \sup_{x \in X} \abs{\angles{\sum_{j = 1}^n f_j(x) y_j, \phi}_{E}} \\
+        &\le \norm{I}_{C_0(X; K)} \cdot \sup_{x \in X} \rho(\lambda(x))
+    \end{align*}
+    
+    Hence the cross seminorm corresponding to $B_{C_0(X; K)^*}(0, 1)$ and $T$ is bounded above by the uniform seminorm on $C_0(X; E)$ with respect to $\rho$, so the inclusion is an embedding. 
+
+    Finally, by \autoref{proposition:c0-properties}, $C_0(X; K)$ is complete. By \autoref{proposition:c0-tensor}, $C_0(X; K) \otimes_\eps E$ is dense in $C_0(X; E)$. Therefore the canonical map extends to an isomorphism through the \hyperref[Linear Extension Theorem]{theorem:linear-extension-theorem-tvs}.
+\end{proof}
+
+\begin{corollary}
+\label{corollary:c0-seq-beq-tensor}
+    Let $I$ be a set and $E$ be a complete locally convex space over $K \in \RC$, then $c_0(I; K) \wh \otimes_\eps E \iso c_0(I; E)$. 
+\end{corollary}
+\begin{proof}
+    By \autoref{theorem:c0-beq-tensor}. 
+\end{proof}
+