11.3.3 The algebraic structure of Cauchy reals

We first define the additivePlanetmathPlanetmath structureMathworldPlanetmath (ℝ𝖼,0,+,-). Clearly, the additive unit element 0 is just 𝗋𝖺𝗍⁒(0), while the additive inverse -:ℝ𝖼→ℝ𝖼 is obtained as the extensionPlanetmathPlanetmathPlanetmathPlanetmath of the additive inverse -:β„šβ†’β„š, using \autorefRC-extend-Q-Lipschitz with Lipschitz constantΒ 1. We have to work a bit harder for additionPlanetmathPlanetmath.

Lemma 11.3.1.

Suppose f:Q×Q→Q satisfies, for all q,r,s:Q,


Then there is a function fΒ―:RcΓ—Rcβ†’Rc such that f¯⁒(rat⁒(q),rat⁒(r))=f⁒(q,r) for all q,r:Q. Furthermore, for all u,v,w:Rc and q:Q+,


We use (ℝ𝖼,∼)-recursion to construct the curried form of fΒ― as a map ℝ𝖼→A where A is the space of non-expanding real-valued functions:


We shall also need a suitable ⌒ϡ on A, which we define as


Clearly, if βˆ€(Ο΅:β„š+).h⌒ϡk then h⁒(u)=k⁒(u) for all u:ℝ𝖼, so ⌒ is separated.

For the base case we define f¯⁒(𝗋𝖺𝗍⁒(q)):A, where q:β„š, as the extension of the Lipschitz map λ⁒r.f⁒(q,r) from β„šβ†’β„š to ℝ𝖼→ℝ𝖼, as constructed in \autorefRC-extend-Q-Lipschitz with Lipschitz constantΒ 1. Next, for a Cauchy approximation x, we define f¯⁒(𝗅𝗂𝗆⁒(x)):ℝ𝖼→ℝ𝖼 as


For this to be a valid definition, λ⁒ϡ.f¯⁒(xΟ΅)⁒(v) should be a Cauchy approximation, so consider any Ξ΄,Ο΅:β„š. Then by assumptionPlanetmathPlanetmath f¯⁒(xΞ΄)⌒δ+Ο΅f¯⁒(xΟ΅), hence f¯⁒(xΞ΄)⁒(v)∼δ+Ο΅f¯⁒(xΟ΅)⁒(v). Furthermore, f¯⁒(𝗅𝗂𝗆⁒(x)) is non-expanding because f¯⁒(xΟ΅) is such by induction hypothesis. Indeed, if u∼ϡv then, for all Ο΅:β„š,


therefore f¯⁒(𝗅𝗂𝗆⁒(x))⁒(u)∼ϡf¯⁒(𝗅𝗂𝗆⁒(x))⁒(v) by the fourth constructor of ∼.

We still have to check four more conditions, let us illustrate just one. Suppose Ο΅:β„š+ and for some Ξ΄:β„š+ we have 𝗋𝖺𝗍⁒(q)∼ϡ-Ξ΄yΞ΄ and f¯⁒(𝗋𝖺𝗍⁒(q))⌒ϡ-Ξ΄f¯⁒(yΞ΄). To show f¯⁒(𝗋𝖺𝗍⁒(q))⌒ϡf¯⁒(𝗅𝗂𝗆⁒(y)), consider any v:ℝ𝖼 and observe that


Therefore, by the second constructor of ∼, we have f¯⁒(𝗋𝖺𝗍⁒(q))⁒(v)∼ϡf¯⁒(𝗅𝗂𝗆⁒(y))⁒(v) as required. ∎

We may apply \autorefRC-binary-nonexpanding-extension to any bivariate rational functionMathworldPlanetmath 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, identitiesPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath 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, (ℝ𝖼,0,+,-) is a commutative group.

We may also apply \autorefRC-binary-nonexpanding-extension to the functions min:β„šΓ—β„šβ†’β„š and max:β„šΓ—β„šβ†’β„š, which turns ℝ𝖼 into a latticeMathworldPlanetmathPlanetmath. The partial orderMathworldPlanetmath ≀ on ℝ𝖼 is defined in terms of max as


