Local logarithm on a Lie group

Assume ${\mathrm{A}\mathrm{C}}_{\omega }$, let $G$ be a finite-dimensional real Lie group with identity $e$, and write $\mathfrak{g}=T_{e}G$. Fix open neighborhoods $V\subseteq \mathfrak{g}$ of $0$ and $U\subseteq G$ of $e$ for which

${\exp }_G{\mathrm{\mid }}_V:V⟶U$

is the diffeomorphism supplied by The exponential map is a local diffeomorphism at zero. The local logarithm associated with $(V,U)$ is its smooth inverse

${\log }_G:U⟶V\mathrm{.}$

Thus ${\log }_G({\exp }_{G}X)=X$ for $X\in V$ and ${\exp }_G({\log }_{G}g)=g$ for $g\in U$. The neighborhoods are part of the notation: no value of ${\log }_G$ is asserted outside $U$, and no global logarithm is claimed.

Here ${\mathrm{A}\mathrm{C}}_{\omega }$ is countable choice. It is inherited exactly through the local-diffeomorphism supplier. Fixing one witness pair $(V,U)$ by existential instantiation is not a choice from a family and adds no choice principle.

The neighborhood $U$ contains $e$ and is nonempty. If $\dim G=0$, one may take $V=\{0\}$ and $U=\{e\}$ and the logarithm is the unique inverse; the definition is unchanged in dimension one. Open neighborhoods rather than closed intervals are involved, so there is no endpoint case. No metric or nondegeneracy condition occurs. The two inverse identities unpack the phrase "inverse map" and do not assert a biconditional characterization.