[[!redirects ordered abelian group]] ## Definition ## ### With strict order ### An __ordered abelian group__ is an [[abelian group]] $A$ with a [[strict order]] $\lt$ and a family of dependent terms $$a:A, b:A \vdash \alpha(a, b): (0 \lt a) \times (0 \lt b) \to (0 \lt a + b)$$ ### With positivity ### An __ordered abelian group__ is an [[abelian group]] $A$ with a [[predicate]] $\mathrm{isPositive}$ such that * zero is not positive: $$\mathrm{isPositive}(0) \to \emptyset$$ * 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)$$ ## Examples ## * The [[integers]] are a strictly ordered abelian group * The [[rational numbers]] are a strictly ordered abelian group * Every [[ordered integral domain]] is a strictly ordered abelian group ## See also ## * [[abelian group]] * [[ramp function]] * [[ordered integral domain]] * [[Archimedean ordered abelian group]] category: not redirected to nlab yet