## Euclidean semirings ## Given a additively cancellative commutative semiring $R$, a term $e:R$ is *left cancellative* if for all $a:R$ and $b:R$, $e \cdot a = e \cdot b$ implies $a = b$. $$\mathrm{isLeftCancellative}(e) \coloneqq \prod_{a:R} \prod_{b :R}(e \cdot a = e \cdot b) \to (a = b)$$ A term $e:R$ is *right cancellative* if for all $a:R$ and $b:R$, $a \cdot e = b \cdot e$ implies $a = b$. $$\mathrm{isRightCancellative}(e) \coloneqq \prod_{a:R} \prod_{b :R}(a \cdot e = b \cdot e) \to (a = b)$$ An term $e:R$ is *cancellative* if it is both left cancellative and right cancellative. $$\mathrm{isCancellative}(e) \coloneqq \mathrm{isLeftCancellative}(e) \times \mathrm{isRightCancellative}(e)$$ The **multiplicative submonoid of cancellative elements in $R$** is the subset of all cancellative elements in $R$ $$\mathrm{Can}(R) \coloneqq \sum_{e:R} \mathrm{isCancellative}(e)$$ A **Euclidean semiring** is a additively cancellative commutative semiring $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*, 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 $a \in R$ and $b \in \mathrm{Can}(R)$, $a = (a \div b) \cdot b + (a\;\%\; b)$ and either $a\;\%\; b = 0$ or $d(a\;\%\; b) \lt d(g)$. ## Non-cancellative and non-invertible elements ## Given a ring $R$, an element $x \in R$ is non-cancellative if: if there is an element $y \in \mathrm{Can}(R)$ with injection $i:\mathrm{Can}(R) \to R$ such that $i(y) = x$, then $0 = 1$. An element $x \in R$ is non-invertible if: if there is an element $y \in R^\times$ with injection $j:R^\times \to R$ such that $j(y) = x$, then $0 = 1$. ## Commutative rings ## ### Commutative $\mathbb{Q}$-algebras ### A commutative ring $R$ is a commutative $\mathbb{Q}$-algebra if there is a commutative ring homomorphism $h:\mathbb{Q} \to R$. ### Totally ordered commutative rings ### A commutative ring $R$ is a totally ordered commutative ring if it comes with a function $\max:R \times R \to R$ such that * for all elements $a:R$, $\max(a, a) = a$ * for all elements $a:R$ and $b:R$, $\max(a, b) = \max(b, a)$ * for all elements $a:R$, $b:R$, and $c:R$, $\max(a, \max(b, c)) = \max(\max(a, b), c)$ * for all elements $a:R$ and $b:R$, $\max(a, b) = b$ implies that for all elements $c:R$, $\max(a + c, b + c) = b + c$ * for all elements $a:R$ and $b:R$, $\max(a, 0) = a$ and $\max(b, 0) = b$ implies $\max(a \cdot b, 0) = a \cdot b$ * for all elements $a:R$ and $b:R$, $\max(a, b) = a$ or $\max(a, b) = b$ ### Totally ordered commutative $\mathbb{Q}$-algebras ### Given totally ordered commutative rings $R$ and $S$, a commutative ring homomorphism $h:R \to S$ is monotonic if for all $a:R$ and $b:R$, $\max(h(a), h(b)) = h(\max(a, b))$. A totally ordered commutative ring $R$ is a totally ordered commutative $\mathbb{Q}$-algebra if there is a monotonic commutative ring homomorphism $h:\mathbb{Q} \to R$. ### Strictly ordered integral ring ### A totally ordered commutative ring $R$ is a strictly ordered integral ring if it comes with a strict order $\lt$ such that * $0 \lt 1$ * for all elements $a:R$ and $b:R$, if $0 \lt a$ and $0 \lt b$, then $0 \lt a + b$ * for all elements $a:R$ and $b:R$, if $0 \lt a$ and $0 \lt b$, then $0 \lt a \cdot b$ * for all elements $a:R$ and $b:R$, if $0 \lt \max(a, -a)$ and $0 \lt \max(b, -b)$, then $0 \lt \max(a \cdot b, -a \cdot b)$ ### Strictly ordered integral $\mathbb{Q}$-algebras ### Given strictly ordered integral rings $R$ and $S$, a monotonic commutative ring homomorphism $h:R \to S$ is strictly monotonic if for all $a:R$ and $b:R$, $a \lt b$ implies $h(a) \lt h(b)$. A strictly ordered integral ring $R$ is a strictly ordered integral $\mathbb{Q}$-algebra if there is a strictly monotonic commutative ring homomorphism $h:\mathbb{Q} \to R$. ### Archimedean ordered integral $\mathbb{Q}$-algebras A strictly ordered integral $\mathbb{Q}$-algebra $A$ is an Archimedean ordered integral $\mathbb{Q}$-algebra if for all elements $a:A$ and $b:A$, if $a \lt b$, then there merely exists a rational number $q:\mathbb{Q}$ such that $a \lt h(q)$ and $h(q) \lt b$. ### Sequentially Cauchy complete Archimedean ordered integral $\mathbb{Q}$-algebra Let $A$ be an Archimedean ordered integral $\mathbb{Q}$-algebra and let $$A_{+} \coloneqq \sum_{a:A} 0 \lt a$$ be the positive elements in $A$. $A$ is **sequentially Cauchy complete** if every Cauchy sequence in $A$ converges: $$isCauchy(x) \coloneqq \forall \epsilon \in A_{+}. \exists N \in I. \forall i \in I. \forall j \in I. (i \geq N) \wedge (j \geq N) \wedge (\vert x_i - x_j \vert \lt \epsilon)$$ $$isLimit(x, l) \coloneqq \forall \epsilon \in A_{+}. \exists N \in I. \forall i \in I. (i \geq N) \to (\vert x_i - l \vert \lt \epsilon)$$ $$\forall x: \mathbb{N} \to A. isCauchy(x) \wedge \exists l \in A. isLimit(x, l)$$ ### Modules Given a commutative ring $R$, an $R$-module is an abelian group $M$ with an abelian group homomorphism $\alpha:R \to (M \to M)$ which is also a curried action. The free $R$-module on a set $S$ is the initial $R$-module $M$ with a function $\iota:S \to M$. ### $A_n$ abelian groups $A_1$-abelian groups are pointed objects in abelian groups $A_2$-abelian groups are unital magma objects in abelian groups $A_3$-abelian groups are monoid objects in abelian groups ### References * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013) category: not redirected to nlab yet