Homotopy Type Theory Sandbox (Rev #67, changes)

A commutative ring $R$ is a totally ordered commutative ring 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, 0) = a$ and $\max(b, 0) = b$ implies $\max(a \cdot b, 0) = a \cdot b$

• for all elements $a:R$ and $b:R$, $\max(a, b) = a$ or $\max(a, b) = b$

Totally ordered commutative $\mathbb{Q}$-algebras

Given totally ordered commutative rings $R$ and $S$, a commutative ring homomorphism $h:R \to S$ is monotonic if for all $a:R$ and $b:R$, $\max(h(a), h(b)) = h(\max(a, b))$.

A totally ordered commutative ring $R$ is a totally ordered commutative $\mathbb{Q}$-algebra if there is a monotonic commutative ring homomorphism $h:\mathbb{Q} \to R$.

Strictly ordered integral ring

A totally ordered commutative ring $R$ is a strictly ordered integral ring if it comes with a strict order $\lt$ such that

• $0 \lt 1$
• for all elements $a:R$ and $b:R$, if $0 \lt a$ and $0 \lt b$, then $0 \lt a + b$
• for all elements $a:R$ and $b:R$, if $0 \lt a$ and $0 \lt b$, then $0 \lt a \cdot b$
• for all elements $a:R$ and $b:R$, if $0 \lt \max(a, -a)$ and $0 \lt \max(b, -b)$, then $0 \lt \max(a \cdot b, -a \cdot b)$

Strictly ordered integral $\mathbb{Q}$-algebras

Given strictly ordered integral rings $R$ and $S$, a monotonic commutative ring homomorphism $h:R \to S$ is strictly monotonic if for all $a:R$ and $b:R$, $a \lt b$ implies $h(a) \lt h(b)$.

A strictly ordered integral ring $R$ is a strictly ordered integral $\mathbb{Q}$-algebra if there is a strictly monotonic commutative ring homomorphism $h:\mathbb{Q} \to R$.

Archimedean ordered integral $\mathbb{Q}$-algebras

A strictly ordered integral $\mathbb{Q}$-algebra $A$ is an Archimedean ordered integral $\mathbb{Q}$-algebra if for all elements $a:A$ and $b:A$, if $a \lt b$, then there merely exists a rational number $q:\mathbb{Q}$ such that $a \lt h(q)$ and $h(q) \lt b$.

Sequentially Cauchy complete Archimedean ordered integral $\mathbb{Q}$-algebra

Let $A$ be an Archimedean ordered integral $\mathbb{Q}$-algebra and let

be the positive elements in $A$. $A$ is sequentially Cauchy complete if every Cauchy sequence in $A$ converges:

Modules

Given a commutative ring $R$, an $R$-module is an abelian group $M$ with an abelian group homomorphism $\alpha:R \to (M \to M)$ which is also a curried action.

The free $R$-module on a set $S$ is the initial $R$-module $M$ with a function $\iota:S \to M$.

$A_n$ abelian groups

$A_1$-abelian groups are pointed objects in abelian groups

$A_2$-abelian groups are unital magma objects in abelian groups

$A_3$-abelian groups are monoid objects in abelian groups

References

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)