Homotopy Type Theory UMyn8W7b (Rev #52, changes)

Showing changes from revision #51 to #52: Added | Removed | Changed

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$.

A term $e:R$ is right cancellative if for all $a:R$ and $b:R$, $a \cdot e = b \cdot e$ implies $a = b$.

An term $e:R$ is cancellative if it is both left cancellative and right cancellative.

The multiplicative submonoid of cancellative elements in $R$ is the subset of all cancellative elements in $R$

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$ (-)\ (-)\;\%\;(-):R \%\ (-):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÷b)\cdot b+(a\%b)$ a = (a \div b) \cdot b + (a\ (a\;\%\; \%\ b) and either $a\%b=0$ a\ a\;\%\; \%\ b = 0 or $d(a\%b)<d(g)$ d(a\ 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$.

To the real numbers

• Q-vector space

• free Q-vector spaces?

• strictly ordered Q-vector space?

• Archimedean Q-vector space?