Archimedean ordered fields are real
As a preliminary, we agree to some conventions. Let denote an ordered field with ordering relation . We will identify the integers with multiples of the multiplicative identity of fields. We further assume that satisfies the Archimedean property: for every element of , there exists an integer such that .
Since is an ordered field, it must have characteristic zero. Hence, the subfield generated by the multiplicative identity is isomorphic to the field of rational numbers. Following the convention proposed above, we will identify this subfield with . We use this subfield to construct a map from to :
For every , we define
For every , we find that is a Dedekind cut.
Because, for all , we have either or , the two sets of form a partition of . Furthermore, every element of the latter set is less than every element of the former set. By the Archimedean property, there exists an integer such that ; hence the former set is not empty. Likewise, there exists and integer such that , or , so the latter set is also not empty. ∎
The map is a monomorphism.
Let and be elements of ; set , set , and set . Since and implies for all rational numbers and , it follows that and implies that . Likewise, since and implies for all rational numbers and , it follows that and implies . Hence, .
Since a rational number is positive if and only if it is greater than , it follows that . Together with the fact proven in the last paragraph, this implies that for all .
Suppose that and are positive elements of . As before, set , set , and set . Since and implies for all rational numbers and , it follows that and implies that . Likewise, since and implies for all rational numbers and , it follows that and implies . Hence, .
By using the fact demonstrated previously that , we may extend what was shown above to the statement that for all . Thus, is a morphism of fields. Since is Archmiedean, if , there must exist a rational number between and , hence , so is a monomorphism. ∎
|Title||Archimedean ordered fields are real|
|Date of creation||2013-03-22 17:26:22|
|Last modified on||2013-03-22 17:26:22|
|Last modified by||rspuzio (6075)|