# nLab Bézout domain

Contents

### Context

#### Algebra

higher algebra

universal algebra

# Contents

## Definition

A Bézout domain is an integral domain that is also a Bézout ring.

### In constructive mathematics

In constructive mathematics, there are different types of integral domains, yielding different types of Bézout domains: the gcd function and Bézout coefficient functions are no longer valued in $R \setminus \{0\}$ in one variable, but in $\{x \in R \vert x \neq 0\}$, $\{x \in R \vert x \# 0\}$, or some other definition, depending on what the base integral domain ends up being (classical, Heyting, discrete, residue, et cetera).

## Properties

Every GCD domain of dimension at most 1 is a Bézout domain.

### In classical mathematics

In classical mathematics, every Bézout domain $R$ that satisfies one of the following conditions is a principal ideal domain

1. $R$ is a unique factorization domain

2. $R$ is a Noetherian ring

3. $R$ is an atomic domain?

4. $R$ satisfies the ascending chain condition on principal ideals.

### In constructive mathematics

In constructive mathematics, Bézout domains are usually better behaved because many important rings may fail to be principal ideal domains.

For instance, the ring of integers is a principal ideal domain if and only if the law of excluded middle holds: In one direction, the usual proofs rely on being able to decide whether any particular integer belongs to the ideal or not.

For the converse, let $\varphi$ be an arbitrary proposition. Consider the ideal $\{ x \in \mathbb{Z} | (x = 0) \vee \varphi \}$. By assumption, it is generated by some number $n$. Since the integers are discrete, it holds that $n = 0$ or $n \neq 0$. In the first case $\neg\varphi$ holds, in the second $\varphi$.

However, this ideal cannot be proved to be finitely generated either. If an ideal is generated by $n_1, \ldots, n_k$, then we may form their gcd one step at a time, which we can do algorithmically. Therefore, $\mathbb{Z}$ remains a Bézout domain.

As a result, in constructive mathematics not every Bézout domain that is a unique factorization domain is a principal ideal domain, as $\mathbb{Z}$ is both a Bézout domain and a unique factorization domain, but is not a principal ideal domain.

Some authors have tried to define a principal ideal domain as a Noetherian Bézout domain, but it is unknown if this still coincides in constructive mathematics with the definition of principal ideal domain as a integral domain whose ideals are all principal ideals.