Formal power series (Q5916404)

Power series are familiar to people working in theoretical computer science, since they are accustomed to considering such series with arbitrary exponents and coefficients, and they know what the series notation means: the distributivity of the multiplication over the infinite sum. Here, we will be interested in the ring structure the set of all series can be provided with, and not in anything which is connected with series considered as functions, such as the notions of kernel or of rank. Nor will we be interested in the individual series -- recognizing whether a series is rational or not is not our problem -- but in the algebraic global structure consisting of the ring of all power series together. We are going to define abstractly formal power series rings and fields. They will be equipped with an additional structure, defined by a valuation, a structure which is slightly richer than a topology compatible with the ring structure. The main question will be the decidability of these structures. In some nice cases, the decidability of the ordered group of the exponents and of the field of constants will imply this decidability. This is in fact the famous Ax-Kochen-Ershov Theorem, which we will present. The existence of a decision algorithm will remain theoretical here. There are some partial results concerning decision algorithms, but here we are not going to talk about effective decision procedures. We will also use the intuition provided by power series to present the notion of saturation and ultraproducts.