Added barreled spaces.

.vscode/project.code-snippets

@@ -27,6 +27,17 @@
       "$0"
     ]
   },
+  "Summary": {
+  "scope": "latex",
+    "prefix": "summ",
+    "body": [
+      "\\begin{summary}[$1]",
+      "\\label{summary:$2}",
+      "    $3",
+      "\\end{summary}",
+      "$0"
+    ]
+  },
   "Lemma Block": {
   "scope": "latex",
     "prefix": "lem",

preamble.sty

@@ -15,6 +15,7 @@
 
 \newtheorem{definition}[theorem]{Definition}
 \newtheorem{example}[theorem]{Example}
+\newtheorem{summary}[theorem]{Summary}
 % \newtheorem{exercise}[subsection]{Exercise}
 % \newtheorem{situation}[subsection]{Situation}
 

src/cat/cat/tensor.tex

@@ -1,8 +1,172 @@
-\section{The Tensor Product}
-\label{section:tensor-product}
+\section{Universal Constructions for Modules}
+\label{section:universal-module}
 
 
 
+\begin{definition}[Product]
+\label{definition:product-module}
+    Let $R$ be a ring and $\seqi{A}$ be $R$-modules, then there exists $(A, \bracsn{\pi_i}_{i \in I})$ such that:
+    \begin{enumerate}
+        \item For each $i \in I$, $\pi_i \in \hom(A; A_i)$. 
+        \item[(U)] For any $(B, \seqi{T})$ satisfying (1), there exists a unique $T \in \hom(B; A)$ such that the following diagram commutes:
+        \[
+        \xymatrix{
+        B \ar@{->}[rd]_{T_i} \ar@{->}[r]^{T} & A \ar@{->}[d]^{\pi_i} \\
+        & A_i
+        }
+        \]
+    \end{enumerate}
+
+    The module $A = \prod_{i \in I}A_i$ is the \textbf{product} of $\seqi{A}$. 
+\end{definition}
+
+\begin{definition}[Direct Sum]
+\label{definition:direct-sum}
+    Let $E$ be a ring and $\seqi{A}$ be $R$-modules, then there exists $(A, \bracsn{\iota_i}_{i \in I})$ such that:
+    \begin{enumerate}
+        \item For each $i \in I$, $\iota_i \in \hom(A_i; A)$. 
+        \item[(U)] For each $(B, \seqi{T})$ satisfying (1), there exists a unique $T \in \hom(A; B)$ such that the following diagram commutes
+        \[
+        \xymatrix{
+        A \ar@{->}[r]^{T} & B \\
+        A_i \ar@{->}[u]^{\iota_i} \ar@{->}[ru]_{T_i} & 
+        }
+        \]
+    \end{enumerate}
+    
+    The module $A = \bigoplus_{i \in I}A_i$ is the \textbf{direct sum} of $\seqi{A}$. 
+\end{definition}
+\begin{proof}
+    Let
+    \[
+    A = \bracs{x \in \prod_{i \in I}A_i \bigg | x_i \ne 0 \quad \text{for finitely many}\ i \in I}
+    \]
+
+    For each $i \in I$, let
+    \[
+    \iota_i: A_i \to A \quad (\iota_ix)_j = \begin{cases}
+        x &i = j \\
+        0 &i \ne j
+    \end{cases}
+    \]
+
+    then $\iota_i \in \hom(A_i; A)$. 
+
+    (U): Let
+    \[
+    T: A \to B \quad x \mapsto \sum_{i \in I}T_ix_i
+    \]
+
+    then $T \in \hom(A; B)$ and the diagram commutes. Since $\bigcup_{i \in I}\iota_i(A_i)$ spans $A$, $T$ is the unique linear map making the diagram commute. 
+\end{proof}
+
+\begin{proposition}
+\label{proposition:module-direct-limit}
+    Let $R$ be a ring and $(\seqi{A}, \bracsn{T^i_j| i, j \in I, i \lesssim j})$ be an upward-directed system of $R$-modules, then there exists $(A, \bracsn{T^i_A}_{i \in I})$ such that:
+    \begin{enumerate}
+        \item For each $i \in I$, $T^i_A \in \hom({A_i; A})$.
+        \item For any $i, j \in I$ with $i \lesssim j$, the following diagram commutes:
+
+        \[
+        \xymatrix{
+        A_i \ar@{->}[rd]_{T^i_A} \ar@{->}[r]^{T^i_j} & A_j \ar@{->}[d]^{T^j_A} \\
+         & A
+        }
+        \]
+
+
+        \item[(U)] For any pair $(B, \bracsn{S^i_B}_{i \in I})$ satisfying (1) and (2), there exists a unique $S \in \hom({A, B})$ such that the following diagram commutes
+
+        \[
+        \xymatrix{
+        A_i \ar@{->}[d]_{T^i_A} \ar@{->}[rd]^{S^i_B} &  \\
+        A \ar@{->}[r]_{g} & B
+        }
+        \]
+
+
+        for all $i \in I$.
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    Let $M = \bigoplus_{i \in I}A_i$. For any $i, j \in I$ with $i \lesssim j$ and $x \in A_i$, let $x_{i, j} \in M$ such that for any $k \in I$,
+    \[
+    \pi_k(x_{i, j}) = \begin{cases}
+        x &k = i \\
+        T^i_j x &k = j \\
+        0 &k \ne i, j
+    \end{cases}
+    \]
+
+    Let $N \subset M$ be the submodule generated by $\bracs{x_{i, j}|i, j \in I, i \lesssim j, x \in A_i}$, $A = M/N$, and $\pi: M \to M/N$ be the canonical map.
+
+    (1): For each $i \in I$, let
+    \[
+    T^i_M: A_i \to M \quad \pi_k T^i_M x = \begin{cases}
+        x &k = i \\
+        0 &k \ne i
+    \end{cases}
+    \]
+
+    and $T^i_A = \pi \circ T^i_M$.
+
+    (2): Let $i, j \in I$ with $i \lesssim j$, then for any $x \in A_i$, $T^i_Mx - T^j_M T^i_j x \in N$. Hence $T^i_Ax = T^j_A T^i_jx$.
+
+    (U): Let
+    \[
+    S_0: M \to B \quad x \mapsto \sum_{i \in I}S^i_B \pi_i x
+    \]
+
+    then $S_0$ is the unique linear map such that $S_0 \circ T^i_M = S^i_B$ for all $i \in I$. For any $i, j \in I$ with $i \lesssim J$, $S^i_B x = S^j_B T^i_j x$, so $\ker S_0 \supset N$. By the first isomorphism theorem, there exists a unique $S \in \hom(A; B)$ such that $S_0 = S \circ \pi$.
+\end{proof}
+
+\begin{proposition}
+\label{proposition:module-inverse-limit}
+    Let $R$ be a ring and $(\seqi{A}, \bracs{T^i_j|i, j \in I, i \lesssim j})$ be a downward-directed system of $R$-modules, then there exists $(A, \bracsn{T^A_i}_{i \in I})$ such that:
+    \begin{enumerate}
+        \item For each $i \in I$, $T^A_i \in \hom(A; A_i)$.
+        \item For any $i, j \in I$ with $i \lesssim j$, the following diagram commutes:
+        \[
+        \xymatrix{
+        A_i \ar@{->}[r]^{T^i_j} & A_j \\
+        A \ar@{->}[u]^{T^A_i} \ar@{->}[ru]_{T^A_j} &
+        }
+        \]
+
+        \item[(U)] For any pair $(B, \bracsn{S^B_i}_{i \in I})$ satisfying (1) and (2), there exists a unique $S \in \hom(B; A)$ such that the following diagram commutes
+
+        \[
+        \xymatrix{
+         & A_i \\
+        B \ar@{->}[r]_{S} \ar@{->}[ru]^{S^B_i} & A \ar@{->}[u]_{T^A_i}
+        }
+        \]
+
+
+        for all $i \in I$.
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    Let
+    \[
+    A = \bracs{x \in \prod_{i \in I}A_i \bigg | \pi_j(x) = T^i_j\pi_i(x) \forall i, j \in I, i \lesssim j}
+    \]
+
+    For each $i \in I$, let $T^A_i = \pi_i$, then $(A, \bracsn{T^A_i}_{i \in I})$ satisfies (1) and (2) by definition of $A$.
+
+    (U): Let $(B, \bracsn{S^B_i}_{i \in I})$ satisfying (1) and (2). Let
+    \[
+    S: B \to \prod_{i \in I}A_i \quad \pi_i(Sx) = S^B_i
+    \]
+
+    then for any $x \in B$ and $i, j \in I$ with $i \lesssim j$,
+    \[
+    \pi_j (Sx) = S^B_jx = T^i_j S^B_ix = T^i_j \pi_i(S x)
+    \]
+
+    so $S \in \hom(B; A)$, and the diagram commutes. Since any map $f: B \to A$ is uniquely determined by its composition with the projections, $S$ is unique.
+\end{proof}
+
 \begin{definition}[Tensor Product]
 \label{definition:tensor-product}
     Let $R$ be a commutative ring and $\seqf{E_j}$ be $R$ modules, then there exists a pair $(\bigotimes_{j = 1}^n E_j, \iota)$ such that:

src/cat/cat/universal.tex

@@ -147,112 +147,5 @@ Let $\catc$ be a category and $(\seqi{A}, \bracsn{f^i_j| i, j \in I, i \lesssim
 \end{enumerate}
 \end{definition}
 
-\begin{proposition}
-\label{proposition:module-direct-limit}
-    Let $R$ be a ring and $(\seqi{A}, \bracsn{T^i_j| i, j \in I, i \lesssim j})$ be an upward-directed system of $R$-modules, then there exists $(A, \bracsn{T^i_A}_{i \in I})$ such that:
-    \begin{enumerate}
-        \item For each $i \in I$, $T^i_A \in \hom({A_i, A})$.
-        \item For any $i, j \in I$ with $i \lesssim j$, the following diagram commutes:
-
-        \[
-        \xymatrix{
-        A_i \ar@{->}[rd]_{T^i_A} \ar@{->}[r]^{T^i_j} & A_j \ar@{->}[d]^{T^j_A} \\
-         & A
-        }
-        \]
-
-
-        \item[(U)] For any pair $(B, \bracsn{S^i_B}_{i \in I})$ satisfying (1) and (2), there exists a unique $S \in \hom({A, B})$ such that the following diagram commutes
-
-        \[
-        \xymatrix{
-        A_i \ar@{->}[d]_{T^i_A} \ar@{->}[rd]^{S^i_B} &  \\
-        A \ar@{->}[r]_{g} & B
-        }
-        \]
-
-
-        for all $i \in I$.
-    \end{enumerate}
-\end{proposition}
-\begin{proof}
-    Let $M = \bigoplus_{i \in I}A_i$. For any $i, j \in I$ with $i \lesssim j$ and $x \in A_i$, let $x_{i, j} \in M$ such that for any $k \in I$,
-    \[
-    \pi_k(x_{i, j}) = \begin{cases}
-        x &k = i \\
-        T^i_j x &k = j \\
-        0 &k \ne i, j
-    \end{cases}
-    \]
-
-    Let $N \subset M$ be the submodule generated by $\bracs{x_{i, j}|i, j \in I, i \lesssim j, x \in A_i}$, $A = M/N$, and $\pi: M \to M/N$ be the canonical map.
-
-    (1): For each $i \in I$, let
-    \[
-    T^i_M: A_i \to M \quad \pi_k T^i_M x = \begin{cases}
-        x &k = i \\
-        0 &k \ne i
-    \end{cases}
-    \]
-
-    and $T^i_A = \pi \circ T^i_M$.
-
-    (2): Let $i, j \in I$ with $i \lesssim j$, then for any $x \in A_i$, $T^i_Mx - T^j_M T^i_j x \in N$. Hence $T^i_Ax = T^j_A T^i_jx$.
-
-    (U): Let
-    \[
-    S_0: M \to B \quad x \mapsto \sum_{i \in I}S^i_B \pi_i x
-    \]
-
-    then $S_0$ is the unique linear map such that $S_0 \circ T^i_M = S^i_B$ for all $i \in I$. For any $i, j \in I$ with $i \lesssim J$, $S^i_B x = S^j_B T^i_j x$, so $\ker S_0 \supset N$. By the first isomorphism theorem, there exists a unique $S \in \hom(A; B)$ such that $S_0 = S \circ \pi$.
-\end{proof}
-
-\begin{proposition}
-\label{proposition:module-inverse-limit}
-    Let $R$ be a ring and $(\seqi{A}, \bracs{T^i_j|i, j \in I, i \lesssim j})$ be a downward-directed system of $R$-modules, then there exists $(A, \bracsn{T^A_i}_{i \in I})$ such that:
-    \begin{enumerate}
-        \item For each $i \in I$, $T^A_i \in \hom(A; A_i)$.
-        \item For any $i, j \in I$ with $i \lesssim j$, the following diagram commutes:
-        \[
-        \xymatrix{
-        A_i \ar@{->}[r]^{T^i_j} & A_j \\
-        A \ar@{->}[u]^{T^A_i} \ar@{->}[ru]_{T^A_j} &
-        }
-        \]
-
-        \item[(U)] For any pair $(B, \bracsn{S^B_i}_{i \in I})$ satisfying (1) and (2), there exists a unique $S \in \hom(B; A)$ such that the following diagram commutes
-
-        \[
-        \xymatrix{
-         & A_i \\
-        B \ar@{->}[r]_{S} \ar@{->}[ru]^{S^B_i} & A \ar@{->}[u]_{T^A_i}
-        }
-        \]
-
-
-        for all $i \in I$.
-    \end{enumerate}
-\end{proposition}
-\begin{proof}
-    Let
-    \[
-    A = \bracs{x \in \prod_{i \in I}A_i \bigg | \pi_j(x) = T^i_j\pi_i(x) \forall i, j \in I, i \lesssim j}
-    \]
-
-    For each $i \in I$, let $T^A_i = \pi_i$, then $(A, \bracsn{T^A_i}_{i \in I})$ satisfies (1) and (2) by definition of $A$.
-
-    (U): Let $(B, \bracsn{S^B_i}_{i \in I})$ satisfying (1) and (2). Let
-    \[
-    S: B \to \prod_{i \in I}A_i \quad \pi_i(Sx) = S^B_i
-    \]
-
-    then for any $x \in B$ and $i, j \in I$ with $i \lesssim j$,
-    \[
-    \pi_j (Sx) = S^B_jx = T^i_j S^B_ix = T^i_j \pi_i(S x)
-    \]
-
-    so $S \in \hom(B; A)$, and the diagram commutes. Since any map $f: B \to A$ is uniquely determined by its composition with the projections, $S$ is unique.
-\end{proof}
-
 
 

src/fa/lc/barrel.tex

@@ -0,0 +1,67 @@
+\section{Barreled Spaces}
+\label{section:barrel}
+
+\begin{definition}[Barrel]
+\label{definition:barrel}
+    Let $E$ be a TVS over $K \in \RC$ and $D \subset E$, then $D$ is a \textbf{barrel} if it is convex, circled, radial, and closed. 
+\end{definition}
+
+\begin{definition}[Barreled Space]
+\label{definition:barreled-space}
+    Let $E$ be a locally convex space over $K \in \RC$, then the following are equivalent:
+    \begin{enumerate}
+        \item The barrels of $E$ forms a fundamental system of neighbourhoods at $0$. 
+        \item Every barrel in $E$ is a neighbourhood of $0$. 
+        \item Every lower semicontinuous seminorm on $E$ is continuous. 
+    \end{enumerate}
+\end{definition}
+\begin{proof}
+    $(2) \Rightarrow (1)$: Let $\fB \subset \cn_E(0)$ be a fundamental system of neighbourhoods at $0$ consisting of convex, circled, and radial sets, then $\ol{\fB} = \bracsn{\ol U|U \in \fB}$ is a fundamental system of neighbourhoods at $0$ consisting of barrels. 
+
+    $(2) \Rightarrow (3)$: Let $\rho: E \to [0, \infty)$ be a lower semicontinuous seminorm, then $\bracs{\rho > 1}$ is open and $\bracs{\rho \le 1}$ is a Barrel. In which case, $\rho$ is continuous by (4) of \autoref{lemma:continuous-seminorm}. 
+
+    $(3) \Rightarrow (2)$: Let $D \subset E$ be a barrel and $\rho: E \to [0, \infty)$ be its gauge. By (4) of \autoref{definition:gauge}, $D = \bracs{\rho \le 1}$, so $\bracs{\rho > 1}$ is open, and $\rho$ is semicontinuous. By assumption, $\rho$ is continuous, so $D \in \cn_E(0)$ by (5) of \autoref{lemma:continuous-seminorm}. 
+\end{proof}
+
+\begin{summary}[Barreled Spaces]
+\label{summary:barreled-space}
+    The following types of locally convex spaces are barreled:
+    \begin{enumerate}
+        \item Every locally convex space with the Baire property.
+        \item Every Banach space and every Fréchet space. 
+        \item Inductive limits of barreled spaces. 
+        \item Spaces of type (LB) and (LF). 
+        \item The locally convex direct sum of barreled spaces. 
+        \item Products of barreled spaces.
+    \end{enumerate}
+\end{summary}
+\begin{proof}
+    (1), (2): \autoref{proposition:baire-barrel}. 
+
+    (3), (4), (5): \autoref{proposition:barrel-limit}. 
+
+    (6): TODO. 
+\end{proof}
+
+
+\begin{proposition}
+\label{proposition:baire-barrel}
+    Let $E$ be a locally convex space over $K \in \RC$. If $E$ is a Baire space, then $E$ is barreled. 
+\end{proposition}
+\begin{proof}[Proof, {{\cite[II.7.1]{SchaeferWolff}}}. ]
+    Let $D \subset E$ be a Barrel, then $E = \bigcup_{n \in \natp}nD$ is a countable union of closed sets. Since $E$ is Baire, there exists $n \in \natp$, $U \in \cn_E(0)$ circled, and $x \in E$ such that $x + U \in nB$. In which case, 
+    \[
+    U \subset (x + U) - (x + U) \subset nB - nB = 2nB
+    \]
+
+    so $2nB$ and thus $B$ is a neighbourhood of $0$. 
+\end{proof}
+
+\begin{proposition}
+\label{proposition:barrel-limit}
+    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 the inductive locally convex topology on $E$ induced by $\seqi{T}$ is barreled.  
+\end{proposition}
+\begin{proof}[Proof, {{\cite[II.7.2]{SchaeferWolff}}}]
+    Let $D \subset E$ be a barrel, then for each $i \in I$, $T_i^{-1}(D) \subset E_i$ is also a barrel, and thus a neighbourhood of $0$ in $E_i$. By (5) of \autoref{definition:lc-inductive}, $D$ is a neighbourhood of $0$ in $E$, so $E$ is barreled. 
+\end{proof}
+

src/fa/lc/bornologic.tex

@@ -47,7 +47,7 @@
 
 \begin{proposition}
 \label{proposition:bornologic-continuous-complete}
-    Let $E$ be a bornologic space and $F$ be a complete Hausdorff locally convex space, then $L_b(E; F)$ is complete. In particular, $E^*$ equipped with the topology of bounded convergence is complete.
+    Let $E$ be a bornologic space and $F$ be a complete separated locally convex space, then $L_b(E; F)$ is complete. In particular, $E^*$ equipped with the topology of bounded convergence is complete.
 \end{proposition}
 \begin{proof}
     By \autoref{proposition:bornologic-bounded}, $L_b(E; F) = B(E; F)$. By \autoref{proposition:operator-space-completeness}, $B(E; F)$ is complete, so $L_b(E; F)$ is complete as well.

src/fa/lc/convex.tex

@@ -118,15 +118,16 @@
         \item $[\cdot]$ is continuous.
         \item $[\cdot]$ is continuous at $0$.
         \item $\bracs{x \in E| [x] < 1} \in \cn_E(0)$.
+        \item $\bracs{x \in E| [x] \le 1} \in \cn_E(0)$.
     \end{enumerate}
 \end{lemma}
 \begin{proof}
-    $(4) \Rightarrow (1)$: Let $x, y \in E$ and $r > 0$. If
+    $(5) \Rightarrow (1)$: Let $x, y \in E$ and $r > 0$. If
     \[
-    x - y \in \bracs{x \in E|[x] < r} = r\bracs{x \in E|[x] < 1} \in \cn_E(0)
+    x - y \in \bracs{x \in E|[x] \le r} = r\bracs{x \in E|[x] \le 1} \in \cn_E(0)
     \]
     
-    then $[x - y] < r$.
+    then $[x - y] \le r$.
 \end{proof}
 
 
@@ -147,7 +148,7 @@
 
 \begin{definition}[Gauge/Minkowski Functional]
 \label{definition:gauge}
-    Let $E$ be a vector space over $K \in \RC$ and $A \subset E$ be a radial set, then the mapping
+    Let $E$ be a vector space over $K \in \RC$ and $A \subset E$ be radial, then the mapping
     \[
     [\cdot]_A: E \to [0, \infty) \quad x \mapsto \inf\bracsn{\lambda > 0| \lambda^{-1}x \in A}
     \]
@@ -157,11 +158,12 @@
         \item For any $x \in E$ and $\lambda \ge 0$, $[\lambda x]_A = \lambda [x]_A$.
         \item If $A$ is convex, then for any $x, y \in E$, $[x + y]_A \le [x]_A + [y]_A$.
         \item If $A$ is circled, then for any $x \in E$ and $\lambda \in K$, $[\lambda x]_A = \abs{\lambda}[x]_A$.
+        \item If $A$ is circled, then $\bracs{\rho < 1} \subseteq A \subseteq \bracs{\rho \le 1} \subseteq \ol A$.
     \end{enumerate}
     In particular,
-    \begin{enumerate}
-        \item[(4)] If $A$ is convex, then $[\cdot]_A$ is a sublinear functional.
-        \item[(5)] If $A$ is convex and circled, then $[\cdot]_A$ is a seminorm.
+    \begin{enumerate}[start=4]
+        \item If $A$ is convex, then $[\cdot]_A$ is a sublinear functional.
+        \item If $A$ is convex and circled, then $[\cdot]_A$ is a seminorm.
     \end{enumerate}
 \end{definition}
 \begin{proof}
@@ -171,6 +173,13 @@
     \]
 
     then $(\lambda + \mu)^{-1} \in A$, and $\lambda + \mu \ge [x + y]_A$. Thus $[x + y]_A \le [x]_A + [y]_A$.
+
+    (4): Let $x \in \bracs{\rho \le 1}$, then $\lambda x \in A$ for all $\lambda \in (0, 1)$. Therefore
+    \[
+    x \in \overline{\bracs{\lambda x|\lambda \in (0, 1)}} \subset A
+    \]
+
+    so $x \in \overline{A}$. 
 \end{proof}
 
 \begin{definition}[Locally Convex Space]

src/fa/lc/hahn-banach.tex

@@ -136,11 +136,11 @@
             \item $\dpb{x, \phi}{E} = \inf_{y \in M}\rho(x + y)$.
         \end{enumerate}
         \item For any $x \in E$ and continuous seminorm $\rho: E \to [0, \infty)$, there exists $\phi \in E^*$ with $|\phi| \le \rho$ and $\dpb{x, \phi}{E} = \rho(x)$.
-        \item If $E$ is Hausdorff, then for any $x, y \in E$, there exists $\phi \in E^*$ with $\dpb{x, \phi}{E} \ne \dpb{y, \phi}{E}$.
+        \item If $E$ is separated, then for any $x, y \in E$, there exists $\phi \in E^*$ with $\dpb{x, \phi}{E} \ne \dpb{y, \phi}{E}$.
     \end{enumerate}
 \end{proposition}
 \begin{proof}
-    (1): Let $\rho_M: E \to [0, \infty)$ be the quotient of $\rho$ by $M$, then $\rho_M \le \rho$ is a continuous seminorm on $E$ by \autoref{definition:quotient-norm}. Let $\phi_0: Kx \to K$ be defined by $\lambda x \mapsto \lambda \rho_M(x)$. By the \hyperref[Hahn-Banach Theorem]{theorem:hahn-banach}, there exists $\phi \in \hom{E; K}$ such that $\dpb{x, \phi}{E} = \rho_M(x)$ and $|\phi| \le \rho_M \le \rho$.
+    (1): Let $\rho_M: E \to [0, \infty)$ be the quotient of $\rho$ by $M$, then $\rho_M \le \rho$ is a continuous seminorm on $E$ by \autoref{definition:quotient-norm}. Let $\phi_0: Kx \to K$ be defined by $\lambda x \mapsto \lambda \rho_M(x)$. By the \hyperref[Hahn-Banach Theorem]{theorem:hahn-banach}, there exists $\phi \in \hom(E; K)$ such that $\dpb{x, \phi}{E} = \rho_M(x)$ and $|\phi| \le \rho_M \le \rho$.
 
     (2): By (1) applied to $M = \bracs{0}$.
 

src/fa/lc/index.tex

@@ -4,6 +4,7 @@
 
 \input{./convex.tex}
 \input{./continuous.tex}
+\input{./barrel.tex}
 \input{./bornologic.tex}
 \input{./quotient.tex}
 \input{./projective.tex}

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,7 +11,13 @@
         \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$. 
@@ -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

src/fa/lc/projective.tex

@@ -25,7 +25,7 @@
 
 \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.
+    Let $E$ be a separated 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}
@@ -51,7 +51,7 @@
 
     (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 E$. Since $E$ is separated 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$,
     \[

src/fa/rs/bv.tex

@@ -66,7 +66,7 @@
         \item $BV([a, b]; E)$ is a vector space.
         \item For each continuous seminorm $\rho$ on $E$, $[\cdot]_{\text{var}, \rho}$ is a seminorm on $BV([a, b]; E)$.
         \item Let $\fF$ be a filter on $BV([a, b]; E)$ and $f: [a, b] \to E$. If
-        \begin{enumerate}
+        \begin{enumerate}[label=\alph*]
             \item $\pi_x(\fF) \to f(x)$ for all $x \in [a, b]$.
             \item For every continuous seminorm $\rho$ on $E$, there exists $U \in \fF$ such that $\sup_{g \in U}[g]_{\text{var}, \rho} = M_\rho < \infty$.
         \end{enumerate}

src/fa/tvs/completion.tex

@@ -5,7 +5,7 @@
 \label{definition:tvs-completion}
     Let $E$ be a TVS over $K \in \RC$, then there exists $(\wh E, \iota)$ such that:
     \begin{enumerate}
-        \item $\wh E$ is a complete Hausdorff TVS.
+        \item $\wh E$ is a complete separated TVS.
         \item $\iota \in L(E; \wh E)$.
         \item[(U)] For any $(F, T)$ satisfying (1) and (2), there exists a unique $\ol{T} \in L(\wh E; F)$ such that the following diagram commutes:
     \end{enumerate}

src/fa/tvs/continuous.tex

@@ -54,7 +54,7 @@
 
 \begin{theorem}[Linear Extension Theorem (TVS)]
 \label{theorem:linear-extension-theorem-tvs}
-    Let $E$ be a TVS over $K \in \RC$, $F$ be a complete Hausdorff TVS over $K$, $D \subset E$ be a dense subspace, and $T \in L(D; F)$, then:
+    Let $E$ be a TVS over $K \in \RC$, $F$ be a complete separated TVS over $K$, $D \subset E$ be a dense subspace, and $T \in L(D; F)$, then:
     \begin{enumerate}
         \item There exists an extension $\ol T \in L(E; F)$ such that $\ol T|_D = T$.
         \item[(U)] For any $S \in C(E; F)$ satisfying (1), $S = \ol T$.

src/fa/tvs/quotient.tex

@@ -40,7 +40,7 @@
 
 \begin{proposition}
 \label{proposition:tvs-quotient-hausdorff}
-    Let $E$ be a TVS over $K \in \RC$, $M \subset E$ be a subspace, then $E/M$ is Hausdorff if and only if $M$ is closed.
+    Let $E$ be a TVS over $K \in \RC$, $M \subset E$ be a subspace, then $E/M$ is separated if and only if $M$ is closed.
 \end{proposition}
 \begin{proof}
     The space $M$ is closed if and only if
@@ -48,5 +48,5 @@
     M = \bigcap_{V \in \cn(0)}M + V
     \]
 
-    which is equivalent to $E/M$ being Hausdorff.
+    which is equivalent to $E/M$ being separated.
 \end{proof}

src/measure/measurable-maps/in-measure.tex

@@ -36,7 +36,7 @@
 
 \begin{proposition}[{{\cite[Theorem 2.30]{Folland}}}]
 \label{proposition:cauchy-in-measure-limit}
-    Let $(X, \cm, \mu)$ be a measure space, $(Y, d)$ be a complete metric space, and $\seq{f_n}$ be Borel measurable functions from $X \to Y$, then:
+    Let $(X, \cm, \mu)$ be a measure space, $(Y, d)$ be a complete metric space, and $\seq{f_n} \subset Y^X$ be a sequence Borel measurable functions from $X \to Y$ that is Cauchy in measure, then:
     \begin{enumerate}
         \item There exists a Borel measurable function $f: X \to Y$ such that $f_n \to f$ in measure.
         \item There exists a subsequence $\seq{n_k}$ such that $f_{n_k} \to f$ almost everywhere.