Is it possible to construct a formal group law from a Lie group without choosing coordinates? There is a three-way correspondence between:


*

*Real (connected and simply connected) Lie groups of dimension $n$;

*$\mathbb R$-Lie algebras of dimension $n$;

*Formal group laws in $n$ variables over the reals.


To get from the first to the second, one only really needs the fact that manifolds have tangent spaces which are vector bundles, and that the tangent space functor is strong (so that one can talk about left-invariant vector fields).
To get from the second to the third, one uses the Baker--Campbell--Hausdorff formula, which in the realm of formal power series is pure abstract algebra. 
However, the only way I know of getting from the first to the third directly involves choosing analytic coordinates around the identity and Taylor expanding the Lie group multiplication.
My question is: can one give a direct geometric construction of a formal group law out of a Lie group without choosing coordinates? The sort of thing I had in mind might, for example, involve using jet bundles. 
 A: Sure: if $G$ is the given analytic group then consider the functor $F$ on finite local $\mathbf{R}$-algebras with residue field $\mathbf{R}$ given by defining $F(A)$ to be the set of maps of real-analytic spaces ${\rm{Sp}}(A) \rightarrow G$ "based" at the identity.  This is a group-valued functor, and it is visibly pro-represented by the completion $O_{G,e}^{\wedge}$ of the noetherian analytic local ring $O_{G,e}$ of $G$ at the identity $e$.  The group law on the functor thereby defines a group-object structure on the formal scheme Spf($O_{G,e}^{\wedge}$), or more specifically defines a formal Hopf algebra structure on $O_{G,e}^{\wedge}$ (i.e., a map $m^{\ast}:O_{G,e}^{\wedge} \rightarrow O_{G,e}^{\wedge} \widehat{\otimes} O_{G,e}^{\wedge}$ satisfying the usual conditions). 
Voila, that's it.  The same procedure works for analytic groups over non-archimedean fields in char. $p > 0$ (such groups might not be smooth, so "local coordinates" might not even exist, yet the method still works), as well as for group schemes of finite type over any field, and so on.  No need for Lie algebras or a BCH formula. The notion of "formal group" makes good sense in terms of complete local noetherian rings even without any notion of formal smoothness (so no "local coordinates").
A: Of course if one wants to avoid coordinates then one should replace formal group laws by the coordinate-invariant things that they are the coordinate-dependent versions of! 
There are two dual ways to do this that I know of.
Commutative: First, observe that an $n$-dimensional formal group law over $k$ is precisely a comultiplication on $k[[x_1, ..., x_n]]$ (with respect to a suitably completed tensor product) with counit the map that kills all terms of positive degree and antipode the map that multiplies each monomial by $(-1)^{\text{deg}}$. This gives $k[[x_1, ..., x_n]]$ the structure of a commutative Hopf algebra (in a suitable category of power series algebras equipped with a suitably completed tensor product) and now we can ask how to construct this Hopf algebra from $G$. This can be done by considering the completion of the algebra of germs of smooth functions at the identity of $G$ with respect to the ideal generated by the germs vanishing at the identity. The comultiplication is induced from the multiplication $G \times G \to G$ via pullback of germs.
Cocommutative: First, recall that if $\mathfrak{g}$ is a Lie algebra then the universal enveloping algebra $U(\mathfrak{g})$ is naturally a cocommutative Hopf algebra. In fact over a field of characteristic zero the functor $\mathfrak{g} \mapsto U(\mathfrak{g})$, when regarded as taking values in Hopf algebras, is full; by PBW $\mathfrak{g}$ is precisely the Lie algebra of primitive elements of $U(\mathfrak{g})$. Hence we should be able to identify Lie algebras with a certain full subcategory of Hopf algebras. 
Theorem (Cartier): Let $k$ be a field of characteristic zero. A Hopf algebra over $k$ is isomorphic to the universal enveloping algebra $U(\mathfrak{g})$ of a Lie algebra over $k$, namely its Lie algebra of primitive elements, if and only if it is cocommutative and conilpotent. 
The definition of conilpotence is mildly involved but see, for example, Cartier's A primer of Hopf algebras. 
Now I claim that $U(\mathfrak{g})$ should be seen as a version of the formal group law associated to $\mathfrak{g}$. The reason is that as a Hopf algebra it is dual in a suitable sense to the Hopf algebra above. So Cartier's theorem should be seen as a coordinate-independent version of the correspondence between Lie algebras and formal group laws which in particular does not require Baker-Campbell-Hausdorff. 
It remains to figure out how to get $U(\mathfrak{g})$ directly from $G$, and the answer is the following:
Theorem (Schwartz): $U(\mathfrak{g})$ can naturally be identified with distributions on $G$ supported at the identity. 
(The dual pairing between the two Hopf algebras above is then the natural pairing between distributions supported at the identity and germs at the identity.)