The relationMathworldPlanetmathPlanetmath ≀ is a partial order because it is such on β„š, and the axioms of a partial order are expressible as equations in terms of min and max, so they transfer to ℝ𝖼.

Another function which extends to ℝ𝖼 by the same method is the absolute valueMathworldPlanetmathPlanetmathPlanetmathPlanetmath |–|. Again, it has the expected properties because they transfer from β„š to ℝ𝖼.

From ≀ we get the strict order < by


That is, u<v holds when there merely exists a pair of rational numbers q<r such that x≀𝗋𝖺𝗍⁒(q) and 𝗋𝖺𝗍⁒(r)≀v. It is not hard to check that < is irreflexiveMathworldPlanetmath and transitiveMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, 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 Rc).

For every u,v:Rc such that u<v there merely exists q:Q such that u<q<v.


From u<v we merely get r,s:β„š such that u≀r<s≀v, and we may take q:≑(r+s)/2. ∎

We now have enough structure on ℝ𝖼 to express u∼ϡv with standard concepts.

Lemma 11.3.3.

If q:Q and u:Rc satisfy u≀rat⁒(q), then for any v:Rc and Ο΅:Q+, if u∼ϡv then v≀rat⁒(q+Ο΅).


Note that the function max⁑(𝗋𝖺𝗍⁒(q),–):ℝ𝖼→ℝ𝖼 is Lipschitz with constant 1. First consider the case when u=𝗋𝖺𝗍⁒(r) is rational. For this we use inductionMathworldPlanetmath on v. If v is rational, then the statement is obvious. If v is 𝗅𝗂𝗆⁒(y), we assume inductively that for any Ο΅,Ξ΄, if 𝗋𝖺𝗍⁒(r)∼ϡyΞ΄ then yδ≀𝗋𝖺𝗍⁒(q+Ο΅), i.e.Β max⁑(𝗋𝖺𝗍⁒(q+Ο΅),yΞ΄)=𝗋𝖺𝗍⁒(q+Ο΅).

Now assuming Ο΅ and 𝗋𝖺𝗍⁒(r)βˆΌΟ΅π—…π—‚π—†β’(y), we have ΞΈ such that 𝗋𝖺𝗍⁒(r)∼ϡ-θ𝗅𝗂𝗆⁒(y), hence 𝗋𝖺𝗍⁒(r)∼ϡyΞ΄ whenever Ξ΄<ΞΈ. Thus, the inductive hypothesis gives max⁑(𝗋𝖺𝗍⁒(q+Ο΅),yΞ΄)=𝗋𝖺𝗍⁒(q+Ο΅) for such Ξ΄. But by definition,


Since the limit of an eventually constant Cauchy approximation is that constant, we have


hence 𝗅𝗂𝗆⁒(y)≀𝗋𝖺𝗍⁒(q+Ο΅).

Now consider a general u:ℝ𝖼. Since u≀𝗋𝖺𝗍⁒(q) means max⁑(𝗋𝖺𝗍⁒(q),u)=𝗋𝖺𝗍⁒(q), the assumption u∼ϡv and the Lipschitz property of max⁑(𝗋𝖺𝗍⁒(q),-) imply max⁑(𝗋𝖺𝗍⁒(q),v)βˆΌΟ΅π—‹π–Ίπ—β’(q). Thus, since 𝗋𝖺𝗍⁒(q)≀𝗋𝖺𝗍⁒(q), the first case implies max⁑(𝗋𝖺𝗍⁒(q),v)≀𝗋𝖺𝗍⁒(q+Ο΅), and hence v≀𝗋𝖺𝗍⁒(q+Ο΅) by transitivity of ≀. ∎

Lemma 11.3.4.

