## Definition ## An __ordered integral domain__ is a [[totally ordered commutative ring]] which comes with a strict order $\lt$ such that * $0 \lt 1$ * for all elements $a:R$ and $b:R$, if $0 \lt a$ and $0 \lt b$, then $0 \lt a + b$ * for all elements $a:R$ and $b:R$, if $0 \lt a$ and $0 \lt b$, then $0 \lt a \cdot b$ * for all elements $a:R$ and $b:R$, if $0 \lt \max(a, -a)$ and $0 \lt \max(b, -b)$, then $0 \lt \max(a \cdot b, -a \cdot b)$ ### With positivity ### An ordered field is a [[commutative ring]] with a [[predicate]] $\mathrm{isPositive}$ such that * zero is not positive: $$\mathrm{isPositive}(0) \to \emptyset$$ * one is positive: $$\mathrm{isPositive}(1)$$ * for every term $a:A$, if $a$ is not positive and $-a$ is not positive, then $a = 0$ $$\prod_{a:A} ((\mathrm{isPositive}(a) \to \emptyset) \times (\mathrm{isPositive}(-a) \to \emptyset)) \to (a = 0)$$ * for every term $a:A$, if $a$ is positive, then $-a$ is not positive. $$\prod_{a:A} \prod_{b:A} \mathrm{isPositive}(a) \to (\mathrm{isPositive}(-a) \to \emptyset)$$ * for every term $a:A$, $b:A$, if $a$ is positive, then either $b$ is positive or $a - b$ is positive. $$\prod_{a:A} \prod_{b:A} \mathrm{isPositive}(a) \to \left[\mathrm{isPositive}(b) + \mathrm{isPositive}(a - b)\right]$$ * for every term $a:A$, $b:A$, if $a$ is positive and $b$ is positive, then $a + b$ is positive $$\prod_{a:A} \prod_{b:A} \mathrm{isPositive}(a) \times \mathrm{isPositive}(b) \to \mathrm{isPositive}(a + b)$$ * for every term $a:A$, $b:A$, if $a$ is positive and $b$ is positive, then $a \cdot b$ is positive $$\prod_{a:A} \prod_{b:A} \mathrm{isPositive}(a) \times \mathrm{isPositive}(b) \to \mathrm{isPositive}(a \cdot b)$$ * for every term $a:A$, if $a$ is positive, then there exists a $b$ such that $a \cdot b = 1$ and $b \cdot a = 1$ $$\prod_{a:A} \mathrm{isPositive}(a) \to \left[\sum_{b:A} (a \cdot b = 1) \times (b \cdot a = 1)\right]$$ ## Examples ## * The [[integers]] are an ordered integral domain. * The [[rational numbers]] are a ordered integral domain ## See also ## * [[ordered abelian group]] category: not redirected to nlab yet