Formal Power Series

Coefficientwise addition inherits associativity, commutativity, zero, and additive inverses from $R$. For multiplication, the coefficient of both $(fg)h$ and $f(gh)$ at $n$ is the finite sum ${\sum }_{i+j+k=n}[x^i]f[x^j]g[x^k]h$ by finite Fubini. Reindexing $(i,j)$ as $(j,i)$ gives commutativity, and splitting finite sums gives both distributive laws. The constant series $1$ is a multiplicative identity, since the only nonzero summand involving it occurs at index $0$.

A product of finitely supported series is finitely supported, and its coefficient formula is exactly the published polynomial convolution. Hence $j$ preserves $0,1,+,$ and multiplication, so it is a unital ring homomorphism; it is injective because equality of coefficient functions is literal equality. Its image consists precisely of the finitely supported functions.

Therefore $R\mathrm{⟦}x\mathrm{⟧}$ is a commutative ring and $j$ identifies $R[x]$ with its finitely supported subring.

The two linearity identities are the pointwise definitions of addition and scalar multiplication. Equality of all extracted coefficients is equality of the underlying functions $\mathbb{N}\to R$, proving both directions of extensionality.

In the convolution for $x^{k}f$, the first factor has one nonzero coefficient, at $k$. It contributes $[x^{n-k}]f$ when $k\le n$ and there is no contributing index when $k>n$; for $k=0$ this says $1f=f$.

The last display is the defining finite convolution, whose $n=0$ instance is $[x^0](fg)=[x^0]f[x^0]g$.

Steps 1.1-1.3 establish every asserted clause and every listed boundary case.

Below the smaller of the two orders, both summand coefficients vanish, so the sum coefficient vanishes. This proves the sum inequality; if one order is strictly smaller, its leading coefficient cannot be cancelled by the other series.

If $p={\mathrm{ord}}_{x}f$ and $q={\mathrm{ord}}_{x}g$ are finite, every convolution summand in degree below $p+q$ has one zero factor. In degree $p+q$, only the pair $(p,q)$ can be nonzero, so the coefficient there is $[x^p]f[x^q]g$. If either series is zero, the stated inequality follows from the $+\mathrm{\infty }$ conventions.

Over a domain the product of the two nonzero leading coefficients is nonzero, so step 1.2 gives exact additivity. In particular two nonzero series have a nonzero product; $R\mathrm{⟦}x\mathrm{⟧}$ also has $1\mathrm{\ne }0$ because its constant coefficients are those of $R$.

Steps 1.1-2.1 prove all order laws and the domain conclusion, including zero factors.

Fix $N$. Only finitely many members of the family survive modulo $x^N$, so bijective reindexing and regrouping are finite operations there. Finite reindexing gives the same coefficients below $N$; coefficient extensionality, as $N$ is arbitrary, proves clause 1.

The coefficient of $h{f}_i$ below $N$ uses only coefficients of $f_i$ below $N$, so only finitely many indices contribute. Finite distributivity gives the displayed identity coefficient by coefficient.

For fixed $N$, eventually every $u_k$ has order at least $N$, so $1+u_k\equiv 1(\mathrm{m}\mathrm{o}\mathrm{d}{x}^N)$. All later factors therefore leave the partial product unchanged modulo $x^N$. A permutation or finite grouping merely reorders the finitely many factors that matter, and multiplication is commutative and associative.

At an empty index set, the same arguments read $0=0$ and $1=1$. Steps 1.1-1.3 prove all clauses.

Let $(f_j)$ be Cauchy. For each $n$, use the Cauchy condition with $N=n+1$: the coefficient $[x^n]f_j$ is eventually constant. Define $[x^n]f$ to be that eventual value. Given $N$, choose a common Cauchy index for the first $N$ coefficients; then $f_j\equiv f(\mathrm{m}\mathrm{o}\mathrm{d}{x}^N)$ thereafter, so $f_j\to f$.

The truncation $f_{<N}$ is finitely supported, hence belongs to the embedded $R[x]$, and it agrees with $f$ in every degree below $N$. Therefore $f_{<N}\to f$; this includes a constant or zero series and remains true in the zero ring.

If both $f$ and $g$ are limits, then for each $N$ their first $N$ coefficients agree with the same sufficiently late $f_j$. Thus every coefficient of $f$ and $g$ agrees, so $f=g$ by extensionality.

