Added properties of inductive limits.

src/fa/lc/inductive.tex

@@ -9,15 +9,16 @@
         \item For each $i \in I$, $T_i \in L(E_i; E)$.
         \item[(U)] For any topology $\mathcal{S}$ on $E$ satisfying (1) and (2), $\mathcal{S} \subset T$.
         \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}
+        \]
+        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}
 \begin{proof}
-    (1): Let
-    \[
-    \mathcal{B} = \bracs{U \subset E|U \text{ convex, radial, circled}, T_i^{-1}(U) \in \cn_{E_i}(0) \forall i \in I}
-    \]
-    To see that $\mathcal{B}$ is a fundamental system of neighbourhoods at $0$ for a vector space topology on $E$, it is sufficient to verify the following and apply \ref{proposition:tvs-0-neighbourhood-base}.
+    (1), (5): To see that $\mathcal{B}$ is a fundamental system of neighbourhoods at $0$ for a vector space topology on $E$, it is sufficient to verify the following and apply \ref{proposition:tvs-0-neighbourhood-base}.
     \begin{enumerate}
         \item[(TVB1)] Every set in $\mathcal{B}$ is radial and circled by definition.
         \item[(TVB2)] For any $U \in \mathcal{B}$, $U$ is circled, so $\frac{1}{2}U + \frac{1}{2}U \subset U$. Since $\frac{1}{2}U$ is also circled and radial, $\frac{1}{2}U \in \mathcal{B}$.
@@ -58,6 +59,11 @@
 
         for all $i \in I$.
         \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_E \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_E)^{-1}(U) \in \cn_{E_i}(0) \forall i \in I}
+        \]
+        is a fundamental system of neighbourhoods for $E$ at $0$.
     \end{enumerate}
     The pair $(E, \bracsn{T^i_E}_{i \in I})$ is the \textbf{inductive limit} of $(\seqi{E}, \bracsn{T^i_j| i, j \in I, i \lesssim j})$.
 \end{definition}
@@ -77,3 +83,96 @@
 
     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}
