Let’s back up from all these definitions for now and see one situation in which all of these things just pop out. It also will show us where these names came from. Suppose is a smooth algebraic affine group scheme over . Then is represented by a finitely generated Hopf algebra, say . If is the augmentation ideal (i.e. ), then by smoothness we get that is free on the generators where is the number of generators of over .

Likewise is free and generated by monomials , thus if we take the completion with respect to the -adic topology, we get . Now notice that , and this is just the maximal ideal defining in the product. Thus the maps pass to the successive quotients, and we get an induced map on completions.

This is just . But any such map is completely described by where each of the get sent to. But they are sent to power series in variables! So we get power series in variables, namely . Notice these came from maps of Hopf algebras (not merely ring maps, otherwise this wouldn’t work), so tracing the coassociativity axiom we get precisely the associativity we need to say that these power series form a formal group law of dimension .

Even more importantly, we could have chosen different generators originally, and this would have changed the construction and given a different formal group law, but they are isomorphic. The isomorphism is just given by a change of variables. So given any smooth affine algebraic group scheme over we get a unique formal group up to isomorphism, and moreover (given appropriate other technical conditions we won’t discuss) there is actually an (anti)equivalence of categories between formal groups and Hopf algebras.

This is exactly how the formal group laws and were formed. We take the affine algebraic group scheme which is represented by , then . The completion is clearly and the map . Thus our one-dimensional additive formal group (scheme) is appropriately named, and it is just as easy to go through and check the multiplicative one gives the right law as well.

Now we see that these definitions of formal groups aren’t just arbitrary isolated things. They actually arise in practice. We will also see another important way in which they appear next time (or the time after) in defining new rings with particularly nice properties.

Lastly, we need to do one more thing that doesn’t really fit anywhere nicely. We started with one-dimensional formal groups, and then moved to arbitrary finite dimension, but really we can just keep going and define infinite dimensional in exactly the same way. If we have an index set , then take a collection of indeterminates indexed by . Define the formal power series ring to be all formal sums where runs through functions with finite support, and .

Now an infinite dimensional formal group law is a collection of elements which we write , and the usual conditions (higher degree) and and we need one extra finiteness condition that for only finitely many .

This may seem implausible to appear in practice, but there is a really simple example where you get this occuring. Take any ring , then we can form a new ring an infinite-dimensional polynomial algebra over . Then take just a single variable power series over this to get . Taking any two arbitrary elements with constant coefficient , we can multiply them: . We know the product has this form, and the form an infinite dimensional formal group law.

Reversing this process, we can define a multiplication given an infinite dimensional group law, and this is how we’ll define our new rings, including the Witt vectors.