Formal group law

In mathematics, a formal group law is (roughly speaking) a formal power series behaving as if it were the product of a Lie group. They were introduced by . The term formal group sometimes means the same as formal group law, and sometimes means one of several generalizations. Formal groups are intermediate between Lie groups (or algebraic groups) and Lie algebras. They are used in algebraic number theory and algebraic topology. A one-dimensional formal group law over a commutative ring R is a power series F(x,y) with coefficients in R, such that F(x,y) = x + y + terms of higher degree F(x, F(y,z)) = F(F(x,y), z) (associativity). The simplest example is the additive formal group law F(x, y) = x + y. The idea of the definition is that F should be something like the formal power series expansion of the product of a Lie group, where we choose coordinates so that the identity of the Lie group is the origin. More generally, an n-dimensional formal group law is a collection of n power series Fi(x1, x2, ..., xn, y1, y2, ..., yn) in 2n variables, such that F(x,y) = x + y + terms of higher degree F(x, F(y,z)) = F(F(x,y), z) where we write F for (F1, ..., Fn), x for (x1, ..., xn), and so on. The formal group law is called commutative if F(x,y) = F(y,x). If R is torsionfree, then one can embed R into a Q-algebra and use the exponential and logarithm to write any one-dimensional formal group law F as F(x,y) = exp(log(x) + log(y)), so F is necessarily commutative. More generally, we have: Theorem. Every one-dimensional formal group law over R is commutative if and only if R has no nonzero torsion nilpotents (i.e., no nonzero elements that are both torsion and nilpotent). There is no need for an axiom analogous to the existence of inverse elements for groups, as this turns out to follow automatically from the definition of a formal group law. In other words we can always find a (unique) power series G such that F(x,G(x)) = 0. A homomorphism from a formal group law F of dimension m to a formal group law G of dimension n is a collection f of n power series in m variables, such that G(f(x), f(y)) = f(F(x,y)).