\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$. For each $z \in \complex(E)$ with $z = x + iy$, $x = \text{Re}(x)$ and $y = \text{Im}(y)$ are the \textbf{real} and \textbf{imaginary parts} of $z$. 
    \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}[Complex Conjugation]
\label{definition:complex-conjugation}
    Let $E$ be a vector space over $\complex$ and $*: E \to E$ be a $\real$-linear map, then $*$ is a \textbf{complex conjugation} if:
    \begin{enumerate}
        \item[(C1)] For each $\lambda \in \complex$, $(\lambda x)^* = \ol \lambda x^*$. 
        \item[(C2)] For each $x \in E$, $x^{**} = x$. 
    \end{enumerate}

    In which case, $\text{Re}(E) = \bracs{x \in E| x^* = x}$ is the \textbf{real part} of $E$. 
\end{definition}

\begin{proposition}
\label{proposition:complex-conjugation-properties}
    Let $E$ be a vector space over $\complex$ and $*: E \to E$ be a complex conjugation, then:
    \begin{enumerate}
        \item $E = \complex(\text{Re}(E))$. 
        \item For each $x \in E$, 
        \[
        \text{Re}(x) = \frac{x + x^*}{2} \quad \text{Im}(x) = \frac{x - x^*}{2i}
        \]
        \item For each $x \in E$, $x^* = \text{Re}(x) - i\text{Im}(x)$. 
    \end{enumerate}
\end{proposition}
\begin{proof}
    (2): By properties of the complex conjugation, $\text{Re}(x), \text{Im}(x) \in \text{Re}(E)$. 

    (1): For any $x, y \in \text{Re}(x)$ with $x = iy$, $x = -iy$ as well by (2) of the complex conjugation, so $x = y = 0$. Thus if $z = x + iy = x' + iy'$, then $x = x'$ and $y = y'$, and the decomposition is unique. 
    
\end{proof}

\begin{definition}[Hermitian]
\label{definition:hermitian-functional}
    Let $E$ be a vector space over $\real$, $*: \complex(E) \to \complex(E)$ be the canonical complex conjugation map, and $\phi \in \hom(\complex(E); \complex)$, then the following are equivalent: 
    \begin{enumerate}
        \item $\phi|_E \in \hom(E; \real)$.
        \item For each $x \in E$, $\dpn{x, \phi}{\complex(E)} = \ol{\dpn{x^*, \phi}{\complex(E)}}$. 
    \end{enumerate}

    If the above holds, then $\phi$ is \textbf{Hermitian}.     
\end{definition}






\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}