Added complexification.

src/fa/tvs/complexify.tex

@@ -0,0 +1,119 @@
+\section{Complexification}
+\label{section:complexification}
+
+\begin{definition}[Complexification]
+\label{definition:complexification}
+    Let $E$ be a vector space over $\real$, then there exists a pair $(\complex(E), \iota)$ such that:
+    \begin{enumerate}
+        \item $\complex(E)$ is a vector space over $\complex$.
+        \item $\iota: E \to \complex(E)$ is a $\real$-linear map.
+        \item[(U)] For any pair $(F, T)$ satisfying (1) and (2), there exists a unique $\complex$-linear map $\complex(T): \complex(E) \to F$ such that the following diagram commutes:
+        \[
+        \xymatrix{
+        \mathbb{C}(E) \ar@{->}[r]^{\mathbb{C}(T)} & F \\
+        E \ar@{->}[u]^{\iota} \ar@{->}[ru]_{T} & 
+        }
+        \]
+        \item $\complex(E) = \iota(E) \oplus i\iota(E)$ as a vector space over $\real$. Under this decomposition, elements of $\complex(E)$ are written as $x + iy$, where $x, y \in E$. 
+    \end{enumerate}
+
+    The pair $(\complex(E), \iota)$ is the \textbf{complexification} of $E$, and
+    \begin{enumerate}
+        \item[(F)] For any vector space $F$ over $\real$ and $\real$-linear map $T: E \to F$, there exists a unique $\complex$-linear map $\complex(T): \complex(E) \to \complex(F)$ such that the following diagram commutes:
+        \[
+        \xymatrix{
+        \mathbb{C}(E) \ar@{->}[r]^{\mathbb{C}(T)} & \mathbb{C}(F) \\
+        E \ar@{->}[u]^{\iota} \ar@{->}[r]_{T} & F \ar@{->}[u]_{\iota}
+        }
+        \]
+
+        which is given by
+        \[
+        \complex(T)(x + iy) = Tx + iTy
+        \]
+    \end{enumerate}
+    
+\end{definition}
+\begin{proof}
+    (1): Let $\complex(E) = E \times E$ with coordinate-wise addition. For each $a, b \in \real$ and $x, y \in E$, let
+    \[
+    (a + bi)(x, y) = (ax - by, bx + ay)
+    \]
+
+    then $\complex(E)$ is a vector space over $\complex$. 
+
+    (2): Let $\iota: E \to \complex(E)$ be defined by $\iota(x) = (x, 0)$, then $\iota$ is $\real$-linear. 
+
+    (U): Let
+    \[
+    \complex(T): \complex(E) \to F \quad (x, y) \mapsto Tx + iTy
+    \]
+
+    then $\complex(T)$ is the unique $\complex$-linear map such that the given diagram commutes. 
+
+    (F): By (U) applied to $\iota \circ T$.
+\end{proof}
+
+\begin{definition}[Complexification of Topological Vector Space]
+\label{definition:complexification-tvs}
+    Let $E$ be a TVS over $\real$, then there exists a pair $(\complex(E), \iota)$ such that:
+    \begin{enumerate}
+        \item $\complex(E)$ is a TVS over $\complex$.
+        \item $\iota: E \to \complex(E)$ is a continuous $\real$-linear map. 
+        \item[(U)] For any pair $(F, T)$ satisfying (1) and (2), there exists a unique continuous $\complex$-linear map $\complex(T): \complex(E) \to F$ such that the following diagram commutes:
+        \[
+        \xymatrix{
+        \mathbb{C}(E) \ar@{->}[r]^{\mathbb{C}(T)} & F \\
+        E \ar@{->}[u]^{\iota} \ar@{->}[ru]_{T} & 
+        }
+        \]
+        \item $\complex(E) = \iota(E) \oplus i\iota(E)$ as a TVS over $\real$.
+    \end{enumerate}
+
+    The pair $(\complex(E), \iota)$ is the \textbf{complexification} of $E$ as a topological vector space, and
+    \begin{enumerate}[start=4]
+        \item If $E$ is locally convex, then so is $\complex(E)$. 
+        \item If $E$ is normed, then $\complex(E)$ is normable, and there exists a norm $\norm{\cdot}_{\complex(E)}: \complex(E) \to [0, \infty)$ such that $\iota: E \to \complex(E)$ is isometric. 
+        \item[(F)] For any vector space $F$ over $\real$ and continuous $\real$-linear map $T: E \to F$, there exists a unique continuous $\complex$-linear map $\complex(T): \complex(E) \to \complex(F)$ such that the following diagram commutes:
+        \[
+        \xymatrix{
+        \mathbb{C}(E) \ar@{->}[r]^{\mathbb{C}(T)} & \mathbb{C}(F) \\
+        E \ar@{->}[u]^{\iota} \ar@{->}[r]_{T} & F \ar@{->}[u]_{\iota}
+        }
+        \]
+
+        which is given by
+        \[
+        \complex(T)(x + iy) = Tx + iTy
+        \]
+    \end{enumerate}
+    
+\end{definition}
+\begin{proof}
+    (1), (2): Let $(\complex(E), \iota)$ be the complexification of $E$ as a vector space, and equip it with the \hyperref[direct sum]{definition:tvs-direct-sum} topology. 
+
+    (U): By (U) of the \hyperref[complexification]{definition:complexification}, there exists a $\complex$-linear map $\complex(T): \complex(E) \to F$ such that the given diagram commutes. Since $T \circ \iota$ and $iT \circ \iota$ are continuous, $T$ is continuous by (U) of the \hyperref[direct sum]{definition:tvs-direct-sum}.
+
+    (4): By \autoref{proposition:finite-lc-product}, the direct sum and product of finitely many locally convex spaces coincide. By \autoref{proposition:lc-projective-topology}, this topology is locally convex. 
+
+    (5): Let $\norm{\cdot}_E: E \to [0, \infty)$ be the norm of $E$, and define
+    \[
+    \norm{\cdot}_{\complex(E)}: \complex(E) \to [0, \infty) \quad (x, y) \mapsto \sup_{\theta \in [0, 2\pi]}\norm{\cos(\theta)x + \sin(\theta)y}_E
+    \]
+
+    then for any $\phi \in [0, 2\pi]$ and $x, y \in E$, 
+    \begin{align*}
+        \normn{e^{i \phi}(x, y)}_{\complex(E)} &= \normn{(\cos(\phi)x - \sin(\phi)y, \sin(\phi)x + \cos(\phi)y)}_{\complex(E)} \\
+        &= \sup_{\theta \in [0, 2\pi]}\norm{\cos(\theta - \phi)x + \sin(\theta - \phi)y}_E \\
+        &= \norm{(x, y)}_{\complex(E)}
+    \end{align*}
+
+    so $\norm{(x, y)}_{\complex(E)}$ is a norm. For any $x \in E$, 
+    \[
+    \norm{\iota x}_{\complex(E)} = \sup_{\theta \in [0, 2\pi]}\norm{\cos(\theta)x}_E = \norm{x}_E \\
+    \]
+
+    Therefore $\iota: E \to \complex(E)$ is isometric. 
+
+    (F): By (U) applied to $\iota \circ T$.
+\end{proof}