Added barreled spaces.

src/fa/lc/inductive.tex

@@ -3,7 +3,7 @@
 
 \begin{definition}[Inductive Locally Convex Topology]
 \label{definition:lc-inductive}
-    Let $\seqi{E}$ be locally convex spaces over $K \in \RC$, $\seqi{T}$ such that $T_i \in \hom(E_i; E)$ for all $i \in I$, and $E$ be a vector space over $K$, then there exists a topology $\topo$ on $E$ such that:
+    Let $\seqi{E}$ be locally convex spaces over $K \in \RC$, $E$ be a vector space over $K$, and $\seqi{T}$ such that $T_i \in \hom(E_i; E)$ for all $i \in I$, then there exists a topology $\topo$ on $E$ such that:
     \begin{enumerate}
         \item $(E, \topo)$ is a locally convex space over $K$.
         \item For each $i \in I$, $T_i \in L(E_i; E)$.
@@ -11,10 +11,16 @@
         \item For any locally convex space $F$ and $T \in \hom(E; F)$, $T \in L(E; F)$ if and only if $T \circ T_i \in L(E_i; F)$ for all $i \in I$.
         \item The family
         \[
-        \mathcal{B} = \bracs{U \subset E|U \text{ convex, radial, circled}, T_i^{-1}(U) \in \cn_{E_i}(0) \forall i \in I}
+        \mathcal{B} = \bracs{U \subset E|U \text{ convex, circled, radial}, T_i^{-1}(U) \in \cn_{E_i}(0) \forall i \in I}
         \]
 
         is a fundamental system of neighbourhoods for $E$ at $0$.
+        \item If $E$ is spanned by $\bigcup_{i \in I}T_i(E_i)$, then
+        \[
+        \fB = \bracs{\Gamma\paren{\bigcup_{i \in I}T_i(U_i)} \bigg | U_i \in \cn_{E_i}(0)}
+        \]
+
+        is a fundamental system of neighbourhoods for $E$ at $0$. 
     \end{enumerate}
     The topology $\topo$ is the \textbf{inductive locally convex topology} on $E$ induced by $\seqi{T}$.
 \end{definition}
@@ -31,7 +37,43 @@
 
     (U): Let $U \in \cn_{(E, \mathcal{S})}(0)$ be convex, circled, and radial. By (2), $T_i^{-1}(U) \in \cn_{E_i}(0)$ for all $i \in I$. Thus the convex, circled, and radial neighbourhoods of $0$ in $(E, \mathcal{S})$ is a subset of $\mathcal{B}$.
 
-    (4): Let $i \in I$ and $U \in \cn_F(0)$ be convex, circled, and radial. Since $T \circ E_i \in L(E_i; F)$, $T_i^{-1}(T^{-1}(U)) \in \cn_{E_i}(0)$, so $T^{-1}(U) \in \mathcal{B} \subset \cn_E(0)$.
+    (5): Let $i \in I$ and $U \in \cn_F(0)$ be convex, circled, and radial. Since $T \circ E_i \in L(E_i; F)$, $T_i^{-1}(T^{-1}(U)) \in \cn_{E_i}(0)$, so $T^{-1}(U) \in \mathcal{B} \subset \cn_E(0)$.
+
+    (6): If $E$ is spanned by $\bigcup_{i \in I}T_i(E_i)$, then each set in $\fB$ is radial. Hence $\fB$ is a family of neighbourhoods of $E$ at $0$. 
+
+    Let $U \in \cn_E(0)$ be convex, circled, and radial, then for each $i \in I$, $T_i^{-1}(U) \in \cn_{E_i}(0)$, so $U \supset \bigcup_{i \in I}T_i[T_i^{-1}(U)]$. Since $U$ is convex and circled, $U \supset \Gamma\paren{\bigcup_{i \in I}T_i[T_i^{-1}(U)]} \in \fB$. Therefore $\fB$ forms a fundamental system of neighbourhoods for $E$ at $0$.
+\end{proof}
+
+\begin{definition}[Locally Convex Direct Sum]
+\label{definition:lc-direct-sum}
+    Let $\seqi{E}$ be locally convex spaces over $K \in \RC$, then there exists $(E, \seqi{\iota})$ such that:
+    \begin{enumerate}
+        \item $E$ is a locally convex space over $K$. 
+        \item For each $i \in I$, $\iota_i \in L(E_i; E)$. 
+        \item[(U)] For each $(F, \seqi{T})$ satisfying (1) and (2), there exists a unique $T \in L(E; F)$ such that the following diagram commutes:
+        \[
+        \xymatrix{
+        A \ar@{->}[r]^{T} & B \\
+        A_i \ar@{->}[u]^{\iota_i} \ar@{->}[ru]_{T_i} & 
+        }
+        \]
+        
+        \item The family
+        \[
+        \fB = \bracs{\Gamma\paren{\bigcup_{i \in I}\iota_i(U_i)} \bigg | U_i \in \cn_{E_i}(0)}
+        \]
+
+        is a fundamental system of neighbourhoods for $E$ at $0$. 
+    \end{enumerate}
+    
+    The space $E = \bigoplus_{i \in I}E_i$ is the \textbf{locally convex direct sum} of $\seqi{E}$. 
+\end{definition}
+\begin{proof}
+    Let $(E, \seqi{\iota})$ be the direct sum of $\seqi{E}$ as vector spaces, and equip it with the inductive topology induced by $\seqi{\iota}$, then $(E, \seqi{\iota})$ satisfies (1) and (2). 
+
+    (U): By (U) of the \hyperref[direct sum]{definition:direct-sum}, there exists a unique $T \in \hom(E; F)$ such that the diagram commutes. In which case, by (4) of \autoref{definition:lc-inductive}, $T \in L(E; F)$. 
+
+    (4): By (6) of \autoref{definition:lc-inductive}.
 \end{proof}
 
 \begin{definition}[Inductive Limit]
@@ -88,6 +130,9 @@
     In addition to the neighbourhood construction given above, the inductive topology may also be constructed as the weak topology generated by all topologies satisfying certain properties. While this more non-constructive method is simpler, it does not directly provide an explicit fundamental system of neighbourhoods at $0$.
 \end{remark}
 
+\subsection{Strict Inductive Limits}
+\label{subsection:lc-induct-strict}
+
 \begin{lemma}[{{\cite[Lemma II.6.4]{SchaeferWolff}}}]
 \label{lemma:lc-induct-separate}
     Let $E$ be a locally convex space over $K$, $M \subset E$ be a subspace, $U \in \cn_M(0)$ be convex and circled, then