Added the complex conjugation.

spec.toml

@@ -19,8 +19,8 @@ searchLimit = 16
 maxSearchPages = 48
 
 recentChanges = 10
-tableOfContentsDepth = 2
-tableOfContentsUnfoldDepth = 1
+tableOfContentsDepth = 3
+tableOfContentsUnfoldDepth = 2
 tableOfContentsShortDepth = 1
 
 hoverPreview = false

src/fa/tvs/complexify.tex

@@ -14,7 +14,7 @@
         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$. 
+        \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{Re}(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
@@ -54,6 +54,39 @@
     (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 For each $\lambda \in \complex$, $(\lambda x)^* = \ol \lambda x^*$. 
+        \item 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}
+        \]
+    \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}[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: