Formal group law
In mathematics, a formal group law is (roughly speaking) the formal power series analogue of a Lie group. Given a Lie group G and a chart around its identity element e, such that e is given coordinates (0, 0, ..., 0), the group operation in G is some function
- F(x1,x2, ..., xn,y1,y2, ..., yn)
where n is the dimension of G, taking values in Rn. Suppose we take the power series expansion of F (formal Taylor series) and look at the identities it should satisfy on the basis of the group axioms - for example the associative law (for the inverse operation take also an expansion of the inverse mapping I). Then we can turn these power series identities into a fresh definition, of a formal group law (often just formal group) in n variables.
The nature of a 'formal group' is not therefore as a group in the set-theoretic sense: it is more like the bare definition
- F(x,y) = x + y + xy
that comes from thinking about multiplication near 1. It is not either a group object in the sense of category theory (as a Lie group is). It does provide an actual group when the variable x is given values in a ring such as
- R[t]/(tk), for k = 1, 2, ...
for which convergence is guaranteed since t has been forced to be nilpotent. There is an abstract sense in which the formal group here is an inverse limit of group schemes; or a functor from artinian R-algebras to groups.
There was early work on formal groups of elliptic curves by Lutz; the idea later became important in the classification of abelian varieties in non-zero characteristic. The theory was also much used in algebraic topology in the 1960s, after it was seen that it played a role in homology theory. To be precise, cobordism theory needed the universal one-dimensional formal group over Z, the existence of which had been proved by Lazard.