# nLab Archimedean ordered local integral domain

### Context

#### Algebra

higher algebra

universal algebra

# Contents

## Idea

Since every ordered local integral domain $R$ has characteristic zero, the positive integers $\mathbb{Z}_+$ are a subset of $R$, with injection $i:\mathbb{Z}_+ \hookrightarrow R$. An Archimedean ordered local integral domain is an ordered local integral domain which satisfies the archimedean property: for all elements $a \in R$ and $b \in R$, if $0 \lt a$ and $0 \lt b$, then there exists a positive integer $n \in \mathbb{Z}_+$ such that such that $a \lt i(n) \cdot b$.

Archimedean ordered local integral domains are important because they are the ordered local rings with infinitesimals but no infinite elements, infinitesimals for which the zero-product property fails, or invertible infinitesimals. These play an important role in some approaches to analysis and differential geometry, such as the approaches where the ring of formal power series with $n$ commuting variables on the real numbers is used to model infinitesimals in the real line.

Archimedean ordered fields are the Archimedean ordered local integral domains in which every non-invertible element is equal to zero. However, unlike Archimedean ordered fields, Archimedean ordered local integral domains can be defined inside of an arbitrary arithmetic pretopos in coherent logic, or in dependent type theory without function types and dependent function types.