[[!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 local rings} An ordered local 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 * one is positive * the sum of two positive elements is positive * the product of two positive elements is positive * if both an element $a$ and its negation $-a$ are not positive, then $a$ is equal to zero. * for all elements $a:R$, $a$ is invertible if and only if it is positive or its negation is positive: There exist elements which are neither positive or negative or equal to zero: the nilpotent infinitesimals. \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{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)$$ and the premetric $a \sim_\epsilon b$ indexed by $a:R$, $b:R$, and $\epsilon:R_+$ as $$a \sim_\epsilon b \coloneqq \mathrm{isPositive}(\epsilon^2 - (a - b)^2)$$ 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^2 - (x(n) - b)^2)$$ 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 \wedge \mathrm{isPositive}(\epsilon^2 - (x(m) - x(n))^2)$$ $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{sequentially Cauchy complete finite rank modules} Let $R$ be an ordered integral domain, and let $V$ be a finite rank $R$-module with basis $X:\mathrm{Fin}(n) \to V$ and inner product $\langle -, -\rangle:V \times V \to R$, where $\langle X_i, X_j \rangle = \delta_i^j$ and $\delta_{(-)}^{(-)}:\mathrm{Fin}(n) \times \mathrm{Fin}(n) \to R$ is the [[Kronecker delta]] on $\mathrm{Fin}(n)$. We define the Euclidean premetric $a \sim_\epsilon b$ indexed by $a:V$, $b:V$, and $\epsilon:R_+$ as $$a \sim_\epsilon b \coloneqq \mathrm{isPositive}\left(\epsilon^2 - \sum_{i:\mathrm{Fin}(n)} \langle a - b, X_i\rangle^2\right)$$ Then, we define the limit relation as $$\mathrm{isLimit}(x, b) \coloneqq \forall \epsilon:R_+.\exists N:\mathbb{N}.\forall p:\mathbb{N}.(p \geq N) \to \mathrm{isPositive}\left(\epsilon^2 - \sum_{i:\mathrm{Fin}(n)} \langle x(p) - b, X_i\rangle^2\right)$$ A **modulus of Cauchy convergence** is a function $M:R_+ \to \mathbb{N}$ with a witness $$q(M, x):\forall \epsilon:R_+.\forall m:\mathbb{N}.\forall n:\mathbb{N}.((m \geq M(\epsilon)) \wedge (p \geq M(\epsilon))) \to \mathrm{isPositive}\left(\epsilon^2 - \sum_{i:\mathrm{Fin}(n)} \langle x(m) - x(p), X_i\rangle^2\right)$$ $R$ is **sequentially Cauchy complete** if every sequence with a modulus of Cauchy convergence has a unique limit. \section{Clifford algebras} Let $R$ be an ordered integral domain, and let $\mathrm{Cl}_{p, q}(R)$ be a Clifford algebra. We define the Minkowski premetric $a \sim_\epsilon b$ indexed by $a \in V$, $b \in V$, and $\epsilon \in R_+$ as $$a \sim_\epsilon b \coloneqq \sum_{i = 0}^{n - 1} \frac{1}{2} \langle a \rangle_1 \langle b \rangle_1 + \langle b \rangle_1 \langle a \rangle_1 \lt \epsilon^2$$ which makes the underlying vector space $\langle \mathrm{Cl}_{p, q}(R) \rangle_1$ a [[Minkowski space]]. \section{Field structure} 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)$$ and the type of negative elements of $R$ as $$R_- \coloneqq \sum_{a:R} \mathrm{isPositive}(-a)$$ 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