## Definition ## ### Abelian groups ### An **abelian group** is a pointed set $(A, 0)$ with a binary operation $(-)-(-):A \times A \to A$ called **subtraction** such that * for all $a \in A$, $a - a = 0$ * for all $a \in A$, $0 - (0 - a) = a$ * for all $a \in A$ and $b \in A$, $a - (0 - b) = b - (0 - a)$ * for all $a \in A$, $b \in A$, and $c \in A$, $a - (b - c) = (a - (0 - c)) - b$ ### Halving groups ### A **halving group** is an abelian group *G* with a function $(-)/2:G \to G$ called **halving** or **dividing by two** such that for all $g \in G$, $g/2 = g - g/2$. ### Totally ordered halving groups ### An abelian group $R$ is a totally ordered abelian group if it comes with a function $\max:R \times R \to R$ such that * for all elements $a:R$, $\max(a, a) = a$ * for all elements $a:R$ and $b:R$, $\max(a, b) = \max(b, a)$ * for all elements $a:R$, $b:R$, and $c:R$, $\max(a, \max(b, c)) = \max(\max(a, b), c)$ * for all elements $a:R$ and $b:R$, $\max(a, b) = b$ implies that for all elements $c:R$, $\max(a - c, b - c) = b - c$ * for all elements $a:R$ and $b:R$, $\max(a, b) = a$ or $\max(a, b) = b$ ### Strictly ordered pointed halving groups ### A totally ordered commutative ring $R$ is a strictly ordered pointed abelian group if it comes with an element $1:R$ and a type family $\lt$ such that * for all elements $a:R$ and $b:R$, $a \lt b$ is a proposition * for all elements $a:R$, $a \lt a$ is false * for all elements $a:R$, $b:R$, and $c:R$, if $a \lt c$, then $a \lt b$ or $b \lt c$ * for all elements $a:R$ and $b:R$, if $a \lt b$ is false and $b \lt a$ is false, then $a = b$ * for all elements $a:R$ and $b:R$, if $a \lt b$, then $b \lt a$ is false. * $0 \lt 1$ * for all elements $a:R$ and $b:R$, if $0 \lt a$ and $0 \lt b$, then $0 \lt a - (0 - b)$ ... ### Archimedean ordered pointed halving groups ### A strictly ordered pointed halving group $A$ is an Archimedean ordered pointed halving group if for all elements $a:A$ and $b:A$, if $a \lt b$, then there merely exists a dyadic rational number $d:\mathbb{D}$ such that $a \lt h(d)$ and $h(d) \lt b$. ### Sequentially Cauchy complete Archimedean ordered pointed halving groups ### Let $A$ be an Archimedean ordered pointed halving group and let $$A_{+} \coloneqq \sum_{a:A} 0 \lt a$$ be the positive elements in $A$. $A$ is **sequentially Cauchy complete** if every Cauchy sequence in $A$ converges: $$isCauchy(x) \coloneqq \forall \epsilon \in A_{+}. \exists N \in I. \forall i \in I. \forall j \in I. (i \geq N) \wedge (j \geq N) \wedge (\vert x_i - x_j \vert \lt \epsilon)$$ $$isLimit(x, l) \coloneqq \forall \epsilon \in A_{+}. \exists N \in I. \forall i \in I. (i \geq N) \to (\vert x_i - l \vert \lt \epsilon)$$ $$\forall x: \mathbb{N} \to A. isCauchy(x) \wedge \exists l \in A. isLimit(x, l)$$ category: not redirected to nlab yet