nLab number line rig







In this article we axiomatize the algebraic, order theoretic, and metric properties which are common to the basic types of numbers found in mathematics: the natural numbers, integers, rational numbers, and Dedekind real numbers, and which remain valid in constructive and predicative mathematics.


A number line rig SS is

  • A commutative rig (S,0,1,+,)(S, 0, 1, +, \cdot). It follows that there is a rig homomorphism h:Sh:\mathbb{N} \to S, since the natural numbers are the initial commutative rig

  • with a strict total order (S,<)(S, \lt) such that

    • 0<10 \lt 1
    • 0<a0 \lt a and 0<b0 \lt b imply that 0<a+b0 \lt a + b
    • 0<a0 \lt a and 0<b0 \lt b imply that 0<ab0 \lt a \cdot b
  • with a tight apartness relation (S,#)(S, \#) such that a#ba \# b if and only if a<ba \lt b or b<ab \lt a

  • with a pseudolattice structure (S,,min,max)(S, \leq, \min, \max) such that

    • aba \leq b if and only if ¬(b<a)\neg (b \lt a)
    • aba \leq b if and only if a+cb+ca + c \leq b + c
  • with a metric ρ:S×SS\rho:S \times S \to S such that ρ(a,b)+min(a,b)=max(a,b)\rho(a, b) + \min(a, b) = \max(a, b). Every element in the image of ρ\rho is always not less than zero, because by definition of a pseudolattice, min(a,b)max(a,b)\min(a, b) \leq \max(a, b). This can be shown to be a translation-invariant metric, where it follows that addition is a cancellative monoid:

    • a=ba = b if and only if ρ(a,b)=0\rho(a, b) = 0
    • ρ(a,b)=ρ(b,a)\rho(a, b) = \rho(b, a)
    • ρ(a,b)ρ(a,c)+ρ(c,b)\rho(a, b) \leq \rho(a, c) + \rho(c, b)
    • ρ(a+c,b+c)=ρ(a,b)\rho(a + c, b + c) = \rho(a, b).
  • The multiplicative subset of cancellative elements is the set of elements apart from zero

  • and SS satisfies the Archimedean property: for every positive element 0<a0 \lt a, there is a positive natural number nn such that a<h(n)a \lt h(n), and there is a positive natural number mm such that 1<h(m)a1 \lt h(m) \cdot a.

Group completion, rig of fractions, and completions

Given any number line rig, one could construct the group completion, which results in a Archimedean integral domain. One could also localize at the subset of regular elements, which results in a rig of fractions. Doing both results in an Archimedean field. One could also complete the resulting field by Dedekind cuts, resulting in the Dedekind real numbers, or complete it by Cauchy sequences, resulting in a sequentially Cauchy complete Archimedean field such as the HoTT book real numbers.

See also

Last revised on December 24, 2023 at 22:09:06. See the history of this page for a list of all contributions to it.