What is the “universal enveloping algebra” of a formal group law?

I posted earlier a query toward exploring the analogy between

smooth algebraic groups over $\mathbb{R}$ or $\mathbb{C}$ ::  Lie algebras

smooth algebraic groups over R (any commutative ring) ::  Formal group law

in which I tried to answer this question, and ended up with “the Lazard ring doesn’t quite work,” which makes sense in retrospect, as the Lazard ring is not associated with any particular formal group law. When I say “formal group law” I mean “1-d formal group law.”

What is a formal group law? It’s an expression of the group structure of G in an infinitesimal neighborhood of the origin. At the Midwest Topology Seminar, talking with Paul V. and Dylan Wilson, I have a somewhat more satisfying answer.

What is a Lie algebra? It’s an expression of the group structure of $G$ at the FIRST infinitesimal neighborhood of the origin. In characteristic 0, this extends to a definition of the group structure in an infinitesimal neighborhood of the origin by the Baker Campell Hausdorff  formula.

Specifically, what is the universal enveloping algebra of a formal group law? It’s the formal group law itself! Well, more specifically:

Universal enveloping algebra :: Lie algebra

Functions on Formal group law  :: Formal group law

According to wikipedia, “The universal enveloping algebra of the free Lie algebra generated by X and Y is isomorphic to the algebra of all non-commuting polynomials in X and Y. In common with all universal enveloping algebras, it has a natural structure of a Hopf algebra, with a coproduct Δ. The ring S used above is just a completion of this Hopf algebra.”

A formal group law already has a Hopf algebra structure. This is just the cogroup on formal power series $R[[x]]$ induced by the formal group law, $f$, that is,

$$R[[x]] \to R[[x]] \widehat{\otimes} R[[x]]$$

$$x \mapsto f(1 \otimes x, x \otimes 1)$$

This is already complete! We’re a formal group law so we’re already completed at the origin! And, if we are a 1-d formal group law, we’re always commutative (unless our ring is nilpotent), so this is promising.