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 the extension of the additive inverse , using \autorefRC-extend-Q-Lipschitz with Lipschitz constant . We have to work a bit harder for addition.
We use -recursion to construct the curried form of as a map where is the space of non-expanding real-valued functions:
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 the extension of the Lipschitz map from to , as constructed in \autorefRC-extend-Q-Lipschitz with Lipschitz constant . Next, for a Cauchy approximation , we define as
For this to be a valid definition, should be a Cauchy approximation, so consider any . Then by assumption , hence . Furthermore, is non-expanding because is such by induction hypothesis. 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 have as required. ∎
We may apply \autorefRC-binary-nonexpanding-extension to any bivariate rational function which is non-expanding separately in each variable. Addition is such a function, therefore we get . Furthermore, the extension is unique as long as we require 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-expanding maps is again non-expanding, we may conclude that addition satisfies the usual properties, such as commutativity and associativity. Therefore, is a commutative group.
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 and transitive, 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 .
From we merely get such that , and we may take . ∎
We now have enough structure on to express with standard concepts.
If and satisfy , then for any and , if then .
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
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 . ∎
Suppose and satisfy . Then:
For any and , if then .
There exists such that for any , if we have .
We are now able to show that the auxiliary relation is what we think it is.
for all and .
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 the map is Lipschitz with constant11We defined Lipschitz constants as positive rational numbers. , and so we can extend it to multiplication by on the real numbers. Therefore is a vector space over . In general, we can define multiplication of real numbers as
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.
There exists a unique function which extends squaring of rational numbers and satisfies
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 to extend 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 sense of \autorefRC-continuous-eq. Therefore, by \autoreflem:images_are_coequalizers the map
factors uniquely through to give us the desired function. ∎
A Cauchy real is invertible if, and only if, it is apart from zero.
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 the inverse function is obtained by an application of \autorefRC-extend-Q-Lipschitz with Lipschitz constant . Finally, \autoreflem:images_are_coequalizers guarantees that the inverse function factors uniquely through . ∎
The Cauchy reals form an archimedean ordered field.
|Title||11.3.3 The algebraic structure of Cauchy reals|