11.3.3 The algebraic structure of Cauchy reals
We first define the additive structure
. Clearly, the additive unit element is just , while the additive inverse is obtained as theextension
of the additive inverse , using \\autorefRC-extend-Q-Lipschitzwith Lipschitz constant . We have to work a bit harder for addition
.
Lemma 11.3.1.
Suppose satisfies, for all ,
Then there is a function such that for all . Furthermore,for all and ,
Proof.
We use -recursion to construct the curried form of as a map where is the space of non-expanding real-valuedfunctions:
We shall also need a suitable on , which we define as
Clearly, if then for all , so is separated.
For the base case we define , where , as theextension of the Lipschitz map from to , asconstructed in \\autorefRC-extend-Q-Lipschitz with Lipschitz constant . Next, for aCauchy approximation , we define as
For this to be a valid definition, should be aCauchy approximation, so consider any . Then by assumption, hence. Furthermore, is non-expanding because is such by inductionhypothesis. Indeed, if then, for all ,
therefore by the fourth constructor of .
We still have to check four more conditions, let us illustrate just one. Suppose and for some we have and . To show, consider any and observe that
Therefore, by the second constructor of , we haveas required.∎
We may apply \\autorefRC-binary-nonexpanding-extension to any bivariate rational functionwhich is non-expanding separately in each variable. Addition is such a function, thereforewe get .Furthermore, the extension is unique as long as werequire it to be non-expanding in each variable, and just as in the univariate case,identities
on rationals extend to identities on reals. Since composition of non-expandingmaps is again non-expanding, we may conclude that addition satisfies the usual properties,such as commutativity and associativity.Therefore, is a commutativegroup.
We may also apply \\autorefRC-binary-nonexpanding-extension to the functions and , which turns into a lattice. The partialorder
on is defined in terms of as
The relation is a partial order because it is such on , and the axioms of apartial order are expressible as equations in terms of and , so they transferto .
Another function which extends to by the same method is the absolute value .Again, it has the expected properties because they transfer from to .
From we get the strict order by
That is, holds when there merely exists a pair of rational numbers such that and . It is not hard to check that is irreflexive andtransitive
, and has other properties that are expected for an ordered field.The archimedean principle follows directly from the definition of .
Theorem 11.3.2 (Archimedean principle for ).
For every such that there merely exists such that .
Proof.
From we merely get such that , and we may take .∎
We now have enough structure on to express with standard concepts.
Lemma 11.3.3.
If and satisfy , then for any and , if then .
Proof.
Note that the function is Lipschitz with constant .First consider the case when is rational.For this we use induction on .If is rational, then the statement is obvious.If is , we assume inductively that for any , if then , i.e. .
Now assuming and , we have such that , hence whenever .Thus, the inductive hypothesis gives for such .But by definition,
Since the limit of an eventually constant Cauchy approximation is that constant, we have
hence .
Now consider a general .Since means , the assumption and the Lipschitz property of imply .Thus, since , the first case implies , and hence by transitivity of .∎
Lemma 11.3.4.
Suppose and satisfy . Then:
- 1.
For any and , if then .
- 2.
There exists such that for any , if we have .
Proof.
By definition, means there is with and .Then by \\autorefthm:RC-le-grow, for any , if then .Conclusion 1 follows immediately since , while for 2 we can take any .∎
We are now able to show that the auxiliary relation is what we think it is.
Theorem 11.3.5.
for all and .
Proof.
The Lipschitz properties of subtraction and absolute value imply that if , then .Thus, for the left-to-right direction, it will suffice to show that if , then .We proceed by -induction on .
If is rational, the statement follows immediately since absolute value and order extend the standard ones on .If is , then by roundedness we have with .By the triangle inequality, therefore, we have , so the inductive hypothesis yields .But , hence by the Lipschitz property, so \\autorefthm:RC-lt-open1 implies .
In the other direction, we use -induction on and .If both are rational, this is the first constructor of .
If is and is , we assume inductively that for any , if then .Fix an such that .Since is order-dense in , there exists with .Now for any we have , hence by the Lipschitz property
Thus, by \\autorefthm:RC-lt-open1, we have .So by the inductive hypothesis, , and thus by the triangle inequality.Thus, it suffices to choose .
The remaining two cases are entirely analogous.∎
Next, we would like to equip with multiplicative structure. For each themap is Lipschitz with constant11We defined Lipschitzconstants as positive rational numbers. , and so we can extend it tomultiplication by on the real numbers. Therefore is a vector space over .In general, we can define multiplication of real numbers as
(11.3.6) |
so we just need squaring as a map . Squaring is not aLipschitz map, but it is Lipschitz on every bounded domain, which allows us to patch ittogether. Define the open and closed intervals
Although technically an element of or is a Cauchy real number together with a proof, since the latter inhabits a mere proposition it is uninteresting.Thus, as is common with subset types, we generally write simply whenever is such that , and similarly.
Theorem 11.3.7.
There exists a unique function which extends squaring of rational numbers and satisfies
Proof.
We first observe that for every there merely exists such that , see \\autorefex:traditional-archimedean, so the map
is surjective. Next, for each , the squaring map
is Lipschitz with constant , so we can use \\autorefRC-extend-Q-Lipschitz toextend it to a map with Lipschitz constant , see\\autorefRC-Lipschitz-on-interval for details. The maps are compatible: if for some then restricted to must agree with because both are Lipschitz, and therefore continuous in the senseof \\autorefRC-continuous-eq. Therefore, by \\autoreflem:images_are_coequalizers the map
factors uniquely through to give us the desired function.∎
At this point we have the ring structure of the reals and the archimedean order. Toestablish as an archimedean ordered field, we still need inverses
.
Theorem 11.3.8.
A Cauchy real is invertible if, and only if, it is apart from zero.
Proof.
First, suppose has an inverse By the archimedean principle there is such that . Then and hence , which is to say that .
For the converse we construct the inverse map
by patching together functions, similarly to the construction of squaring in\\autorefRC-squaring. We only outline the main steps. For every let
Then, as ranges over , the types and jointly cover. On each such and theinverse function is obtained by an application of \\autorefRC-extend-Q-Lipschitzwith Lipschitz constant . Finally, \\autoreflem:images_are_coequalizersguarantees that the inverse function factors uniquely through .∎
We summarize the algebraic structure of with a theorem.
Theorem 11.3.9.
The Cauchy reals form an archimedean ordered field.