#Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|nLab]] again, this article should be ported over there. ## Idea ## The rational numbers as familiar from school mathematics. ## Definition ## ### In set theory ### Let $\mathbb{Z}$ be the [[integers]] and let $$\mathbb{Z}_{#0} \coloneqq \{a \in \mathbb{Z} \vert a \lt 0 \vee 0 \lt a \}$$ be the set of integers apart from zero. Let us define a *rational number algebra* to be a set $A$ with a function $\iota \in A^{\mathbb{Z} \times \mathbb{Z}_{#0}}$ with domain the Cartesian product $\mathbb{Z} \times \mathbb{Z}_{#0}$ and codomain $A$, such that $$\forall a \in \mathbb{Z}. \forall b \in \mathbb{Z}_{#0}. \forall c \in \mathbb{Z}. \forall d \in \mathbb{Z}_{#0}. (a \cdot d = c \cdot b) \implies (\iota(a, b) = \iota(c, d))$$ A *rational number algebra homomorphism* between two rational number algebras $A$ and $B$ is a function $f \in B^A$ such that $$\forall a \in \mathbb{Z}. \forall b \in \mathbb{Z}_{#0}. f(\iota_A(a, b)) = \iota_B(a, b)$$ The *category of rational number algebras* is the category $RNA$ whose objects $Ob(RNA)$ are decimal fraction algebras and whose morphisms $Mor(RNA)$ are rational number algebra homomorphisms. The set of **rational numbers**, denoted $\mathbb{Q}$, is defined as the initial object in the category of rational number algebras. ### In homotopy type theory ### The type of **rational numbers**, denoted $\mathbb{Q}$, is defined as the [[higher inductive type]] generated by: * A function $(-)/(-) : \mathbb{Z} \times \mathbb{Z}_{#0} \rightarrow \mathbb{Q}$, where $$\mathbb{Z}_{#0} \coloneqq \sum_{a:\mathbb{Z}} a # 0$$ and $#$ is the apartness relation on the integers. * A dependent product of functions between identities representing that equivalent fractions are equal: $$equivfrac : \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}_{#0}} \prod_{c:\mathbb{Z}} \prod_{d:\mathbb{Z}_{#0}} (a \cdot i(d) = c \cdot i(b)) \to (a/b = c/d)$$ where $i: \mathbb{Z}_{#0} \to \mathbb{Z}$ is the inclusion of the nonzero integers in the integers. * A set-truncator $$\tau_0: \prod_{a:\mathbb{Q}} \prod_{b:\mathbb{Q}} isProp(a=b)$$ ## Properties ## TODO: Show that the rational numbers are an ordered Heyting field with decidable equality, decidable apartness, and decidable linear order, and that the rational numbers are initial in the category of ordered Heyting fields. The HoTT book unfortunately skips the proof entirely. ### Commutative ring structure on the rational numbers ### +--{: .num_defn} ###### Definition The rational number **zero** $0:\mathbb{Q}$ is defined as $$0 \coloneqq 0/1$$ =-- +--{: .num_defn} ###### Definition The binary operation **addition** $(-)+(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as $$a/b + c/d \coloneqq (a \cdot i(d) + c \cdot i(b))/(b \cdot d)$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$, $(-)+(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$, $(-)\cdot(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$, $i: \mathbb{Z}_{#0} \to \mathbb{Z}$. =-- +--{: .num_theorem} ###### Theorem For any $q:\mathbb{Q}$ and $r:\mathbb{Q}$, there are identities $p: q + r = r + q$. =-- +--{: .proof} ###### Proof TODO =-- +--{: .num_defn} ###### Definition The unary operation **negation** $-(-):\mathbb{Q} \to \mathbb{Q}$ is defined as $$-(a/b) \coloneqq (-a)/b$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $-(-):\mathbb{Z} \to \mathbb{Z}$. =-- +--{: .num_defn} ###### Definition The binary operation **subtraction** $(-)-(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as $$a/b - c/d \coloneqq (a \cdot i(d) - c \cdot i(b))/(b \cdot d)$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$, $(-)-(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$, $(-)\cdot(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$, $i: \mathbb{Z}_{#0} \to \mathbb{Z}$. =-- +--{: .num_defn} ###### Definition The rational number **one** $1:\mathbb{Q}$ is defined as $$1 \coloneqq 1/1$$ =-- +--{: .num_defn} ###### Definition The binary operation **multiplication** $(-)\cdot(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as $$a/b \cdot c/d \coloneqq (a \cdot c)/(b \cdot d)$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$, $(-)\cdot(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$, $i: \mathbb{Z}_{#0} \to \mathbb{Z}$. =-- +--{: .num_defn} ###### Definition The right $\mathbb{N}$-action **exponentiation** $(-)^{(-)}:\mathbb{Q} \times \mathbb{N} \to \mathbb{Q}$ is defined as $$(a/b)^n \coloneqq (a^n)/(b^n)$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $n:\mathbb{N}$, $(-)^{(-)}:\mathbb{Z} \times \mathbb{N} \to \mathbb{Z}$, $(-)^{(-)}:\mathbb{Z}_{#0} \times \mathbb{N} \to \mathbb{Z}_{#0}$. =-- This makes the rational numbers into a commutative ring. ### Order structure on the rational numbers ### +--{: .num_defn} ###### Definition The dependent type *is positive*, denoted as $isPositive(a/b)$, is defined as $$isPositive(a/b) \coloneqq \Vert (a \gt 0) \times (i(b) \gt 0) + (a \lt 0) \times (i(b) \lt 0) \Vert$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, dependent types $m\lt n$, $m\gt n$ indexed by $m, n:\mathbb{Z}$. =-- +--{: .num_defn} ###### Definition The dependent type *is negative*, denoted as $isNegative(a/b)$, is defined as $$isNegative(a/b) \coloneqq \Vert (a \gt 0) \times (i(b) \lt 0) + (a \lt 0) \times (i(b) \gt 0) \Vert$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, dependent types $m\lt n$, $m\gt n$ indexed by $m, n:\mathbb{Z}$. =-- +--{: .num_defn} ###### Definition The dependent type *is zero*, denoted as $isZero(a/b)$, is defined as $$isZero(a/b) \coloneqq a = 0$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The dependent type *is non-positive*, denoted as $isNonPositive(a/b)$ is defined as $$isNonPositive(a/b) \coloneqq isPositive(a/b) \to \emptyset$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The dependent type *is non-negative*, denoted as $isNonNegative(a/b)$, is defined as $$isNonNegative(a/b) \coloneqq isNegative(a/b) \to \emptyset$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The dependent type *is non-zero*, denoted as $isNonZero(a/b)$, is defined as $$isNonZero(a/b) \coloneqq \Vert isPositive(a/b) + isNegative(a/b) \Vert$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The dependent type *is less than*, denoted as $a/b \lt c/d$, is defined as $a/b \lt c/d \coloneqq isPositive(c/d - a/b)$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The dependent type *is greater than*, denoted as $a/b \gt c/d$, is defined as $a/b \gt c/d \coloneqq isNegative(c/d - a/b)$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The dependent type *is apart from*, denoted as $a/b # c/d$, is defined as $a/b # c/d \coloneqq isNonZero(c/d - a/b)$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The dependent type *is less than or equal to*, denoted as $a/b \leq c/d$, is defined as $a/b \leq c/d \coloneqq isNonNegative(c/d - a/b)$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The dependent type *is greater than or equal to*, denoted as $a/b \geq c/d$, is defined as $a/b \geq c/d \coloneqq isNonPositive(c/d - a/b)$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$. =-- ### Pseudolattice structure on the rational numbers ### +--{: .num_defn} ###### Definition The **ramp function** $ramp:\mathbb{Q} \to \mathbb{Q}$ is defined as $$ramp(a/b) \coloneqq (ramp(a) \cdot ramp(i(b)) + ramp(-a) \cdot ramp(i(-b)))/(b \cdot b)$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $ramp:\mathbb{Z} \to \mathbb{Z}$, $(-)+(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$, $(-)\cdot(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$, $i: \mathbb{Z}_{#0} \to \mathbb{Z}$. =-- +--{: .num_defn} ###### Definition The **minimum** $min:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as $$min(a/b,c/d) \coloneqq a/b - ramp(a/b - c/d)$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The **maximum** $max:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as $$max(a/b,c/d) \coloneqq a/b + ramp(c/d - a/b)$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The **absolute value** $\vert(-)\vert:\mathbb{Q} \to \mathbb{Q}$ is defined as $$\vert a/b \vert \coloneqq max(a/b, -a/b)$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$. =-- ### Other ### Addition, subtraction, and multiplication of rational numbers are [[uniformly continuous function|uniformly continuous]] with respect to the absolute value. The rational numbers are a [[Hausdorff space]]. ## See also ## * [[higher inductive type]] * [[natural numbers]] * [[integers]] * [[decimal numbers]] * [[irrational numbers]] * [[real numbers]] * [[rational root theorem]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)