Suppose q:Q and u:Rc satisfy u<rat⁒(q). Then:

  1. 1.

    For any v:ℝ𝖼 and Ο΅:β„š+, if u∼ϡv then v<𝗋𝖺𝗍⁒(q+Ο΅).

  2. 2.

    There exists Ο΅:β„š+ such that for any v:ℝ𝖼, if u∼ϡv we have v<𝗋𝖺𝗍⁒(q).


By definition, u<𝗋𝖺𝗍⁒(q) means there is r:β„š with r<q and u≀𝗋𝖺𝗍⁒(r). Then by \autorefthm:RC-le-grow, for any Ο΅, if u∼ϡv then v≀𝗋𝖺𝗍⁒(r+Ο΅). ConclusionMathworldPlanetmathΒ 1 follows immediately since r+Ο΅<q+Ο΅, while forΒ 2 we can take any Ο΅<q-r. ∎

We are now able to show that the auxiliary relation ∼ is what we think it is.

Theorem 11.3.5.

(u∼ϡv)≃(|u-v|<𝗋𝖺𝗍(Ο΅)) for all u,v:Rc and Ο΅:Q+.


The Lipschitz properties of subtractionPlanetmathPlanetmath and absolute value imply that if u∼ϡv, then |u-v|∼ϡ|u-u|=0. Thus, for the left-to-right direction, it will suffice to show that if u∼ϡ0, then |u|<𝗋𝖺𝗍⁒(Ο΅). We proceed by ℝ𝖼-induction on u.

If u is rational, the statement follows immediately since absolute value and order extend the standard ones on β„š+. If u is 𝗅𝗂𝗆⁒(x), then by roundedness we have ΞΈ:β„š+ with 𝗅𝗂𝗆⁒(x)∼ϡ-ΞΈ0. By the triangle inequalityMathworldMathworldPlanetmath, therefore, we have xΞΈ/3∼ϡ-2⁒θ/30, so the inductive hypothesis yields |xΞΈ/3|<𝗋𝖺𝗍⁒(Ο΅-2⁒θ/3). But xΞΈ/3∼2⁒θ/3𝗅𝗂𝗆⁒(x), hence |xΞΈ/3|∼2⁒θ/3|𝗅𝗂𝗆⁒(x)| by the Lipschitz property, so \autorefthm:RC-lt-open1 implies |𝗅𝗂𝗆⁒(x)|<𝗋𝖺𝗍⁒(Ο΅).

In the other direction, we use ℝ𝖼-induction on u and v. If both are rational, this is the first constructor of ∼.

If u is 𝗋𝖺𝗍⁒(q) and v is 𝗅𝗂𝗆⁒(y), we assume inductively that for any Ο΅,Ξ΄, if |𝗋𝖺𝗍⁒(q)-yΞ΄|<𝗋𝖺𝗍⁒(Ο΅) then 𝗋𝖺𝗍⁒(q)∼ϡyΞ΄. Fix an Ο΅ such that |𝗋𝖺𝗍⁒(q)-𝗅𝗂𝗆⁒(y)|<𝗋𝖺𝗍⁒(Ο΅). Since β„š is order-dense in ℝ𝖼, there exists ΞΈ<Ο΅ with |𝗋𝖺𝗍⁒(q)-𝗅𝗂𝗆⁒(y)|<𝗋𝖺𝗍⁒(ΞΈ). Now for any Ξ΄,Ξ· we have 𝗅𝗂𝗆⁒(y)∼2⁒δyΞ΄, hence by the Lipschitz property


Thus, by \autorefthm:RC-lt-open1, we have |𝗋𝖺𝗍⁒(q)-yΞ΄|<𝗋𝖺𝗍⁒(ΞΈ+2⁒δ). So by the inductive hypothesis, 𝗋𝖺𝗍⁒(q)∼θ+2⁒δyΞ΄, and thus 𝗋𝖺𝗍⁒(q)∼θ+4⁒δ𝗅𝗂𝗆⁒(y) by the triangle inequality. Thus, it suffices to choose Ξ΄:≑(Ο΅-ΞΈ)/4.

