Homotopy Type Theory UMyn8W7b (Rev #66)

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.

Commutative rings

Commutative \mathbb{Q}-algebras

A commutative ring RR is a commutative \mathbb{Q}-algebra if there is a commutative ring homomorphism h:Rh:\mathbb{Q} \to R.

Totally ordered commutative rings

A commutative ring RR is a totally ordered commutative ring if it comes with a function max:R×RR\max:R \times R \to R such that

  • for all elements a:Ra:R, max(a,a)=a\max(a, a) = a

  • for all elements a:Ra:R and b:Rb:R, max(a,b)=max(b,a)\max(a, b) = \max(b, a)

  • for all elements a:Ra:R, b:Rb:R, and c:Rc:R, max(a,max(b,c))=max(max(a,b),c)\max(a, \max(b, c)) = \max(\max(a, b), c)

  • for all elements a:Ra:R and b:Rb:R, max(a,b)=b\max(a, b) = b implies that for all elements c:Rc:R, max(a+c,b+c)=b+c\max(a + c, b + c) = b + c

  • for all elements a:Ra:R and b:Rb:R, max(a,0)=a\max(a, 0) = a and max(b,0)=b\max(b, 0) = b implies max(ab,0)=ab\max(a \cdot b, 0) = a \cdot b

  • for all elements a:Ra:R and b:Rb:R, max(a,b)=a\max(a, b) = a or max(a,b)=b\max(a, b) = b

Totally ordered commutative \mathbb{Q}-algebras

Given totally ordered commutative rings RR and SS, a commutative ring homomorphism h:RSh:R \to S is monotonic if for all a:Ra:R and b:Rb:R, max(h(a),h(b))=h(max(a,b))\max(h(a), h(b)) = h(\max(a, b)).

A totally ordered commutative ring RR is a totally ordered commutative \mathbb{Q}-algebra if there is a monotonic commutative ring homomorphism h:Rh:\mathbb{Q} \to R.

Strictly ordered integral ring

A totally ordered commutative ring RR is a strictly ordered integral ring if it comes with a strict order <\lt such that

  • 0<10 \lt 1
  • for all elements a:Ra:R and b:Rb:R, if 0<a0 \lt a and 0<b0 \lt b, then 0<a+b0 \lt a + b
  • for all elements a:Ra:R and b:Rb:R, if 0<a0 \lt a and 0<b0 \lt b, then 0<ab0 \lt a \cdot b
  • for all elements a:Ra:R and b:Rb:R, if 0<max(a,a)0 \lt \max(a, -a) and 0<max(b,b)0 \lt \max(b, -b), then 0<max(ab,ab)0 \lt \max(a \cdot b, -a \cdot b)

Strictly ordered integral \mathbb{Q}-algebras

Given strictly ordered integral rings RR and SS, a monotonic commutative ring homomorphism h:RSh:R \to S is strictly monotonic if for all a:Ra:R and b:Rb:R, a<ba \lt b implies h(a)<h(b)h(a) \lt h(b).

A strictly ordered integral ring RR is a strictly ordered integral \mathbb{Q}-algebra if there is a strictly monotonic commutative ring homomorphism h:Rh:\mathbb{Q} \to R.

Archimedean ordered integral \mathbb{Q}-algebras

A strictly ordered integral \mathbb{Q}-algebra AA is an Archimedean ordered integral \mathbb{Q}-algebra if for all elements a:Aa:A and b:Ab:A, if a<ba \lt b, then there merely exists a rational number q:q:\mathbb{Q} such that a<h(q)a \lt h(q) and h(q)<bh(q) \lt b.

Sequentially Cauchy complete Archimedean ordered integral \mathbb{Q}-algebra

Let AA be an Archimedean ordered integral \mathbb{Q}-algebra and let

A + a:A0<aA_{+} \coloneqq \sum_{a:A} 0 \lt a

be the positive elements in AA. AA is sequentially Cauchy complete if every Cauchy sequence in AA converges:

isCauchy(x)ϵA +.NI.iI.jI.(iN)(jN)(|x ix j|<ϵ)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)ϵA +.NI.iI.(iN)(|x il|<ϵ)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)
x:A.isCauchy(x)lA.isLimit(x,l)\forall x: \mathbb{N} \to A. isCauchy(x) \wedge \exists l \in A. isLimit(x, l)

Modules

Given a commutative ring RR, an RR-module is an abelian group MM with an abelian group homomorphism α:R(MM)\alpha:R \to (M \to M) which is also a curried action.

The free RR-module on a set SS is the initial RR-module MM with a function ι:SM\iota:S \to M.

A nA_n abelian groups

A 1A_1-abelian groups are pointed objects in abelian groups

A 2A_2-abelian groups are unital magma objects in abelian groups

A 3A_3-abelian groups are monoid objects in abelian groups

References

Revision on June 16, 2022 at 18:28:57 by Anonymous?. See the history of this page for a list of all contributions to it.