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

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

Definition

Totally Abelian ordered abelian groups

An abelian groupRRabelian group is a totally pointed ordered set abelian group if it comes with a functionmax(:AR,×0R)R \max:R (A, \times 0) R \to R with a binary operation ()():A×AA(-)-(-):A \times A \to A called subtraction such that

  • for all elementsa : R A a:R a \in A, max(a ,a)=a0 \max(a, a) = a - a = 0

  • for all elementsa : R A a:R a \in A , andb0 :R(0a)=a b:R 0 - (0 - a) = a, max(a,b)=max(b,a)\max(a, b) = \max(b, a)

  • for all elementsa : R A a:R a \in A , andb : R A b:R b \in A , and c a :R(0b)=b(0a) c:R a - (0 - b) = b - (0 - a), max(a,max(b,c))=max(max(a,b),c)\max(a, \max(b, c)) = \max(\max(a, b), c)

  • for all elementsa : R A a:R a \in A , andb : R A b:R b \in A , and max c ( a A,b)=b \max(a, c b) \in = A b , implies that for all elementsa(bc : )R=(a(0c))b c:R a - (b - c) = (a - (0 - c)) - b, 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,b)=a\max(a, b) = a or max(a,b)=b\max(a, b) = b

Strictly Halving ordered pointed abelian groups

A totally ordered commutative ringRRhalving group is a an strictly ordered pointed abelian group if it comes with an element1:R1:RG and with a type function family < ()/2:GG \lt (-)/2:G \to G such called thathalving or dividing by two such that for all gGg \in G, g/2=gg/2g/2 = g - g/2.

  • 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

Totally ordered halving groups

Strictly ordered pointed \mathbb{Q}-vector space

An abelian group RR is a totally ordered abelian group 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(ac,bc)=bc\max(a - c, b - c) = b - c

  • 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

Strictly ordered pointed halving groups

A totally ordered commutative ring RR is a strictly ordered pointed abelian group if it comes with an element 1:R1:R and a type family <\lt such that

  • 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(0b)0 \lt a - (0 - b)

Archimedean ordered pointed halving groups\mathbb{Q}-vector space

A strictly ordered pointed halving group A \mathbb{Q} A -vector space is an Archimedean ordered pointed halving group if for all elementsa:A A a:A is and an Archimedean ordered pointed b:A \mathbb{Q} b:A -vector , space if for all elementsa : < A b a:A a \lt b , and then there merely exists a dyadic rational number b d: A 𝔻 b:A d:\mathbb{D} , if such thata< b h(d) a \lt b h(d) , then and there merely exists a rational number q h : ( d)<b q:\mathbb{Q} h(d) \lt b such that a<h(q)a \lt h(q) and h(q)<bh(q) \lt b.

Sequentially Cauchy complete Archimedean ordered pointed halving groups\mathbb{Q}-vector space

Let AA be an Archimedean ordered pointed halving group and let\mathbb{Q}-vector space 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 19:34:22 by Anonymous?. See the history of this page for a list of all contributions to it.