nLab Archimedean property

Contents

 Idea

The Archimedean property states that every positive element in a strictly weakly ordered cancellative commutative monoid is bounded above by a natural number.

So an object satisfying the Archimedean property has no infinite elements. If the strict weak order is additionally a connected relation and thus a pseudo-order, every infinitesimal element is equal to zero.

Definition

In general

Let ( +,1: +,s: + +)(\mathbb{N}^+,1:\mathbb{N}^+,s:\mathbb{N}^+\to \mathbb{N}^+) be the set of positive integers.

Let (A,<,+,0)(A,\lt, +, 0) be a strictly ordered cancellative commutative monoid. The positive integers are embedded into the function monoid AAA \to A; there is an injection inj: +(AA)inj:\mathbb{N}^+\to (A \to A) such that inj(1)=id Ainj(1) = id_A and inj(s(n))=inj(n)+id Ainj(s(n)) = inj(n) + id_A for all n: +n:\mathbb{N}^+.

The archimedean property states that for every a,b:Aa,b:A such that 0<a0 \lt a and 0<b0 \lt b, then there exist n: +n:\mathbb{N}^+ such that a<inj(n)(b)a \lt inj(n)(b).

By uncurrying injinj one gets an action act:( +×A)Aact: (\mathbb{N}^+\times A) \to A such that act(1,a)=aact(1,a) = a and act(s(n),a)=act(n,a)+aact(s(n),a) = act(n,a) + a for all n: +n:\mathbb{N}^+ and a:Aa:A. The archimedean property then states that for all a,b:Aa,b:A such that 0<a0 \lt a and 0<b0 \lt b, there exist n: +n:\mathbb{N}^+ such that a<act(n,b)a \lt act(n,b).

For ordered fields

For ordered fields FF, since \mathbb{Q} is the initial ordered field, there exists a unique ordered field homomorphism i:Fi:\mathbb{Q} \to F for all ordered fields FF. Then the archimedean property for FF states that the rational numbers are dense in FF:

  • for all xFx \in F and yFy \in F such that x<yx \lt y, there exists a rational number q:q:\mathbb{Q} such that x<i(q)<yx \lt i(q) \lt y.

Archimedean structure

In dependent type theory, both definitions of the usual archimedean property above use the phrase “there exists…”. This existence in the definitions is mere existence; i.e. using the existential quantifier rather than the dependent sum type. The untruncated version of the archimedean property using dependent sum types can be called archimedean structure.

In general

Archimedean structure for strictly ordered cancellative commutative monoids (A,<,+,0)(A,\lt, +, 0) using the positive natural numbers says that

  • for every x:Ax:A, y:Ay:A such that 0<x0 \lt x and 0<y0 \lt y, then there exist as structure a positive natural number n: +n:\mathbb{N}^+ such that x<inj(n)(y)x \lt \mathrm{inj}(n)(y).
x:A y:A(0<x)×(0<y) n: +x<inj(n)(y)\prod_{x:A} \prod_{y:A} (0 \lt x) \times (0 \lt y) \to \sum_{n:\mathbb{N}^+} x \lt \mathrm{inj}(n)(y)

Defining the type of positive elements in AA as A + x:A0<xA^+ \coloneqq \sum_{x:A} 0 \lt x, by uncurrying and using the type theoretic axiom of choice, one gets the equivalent statement

x:A + y:A + n: +x<inj(n)(y)\prod_{x:A^+} \prod_{y:A^+} \sum_{n:\mathbb{N}^+} x \lt \mathrm{inj}(n)(y)

which by the type theoretic axiom of choice is the same as saying that

  • there exists as structure a function M:(A +×A +) +M:(A^+ \times A^+) \to \mathbb{N}^+ such that for every x:A +x:A^+ and y:A +y:A^+, x<inj(M(x,y))(y)x \lt \mathrm{inj}(M(x, y))(y)
M:(A +×A +) + x:A + y:A +x<inj(M(x,y))(y)\sum_{M:(A^+ \times A^+) \to \mathbb{N}^+} \prod_{x:A^+} \prod_{y:A^+} x \lt \mathrm{inj}(M(x, y))(y)

These functions can be called the archimedean modulus in parallel to the modulus of convergence and modulus of continuity which are defined for the untruncated versions of the definitions of Cauchy sequence and continuous function.

 For ordered fields

Similarly, archimedean structure for ordered fields states that

  • for all x:Fx:F and y:Fy:F such that x<yx \lt y, there exists as structure a rational number q:q:\mathbb{Q} such that x<i(q)<yx \lt i(q) \lt y.
x:F y:Fx<y q:(x<i(q))×(i(q)<y)\prod_{x:F} \prod_{y:F} x \lt y \to \sum_{q:\mathbb{Q}} (x \lt i(q)) \times (i(q) \lt y)

One could construct archimedean structure for any Archimedean ordered field where every element has a locator. See lemma 6.7.3 of Booij20.

In particular, one could construct archimedean structure for any Archimedean ordered field satisfying trichotomy, that for all x:Fx:F and y:Fy:F, exactly one of x>yx \gt y, x<yx \lt y, x=yx = y is true.

Suppose the Archimedean ordered field FF satisfies trichotomy. Then, the ceiling xxx \mapsto \lceil x \rceil and floor xxx \mapsto \lfloor x \rfloor partial functions are total functions over the entire domain of FF. By definition of the ceiling and the fact that x<yx \lt y, we have that

2yx2yx\left\lceil\frac{2}{y - x}\right\rceil \geq \frac{2}{y - x}

and thus

2yx(yx)=2yxy2yxx2\left\lceil\frac{2}{y - x}\right\rceil (y - x) = \left\lceil\frac{2}{y - x}\right\rceil y - \left\lceil\frac{2}{y - x}\right\rceil x \geq 2

so we have

2yxx<2yxx+2yxy2<2yxy\left\lceil\frac{2}{y - x}\right\rceil x \lt \frac{\left\lceil \left\lceil\frac{2}{y - x}\right\rceil x \right\rceil + \left\lfloor \left\lceil\frac{2}{y - x}\right\rceil y \right\rfloor}{2} \lt \left\lceil\frac{2}{y - x}\right\rceil y

Since x<yx \lt y, 0<2yx0 \lt \left\lceil\frac{2}{y - x}\right\rceil, and so it is possible to divide all sides by 2yx\left\lceil\frac{2}{y - x}\right\rceil and keep the elements in the inequality in order.

x<2yxx+2yxy22yx<yx \lt \frac{\left\lceil \left\lceil\frac{2}{y - x}\right\rceil x \right\rceil + \left\lfloor \left\lceil\frac{2}{y - x}\right\rceil y \right\rfloor}{2 \left\lceil\frac{2}{y - x}\right\rceil} \lt y

Thus, if the Archimedean ordered field satisfies trichotomy, then the Archimedean ordered field has Archimedean structure. In classical mathematics, as well as in constructive mathematics in which the analytic LPO for the terminal Archimedean ordered field is true, every Archimedean ordered field has Archimedean structure.

Examples

References

This is called the archimedean axiom in

The alternative definition of the Archimedean property for ordered fields using the rational numbers is defined in section 11.2.1 of

and in section 4.3 of

Last revised on July 31, 2024 at 22:52:07. See the history of this page for a list of all contributions to it.