Theorem
Equivalence between Lie algebras and formal groups
Over a characteristic-zero field, finite-dimensional Lie algebras are equivalent to formally smooth formal groups on finite formal discs.
Statement
Let be a field of characteristic . Let be the category of finite-dimensional Lie algebras over , and let be the category of formal groups over whose pointed underlying formal scheme is isomorphic to a finite-dimensional formal disc . Then the tangent functor
is an equivalence of categories.
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 , take the formal completion of its underlying affine space at . On formal points define
where is the universal completed Lie series. Characteristic zero allows all its rational coefficients. The formal BCH identity gives associativity, is the identity, and is the inverse.
A Lie algebra homomorphism preserves every iterated bracket, hence every homogeneous BCH term, so it gives a formal group homomorphism. This constructs a functor
quasi-inverse to .
Coordinate formal-group-law corollary
After choosing coordinates on each formal disc, formal groups become formal group laws. Therefore the category of finite-dimensional, possibly noncommutative formal group laws over , with formal-group-law morphisms, is also equivalent to . Its tangent functor takes
to the bracket .
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 one-dimensional formal group law over a characteristic-zero field is isomorphic to the additive law, and every commutative one-dimensional law has its more explicit formal logarithm. 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. Fundamental 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 : tangent brackets do not see height, Frobenius, or the full -series.
- Pronilpotent and complete filtered Lie algebras admit broader BCH correspondences, but they require their own completeness hypotheses and are not part of this finite-dimensional statement.
References
- A. Fröhlich, Formal Groups, Lecture Notes in Mathematics 74, Springer, 1968. Publisher record. Relevant: Chapter 2, Lie theory.
- Nicolas Bourbaki, Lie Groups and Lie Algebras: Chapters 1–3, Springer, 1989. Publisher record. Relevant: Chapter 2, formal exponential, logarithmic, and Hausdorff series.
- Michiel Hazewinkel, Formal Groups and Applications, AMS Chelsea Publishing, 2012. AMS book record. Relevant: Chapter 2 and the Lie-theory portion of the text.