Context
Algebra
- algebra, higher algebra
- universal algebra
- monoid, semigroup, quasigroup
- nonassociative algebra
- associative unital algebra
- commutative algebra
- Lie algebra, Jordan algebra
- Leibniz algebra, pre-Lie algebra
- Poisson algebra, Frobenius algebra
- lattice, frame, quantale
- Boolean ring, Heyting algebra
- commutator, center
- monad, comonad
- distributive law
Group theory
Ring theory
Module theory
Contents
Definition
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).
As adic completions
Let be a commutative ring, and let be the polynomial ring on one indeterminant . Then is a maximal ideal in , and results in an adic topology on . The ring of formal power series in is the adic completion of the limit of the quotient of by powers of :
The ring of formal power series for multiple indeterminants is constructed iteratively: because is a commutative ring, one could construct the polynomial ring on the indeterminant . As above, is a maximal ideal in with a corresponding adic topology, and one can then take the adic completion
The resulting commutative ring is usually just written as .
Examples
Polynomials
For a natural number , a power series such that for all is a polynomial of degree at most .
Taylor series
MacLaurin series
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.
Laurent series
Puiseux series
Properties
- An element in is (multiplicatively) invertible iff is invertible.
This follows easily from the observation that we can invert for any power series by forming and collecting only finitely many terms in each degree. As a simple corollary,
- If is a local ring, then the power series ring is also a local ring.
Functional substitution and inversion
Proposition
equipped with the ideal is the free adic -algebra on generators, in the sense that it is the value of the left adjoint to the forgetful functor
as applied to the set .
Proof
The idea is that for each adic -algebra and element , there is a unique adic algebra map that sends to ; this adic algebra map sends a power series to the sequence of truncations
belonging to .
It follows that we may define a clone or cartesian operad as follows: the component is the set which is the monad value . Letting denote the monad , with monad multiplication , and the set , the clone multiplication
is the composition of the maps
The clone multiplication thus defined is called substitution of power series; it takes a tuple consisting of to a power series denoted as
The resulting clone or operad yields, in the particular case , an associative substitution operation
with the power series .
Proposition
The group of invertible elements in the substitution monoid consists of power series of the form where is multiplicatively invertible in the ring .
In other words, we can functionally invert a power series provided that the linear coefficient is invertible in .
Proof
Given power series and , we may read off coefficients of the composite as
where in particular . Now is the left functional inverse of , or is the right inverse of , if , i.e., if if and otherwise. The first equation says simply which implies is invertible. Conversely, if is multiplicatively invertible and , then the equations
may be uniquely solved for the remaining 's given the 's, and uniquely solved for the remaining 's given the 's, by an inductive procedure: for we have
and this allows us to solve for ,
given the values and earlier -values for given by inductive hypothesis. Similarly we can solve for in terms of given coefficients and earlier -values , . Thus every power series has a right inverse if exists, and has a left inverse if exists, and this completes the proof.
Is a principal ideal domain over a field
If is a field then the nonzero ideals of the power series ring are entirely of the form :
Lemma
(ideals of a power series ring over a field) let be a field and let be a nonzero ideal of the algebra of power-series over . There is such that .
Proof
let be a nonzero element of chosen to satisfy
-
where .
-
for each nonzero ,
where for a given nonzero element in ,
Such an element exists since, if is any nonzero element of satisfying the second property, then we can set
Define a sequence by induction on satisfying the inductive hypothesis that for such that
-
-
For the case in which , set .
For the inductive case, suppose that for some we have defined satisfying for such that
-
-
Then for such that
-
-
This concludes the construction of the elements
Next consider the sequence
and consider that
for . This identity implies that
is well defined.
For each , agrees with through degree . The coefficients of and agree in every degree, so .
This shows that for , hence .
Since , .
If , then by minimality of , . Hence for some . So . So .
It follows from this argument that for some .
It follows from this argument that is a principal ideal domain for any field .
One way to define the formal differentiation operator, as a function , is via the usual formula
Then is an -linear function on which satisfies the Leibniz rule, meaning that it is a derivation and is a differential algebra.
Here is a conceptual story underlying the formalism. Let be the representing object for derivations (the “ring of dual numbers”). Let be the unique topological -algebra map (under the -adic topologies described above) that sends to . (If it helps, think .)
Definition
For , the derivative is the unique element of satisfying
We leave as an exercise the proof that the two definitions of derivative match:
(Hint: the restriction of to is by construction a derivation such that , and by induction. This induces derivations on quotient algebras , satisfying the same formula. Then pass to the inverse limit.)
Proposition
(Chain rule) For and ,
See here for a conceptual proof, using the universal property of adic completion.
Relatedly but in a slightly different direction, we can consider differentiation in coalgebraic terms. Suppose the commutative ring is a commutative algebra over (thus permitting division by nonzero integers). Then the set may be identified with the terminal coalgebra of the endofunctor via the map
whereby the coalgebra structure on ,
corresponds to
One may then apply coinductive techniques to prove various facts. One illustration is given here, where coinduction on power series is used to prove the general binomial theorem
where, remarkably, is an arbitrary element of .
Ring of power series as rings with infinitesimals
Purely real and purely infinitesimal elements
Suppose that is a Archimedean ordered field and is the ring of power series in . Since is a local ring, the quotient of by its ideal of non-invertible elements is the residue field itself, and the canonical function used in defining the quotient is the function which takes a number to its purely real component and takes . Since is an ordered -algebra, there is a strictly monotone ring homomorphism . An element is purely real if , and an element is purely infinitesimal if it is in the fiber of at . Zero is the only element in which is both purely real and purely infinitesimal.
Analytic functions
Suppose that is a sequentially Cauchy complete Archimedean ordered field with lattice structure, and is the ring of power series of . Then analytic functions are each definable on using the algebraic, order, metric, and convergence structure on .
The ring homomorphism preserves analytic functions: given a natural number and a purely infinitesimal element , then for every analytic function , there is a function such that for all elements , and
References
A formalization in homotopy type theory and there in Coq is discussed in section 4 of
The discussion of the differentiation of a converging power series term by term is at