Reference request: equivalence of formal group laws and Lie algebras in characteristic zero

Let $k$ be a field of characteristic zero. Wikipedia states that the natural functor from finite-dimensional formal group laws over $k$ to finite-dimensional Lie algebras over $k$ is an equivalence of categories but does not provide a reference, and I'm not sure where to find one. Does anyone know of one?

(Not really sure how to tag this. I am not necessarily interested in any particular application.)

-

This follows from the Baker--Campbell--Hausdorf formula. Serre's lecture notes on Lie algebras and Lie groups should cover it.

-
This seems plausible, but I'd like to see the details written down, and Serre doesn't seem to actually explicitly state and prove this; he discusses BCH in a sufficiently general context but doesn't mention formal group laws until later, and when he does he only says, somewhat mysteriously, "it will be useful to know that we have an equivalence of categories." – Qiaochu Yuan Feb 12 '11 at 22:12
Dear Qiaochu, You can probably work out the details for yourself: Given a Lie algebra, the BCH formula lets you construct a formal group. (The denominators are harmless since we are in char. 0 by assumption.) Conversely, given a formal group, you can certainly form its Lie algebra. The derivation of the BCH formula ensures that these functors a mutually quasi-inverse. Writing down the details is essentially an exercise (unless I am missing a subtlety, but I don't think that I am.) Best wishes, Matthew – Emerton Feb 13 '11 at 3:02
@Emerton: upon reading the question, this was going to be my response as well. Also like you, I am 99% sure (but not 100% sure) that filling in the details here is straightforward. It might be worth it for Qiaochu (or someone else) to post an answer from the perspective of elaborating on Serre's book. – Pete L. Clark Feb 13 '11 at 7:14
Works for me. I guess I just needed to be reassured that this was straightforward. – Qiaochu Yuan Feb 13 '11 at 15:55

As indicated by Serre's reference list, a basic source of ideas about formal group laws would be the papers by Michel Lazard in the period 1955-1965. Just do a quick search in www.numdam.org using his last name. One of his shorter papers is Sur les groupes de Lie formels à un paramètre. Bulletin de la Société Mathématique de France, 83 (1955), p. 251-274. But I'm not sure these papers will be explicit enough to answer your question completely. Lazard was especially interested in dealing with $p$-adic fields, while Dieudonne dealt further with fields of prime characteristic. Certainly Lazard did more than anyone else to establish the abstract foundations of formal group laws.

Another possibly more readable source would be Bourbaki's Groupes et algebres de Lie, Chapters II-III (especially Chapter II) together with the historical notes at the end of that volume. Here in particular the connections with work of Dynkin and others, along with the Baker-Campbell-Hausdorff formula, are emphasized.

ADDED: I think Emerton's brief answer and the added comments essentially answer the original question; but I wanted to point to the broader background sources as well. Serre's 1965 lecture notes Lie Algebras and Lie Groups (Benjamin) end up in Chapter V of Part II at Lie Theory, with the initial convention: "Unless otherwise specified, $k$ will denote a field complete with respect to a non-trivial absolute value." In some places it is required that $k$ be of characteristic 0; then it may be allowed to be just a $\mathbb{Q}$-algebra. For some classical Lie theory, $k$ is assumed to be the real or complex field. But much is also done with analytic groups over ultrametric fields, etc. So it's important to keep track of which kind of base ring or field you are working over.

Theorem 3 on page 5.28 is the theorem in question here. Serre gives a complete proof but relies heavily on previous material. By now he is making a distinction between the "formal" case and the "analytic" case; it's essential to be in the "formal" case when you want to work over an arbitrary field of characteristic 0. With these qualifications, I'd agree that for Theorem 3 a relatively intuitive proof is possible avoiding much of the surrounding "analytic" material.

-
Unfortunately my mathematical French is not yet good enough for either of these... – Qiaochu Yuan Feb 12 '11 at 23:37
This is unfortunately rather a "French" subject. By the way, Lazard's short Bourbaki seminar talk Groupes analytiques en caractéristique 0. Séminaire Bourbaki, 2 (1951-1954), Exposé No. 76, may come very close to answering your question, I think. On the other hand, the relevant Bourbaki books have been published by Springer in English translation. – Jim Humphreys Feb 12 '11 at 23:40