A formal Lie correspondence

TL;DR

This paper establishes a categorical equivalence between formally nilpotent Lie algebras and exponential groups in characteristic zero, extending classical results and applying to formal series automorphisms.

Contribution

It generalizes and extends the equivalences of Mal'cev, Lazard, Quillen, and Warfield to a broader class of groups and Lie algebras, with applications to equations and definability in formal series groups.

Findings

Established a categorical equivalence between formally nilpotent Lie algebras and exponential groups.

Extended classical Lie correspondence results to new contexts involving formal series automorphisms.

Provided applications to solving equations and definability in groups of formal series.

Abstract

We establish an equivalence between categories of 'formally nilpotent' Lie algebras and exponential groups in characteristic zero. It extends the equivalences of Mal'cev, Lazard, Quillen and Warfield, and applies to groups under composition of generalized formal series or automorphisms of algebras of generalized formal series. We obtain first-order transfer results from finite dimensional nilpotent objects to formally nilpotent ones. We give applications to solving equations over groups, to the theory of nilpotent exponential groups as per Miasnikov-Remeslennikov, and to definability problems in certain groups of formal series.