Quotients of nuclear spaces are nuclear.

src/fa/lc/nuclear-space.tex

@@ -109,7 +109,7 @@
 
     which enables identifying $\widehat F_{U \cap F}$ as a closed subspace of $\widehat E_{U}$.
 
-    To start the proof, let $U \in \cn_E(0)$ be a given convex and circled neighbourhood. Since $E$ is nuclear, there exists a convex and circled neighbourhood $V \in \cn_E(0)$ such that the induced map $\widehat \pi_U: \widehat E_V \to \widehat E_U$ is nuclear. By prior discussion, the following diagram commutes:
+    To start the proof, let $U \in \cn_E(0)$ be a given convex and circled neighbourhood. Since $E$ is nuclear, there exists a convex and circled neighbourhood $V \in \cn_E(0)$ with $V \subset U$ such that the induced map $\widehat \pi_U: \widehat E_V \to \widehat E_U$ is nuclear. By prior discussion, the following diagram commutes:
     \[
     \xymatrix{
     E \ar@{->}[r]^{\pi_V} & \widehat E_V \ar@{->}[r]^{\widehat \pi_{U}} & \widehat E_U \\
@@ -139,3 +139,54 @@
 \end{proof}
 
 
+\begin{proposition}
+\label{proposition:nuclear-quotient}
+    Let $E$ be a nuclear space over $K \in \RC$, and $F$ be a closed subspace of $E$, then $E/F$ is also nuclear. 
+\end{proposition}
+\begin{proof}
+    Firstly, a setup about auxiliary spaces and quotients is required. Let $p: E \to E/F$ be the canonical projection and $U \in \cn_E(0)$ be a convex and circled neighbourhood, then the composition of maps $E \to E/F \to (E/F)_{p(U)}$ factors through $E_{U}$ as follows: 
+    \[
+    \xymatrix{
+    E \ar@{->}[r]^{\pi_U} \ar@{->}[d]_{p} & E_U \ar@{->}[d] \\
+    E/F \ar@{->}[r]_{\pi_{p(U)}} & (E/F)_{p(U)}
+    }
+    \]
+
+    This extends through the completion
+    \[
+    \xymatrix{
+    E \ar@{->}[r]^{\pi_U} \ar@{->}[d]_{p} & E_U \ar@{->}[d] \ar@{->}[r] & \widehat E_U \ar@{->}[d] \\
+    E/F \ar@{->}[r]_{\pi_{p(U)}} & (E/F)_{p(U)} \ar@{->}[r] & \widehat{(E/F)}_{p(U)}
+    }
+    \]
+
+    and yields that $\widehat{(E/F)}_{p(U)}$ is a quotient space of $\widehat E_{U}$. 
+
+    To begin the proof, let $U \in \cn_E(0)$ be a convex and circled neighbourhood. Since $E$ is nuclear, there exists a convex and circled neighbourhood $V \in \cn_E(0)$ with $V \subset U$ such that the induced map $\widehat \pi_{U}: \widehat E_V \to \widehat E_{U}$ is nuclear. The composition of maps $\wh E_V \to \wh E_U \to \wh{(E/F)}_{p(U)}$ then factors through $\widehat{(E/F)}_{p(V)}$ as $\widehat \pi_{p(U)}$:
+    \[
+    \xymatrix{
+    E \ar@{->}[r]^{\pi_V} \ar@{->}[d]_{p} & \widehat E_V \ar@{->}[d] \ar@{->}[r]^{\widehat \pi_U} & \widehat E_U \ar@{->}[d]^{\widehat p} \\
+    E/F \ar@{->}[r]_{\pi_{p(V)}} & \widehat{(E/F)}_{p(V)} \ar@{->}[r]_{\widehat \pi_{p(U)}} & \widehat{(E/F)}_{p(U)}
+    }
+    \]
+
+    Since $\wh \pi_U: \wh E_V \to \wh E_U$ is nuclear, there exists $\seq{\phi_n} \subset E_V^*$ and $\seq{y_n} \subset \wh E_U$ such that
+    \[
+    \wh \pi_U x = \sum_{n = 1}^\infty y_n \dpn{x, \phi_n}{\wh E_V} \quad \forall x \in \wh E_V
+    \]
+
+    and $\sum_{n \in \natp}\norm{y_n}_{\wh E_U}\norm{\phi_n}_{E_V^*} < \infty$. 
+
+    Now, using \autoref{theorem:nuclear-lp}, further assume without loss of generality that $\wh E_V$ is a Hilbert space. Identify $(\widehat{E/F})_{p(V)}$ as a closed subspace of $\widehat E_V$, and let $P: \widehat E_V \to (\widehat{E/F})_{p(V)}$ be the orthogonal projection of $\widehat E_V$ onto $(\widehat{E/F})_{p(V)}$. This allows rewriting
+    \[
+        \widehat \pi_{p(U)}x = \sum_{n = 1}^\infty \widehat p(y_n) \dpn{Px, \phi_n}{\wh E_V} = \sum_{n = 1}^\infty \widehat p(y_n) \dpn{x, P\phi_n}{(\widehat{E/F})_{p(V)}}
+    \]
+
+    where
+    \begin{align*}
+    \normn{\widehat \pi_{p(U)}}_{N((\widehat{E/F})_{p(V)}; (\widehat{E/F})_{p(U)})} &\le \sum_{n \in \natp}\normn{\widehat p(y_n)}_{(\widehat{E/F})_{p(U)}}\norm{P\phi_n}_{(\widehat{E/F})_{p(V)}} \\
+    &\le \sum_{n \in \natp}\norm{y_n}_{\wh E_U}\norm{\phi_n}_{E_V^*} < \infty
+    \end{align*}
+
+    Therefore $\widehat \pi_{p(U)}$ is nuclear, and $E/F$ is a nuclear space. 
+\end{proof}