Algebras and modules
Model category presentations
Geometry on formal duals of algebras
A power series in a variable and with coefficients in a ring is a series of the form
where is in for each . Given that there are no additional convergence conditions, a power series is also termed emphatically as a formal power series. If is commutative, then the collection of formal power series in a variable with coefficients in forms a commutative ring denoted by .
More generally, a power series in commuting variables with coefficients in a ring has the form . If is commutative, then the collection of formal power series in commuting variables form a formal power series ring denoted by .
More generally, we can consider noncommutative (associative unital) ring and words in noncommutative variables of the form
(where has nothing to do with ) and with coefficient (here is a word of any length, not a multiindex in the previous sense). Thus the power sum is of the form and they form a formal power series ring in variables denoted by . Furthermore, can be even a noncommutative semiring in which case the words belong to the free monoid on the set , the partial sums are then belong to a monoid semiring . The formal power series then also form a semiring, by the multiplication rule
Of course, this implies that in a specialization, -s commute with variables ; what is usually generalized to take some endomorphisms into an account (like at noncommutative polynomial level of partial sums where we get skew-polynomial rings, i.e. iterated Ore extensions).
For a natural number , a power series such that for all is a polynomial of degree at most .
For a smooth function on the real line, and for denoting its th derivative its MacLaurin series (its Taylor series at ) is the power series
If this power series converges to , then we say that is analytic.
A formalization in homotopy type theory and there in Coq is discussed in section 4 of