nLab ordered field

Ordered fields

Ordered fields

Idea

An ordered field is a field equipped with a compatible strict total order.

Note that while the adjective ‘ordered’ usually refers to a partial order, it is traditionally used more strictly when placed before ‘field’.

Definition

Classically:

Definition

An ordered field is a field KK equipped with a strict total order <\lt such that 1>01 \gt 0 and if a,b>0a, b \gt 0, then so are a+ba + b and aba b.

One often sees the definition using a weak total order \leq instead of the strict total order <\lt. This makes no difference in classical mathematics, but the definition of the strict total order is the one that generalizes to constructive mathematics.

An ordered field could also be defined as a field with a predicate isPositive\mathrm{isPositive} such that

  • zero is not positive:
¬isPositive(0)\not \mathrm{isPositive}(0)
  • one is positive:
isPositive(1)\mathrm{isPositive}(1)
  • for every element a:Aa:A, if aa is not positive and a-a is not positive, then a=0a = 0
a:A.¬isPositive(a)¬isPositive(a)(a=0)\forall a:A.\neg\mathrm{isPositive}(a) \wedge \neg\mathrm{isPositive}(-a) \Rightarrow (a = 0)
  • for every term a:Aa:A, if aa is positive, then a-a is not positive.
a:A.b:A.isPositive(a)¬isPositive(a)\forall a:A. \forall b:A. \mathrm{isPositive}(a) \Rightarrow \neg\mathrm{isPositive}(-a)
  • for every term a:Aa:A, b:Ab:A, if aa is positive, then either bb is positive or aba - b is positive.
a:A.b:A.isPositive(a)(isPositive(b)isPositive(ab))\forall a:A. \forall b:A. \mathrm{isPositive}(a) \Rightarrow \left(\mathrm{isPositive}(b) \vee \mathrm{isPositive}(a - b)\right)
  • for every term a:Aa:A, b:Ab:A, if aa is positive and bb is positive, then a+ba + b is positive
a:A.b:A.isPositive(a)isPositive(b)isPositive(a+b)\forall a:A. \forall b:A. \mathrm{isPositive}(a) \wedge \mathrm{isPositive}(b) \Rightarrow \mathrm{isPositive}(a + b)
  • for every term a:Aa:A, b:Ab:A, if aa is positive and bb is positive, then aba \cdot b is positive
a:A.b:A.isPositive(a)isPositive(b)isPositive(ab)\forall a:A. \forall b:A. \mathrm{isPositive}(a) \wedge \mathrm{isPositive}(b) \implies \mathrm{isPositive}(a \cdot b)

The strict total order is defined as

a<bisPositive(ba)a \lt b \coloneqq \mathrm{isPositive}(b - a)

In constructive mathematics.

Due to the fact that in constructive mathematics, a set having a strict total order no longer implies that the set has a weak total order, and a set having a weak total order no longer implies that the set has a strict total order, the notion of ordered field bifurcates into multiple inequivalent notions.

In particular, the traditional definition of an ordered field as defined above no longer implies that

  1. that the ordered field is a lattice, that it has binary joins and meets

  2. that the ordered field, depending on how field is defined (see field#Constructive notions), is no longer Heyting.

Thus, some authors in constructive mathematics, such as Booij 2020 and Univalent Foundatiins Project 2013, have defined an ordered field to additionally have a lattice structure on \leq and be a Heyting field, with the tight apartness relation defined as a#ba \# b if and only if a<ba \lt b or b<ab \lt a.

However, other fields with a strict total order, such as the surreal numbers, do not necessarily have a lattice structure, nor are Heyting, so other authors prefer the more traditional definition given above.

Examples

The field \mathbb{R} of real numbers is the Dedekind-complete ordered field.

The field \mathbb{Q} of rational numbers is a subfield of \mathbb{R} that is too small to be complete.

The field of surreal numbers is a field extension of \mathbb{R} that is too large to be complete.

Properties

Every ordered field must have characteristic 00, since we can prove by induction that n>0n \gt 0 for every positive natural number nn.

As a result, the rational numbers are the initial ordered field, and every ordered field is a \mathbb{Q} -algebra.

The archimedean ordered fields are precisely the subfields of the field of real numbers.

Proposition

Every Dedekind complete ordered field is archimedean.

Proof

Suppose otherwise: let a,b>0a, b \gt 0 be given, and suppose bb is an upper bound of a,2a,3a,a, 2a, 3a, \ldots. Then bab - a is an upper bound of 0,a,2a,0, a, 2a, \ldots and consequently there can be no least upper bound of the sequence, contradicting Dedekind completeness.

The following is a result in classical mathematics.

Proposition

A field admits an order (“is orderable”) if and only if it is a real field, i.e., if the element 1-1 is not a sum of squares.

Proof

Given an ordered field, any non-zero square is positive since either α-\alpha or α\alpha is positive, and so (α) 2=α 2(-\alpha)^2 = \alpha^2 is positive. Hence a sum of non-zero squares cannot be negative, and in particular cannot be equal to 1-1.

In the other direction, every real field FF may be embedded in a real closed field (this requires Zorn's lemma), and a real closed field admits a unique ordering. The restriction of this ordering to the embedded field FF gives an ordering on FF.

See also

References

Last revised on December 5, 2022 at 21:24:39. See the history of this page for a list of all contributions to it.