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.
Say that an ordered fieldΒ is admissible for when the strict order onΒ is a map .
Theorem 11.2.1.
Every archimedean ordered field which is admissible for is a subfield ofΒ .
Proof.
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 .
We claim that is a field embedding which preserves and reflects the order. First of all, notice that for a rational number . Next we have the equivalences, for all ,
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.
Lemma 11.2.2.
If is admissible for then so is its Dedekind completion.
Proof.
Let be the Dedekind completion of . The strict order on is defined by
Since and are elements of , the lemma holds as long as is closed under conjunctions and countable existentials, which we assumed from the outset. β
Corollary 11.2.3.
The Dedekind reals are Dedekind complete: for every real-valued Dedekind cut there is a unique such that and for all .
Proof.
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 |
\metatable |