# Constructively correct notion of unique factorization domain

Recall the well-known proof that a unique factorization domain is a GCD domain:

Let $x, y \in R \setminus \{ 0 \}$. Factor $x$ and $y$ into pairwise non-associated irreducible elements: \begin{align*}x &= p_1^{e_1} \cdots p_n^{e_n}, \\ y &= p_1^{f_1} \cdots p_n^{f_n}.\end{align*} Then one can check that the product $p_1^{r_1} \cdots p_n^{r_n}$ with $r_i := \min\{ e_i, f_i \}$ is a greatest common divisor of $x$ and $y$.

Here, a unique factorization domain is an integral domain such that every nonzero element admits a factorization into irreducible elements which is unique up to reordering and associatedness, and a GCD domain is an integral domain such that there exists a greatest common divisor for any two elements.

Constructively, the problem with the above proof is that we may not be able to decide for given irreducible elements whether they are associated or not. Using the given (classically standard) definitions, I thus do not see that the implication $$\text{R is a unique factorization domain} \Longrightarrow \text{R is a GCD domain}$$ is constructively provable.

Question. Is there an elegant constructive notion of unique factorization domain such that the implication does hold constructively?

Remark 1. Note that in unique factorization domains which happen to be GCD domains, associatedness and even divisibility are indeed decidable: Given elements $x$ and $y$, consider a gcd $d$ of $x$ and $y$. Write $x = ds$. Then $x|y$ iff $s$ is invertible. This is the case iff the number of factors in a factorization of $s$ into irreducible elements is zero. Because the natural numbers are discrete, this can be decided.

Remark 2. In Mines, Richman, Ruitenburg: A Course in Constructive Algebra approximately the same definitions are used and the implication is stated without proof (see theorem IV.2.3 on page 114). Richman wrote elsewhere (section 6) that he considers the treatment of unique factorization domains in this book to be incomplete.

• It seems that Lombardi and Quitté in their book "Commutative Algebra: Constructive Methods" define UFDs as GCD-domains such that every regular element is a product of irreducibles (does this classically coincide with the usual definition, i.e. is the decomposition unique?). Sep 16, 2016 at 19:09
• @HeinrichD: Thanks! I'd be willing to accept this as an answer. You can show that the decomposition is unique by verifying that irreducible elements are prime; this is possible with Euclid's lemma (which holds in GCD domains and which admits a constructive proof). Furthermore, one can show that a domain is an UFD in their sense if and only if it is a UFD in the sense of my question and associatedness of irreducible elements is decidable. Sep 21, 2016 at 18:53