The reals (constructed as Dedekind cuts) form a field

by Patrick Stevens Jul 5 2016 updated Jul 8 2016

The reals are an archetypal example of a field, but if we are to construct them from simpler objects, we need to show that our construction does indeed have the right properties.

The real numbers, when constructed as Dedekind cuts over the rationals, form a field.

We shall often write the one-sided [dedekind_cut Dedekind cut] $~$(A, B)$~$ %%note:Recall: "one-sided" means that $~$A$~$ has no greatest element.%% as simply $~$\mathbf{A}$~$ (using bold face for Dedekind cuts); we can do this because if we already know $~$A$~$ then $~$B$~$ is completely determined. This will make our notation less messy.

The field structure, together with the [total_order total ordering] on it, is as follows (where we write $~$\mathbf{0}$~$ for the Dedekind cut $~$(\{ r \in \mathbb{Q} \mid r < 0\}, \{ r \in \mathbb{Q} \mid r \geq 0 \})$~$):

where $~$(A, B)$~$ is a one-sided [dedekind_cut Dedekind cut] (so that $~$A$~$ has no greatest element).

(Here, the "set sum" $~$A+C$~$ is defined as "everything that can be made by adding one thing from $~$A$~$ to one thing from $~$C$~$": namely, $~$\{ a+c \mid a \in A, c \in C \}$~$ in Set builder notation; and $~$A \times C$~$ is similarly $~$\{ a \times c \mid a \in A, c \in C \}$~$.)



We need to show firstly that these operations do in fact produce [dedekind_cut Dedekind cuts].


Firstly, we need everything in $~$A+C$~$ to be less than everything in $~$B+D$~$. This is true: if $~$a+c \in A+C$~$, and $~$b+d \in B+D$~$, then since $~$a < b$~$ and $~$c < d$~$, we have $~$a+c < b+d$~$.

Next, we need $~$A+C$~$ and $~$B+D$~$ together to contain all the rationals. This is true: [todo: this, it's quite boring]

Finally, we need $~$(A+C, B+D)$~$ to be one-sided: that is, $~$A+C$~$ needs to have no top element, or equivalently, if $~$a+c \in A+C$~$ then we can find a bigger $~$a' + c'$~$ in $~$A+C$~$. This is also true: if $~$a+c$~$ is an element of $~$A+C$~$, then we can find an element $~$a'$~$ of $~$A$~$ which is bigger than $~$a$~$, and an element $~$c'$~$ of $~$C$~$ which is bigger than $~$C$~$ (since both $~$A$~$ and $~$C$~$ have no top elements, because the respective Dedekind cuts are one-sided); then $~$a' + c'$~$ is in $~$A+C$~$ and is bigger than $~$a+c$~$.


[todo: this section]


[todo: this section]

Additive commutative group structure

[todo: identity, associativity, inverse, commutativity]

Ring structure

[todo: multiplicative identity, associativity, distributivity]

Field structure

[todo: inverses]

Ordering on the field

[todo: a <= b implies a+c <= b+c, and 0 <= a, 0 <= b implies 0 <= ab]