Filtrative and multiplicatively monotone Euclidean implies uniquely Euclidean

From Commalg

Statement

Suppose is an integral domain with a Euclidean norm satisfying the following two conditions:

Then, is a uniquely Euclidean norm: for any with , there exists a unique pair satisfying and or .

Proof

Given: Integral domain , Euclidean norm that is filtrative and multiplicatively monotone.

To prove: is uniquely Euclidean: for any with , there exists a unique pair for which and or .

Proof: Suppose there are two solution pairs: and . Then, we have:

.

  1. We have : This follows by manipulating the equation .
  2. Either or : By the definition of Euclidean norm, both and belong to the set . Since is filtrative, this set is a subgroup, so also belongs to this set.
  3. Either or : If , then . Since is an integral domain, the product is nonzero, so by the fact that is multiplicatively monotone, we get .
  4. : Combining steps (1), (2) and (3), we obtain that we cannot have both and . Thus, either or . But yields, by step (1), that . Similarly , along with step (1) and the fact that is an integral domain, yields . Hence, .