Euclideanness is localization-closed
This article gives the statement, and possibly proof, of a commutative unital ring property (i.e., Euclidean ring) satisfying a commutative unital ring metaproperty (i.e., localization-closed property of commutative unital rings)
View all commutative unital ring metaproperty satisfactions | View all commutative unital ring metaproperty dissatisfactions |Get help on looking up metaproperty (dis)satisfactions for commutative unital ring properties
Get more facts about Euclidean ring|Get more facts about localization-closed property of commutative unital rings
Suppose is a Euclidean ring and is a multiplicatively closed subset of not containing any zero divisors (without loss of generality, we may assume that is a saturated multiplicatively closed subset. Let be the localization of at . Then, is also a Euclidean ring. Further, if is a Euclidean norm on , we can define a new Euclidean norm on as follows:
To see that this is well-defined, observe that any can be expressed as for some , , and if , . Thus, . Hence, the set on the right side is nonempty. A minimum over a nonempty well-ordered set is well-defined, so the expression is well-defined.
Note that doing this operation for does not necessarily give back the same Euclidean norm as we started with. It gives back the same norm only if the original norm was multiplicatively monotone.
- Using the fact that the polynomial ring over a field is Euclidean, we can prove that the Laurent polynomial ring over a field is also Euclidean. The Euclidean norm of a Laurent polynomial is defined as the difference between the highest and lowest degrees among the constituent monomials with nonzero coefficients. Further information: Polynomial ring over a field is Euclidean with norm equal to degree, Laurent polynomial ring over a field is Euclidean with norm equal to degree gap
- Euclideanness is quotient-closed
- Minimum over principal ideal of Euclidean norm is a smaller multiplicatively monotone Euclidean norm: In fact, this is precisely the new norm we get when we do the process outlined above, setting .
Fill this in later