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 |