[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \tableofcontents \section{Commutative rings} A commutative ring is a set $R$ with * a dependent term $x:R, y:R \vdash x + y:R$ * a term $0:R$ * a dependent term $x:R \vdash -x:R$ * a dependent term $x:R, y:R \vdash x \cdot y:R$ * a term $1:R$ * a dependent term $x:R, y:R, z:R \vdash \mathrm{assoc}_+(x, y, z):x + (y + z) =_R (x + y) + z$ * a dependent term $x:R \vdash \mathrm{lunit}_+(x):0 + x =_R x$ * a dependent term $x:R \vdash \mathrm{runit}_+(x):x + 0 =_R x$ * a dependent term $x:R \vdash \mathrm{linv}_+(x):(-x) + x =_R 0$ * a dependent term $x:R \vdash \mathrm{rinv}_+(x):x + (-x) =_R 0$ * a dependent term $x:R, y:R \vdash \mathrm{comm}_+(x, y):x + y =_R y + x$ * a dependent term $x:R, y:R, z:R \vdash \mathrm{assoc}_\cdot(x, y, z):x \cdot (y \cdot z) =_R (x \cdot y) \cdot z$ * a dependent term $x:R \vdash \mathrm{lunit}_\cdot(x):1 \cdot x =_R x$ * a dependent term $x:R \vdash \mathrm{runit}_\cdot(x):x \cdot 1 =_R x$ * a dependent term $x:R, y:R, z:R \vdash \mathrm{ldist}_\cdot(x, y, z):x \cdot (y + z) =_R x \cdot y + x \cdot z$ * a dependent term $x:R, y:R, z:R \vdash \mathrm{rdist}_\cdot(x, y, z):(y + z) \cdot x =_R y \cdot x + z \cdot x$ * a dependent term $x:R, y:R \vdash \mathrm{comm}_\cdot(x, y):x \cdot y =_R y \cdot x$ \section{Ordered commutative rings} An ordered commutative ring is a commutative ring $R$ with a predicate $\mathrm{isPositive}(a)$ indicating that element $a:R$ is positive, such that * zero is not positive * given element $a:R$, if $a$ is positive, then $-a$ is not positive * given elements $a:R$ and $b:R$; if $a$ is positive, then either $b$ is positive or $a - b$ is positive * if both an element $a$ and its negation $-a$ are not positive, then $a$ is equal to zero. * one is positive * the sum of two positive elements is positive * the product of two positive elements is positive \section{Ordered integral domains} Given a commutative ring $R$, an element $a:R$ is regular if for all $b:R$, and $c:R$ the canonical functions $$\mathrm{idtoleftmul}(a, b, c):(b =_R c) \to (a \cdot b =_R a \cdot c)$$ $$\mathrm{idtorightmul}(a, b, c):(b =_R c) \to (b \cdot a =_R c \cdot a)$$ are equivalences: $$\mathrm{isRegular}(a) \coloneqq \prod_{b:A} \prod_{c:A} \mathrm{isEquiv}(\mathrm{idtoleftmul}(a, b, c)) \times \mathrm{isEquiv}(\mathrm{idtorightmul}(a, b, c))$$ An ordered integral domain is an ordered commutative ring $R$ such that for all elements $a:R$, $a$ is regular if and only if it is positive or its negation is positive: $$\mathrm{isRegular}(a) \simeq \mathrm{isPositive}(a) \vee \mathrm{isPositive}(-a)$$ \section{Sequential convergence and premetrics} A predicate $P$ on $A$ is a subsingleton-valued type family $P$ indexed by elements of $A$. A binary relation $R$ on $A$ and $B$ is a subsingleton-valued type family $R$ jointly indexed by elements of $A$ and elements of $B$. A binary relation $R$ is functional if for every element $a:A$ the type of all elements $b:B$ such that there is a witness $p:R(a, b)$ is a subsingleton. A **sequential preconvergence space** is a type $S$ with a binary relation $\mathrm{isLimit}(x, b)$ indexed by sequence $x:\mathbb{N} \to S$ and element $b:S$. Given an sequence $x:\mathbb{N} \to S$, an element $b:S$ is a **limit** of $x$ if there is a witness $p:\mathrm{isLimit}(x, b)$. A sequential convergence space is **sequentially Hausdorff** if the binary relation is a functional relation. Now, let $T$ be a type. A **$T$-premetric space** is a type $S$ with a ternary relation $a \sim_\epsilon b$ indexed by elements $a:S$, $b:S$, and $\epsilon:T$. Every $T$-premetric space is a sequential convergence space with $$\mathrm{isLimit}(x, b) \coloneqq \forall \epsilon:T.\exists N:\mathbb{N}.\forall n:\mathbb{N}.(n \geq N) \to (x(n) \sim_\epsilon b)$$ Given a $T$-premetric space $(S, \sim)$ and a sequence $x:\mathbb{N} \to S$, a **modulus of Cauchy convergence** is a function $M:T \to \mathbb{N}$ with a witness $$p(M, x):\forall \epsilon:T.\forall m:\mathbb{N}.\forall n:\mathbb{N}.((m \geq M(\epsilon)) \wedge (n \geq M(\epsilon))) \to (x(m) \sim_\epsilon x(n))$$ A function $f:T \to S$ is a **Cauchy approximation** if it comes with a sequence $x:\mathbb{N} \to S$ and a modulus of Cauchy convergence $M:T \to \mathbb{N}$ and an identity $p:x \circ M =_{T \to S} f$. A $T$-premetric space $S$ is **sequentially Cauchy complete** if every sequence with a modulus of Cauchy convergence has a unique limit. \section{sequentially Cauchy complete ordered integral domains} Let $R$ be an ordered integral domain. We define the type of positive elements of $R$ as $$R_+ \coloneqq \sum_{a:R} \mathrm{isPositive}(a)$$ the strict linear order $a \lt b$ indexed by $a:R$ and $b:R$ as $$a \lt b \coloneqq \mathrm{isPositive}(b - a)$$ and the premetric $a \sim_\epsilon b$ indexed by $a:R$, $b:R$, and $\epsilon:R_+$ as $$a \sim_\epsilon b \coloneqq (a - b \lt \epsilon) \wedge (-\epsilon \lt a - b)$$ $$a \sim_\epsilon b \coloneqq \mathrm{isPositive}(\epsilon - (a - b)) \wedge \mathrm{isPositive}(\epsilon + (a - b))$$ Then, we define the limit relation as $$\mathrm{isLimit}(x, b) \coloneqq \forall \epsilon:R_+.\exists N:\mathbb{N}.\forall n:\mathbb{N}.(n \geq N) \to (\mathrm{isPositive}(\epsilon - (x(n) - b)) \wedge \mathrm{isPositive}(\epsilon + (x(n) - b)))$$ A **modulus of Cauchy convergence** is a function $M:R_+ \to \mathbb{N}$ with a witness $$p(M, x):\forall \epsilon:R_+.\forall m:\mathbb{N}.\forall n:\mathbb{N}.((m \geq M(\epsilon)) \wedge (n \geq M(\epsilon))) \to (\mathrm{isPositive}(\epsilon - (x(m) - x(n))) \wedge \mathrm{isPositive}(\epsilon + (x(m) - x(n))))$$ $R$ is **sequentially Cauchy complete** if every sequence with a modulus of Cauchy convergence has a unique limit. The integers are the initial sequentially Cauchy complete ordered integral domain. \section{Field structure} An ordered integral domain is **dense** if it has an positive element $x$ such that $1 - x$ is also positive. The Cauchy real numbers are the initial dense sequentially Cauchy complete ordered integral domain. Given a dense sequentially Cauchy complete ordered integral domain with specified positive element $p:R$ such that $1 - p$ is also positive, the __reciprocal__ $x:R_{-}\union R_{+} \vdash \frac{1}{x}:R$ is piecewise defined as $$ \frac{1}{x} \coloneqq \begin{cases} \lim_{i \to \infty} p^i \sum_{n=0}^{\infty} (-p^i)^n \left(x-\sum_{m=0}^{\infty} (-p^i+1)^m\right)^n & x:R_{-} \\ \lim_{i \to \infty} p^i \sum_{n=0}^{\infty} (-p^i)^n \left(x+\sum_{m=0}^{\infty} (-1)^m (p^i-1)^m\right)^n & x:R_+ \end{cases} $$ One can confirm that the product of every element $x:R_{-}\union R_{+}$ and its reciprocal is equal to 1. Thus, every dense sequentially Cauchy complete ordered integral domain is a field. category: redirected to nlab