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

Definition

Abelian groups

An abelian group is a pointed set (A,0)(A, 0) with a binary operation ()():A×AA(-)-(-):A \times A \to A called subtraction such that

  • for all aAa \in A, aa=0a - a = 0

  • for all aAa \in A, 0(0a)=a0 - (0 - a) = a

  • for all aAa \in A and bAb \in A, a(0b)=b(0a)a - (0 - b) = b - (0 - a)

  • for all aAa \in A, bAb \in A, and cAc \in A, a(bc)=(a(0c))ba - (b - c) = (a - (0 - c)) - b

Halving groups

A halving group is an abelian group G with a function ()/2:GG(-)/2:G \to G called halving or dividing by two such that for all gGg \in G, g/2=gg/2g/2 = g - g/2.

Totally ordered halving groups

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

A strictly ordered pointed halving group AA is an Archimedean ordered pointed halving group if for all elements a:Aa:A and b:Ab:A, if a<ba \lt b, then there merely exists a dyadic rational number d:𝔻d:\mathbb{D} such that a<h(d)a \lt h(d) and h(d)<bh(d) \lt b.

Sequentially Cauchy complete Archimedean ordered pointed halving groups

Let AA be an Archimedean ordered pointed halving group 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 23:34:22 by Anonymous?. See the history of this page for a list of all contributions to it.