Homotopy Type Theory UMyn8W7b (Rev #52)

Euclidean semirings

Given a additively cancellative commutative semiring RR, a term e:Re:R is left cancellative if for all a:Ra:R and b:Rb:R, ea=ebe \cdot a = e \cdot b implies a=ba = b.

isLeftCancellative(e) a:R b:R(ea=eb)(a=b)\mathrm{isLeftCancellative}(e) \coloneqq \prod_{a:R} \prod_{b :R}(e \cdot a = e \cdot b) \to (a = b)

A term e:Re:R is right cancellative if for all a:Ra:R and b:Rb:R, ae=bea \cdot e = b \cdot e implies a=ba = b.

isRightCancellative(e) a:R b:R(ae=be)(a=b)\mathrm{isRightCancellative}(e) \coloneqq \prod_{a:R} \prod_{b :R}(a \cdot e = b \cdot e) \to (a = b)

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

isCancellative(e)isLeftCancellative(e)×isRightCancellative(e)\mathrm{isCancellative}(e) \coloneqq \mathrm{isLeftCancellative}(e) \times \mathrm{isRightCancellative}(e)

The multiplicative submonoid of cancellative elements in RR is the subset of all cancellative elements in RR

Can(R) e:RisCancellative(e)\mathrm{Can}(R) \coloneqq \sum_{e:R} \mathrm{isCancellative}(e)

A Euclidean semiring is a additively cancellative commutative semiring RR for which there exists a function d:Can(R)d \colon \mathrm{Can}(R) \to \mathbb{N} from the multiplicative submonoid of cancellative elements in RR to the natural numbers, often called a degree function, a function ()÷():R×Can(R)R(-)\div(-):R \times \mathrm{Can}(R) \to R called the division function, and a function ()%():R×Can(R)R(-)\;\%\;(-):R \times \mathrm{Can}(R) \to R called the remainder function, such that for all aRa \in R and bCan(R)b \in \mathrm{Can}(R), a=(a÷b)b+(a%b)a = (a \div b) \cdot b + (a\;\%\; b) and either a%b=0a\;\%\; b = 0 or d(a%b)<d(g)d(a\;\%\; b) \lt d(g).

Non-cancellative and non-invertible elements

Given a ring RR, an element xRx \in R is non-cancellative if: if there is an element yCan(R)y \in \mathrm{Can}(R) with injection i:Can(R)Ri:\mathrm{Can}(R) \to R such that i(y)=xi(y) = x, then 0=10 = 1. An element xRx \in R is non-invertible if: if there is an element yR ×y \in R^\times with injection j:R ×Rj:R^\times \to R such that j(y)=xj(y) = x, then 0=10 = 1.

To the real numbers

  • Q-vector space

  • free Q-vector spaces?

  • strictly ordered Q-vector space?

  • Archimedean Q-vector space?

An Archimedean ordered field is Cauchy if every Cauchy sequence of rational numbers in the field converges. The initial Cauchy field is the Cauchy real numbers.

Revision on June 2, 2022 at 14:41:43 by Anonymous?. See the history of this page for a list of all contributions to it.