nLab Archimedean ordered field setoid

Idea

A setoid or Bishop set whose quotient set is an Archimedean ordered field.

“Archimedean ordered field setoid” and “Bishop Archimedean ordered field” are placeholder names for a concept which may or may not have another name in the mathematics literature.

Definition

Given any ordered field setoid $F$, there exists a ring setoid homomorophism $h$ from the rational numbers $\mathbb{Q}$ to $F$. This setoid homomorphism is also an injection, which implies that one can suppress the homomorphism via coercion, such that given $q \in \mathbb{Q}$ one can derive that $q \in F$.

Then, an ordered field setoid $F$ is Archimedean if for all elements $x \in F$ and $y \in F$, if $x \lt y$, then there exists a rational number $q \in \mathbb{Q}$ such that $x \lt q$ and $q \lt y$.

Properties

• Every Archimedean ordered field setoid is a pseudometric space.

Examples

• Given any Archimedean ordered field $F$, the set of Cauchy sequences in $F$ is an Archimedean ordered field setoid.

• Given any Archimedean ordered field $F$, the set of all locators of all elements of $F$ is an Archimedean ordered field setoid.

Related concepts

• setoid, Bishop set

• ordered field setoid

• pseudometric space

• Archimedean ordered field

• sequentially Cauchy complete Archimedean ordered field setoid