formal power series over field

Theorem.  If K is a field, then the ring K[[X]] of formal power series is a discrete valuation ring with (X) its unique maximal idealMathworldPlanetmath.

Proof.  We show first that an arbitrary ideal I of K[[X]] is a principal idealMathworldPlanetmathPlanetmath.  If  I=(0),  the thing is ready.  Therefore, let  I(0).  Take an element


of I such that it has the least possible amount of successive zero coefficients in its beginning; let its first non-zero coefficient be ak.  Then


Here we have in the parentheses an invertible formal power series g(X), whence get the equation


implying  XkI  and consequently  (Xk)I.
For obtaining the reverse inclusion, suppose that


is an arbitrary nonzero element of I where  bn0.  Because  nk,  we may write


This equation says that  h(X)(Xk),  whence  I(Xk).
Thus we have seen that I is the principal ideal (Xk), so that K[[X]] is a principal ideal domainMathworldPlanetmath.
Now, all ideals of the ring K[[X]] form apparently the strictly descending chain


whence the ring has the unique maximal ideal (X).  A principal ideal domain with only one maximal ideal is a discrete valuation ring.

Title formal power series over field
Canonical name FormalPowerSeriesOverField
Date of creation 2015-10-19 9:13:35
Last modified on 2015-10-19 9:13:35
Owner pahio (2872)
Last modified by pahio (2872)
Numerical id 7
Author pahio (2872)
Entry type Theorem
Classification msc 13H05
Classification msc 13J05
Classification msc 13F25