Homotopy Type Theory an axiomatization of the real numbers > history (Rev #9, changes)

Showing changes from revision #8 to #9: Added | Removed | Changed

Definition

Totally ordered commutative abelian rings groups

A An commutative abelian ring groupRR is a totally ordered commutative abelian ring group if it comes with a functionmax: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,0b)=a \max(a, 0) b) = a and ormax( b a,0b)=b \max(b, \max(a, 0) b) = 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 Strictly ordered commutative pointed abelian groups\mathbb{Q}-algebras

Given A totally ordered commutative rings ringRR and is a strictly ordered pointed abelian group if it comes with an elementS1:R S 1:R , and a commutative type ring family homomorphismh<:RS h:R \lt \to S is such monotonic that if for alla:Ra:R and b:Rb:R, max(h(a),h(b))=h(max(a,b))\max(h(a), h(b)) = h(\max(a, b)).

Every totally ordered commutative ring RR has a monotonic commutative ring homomorphism h:Rh:\mathbb{Z} \to R from the integers to RR, and there is an monotonic injection i: +i:\mathbb{Z}_+ \to \mathbb{Z} from the positive integers to the integers.

  • for all elements a:Ra:R and b:Rb:R, a<ba \lt b is a proposition
  • for all elements a:Ra:R, a<aa \lt a is false
  • for all elements a:Ra:R, b:Rb:R, and c:Rc:R, if a<ca \lt c, then a<ba \lt b or b<cb \lt c
  • for all elements a:Ra:R and b:Rb:R, if a<ba \lt b is false and b<ab \lt a is false, then a=ba = b
  • for all elements a:Ra:R and b:Rb:R, if a<ba \lt b, then b<ab \lt a is false.
  • 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

A totally ordered commutative ring RR is a totally ordered commutative \mathbb{Q}-algebra if there is a function j: +Rj:\mathbb{Z}_+ \to R such that for all positive integers a: +a:\mathbb{Z}_+, h(i(a))j(a)=1h(i(a)) \cdot j(a) = 1.

Strictly ordered pointed \mathbb{Q}-vector space

Strictly ordered integral ring

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

Archimedean ordered pointed \mathbb{Q}-vector space

  • for all elements a:Ra:R and b:Rb:R, a<ba \lt b is a proposition
  • for all elements a:Ra:R, a<aa \lt a is false
  • for all elements a:Ra:R, b:Rb:R, and c:Rc:R, if a<ca \lt c, then a<ba \lt b or b<cb \lt c
  • for all elements a:Ra:R and b:Rb:R, if a<ba \lt b is false and b<ab \lt a is false, then a=ba = b
  • for all elements a:Ra:R and b:Rb:R, if a<ba \lt b, then b<ab \lt a is false.
  • 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)

A strictly ordered pointed \mathbb{Q}-vector space AA is an Archimedean ordered pointed \mathbb{Q}-vector space 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.

Strictly Sequentially Cauchy complete Archimedean ordered integral pointed\mathbb{Q} -algebras -vector space

Given Let strictly ordered integral rings R A R A and be an Archimedean ordered pointed S S \mathbb{Q} , -vector a space monotonic and commutative let ring homomorphismh: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).

Every strictly ordered ring RR has a strictly monotonic commutative ring homomorphism h:Rh:\mathbb{Z} \to R from the integers to RR, and there is an strictly monotonic injection i: +i:\mathbb{Z}_+ \to \mathbb{Z} from the positive integers to the integers.

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

A be strictly the ordered positive integral elements ring in R A R A . is a strictly ordered integral A \mathbb{Q} A -algebra if there is a functionj: +Rj:\mathbb{Z}_+ \to Rsequentially Cauchy complete such if that every for Cauchy all sequence positive in integers a A: + a:\mathbb{Z}_+ A , converges:h(i(a))j(a)=1h(i(a)) \cdot j(a) = 1.

Archimedean ordered integral \mathbb{Q}-algebras

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)

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.

x:A.isCauchy(x)lA.isLimit(x,l)\forall x: \mathbb{N} \to A. isCauchy(x) \wedge \exists l \in A. isLimit(x, l)

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

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)

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