Added projective limits for LC spaces.

src/fa/lc/index.tex

@@ -5,4 +5,5 @@
 \input{./src/fa/lc/convex.tex}
 \input{./src/fa/lc/continuous.tex}
 \input{./src/fa/lc/quotient.tex}
+\input{./src/fa/lc/projective.tex}
 \input{./src/fa/lc/hahn-banach.tex}

src/fa/lc/projective.tex

@@ -0,0 +1,23 @@
+\section{Projective Limits}
+\label{section:lc-projective}
+
+
+\begin{proposition}
+\label{proposition:lc-projective-topology}
+    Let $E$ be a vector space over $K \in \RC$, $\seqi{F}$ be locally convex spaces over $K$, and $\seqi{T}$ where $T_i \in \hom(E; F_i)$ for all $i \in I$, then the projective topology on $E$ is locally convex.
+\end{proposition}
+\begin{proof}
+    By \ref{definition:tvs-initial},
+    \[
+    \mathcal{B} = \bracs{\bigcap_{j \in J}T_j^{-1}(U_j) \bigg | J \subset I \text{ finite}, U_j \in \cn_{F_j}(0)}
+    \]
+    is a fundamental system of neighbourhoods at $0$. For each $i \in I$, $U_i \in \cn_{F_i}(0)$ convex, $T^{-1}(U_i)$ is also convex. Since each $F_i$ is locally convex, $\mathcal{B}$ contains a fundamental system of neighbourhoods at $0$ consisting of only convex sets.
+\end{proof}
+
+\begin{proposition}
+\label{proposition:lc-projective}
+    Let $(\seqi{E}, \bracsn{T^i_j|i, j \in I, i \lesssim j})$ be a downward-directed system of locally convex spaces over $K \in \RC$, then $E = \lim_{\longleftarrow}E_i$ is locally convex.
+\end{proposition}
+\begin{proof}
+    By (U) of \ref{definition:tvs-projective-limit} and \ref{definition:tvs-initial}, $E$ is equipped with the projective topology generated by the projection maps $E \to E_i$. By \ref{proposition:lc-projective-topology}, $E$ is locally convex.
+\end{proof}