11.2.3 Dedekind reals are Dedekind complete
We obtained as the type of Dedekind cuts on . But we could have instead started with any archimedean ordered field and constructed Dedekind cuts on . These would again form an archimedean ordered field , the Dedekind completion of , with contained as a subfield. What happens if we apply this construction to , do we get even more real numbers? The answer is negative. In fact, we shall prove a stronger result: is final.
Every archimedean ordered field which is admissible for is a subfield of .
Let be an archimedean ordered field. For every define by
(We have just used the assumption that is admissible for .) Then is a Dedekind cut. Indeed, the cuts are inhabited and rounded because is archimedean and is transitive, disjoint because is irreflexive, and located because is a weak linear order. Let be the map .
so indeed preserves and reflects the order. That holds because, for all ,
The implication from right to left is obvious. For the other direction, if then there merely exists such that , and by taking we get the desired and . We leave preservation of multiplication by as an exercise. ∎
To establish that the Dedekind cuts on do not give us anything new, we need just one more lemma.
If is admissible for then so is its Dedekind completion.
The Dedekind reals are Dedekind complete: for every real-valued Dedekind cut there is a unique such that and for all .
By \autoreflem:cuts-preserve-admissibility the Dedekind completion of is admissible for , so by \autorefRD-final-field we have an embedding , as well as an embedding . But these embeddings must be isomorphisms, because their compositions are order-preserving field homomorphisms which fix the dense subfield , which means that they are the identity. The corollary now follows immediately from the fact that is an isomorphism. ∎
|Title||11.2.3 Dedekind reals are Dedekind complete|