Added a proposition concerning the structure of complete locally convex spaces.

src/fa/tvs/projective.tex

@@ -70,7 +70,7 @@
     \end{enumerate}
 \end{definition}
 \begin{proof}
-    Let $(E, \bracsn{T^E_i}_{i \in I})$ be the inverse limit of $(\seqi{E}, \bracs{T^i_j|i, j \in I, i \lessim j})$ as $K$-vector spaces (\ref{proposition:module-inverse-limit}).
+    Let $(E, \bracsn{T^E_i}_{i \in I})$ be the inverse limit of $(\seqi{E}, \bracsn{T^i_j|i, j \in I, i \lesssim j})$ as $K$-vector spaces (\ref{proposition:module-inverse-limit}).
 
     Equip $E$ with the projective topology generated by $\bracsn{T^E_i}_{i \in I}$, then $(E, \bracsn{T^E_i}_{i \in I})$ satisfies (1) and (2).
 
@@ -78,3 +78,46 @@
 
     (U): By (U) of \ref{proposition:module-inverse-limit}, there exists a unique $S \in \hom(F; E)$ such that the given diagram commutes. By (4), $S \in L(F; E)$.
 \end{proof}
+
+\begin{proposition}[{{\cite[II.5.4]{SchaeferWolff}}}]
+\label{proposition:complete-lc-projective-limit}
+    Let $E$ be a Hausdorff complete locally convex space over $K \in \RC$, $\mathcal{B} \subset \cn_E(0)$ be a fundamental system of neighbourhoods consisting of convex, circled, and radial sets, directed under inclusion.
+
+    For each $U \in \mathcal{B}$, let $[\cdot]_U$ be its gauge, $M_U = \bracs{x \in E|[\cdot]_U = 0}$, $E_U = E/M_U$, and $\norm{\cdot}_U: E_U \to [0, \infty)$ be the quotient of $[\cdot]_U$ by $M_U$, then
+    \begin{enumerate}
+        \item For each $U, V \in \mathcal{B}$ with $U \subset V$, let
+        \[
+        \pi^U_V: E_U \to E_V \quad x + M_U \mapsto x + M_V
+        \]
+        then $\pi^U_V \in L(E_U; E_V)$.
+        \item $(\bracsn{E_U}_{U \in \mathcal{B}}, \bracs{\pi^U_V|U, V \in \mathcal{B}, U \subset V})$ is a downward-directed system of topological vector spaces.
+        \item The map $\pi \in L(E, \lim_{\longleftarrow}E_U)$ induced by $\bracs{\pi_U}_{U \in \mathcal{B}}$ is a bijection.
+        \item For each $U, V \in \mathcal{B}$, let $\ol E_U$ be the completion of $E_U$, $\ol{\pi_U} \in L(E; \ol E_U)$, and $\ol{\pi^U_V} \in L(\ol E_U; \ol E_V)$ be the unique extensions of $\pi_U$ and $\pi^U_V$, respectively. Then,
+        \[
+        E = \lim_{\longleftarrow}E_U = \lim_{\longleftarrow} \ol E_U
+        \]
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    (1): Since $V \supset U$, $[\cdot]_V \ge [\cdot]_U$, so $M_V \supset M_U$. Thus $\ker(\pi_V) \supset M_U$. By (U) of the quotient (\ref{definition:tvs-quotient}), $\pi_V$ factors through $E_U$ as $\pi^U_V$, so $\pi^U_V \in L(E_U; E_V)$.
+
+    (2): Since $\mathcal{B}$ is a fundamental system of neighbourhoods, it is downward-directed under inclusion. For any $U, V, W \in \mathcal{B}$ with $U \subset V \subset W$, $M_U \supset M_V \supset M_W$. Thus $\pi^U_W = \pi^V_W \circ \pi^U_V$.
+
+    (3): Let $\lim E_U$ be the projective limit. For each $U \in \mathcal{B}$, let $p_U: \lim E_U \to E_U$ be the canonical map.
+
+    Let $x \in E$. Since $E$ is Hausdorff and $\mathcal{B}$ is a fundamental system of neighbourhoods at $0$, there exists $U \in \mathcal{B}$ such that $\pi_U(x) \ne 0$. In which case, $p_U \circ \pi(x) = \pi_U(x) \ne 0$, so $\pi$ is injective.
+
+    Let $x \in \lim E_U$. For each $U \in \mathcal{B}$, let $x_U \in E$ such that $\pi_U(x_U) = p_U(x)$. For any $V \in \cn_E(0)$, there exists $W \in \mathcal{B}$ with $W \subset V$. In which case, for any $U \in \mathcal{B}$ with $U \subset W$,
+    \[
+    \pi_W(x_U) = \pi_W^U \circ \pi_U(x_U) = \pi_W^U p_U(x)
+    \]
+    Thus for any $U' \in \mathcal{B}$ with $U \subset W$, $[x_U - x_{U'}]_W = 0$, and $x_U - x_{U'} \in W$. Therefore $\bracs{x_U}_{U \in \mathcal{B}}$ is a Cauchy net, and converges to $x_0 \in E$ by completeness of $E$.
+
+    For any $U \in \mathcal{B}$, $\pi_U(x_0) = \lim_{V \in \mathcal{B}}\pi_U(x_V) = p_U(x)$, so $\pi(x_0) = x$, and $\pi$ is surjective.
+
+    (4): Since $\mathcal{B} \subset \cn_E(0)$ is a fundamental system of neighbourhoods, the topology on $E$ is the projective topology generated by $\bracs{\pi_U|U \in \mathcal{B}}$. As $\pi_U \circ \pi^{-1} = p_U \in L(\lim E_U; E_U)$ for all $U \in \mathcal{B}$, $\pi^{-1} \in L(\lim E_U; E)$ by (U) of the projective topology (\ref{definition:tvs-initial}).
+
+    Let $x \in \lim\ol{E}_U$ and $V \in \cn(x)$. Since $\mathcal{B}$ is downward-directed and $\lim\ol{E}_U$ is equipped with the projective topology induced by $\bracs{p_U|U \in \mathcal{B}}$, there exists $U \in \mathcal{B}$ and $W \in \cn_{\ol E_U}(x)$ such that $p_U^{-1}(W) \subset V$. As $E_U$ is dense in $\ol E_U$, there exists $y_U \in W$, and $y \in E$ such that $y_U = \pi_U(y)$. Therefore $\pi(y_U) \in p_U^{-1}(W) \subset V$, and $\lim E_U$ is dense in $\lim \ol{E}_U$.
+
+    Since $E$ is complete and isomorphic to $\lim E_U$, $\lim E_U$ is a complete, and thus closed subset of $\lim \ol{E}_U$. Therefore $E = \lim E_U = \lim \ol{E}_U$.
+\end{proof}