+
+\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
+    \begin{enumerate}
+        \item There exists $V \in \cn_E(0)$ circled and radial such that $U = M \cap V$.
+        \item For any $x \in E \setminus \ol M$, there exists $V \in \cn_E(0)$ circled and radial such that $U = M \cap V$ and $x \not\in U$.
+    \end{enumerate}
+\end{lemma}
+\begin{proof}
+    (1): Let $W \in \cn_E(0)$ be circled and radial with $W \cap M \subset U$, and $V = \text{Conv}(W \cup U)$.
+    \begin{itemize}
+        \item For any $u \in U$, $w \in W$, and $t \in [0, 1]$, there exists $\alpha \in (0, 1)$ such that $x = \alpha^{-1}w \in W$. In which case,
+        \[
+        (1 - \alpha)U + w = (1 - \alpha) U + \alpha x \subset V
+        \]
+        so $V \in \cn(0)$.
+        \item For any $\lambda \in K$ with $\abs{\lambda} \le 1$, $u \in U$, $w \in W$, and $t \in [0, 1]$,
+        \[
+        \lambda (1 - t)u + \lambda tw = (1 - t)\lambda u + t \lambda w \in V
+        \]
+        as $U$ and $W$ are both circled.
+    \end{itemize}
+    so $V \in \cn_E(0)$ is convex and circled.
+
+    For any $u \in U$, $w \in W$, and $t \in [0, 1]$, if $(1 - t)u + tw \in M$, then $u \in M \cap U \subset M \cap W$, so $(1 - t)u + tw \in W$.
+
+    (2): Since $x \not\in \ol M$, there exists $W \in \cn_E(0)$ circled and radial with $x + W \cap M = \emptyset$. Let $V$ as in (1), then $x \not\in W + M \supset W + U = V$.
+\end{proof}
+
+\begin{proposition}[{{\cite[II.6.4, II.6.5, II.6.6]{SchaeferWolff}}}]
+\label{proposition:lc-strict-inductive-countable}
+    Let $(\seq{E_n}, \seq{\iota_n^m|m, n \in \natp, m \le n})$ be a strict inductive system of locally convex spaces over $K \in \RC$ and $(E, \seq{\iota_n})$ be its direct limit, then:
+    \begin{enumerate}
+        \item For each $n \in \natp$, the topology of $E_n$ is induced by $\iota_n$, which allows the identification of $E_n$ as a subspace of $E$.
+        \item If $E_n$ is separated for all $n \in \natp$, then $E$ is also separated.
+        \item If $\iota^m_n(E_m) \subset E_n$ is closed for all $m, n \in \natp$ with $m \le n$, then the following are equivalent for any $B \subset E$:
+        \begin{enumerate}
+            \item[(a)] $B$ is bounded.
+            \item[(b)] There exists $n \in \natp$ such that $B \subset E_n$ is bounded.
+        \end{enumerate}
+        \item If $E_n$ is complete for each $n \in \natp$, then $E$ is also complete.
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    (1): Let $U \in \cn_{E_n}(0)$. By \ref{lemma:lc-induct-separate}, there exists $\bracs{U_m| m \in \natp, m \ge n} \subset 2^E$ such that $U_n = U$, $U_m \in \cn_{E_m}(0)$ and $U_{m} = U_{m + 1} \cap E_m$ for all $m \in \natp$. Let $V = \bigcup_{m \ge n}U_m$, then $V \cap E_m = U_m$ for all $m \ge n$. In particular, $V \cap E_n = U_n = U$.
+
+    (2): Let $x \in E \setminus \bracs{0}$, then there exists $n \in \natp$ such that $x \in E_n$. Since $E_n$ is separated, there exists $U \in \cn_{E_n}(0)$ with $x \not\in U$. By \ref{lemma:lc-induct-separate} and (1), there exists $V \in \cn_E(0)$ such that $V \cap E_n = U$, so $x \not\in V$.
+
+    (3), $\neg (b) \Rightarrow \neg (a)$: If $B \not\subset E_n$ for all $n \in \natp$, then there exists a subsequence $\bracsn{n_k}_0^\infty \subset \natp$ and $\seq{x_k} \subset B$ such that $x_k \in E_{n_{k}} \setminus E_{n_{k - 1}}$ for all $k \in \natp$.
+
+    Since $E_{n_k} \subset E_{n_{k+1}}$ is closed for all $k \in \natp$, there exists $\seq{U_k} \subset 2^E$ such that:
+    \begin{enumerate}
+        \item For each $k \in \natp$, $U_k \in \cn_{E_{n_k}}(0)$.
+        \item For each $k \in \natp$, $U_k = U_{k+1} \cap E_{n_k}$.
+        \item For each $k \in \natp$, $n^{-1}x_k \not\in U_k$.
+    \end{enumerate}
+    then $V = \bigcup_{k \in \natp}U_k \in \cn_E(0)$ with $V \cap E_{n_k} = U_k$ for all $k \in \natp$. For any $n \in \natp$, $x_k \not\in nU_k = nV \cap E_{n_k}$. Therefore $B$ is not bounded.
+
+    (3), $(b) \Rightarrow (a)$: Let $U \in \cn_E(0)$, then $U \cap E_n \in \cn_{E_n}(0)$, so there exists $\lambda \in K$ with $\lambda (U \cap E_n) \supset B$.
+
+    (4): Let $\fF \subset 2^E$ be a Cauchy filter and
+    \[
+    \fU = \bracs{F + U|F \in \mathcal{F}, U \in \cn_E(0)}
+    \]
+    then $\fU$ is also a Cauchy filter, which converges if and only if $\fF$ does.
+
+    Since each $E_n$ is complete, it is sufficient to show that there exists $n \in \natp$ such that $F + U \cap E_n \ne \emptyset$ for all $F \in \fF$ and $U \in \cn_E(0)$.
+
+    Suppose for contradiction that for every $n \in \natp$, there exists $F_n \in \fF$ and $U_n \in \cn_E(0)$ such that $E_n \cap F_n + U_n = \emptyset$. Assume without loss of generality that for every $n \in \natp$, $U_n$ is convex and circled with $U_n \supset U_{n+1}$. Let
+    \[
+    U = \text{Conv}\paren{\bigcup_{n \in \natp}(U_n \cap E_n)}
+    \]
+    then since each $U_n$ is circled, so is $U$. Thus $U \cap E_n \supset U_n \cap E_n \in \cn_{E_n}(0)$, and $U \in \cn_E(0)$.
+
+    Now, suppose that $(F_n + U) \cap E_n \ne \emptyset$. Let $y \in (F_n + U) \cap E_n$, then there exists $N \in \natp$, $\bracs{x_k}_1^N \subset E$, $\bracs{\lambda_k}_1^N \subset [0, 1]$, and $z \in F_n$ such that
+    \begin{itemize}
+    \item For each $1 \le k \le N$, $x_k \in U_k \cap E_k$.
+    \item $\sum_{k = 1}^N \lambda_k = 1$.
+    \item $y = z + \sum_{k = 1}^N \lambda_k x_k$.
+    \end{itemize}
+    In which case, since $U_{k} \supset U_{k+1}$ for all $k \in \natp$,
+    \[
+    \underbracs{y - \sum_{k = 1}^n \lambda_kx_k}_{\in E_n} = \underbrace{z + \sum_{k = n + 1}^N \lambda_kx_k}_{\in F_n + U_n}
+    \]
+    which is impossible. Therefore $(F_n + U) \cap E_n = \emptyset$ for all $n \in \natp$.
+
+    Finally, since $\fF$ is a Cauchy filter, there exists $F \in \fF$ such that $F - F \subset U$. Let $z \in F$, then there exists $n \in \natp$ such that $z \in E_n$. In which case, for any $y \in F \cap F_n$,
+    \[
+    z = y + (z - y) \in y + (F - F) \subset y + U \subset F_n + U
+    \]
+    which contradicts the fact that $(F_n + U) \cap E_n = \emptyset$.
+\end{proof}