Existence and uniqueness are steps 1.1 and 2.1, and density is step 1.2.

If $fg=1$, constant-coefficient extraction gives $a_0[x^0]g=1$. Commutativity gives the reverse product too, so $a_0$ is a unit.

Conversely suppose $a_0$ is a unit and define $b_n$ by the displayed recursion. The coefficient of $fg$ at $0$ is $a_0{b}_0=1$. For $n\ge 1$ it is $a_0{b}_n+{\sum }_{i=1}^n{a}_i{b}_{n-i}=0$. Hence $fg=1$ by extensionality, and commutativity gives $gf=1$.

Any inverse must satisfy the same constant equation and then, successively, the same equation for each $b_n$; multiplication by $a_0^{-1}$ makes every coefficient unique. In the zero ring, $0=1$ and the unit theorem makes the same recursion and equivalence valid.

Steps 1.1 and 1.2 prove both directions, while step 2.1 proves uniqueness and the boundary case.

A field is a nonzero integral domain, so exact order additivity shows that a product of two nonzero series is nonzero. Thus $K\mathrm{⟦}x\mathrm{⟧}$ is a domain.

The unit criterion says that a series is a nonunit exactly when its constant coefficient is $0$. The shift formula says these are exactly the multiples of $x$: for such $f$, define $g$ by $[x^n]g=[x^{n+1}]f$ and obtain $f=xg$. This set is a proper ideal because $1$ has constant coefficient $1\mathrm{\ne }0$.

If an ideal strictly contains $xK\mathrm{⟦}x\mathrm{⟧}$, it contains a series with nonzero constant coefficient, hence a unit, and therefore is the whole ring. Thus $xK\mathrm{⟦}x\mathrm{⟧}$ is maximal. Conversely, every proper ideal contains no unit, so every maximal ideal is contained in the set of nonunits $xK\mathrm{⟦}x\mathrm{⟧}$ and hence equals it by maximality.

Steps 1.1-2.1 prove the domain claim and identify the unique maximal ideal, including the zero series and constant-series cases.

Linearity follows by splitting the locally finite defining sum. For multiplication, expand $(fh)\circ g$ using the Cauchy coefficients of $fh$ and regroup the locally finite double family to obtain $({\sum }_i[x^i]f{g}^i)({\sum }_j[x^j]h{g}^j)$. Constants give $1\circ g=1$.

For associativity assume $[x^0]g=[x^0]h=0$. Then ${\mathrm{ord}}_x(g^n)\ge n$ and ${\mathrm{ord}}_x(h^m)\ge m$, so expanding either side by [F1] gives the same doubly indexed family $[x^n]f[x^m](g^n)h^m$, in which only finitely many terms contribute below each degree. [F2] therefore rearranges one into the other. The hypothesis is used exactly here: without it a term of arbitrarily high index can contribute in low degree, and the two sides need not agree even when all four compositions are individually admissible.

Substituting $x$ leaves every coefficient in place, while substituting into the polynomial $x$ returns the inner series. Finally, $x^2\circ (x+x^2)=x^2+2x^3+x^4$ whereas $(x+x^2)\circ x^2=x^2+x^4$ over $\mathbb{Z}$, so composition is not commutative.

Steps 1.1-1.3 give the homomorphism, associativity, identity, and noncommutativity claims.

If $f\circ g=x$, then the coefficient of $x$ is $[x]f[x]g=1$. Thus $[x]f$ is a unit. The same equation also determines $[x]g$ as its inverse.

Conversely write $f=a_{1}x+a_2{x}^2+\cdots$ with $a_1$ a unit. Choose $b_1=a_1^{-1}$. After $b_1,\dots ,b_{n-1}$ have been chosen, the coefficient of $x^n$ in $f\circ (b_{1}x+\cdots +b_n{x}^n)$ is $a_1{b}_n+c_n$, where $c_n$ depends only on the earlier $b_j$. Set $b_n=-a_1^{-1}{c}_n$. The resulting $g$ has $f\circ g=x$, and the same equations show that it is the unique left inverse.

Apply the construction to $g$: its linear coefficient $a_1^{-1}$ is a unit, so there is $h$ with $g\circ h=x$. Associativity gives $f=f\circ x=f\circ (g\circ h)=(f\circ g)\circ h=x\circ h=h$. Thus $g\circ f=x$ as well, and any two-sided inverse is the already unique solution of $f\circ g=x$.

