11.3.4 Cauchy reals are Cauchy complete

We constructed ${ℝ}_{𝖼}$ by closing $\mathbb{Q}$ under limits of Cauchy approximations, so it betterbe the case that ${ℝ}_{𝖼}$ is Cauchy complete. Thanks to RC-sim-eqv-le there is nodifference between a Cauchy approximation $x:{\mathbb{Q}}_{+}\to {ℝ}_{𝖼}$ as defined in the constructionof ${ℝ}_{𝖼}$, and a Cauchy approximation in the sense of defn:cauchy-approximation(adapted to ${ℝ}_{𝖼}$).

Thus, given a Cauchy approximation $x:{\mathbb{Q}}_{+}\to {ℝ}_{𝖼}$ it is quite natural to expect that$\mathrm{𝗅𝗂𝗆}(x)$ is its limit, where the notion of limit is defined as indefn:cauchy-approximation. But this is so by RC-sim-eqv-le andthm:RC-sim-lim-term. We have proved:

Theorem 11.3.1.

Every Cauchy approximation in ${\mathrm{R}}_{\mathrm{c}}$ has a limit.

An archimedean ordered field in which every Cauchy approximation has a limit is calledCauchy complete.The Cauchy reals are the least such field.

Theorem 11.3.2.

The Cauchy reals embed into every Cauchy complete archimedean ordered field.

Proof.

Suppose $F$ is a Cauchy complete archimedean ordered field. Because limits are unique,there is an operator $lim$ which takes Cauchy approximations in $F$ to their limits. Wedefine the embedding $e:{ℝ}_{𝖼}\to F$ by $({ℝ}_{𝖼},\mathrm{\sim })$-recursion as

$$e(\mathrm{𝗋𝖺𝗍}(q)):\equiv q\mathit{\hspace{1em}\hspace{1em}}\text{and}\mathit{\hspace{1em}\hspace{1em}}e(\mathrm{𝗅𝗂𝗆}(x)):\equiv lim(e\circ x).$$

A suitable $⌢$ on $F$ is

This is a separated relation because $F$ is archimedean. The rest of the clauses for$({ℝ}_{𝖼},\mathrm{\sim })$-recursion are easily checked. One would also have to check that $e$ isan embedding of ordered fields which fixes the rationals.∎