A formal group law over a commutative ring $R$, (by nLab) is a sequence of power srires
$$
f_1,…,f_n\in R[[x_1,…,x_n,y_1,…,y_n]]
$$
such that, using the notation
$$
x=(x_1,…,x_n),y=(y_1,…,y_n),f=(f_1,…,f_n)
$$
we have
$$
f(x,f(y,z))=f(f(x,y),z)
$$
$$
f(x,y)=x+y+\text{higher order terms}
$$
I understand vaguely the idea of a formal group law as a power series expansion of the group law of a lie group or an algebraic group (actual or hypothetical) in the neighborhood of the identity. But I would be happy to know, if only for psychological reasons, if this definition can be recovered as simply a group object in some category.
In the nLab entry about formal groups, it is written that formal group laws are one approach to formal groups, and the later is a group object in 'infinitesimal spaces', but I was unable to understand what is an infinitesimal space from the linked entry. I would appreciate if someone could explain this circle of ideas or point to the relevant literature.
Best Answer
A formal group law over a scheme $S$ is a group object in the category of framed formal schemes over $S$. Objects in this category are formal schemes $X$ over $S$ equipped with an $S$-isomorphism $X \to \operatorname{Spf} \mathscr{O}_S[[t_1,\ldots,t_n]]$ for some $n$.
There is a functor from framed formal schemes over $S$ to formal schemes over $S$, given by forgetting the $S$-isomorphism. The essential image is the category of formal Lie varieties over $S$. This functor takes formal group laws to the class of formal groups that admit a framing.