11.3.4 Cauchy reals are Cauchy complete

We constructed ${ℝ}_{𝖼}$ by closing $\mathbb{Q}$ under limits of Cauchy approximations, so it better be the case that ${ℝ}_{𝖼}$ is Cauchy complete. Thanks to RC-sim-eqv-le there is no difference between a Cauchy approximation $x:{\mathbb{Q}}_{+}\to {ℝ}_{𝖼}$ as defined in the construction of ${ℝ}_{𝖼}$, 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 in defn:cauchy-approximation. But this is so by RC-sim-eqv-le and thm: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 called Cauchy 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. We define 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$ is an embedding of ordered fields which fixes the rationals. ∎

Title	11.3.4 Cauchy reals are Cauchy complete