Recordemos la conocida prueba de que un dominio de factorización único es un dominio GCD:
Sea $x, y \in R \setminus \{ 0 \}$ . Factor $x$ y $y$ en elementos irreducibles no asociados por pares: $$\begin{align*}x &= p_1^{e_1} \cdots p_n^{e_n}, \\ y &= p_1^{f_1} \cdots p_n^{f_n}.\end{align*} $$ Entonces se puede comprobar que el producto $p_1^{r_1} \cdots p_n^{r_n}$ con $r_i := \min\{ e_i, f_i \}$ es el máximo común divisor de $x$ y $y$ .
Aquí, un dominio de factorización única es un dominio integral tal que cada elemento distinto de cero admite una factorización en elementos irreducibles que es única hasta el reordenamiento y la asociatividad, y un dominio GCD es un dominio integral tal que existe un máximo común divisor para dos elementos cualesquiera.
Constructivamente, el problema con la prueba anterior es que puede que no seamos capaces de decidir para elementos irreducibles dados si están asociados o no. Utilizando las definiciones (clásicamente estándar) dadas, no veo que la implicación $$\text{$ R $ is a unique factorization domain} \Longrightarrow \text{$ R $ is a GCD domain}$$ es demostrable constructivamente.
Pregunta. ¿Existe una noción constructiva elegante de dominio de factorización único tal que la implicación se cumpla constructivamente?
Observación 1. Obsérvese que en dominios de factorización única que resultan ser dominios GCD, la asociabilidad e incluso la divisibilidad son decidibles: Dados elementos $x$ y $y$ considere un gcd $d$ de $x$ y $y$ . Escriba a $x = ds$ . Entonces $x|y$ si $s$ es invertible. Este es el caso si el número de factores en una factorización de $s$ en elementos irreducibles es cero. Como los números naturales son discretos, esto se puede decidir.
Observación 2. En Minas, Richman, Ruitenburg: Un curso de álgebra constructiva se utilizan aproximadamente las mismas definiciones y la implicación se afirma sin pruebas (véase el teorema IV.2.3 en la página 114). Richman escribió en otro lugar (sección 6) que considera incompleto el tratamiento de los dominios de factorización única en este libro.
