[[!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 * one is positive * the sum of two positive elements is positive * the product of two positive elements is positive Every ordered commutative ring has a strict order given by $a \lt b \coloneqq \mathrm{isPositive}(b - a)$ and a preorder given by $a \leq b \coloneqq \neg (b \lt a)$. An ordered commutative ring is **linearly ordered** if additionally if both an element $a$ and its negation $-a$ are not positive, then $a$ is equal to zero. The preorder becomes a partial order. \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{Ordered field} Given a commutative ring $R$, an element $a:R$ is invertible if the type of all $b:B$ such that $a \cdot b =_R 1$ is contractible $$\mathrm{isInvertible}(a):\mathrm{isContr}\left(\sum_{b:B} a \cdot b =_R 1\right)$$ An ordered field is an ordered commutative ring $R$ such that for all elements $a:R$, $a$ is invertible if and only if it is positive or its negation is positive: $$\mathrm{isInvertible}(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]]. category: redirected to nlab