Today we’ll start our long journey on the definition of the ring of Witt vectors. Our first step will be to think about formal group laws, since this will be useful to us for things I have planned later on (the formal groups attached to varieties in positive characteristic).
Let be commutative ring with . Then a one-dimensional formal group law over is just a formal power series in two variables of the form that satisfies “associativity”. This means that .
A key thing is that the power series has no constant term. We call the ring equipped with this a (one-dimensional) formal group. This terminology makes some sense considering it is sort of giving a group operation on , but since these are just formal series, we may not have convergence when plugging actual elements of in.
The formal group is called commutative if .
Here are two easy examples to see that this is really quite concrete. The additive formal group is using and the multiplicative formal group uses . They are both commutative. We’ll suggestively write and .
Let’s not shy away from positive characteristic, since that will be our main usage of formal groups in the future. We have a nice non-commutative formal group on where given by .
Now we can get honest groups out of our formal groups. Suppose is a formal group law on , then we can consider power series in one variable with no constant term. We take this just as a set, so given , it makes sense to do , so we’ll define . This turns our set into an honest group which we denote .
But why are there inverses? We need some sort of lemma that says: given any formal group law over there is a power series such that . This is just a special case of what is known as the “Formal Implicit Function Theorem”.
With an eye towards our goal of the Witt vectors , we’ll just say here that is the underlying additive group of the ring of Witt vectors over .