symmetric monoidal (∞,1)-category of spectra
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
In the same vein that commutative rings are to integral domains and GCD rings are to GCD domains, Euclidean rings are to Euclidean domains.
A Euclidean ring is a commutative ring $R$ for which there exists a function $d \colon \mathrm{Can}(R) \to \mathbb{N}$ from the multiplicative submonoid of cancellative elements in $R$ to the natural numbers, often called a degree function, such that for all $f \in R$ and $g \in \mathrm{Can}(R)$, there exist $q, r \in R$ such that $f = q \cdot g + r$ and either $r = 0$ or $d(r) \lt d(g)$. There is no uniqueness requirement for $q, r$.
One could posit, instead of the property that for all $f \in R$ and $g \in \mathrm{Can}(R)$, there exist $q, r \in R$ such that $f = q \cdot g + r$ and either $r = 0$ or $d(r) \lt d(g)$; that the commutative ring has the structure of a function $(-)\div(-):R \times \mathrm{Can}(R) \to R$ called the division function, and a function $(-)\ \%\ (-):R \times \mathrm{Can}(R) \to R$ called the remainder function, such that for all $f \in R$ and $g \in \mathrm{Can}(R)$, $f = (f \div g) \cdot g + (f\ \%\ g)$ and either $f\ \%\ g = 0$ or $d(f\ \%\ g) \lt d(g)$. There might be multiple such division and remainder functions for the commutative ring $R$.
One could also add the requirement that $d(a) \leq d(a b)$ for all nonzero $a, b$. There is no loss of generality in assuming it; every Euclidean ring admits such a degree function $d'$, defining $d'(a) = \min \{d(a b): b \in \mathrm{Can}(R)\}$.
The definition of the Euclidean ring further bifurcates in constructive mathematics due to the disjunctive condition above. These statements, which are equivalent in the presence of excluded middle, include:
or equivalently,
Every Euclidean ring is a Bézout ring, and every prefield is an Euclidean ring.
The integers $\mathbb{Z}$ are a Euclidean ring.
A classical Euclidean domain $A$ is a Euclidean ring where $\mathrm{Can}(A)$ is the multiplicative monoid of elements not equal to zero (where inequality is denial inequality)
Last revised on December 10, 2022 at 14:53:18. See the history of this page for a list of all contributions to it.