The remaining two cases are entirely analogous. ∎

Next, we would like to equip ℝ𝖼 with multiplicative structure. For each q:β„š the map r↦qβ‹…r is Lipschitz with constant11We defined Lipschitz constants as positive rational numbers. |q|+1, and so we can extend it to multiplication by q on the real numbers. Therefore ℝ𝖼 is a vector space over β„š. In general, we can define multiplication of real numbers as

uβ‹…v:≑12β‹…((u+v)2-u2-v2), (11.3.6)

so we just need squaring u↦u2 as a map ℝ𝖼→ℝ𝖼. Squaring is not a Lipschitz map, but it is Lipschitz on every bounded domain, which allows us to patch it together. Define the open and closed intervalsMathworldPlanetmath

[u,v]:≑\setofx:ℝ𝖼|u≀x≀v  and  (u,v):≑\setofx:ℝ𝖼|u<x<v.

Although technically an element of [u,v] or (u,v) 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 x:[u,v] whenever x:ℝ𝖼 is such that u≀x≀v, and similarly.

Theorem 11.3.7.

There exists a unique function (–)2:Rcβ†’Rc which extends squaring q↦q2 of rational numbers and satisfies


We first observe that for every u:ℝ𝖼 there merely exists n:β„• such that -n≀u≀n, see \autorefex:traditional-archimedean, so the map

e:(βˆ‘n:β„•[-n,n])→ℝ𝖼  defined by  e(n,x):≑x

is surjective. Next, for each n:β„•, the squaring map

sn:\setofq:β„š|-n≀q≀nβ†’β„šβ€ƒβ€ƒdefined by  sn(q):≑q2

is Lipschitz with constant 2⁒n, so we can use \autorefRC-extend-Q-Lipschitz to extend it to a map sΒ―n:[-n,n]→ℝ𝖼 with Lipschitz constant 2⁒n, see \autorefRC-Lipschitz-on-interval for details. The maps sΒ―n are compatible: if m<n for some m,n:β„• then sn restricted to [-m,m] must agree with sm because both are Lipschitz, and therefore continuousMathworldPlanetmathPlanetmath in the sense ofΒ \autorefRC-continuous-eq. Therefore, by \autoreflem:images_are_coequalizers the map

(βˆ‘n:β„•[-n,n])→ℝ𝖼,given by  (n,x)↦sn⁒(x)

factors uniquely through ℝ𝖼 to give us the desired function. ∎

At this point we have the ring structure of the reals and the archimedeanPlanetmathPlanetmathPlanetmath order. To establish ℝ𝖼 as an archimedean ordered field, we still need inversesMathworldPlanetmathPlanetmathPlanetmathPlanetmath.

Theorem 11.3.8.

A Cauchy real is invertible if, and only if, it is apart from zero.


First, suppose u:ℝ𝖼 has an inverse v:ℝ𝖼 By the archimedean principle there is q:β„š such that |v|<q. Then 1=|u⁒v|<|u|β‹…v<|u|β‹…q and hence |u|>1/q, which is to say that u#0.

For the converseMathworldPlanetmath 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 q:β„š let

[q,∞):≑\setofu:ℝ𝖼|q≀u  and  (-∞,q]:≑\setofu:ℝ𝖼|u≀-q.

Then, as q ranges over β„š+, the types (-∞,q] and [q,∞) jointly cover \setofu:ℝ𝖼|u#0. On each such [q,∞) and (-∞,q] the inverse function is obtained by an application of \autorefRC-extend-Q-Lipschitz with Lipschitz constant 1/q2. Finally, \autoreflem:images_are_coequalizers guarantees that the inverse function factors uniquely through \setofu:ℝ𝖼|u#0. ∎

We summarize the algebraic structurePlanetmathPlanetmath of ℝ𝖼 with a theorem.

Theorem 11.3.9.

The Cauchy reals form an archimedean ordered field.

Title 11.3.3 The algebraic structure of Cauchy reals