Added lemmas on the identity component of the general linear group.

src/op/banach/fc.tex

@@ -123,5 +123,30 @@
     By \hyperref[Runge's Theorem]{corollary:runge-rational-approximation} again and continuity of the holomorphic functional calculus, the above also holds for all $f \in H(\sigma_A(x); \complex)$ and $g \in H(f(\sigma_A(x)); \complex)$. 
 \end{proof}
 
+\begin{proposition}
+\label{proposition:functional-calculus-exp}
+    Let $A$ be a unital Banach algebra and $x \in A$, then
+    \begin{enumerate}
+        \item $\exp(x) = \sum_{n = 0}^\infty \frac{x^n}{n!}$. 
+        \item $\exp(x) \in G_0(A)$ with $\exp(x)^{-1} = \exp(-x)$. 
+        \item For any $y \in A$ commuting with $x$, $\exp(x + y) = \exp(x)\exp(y)$. 
+        \item Let $\ell: \complex \setminus (\infty, 0] \to \complex$ be the principal logarithm. If $\sigma_A(x) \subset \bracs{\lambda \in \complex| \text{Im}(\lambda) \in (-\pi, \pi)}$, then $\ell(\exp(x)) = x$. 
+    \end{enumerate}
+\end{proposition}
+\begin{proof}
+    (1): By the power series representation of $\exp(x)$ and continuity of the holomorphic functional calculus. 
+
+    (2): By the homomorphism property of the functional calculus, $\exp(x)^{-1} = \exp(-x)$. Thus $\exp(x)$ is connected to $1$ by the path $t \mapsto \exp(tx)$. 
+
+    (3): Since the exponential is an entire function, the following series converges absolutely, and is eligible for arbitrary manipulations: 
+    \begin{align*}
+        \exp(x)\exp(y) &= \sum_{n = 0}^\infty \sum_{k = 0}^\infty \frac{x^ny^k}{n!k!} = \sum_{n = 0}^\infty \sum_{k = 0}^n \frac{x^ky^{n-k}}{k!(n-k)!} \\
+        &= \sum_{n = 0}^\infty \frac{1}{n!}\sum_{k = 0}^n {n \choose k}x^ky^{n-k} \\
+        &= \sum_{n = 0}^\infty \frac{(x + y)^n}{n!} = \exp(x + y)
+    \end{align*}
+    
+    
+    (4): By the \hyperref[Spectral Mapping Theorem]{theorem:spectral-mapping-holomorphic}. 
+\end{proof}
 
 

src/op/banach/igroup.tex

@@ -19,6 +19,20 @@
     (2): For each $x \in G(A)$, $xG_0(A)$ is connected, closed, and open, so it is a connected component by \autoref{lemma:union-connected-components}. 
 \end{proof}
 
+\begin{proposition}
+\label{proposition:log-identity-component}
+    Let $A$ be a unital Banach algebra and $x \in A$. If there exists $\theta \in [0, 2\pi)$ such that
+    \[
+    \sigma_A(x) \subset \complex \setminus e^{i\theta}[0, \infty)
+    \]
+
+    then $x \in G_0(A)$. 
+\end{proposition}
+\begin{proof}
+    Since there exists a branch of the logarithm $\ell: \complex \setminus e^{i\theta}[0, \infty) \to \complex$, there exists $y \in A$ such that $x = \exp(y)$. In which case, $x \in G_0(A)$ by \autoref{proposition:functional-calculus-exp}. 
+\end{proof}
+
+
 % Note: this setup appears to work in general topological groups. There does not seem to be any payoffs as of now.
 % However, should there be any, the proof should be improved to avoid the path argument.