Exponential diffeomorphism for simply connected nilpotent Lie groups

By [L1], every term of BCH above some bracket length is zero. Thus $x\ast y=\mathrm{BCH}(x,y)$ is a polynomial map on the entire vector space $\mathfrak{n}$. On a neighborhood of $(0,0)$ it agrees with multiplication in exponential coordinates by [L2]. Both expressions $(x\ast y)\ast z$ and $x\ast (y\ast z)$ are polynomial maps, and they agree on a nonempty open neighborhood of $(0,0,0)$; their coordinate polynomials therefore agree everywhere. Hence $\ast$ is associative globally.

The formal BCH identities give $x\ast 0=0\ast x=x$ and $x\ast (-x)=0$; alternatively they hold locally by [L2] and then globally by the same polynomial-identity argument. Thus the vector space with $\ast$ is a real Lie group $B$. Its underlying manifold is ${\mathbb{R}}^{\dim \mathfrak{n}}$, hence connected and simply connected. The quadratic commutator term of BCH is the original bracket, so $\mathrm{Lie}(B)=\mathfrak{n}$.

For fixed $x$, all brackets involving only $x$ vanish, so $(sx)\ast (tx)=(s+t)x$. Hence $t\mapsto tx$ is the one-parameter subgroup of $B$ tangent to $x$, and [L4] gives ${\exp }_B(x)=x$.

Apply [L3] to the identity map on $\mathfrak{n}$ to obtain homomorphisms $F:B\to N$ and $Q:N\to B$. Both composites have identity differential, so uniqueness in [L3] makes them the identity homomorphisms. Thus $F$ is a Lie-group isomorphism. Homomorphisms preserve one-parameter subgroups, so $F(x)=F({\exp }_{B}x)={\exp }_{N}x$ by step 1.3. Therefore ${\exp }_N=F$ is a diffeomorphism and transports multiplication to the stated BCH polynomial. For $\mathfrak{n}=0$, all groups and maps are one-point objects. Countable choice is used exactly through [L2]–[L4].