Homotopy Type Theory Sandbox (Rev #48, changes)

Showing changes from revision #47 to #48: Added | Removed | Changed

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

Z-modules and commutative rings

Z-modulecommutative ring
torsion elementzero divisior
torsion-free elementregular element
torsion subgroupzero divisor subsemigroup
torsion-free subsetregular submonoid
torsion-free Z-moduleintegral domain

Revision on May 20, 2022 at 01:02:03 by Anonymous?. See the history of this page for a list of all contributions to it.