In the zero ring, $x=0$ and the sole series is its own inverse. In a nonzero ring, $0$ is not a unit, so a zero linear coefficient fails necessity. Together with steps 1.1-2.1 this proves the equivalence and uniqueness.

Linearity is immediate coefficientwise. In degree $n-1$, $D(fg)$ has coefficient $n{\sum }_{i+j=n}{a}_i{b}_j$, while $(Df)g+fDg$ has ${\sum }_{i+j=n}(i+j)a_i{b}_j$; these are equal. Induction on $m$ gives the power rule, including the separately stated $m=0$ case.

Iterating the derivative gives $(D^{n}f)(0)=n![x^n]f$; in a $\mathbb{Q}$-algebra $n!$ is invertible, proving ordinary recovery. The constant coefficient of $D^{[n]}f$ is the $m=n$ term $\left(\genfrac{}{}{0px}{}{n}{n}\right)[x^n]f=[x^n]f$, so Hasse recovery needs no division and works in every characteristic.

Write $f=xF$ and $g=xG$ using the shift formula. Then $G(0)=g^{\mathrm{\prime }}(0)$ is a unit, so $g=xG$ and $f=xF$ give $f\mathrm{/}g=F{G}^{-1}$. Its constant coefficient is $F(0)G(0{)}^{-1}=f^{\mathrm{\prime }}(0)g^{\mathrm{\prime }}(0{)}^{-1}$.

Differentiating $f{f}^{-1}=1$ and using the product rule gives $(Df)f^{-1}+fD(f^{-1})=0$; multiplying by $f^{-1}$ gives the inverse rule. Applying the product rule to $f\mathrm{/}g=f{g}^{-1}$ and then the inverse rule gives $D(f\mathrm{/}g)=((Df)g-fDg)g^{-2}$.

The chain rule holds for an outer monomial by the power rule. Linearity and locally finite rearrangement extend it to every admissible composition for which the differentiated family is summable.

Steps 1.1-2.2 prove every displayed law and its stated hypotheses.

Expanding the product and regrouping in each degree gives $\exp (u)\exp (v)={\sum }_{n\ge 0}(u+v{)}^n\mathrm{/}n!$ by the finite binomial identity, so the exponential addition law holds.

Termwise differentiation gives $D\exp (u)=(\exp u)Du$ and $D\log (1+u)=(1+u{)}^{-1}Du$. Hence $D(\log (\exp u)-u)=0$, and its constant coefficient is $0$, so $\log (\exp u)=u$. For $z=1+u$ and $y=\exp (\log z)$, the same formulas give $D(y{z}^{-1})=0$ and $(y{z}^{-1})(0)=1$, so $y=z$. Here a zero derivative forces every positive-degree coefficient to vanish because every positive integer is invertible in a $\mathbb{Q}$-algebra.

In an independent indeterminate $z$, let $B_c(z)$ denote the displayed generalized-binomial series. Direct coefficient algebra gives $B_c(0)=1$ and $(1+z)D_z{B}_c(z)=c{B}_c(z)$. The formally defined $(1+z{)}^c$ has the same constant coefficient and differential equation. Recursively comparing coefficients, where $n$ is invertible for $n\ge 1$, makes the two series equal; admissible substitution $z=u$ gives the asserted formula.

Step 1.2 and the exponential addition law give $\exp (\log (1+u)+\log (1+v))=(1+u)(1+v)$; applying $\log$ gives the logarithm addition law. The two power laws follow by substituting their definition and applying the exponential and logarithm laws.

Steps 1.1-2.1 prove the inverse homomorphisms, both power laws, and the coefficient formula, including $u=0$, $c=0$, and $n=0$.

The power law gives $((1+u{)}^{1\mathrm{/}k}{)}^k=(1+u{)}^1=1+u$, so the stated series is a root with constant coefficient $1$.

If $v\in 1+xR\mathrm{⟦}x\mathrm{⟧}$ and $v^k=1+u$, the logarithm addition law gives $k\log v=\log (1+u)$. Since $k$ is invertible in a $\mathbb{Q}$-algebra, $\log v=(1\mathrm{/}k)\log (1+u)$; applying $\exp$ gives $v=(1+u{)}^{1\mathrm{/}k}$. This proves uniqueness.

For $u=0$, the construction is $\exp (0)=1$, and step 1.2 excludes any other constant-one root.