Statement

Let kk be a field of characteristic 00. Let LieAlgkfd\mathbf{LieAlg}^{\mathrm{fd}}_k be the category of finite-dimensional over kk, and let FGrpkdisc\mathbf{FGrp}^{\mathrm{disc}}_k be the category of over kk whose pointed underlying formal scheme is isomorphic to a finite-dimensional Spfk[[X1,,Xn]]\operatorname{Spf}k[[X_1,\ldots,X_n]]. Then the

Lie:FGrpkdiscLieAlgkfd\operatorname{Lie}: \mathbf{FGrp}^{\mathrm{disc}}_k \longrightarrow \mathbf{LieAlg}^{\mathrm{fd}}_k

is an .

Equivalently, every finite-dimensional Lie algebra integrates to a formal group, every homomorphism of such Lie algebras integrates uniquely to a formal group homomorphism, and the isomorphism class of every formal group in this category is determined by its tangent Lie algebra. The isomorphism between two integrations need not be unique unless an isomorphism of their tangent Lie algebras has been specified; that specified map has a unique integrated isomorphism.

The BCH quasi-inverse

Given gLieAlgkfd\mathfrak g\in\mathbf{LieAlg}^{\mathrm{fd}}_k, take the formal completion of its underlying at 00. On formal points define

XY:=BCHg(X,Y),X*Y:=\operatorname{BCH}_{\mathfrak g}(X,Y),

where is the universal completed Lie series. Characteristic zero allows all its rational coefficients. The formal BCH identity gives associativity, 00 is the identity, and X-X is the inverse.

A preserves every iterated bracket, hence every homogeneous BCH term, so it gives a formal group homomorphism. This constructs a functor

BCH:LieAlgkfdFGrpkdisc\operatorname{BCH}: \mathbf{LieAlg}^{\mathrm{fd}}_k \longrightarrow \mathbf{FGrp}^{\mathrm{disc}}_k

quasi-inverse to Lie\operatorname{Lie}.

Coordinate formal-group-law corollary

After choosing coordinates on each formal disc, . Therefore the category of finite-dimensional, possibly noncommutative over kk, with formal-group-law morphisms, is also equivalent to LieAlgkfd\mathbf{LieAlg}^{\mathrm{fd}}_k. Its tangent functor takes

F(X,Y)=X+Y+B(X,Y)+O(3)F(X,Y)=X+Y+B(X,Y)+O(3)

to the bracket [u,v]=B(u,v)B(v,u)[u,v]=B(u,v)-B(v,u).

The coordinate formulation involves a choice of basis for an abstract tangent space; the intrinsic formal-group equivalence does not.

Commutative one-dimensional case

A one-dimensional Lie algebra is abelian. Consequently every over a characteristic-zero field is isomorphic to the additive law, and every has its more explicit . Integral and positive-characteristic forms are much richer because that logarithm may require unavailable denominators.

What the theorem does not say
  • It is not an equivalence between Lie algebras and global Lie groups. , disconnected components, lattices, and other global data disappear upon formal completion.
  • It does not classify arbitrary formal schemes carrying group structures; the underlying pointed object must be a finite-dimensional formally smooth formal disc.
  • It fails in characteristic p>0p>0: tangent brackets do not see height, Frobenius, or the full pp-series.
  • Pronilpotent and admit broader BCH correspondences, but they require their own completeness hypotheses and are not part of this finite-dimensional statement.
References
  1. A. Fröhlich, Formal Groups, Lecture Notes in Mathematics 74, Springer, 1968. Publisher record. Relevant: Chapter 2, Lie theory.
  2. Nicolas Bourbaki, Lie Groups and Lie Algebras: Chapters 1–3, Springer, 1989. Publisher record. Relevant: Chapter 2, formal exponential, logarithmic, and Hausdorff series.
  3. Michiel Hazewinkel, Formal Groups and Applications, AMS Chelsea Publishing, 2012. AMS book record. Relevant: Chapter 2 and the Lie-theory portion of the text.