11.1 The field of rational numbers
We first construct the rational numbers , as the reals can then be seen as a completion of . An expert will point out that could be replaced by any approximate field, i.e., a subring of in which arbitrarily precise approximate inverses exist. An example is the ring of dyadic rationals, which are those of the form . If we were implementing constructive mathematics on a computer, an approximate field would be more suitable, but we leave such finesse for those who care about the digits of .
We constructed the integers in \autorefsec:set-quotients as a quotient of , and observed that this quotient is generated by an idempotent. In \autorefsec:free-algebras we saw that is the free group on ; we could similarly show that it is the free commutative ring on . The field of rationals is constructed along the same lines as well, namely as the quotient
In other words, a pair represents the rational number . There can be no division by zero because we cunningly added one to the denominator . Here too we have a canonical choice of representatives, namely fractions in lowest terms. Thus we may apply \autoreflem:quotient-when-canonical-representatives to obtain a set , which again has a decidable equality.
We do not bother to write down the arithmetical operations on as we trust our readers know how to compute with fractions even in the case when one is added to the denominator. Let us just record the conclusion that there is an entirely unproblematic construction of the ordered field of rational numbers , with a decidable equality and decidable order. It can also be characterized as the initial ordered field.
Let be the type of positive rational numbers.
|Title||11.1 The field of rational numbers|