Denote by $F[[T]]$ the ring of formal power series over a field $F$ (i.e expressions of the form $\sum_{n=0}^{\infty}a_nT^n$, $a_i \in F$).
I need to show that this is a euclidean ring with respect to the norm $\mathrm{ord}(\sum a_iT^i) = \min\{n \mid a_n \neq 0\}$.
This just feels too trivial and I think I am missing something obvious, so I would like to get a feedback on my proof (if it is even correct).
Take $f,g$ in the ring. If $\mathrm{ord}(g) < \mathrm{ord}(f)$ we get $g=f \cdot 0 + g$, so we can divide $g$ by $f$ and get a remainder.
Now suppose $\mathrm{ord}(g)=n>\mathrm{ord}(f)=k$.
I claim $f\mid g$ and therefore $g=fq+0$ for some $q$.
First, if $f=T^k$ then obviously $f\mid g$. So take $q_1$ such that $g=T^kq_1$.
Now since $\mathrm{ord}(f) = k$ we can write $f=T^kf_1$ for some $f_1$ that is invertible (since the coefficient of $1=T^0$ in it is nonzero). Taking $q = f_1^{-1}q_1$ we get $g=fq$, so $f\mid g$ and we are done.
Is this true? Am I missing something? This is suspicious for me because it seems like I proved that whenever $\mathrm{ord}(g) > \mathrm{ord}(f)$ we have $f\mid g$ which seems like a much stronger result than what I was asked to prove.
Best Answer
No, that's correct. Since a power series is invertible iff its constant term is non-zero, that means that once you add $T^{-1}$, everything becomes invertible. If $f = T^ng$ where $g(0) \ne 0$ then $f^{-1} = T^{-n}g^{-1}$. So the fraction field of $F[[T]]$ is the field of Laurent series:
$$ F((T)) = F[[T]][T^{-1}] = \{ T^{-N}f : N \in \mathbb{Z}, f \in F[[T]] \} = \left\{ \sum_{n \ge -N} a_nT^n : a_n \in F, N \in \mathbb{Z} \right\}. $$
So if I have any quotient $f/g$ of two power series, then $f/g \in \operatorname{Frac}(F[[T]]) = F((T))$, so I can always write
$$ \frac{f}{g} = T^{N}h $$
where $h \in F[[T]]^\times$ and $N = \operatorname{ord}{f} - \operatorname{ord}g$.
Now if $N \ge 0$ then $f = (T^Nh) g$ and if $N < 0$ then $f = 0g + f$ (i.e. the remainder is $f$). It is precisely because the fraction field has such a simple description that the Euclidean algorithm also has a simple description.