transfinite arithmetic, cardinal arithmetic, ordinal arithmetic
prime field, p-adic integer, p-adic rational number, p-adic complex number
arithmetic geometry, function field analogy
symmetric monoidal (∞,1)-category of spectra
A rational number is a fraction of two integer numbers.
The field of rational numbers, $\mathbb{Q}$, is the field of fractions of the commutative ring of integers, $\mathbb{Z}$, hence the field consisting of formal fractions (“ratios”) of integers.
Let $(\mathbb{N}^+,1:\mathbb{N}^+,s:\mathbb{N}^+\to \mathbb{N}^+)$ be the set of positive integers. The positive integers are embedded into every commutative ring $R$: there is an injection $inj:\mathbb{N}^+\to\R$ such that $inj(1) = 1$ and $inj(s(n)) = inj(n) + 1$ for all $n:\mathbb{N}^+$.
Suppose $R$ has an injection $inv:\mathbb{N}^+\to\R$ such that $inj(n) \cdot inv(n) = 1$ and $\inv(n) \cdot \inj(n) = 1$ for all $n:\mathbb{N}^+$. Then $R$ is called a $\mathbb{Q}$-algebra, and the commutative ring of rational numbers $\mathbb{Q}$ is the initial commutative $\mathbb{Q}$-algebra.
It can then be proven from the ring axioms and the properties of the integers that every rational number apart from zero and has a multiplicative inverse, making $\mathbb{Q}$ a field.
Let $(\mathbb{N},\leq)$ be the directed set of positive integers, and let $A:\mathbb{N}\to CRing$ be a family of commutative rings where $A_n$ is defined to be $\mathbb{Z}[1/n!]$, the localization of the integers $\mathbb{Z}$ away from the factorial $n!$, and for $i, j:\mathbb{N}$, $i\leq j$, there is a commutative ring homomorphism from $f_{ij}:\mathbb{Z}[1/i!]\to\mathbb{Z}[1/j!]$, with $f_{ii}$ being the identity commutative ring homomorphism on $\mathbb{Z}[1/i!]$. Then the commutative ring of rational numbers $\mathbb{Q}$ is the directed colimit $\underset{\to}\lim_i A_i$ of the system.
Let $(\mathbb{N}^+,1:\mathbb{N}^+,s:\mathbb{N}^+\to \mathbb{N}^+)$ be the set of positive integers and let $(\mathbb{Z},0,+,-,1)$ be the free abelian group on the set ${1}$.
Let $A$ be an abelian group containing $\mathbb{Z}$ as an abelian subgroup. The positive integers are embedded into the function abelian group $A \to A$, with $id_A:A \to A$ being the identity function on $A$; i.e. there is an injection $inj:\mathbb{N}^+\to (A \to A)$ such that $inj(1) = id_A$ and $inj(s(n)) = inj(n) + id_A$ for all $n:\mathbb{N}^+$.
Suppose $A$ has an injection $inv:\mathbb{N}^+\to (A \to A)$ such that for all $n:\mathbb{N}^+$, $inj(n) \circ inv(n) = id_A$ and $inv(n) \circ inj(n) = id_A$. Then the abelian group of rational numbers $\mathbb{Q}$ is the initial such abelian group.
Let $\mathbb{Z}$ be the integers and let
be the set of integers apart from zero.
For lack of a better name, let us define a set with rational numbers to be a set $A$ with a function $\iota \in \mathbb{Z} \times \mathbb{Z}_{#0} \to A$ with domain the Cartesian product $\mathbb{Z} \times \mathbb{Z}_{#0}$ and codomain $A$, such that
A homomorphism of sets with rational numbers between two sets with rational numbers $A$ and $B$ is a function $f \in B^A$ such that
The category of sets with rational numbers is the category $SwRN$ whose objects $Ob(SwRN)$ are sets with rational numbers and whose morphisms $Mor(A,B)$ for sets with rational numbers $A \in Ob(SwDF)$, $B \in Ob(SwRN)$ are homomorphisms of sets with rational numbers. The set of rational numbers, denoted $\mathbb{Q}$, is defined as the initial object in the category of sets with rational numbers.
In homotopy type theory, the type of rational numbers, denoted $\mathbb{Q}$, is defined (UBP13, §11.1) as the higher inductive type generated by:
A function $(-)/(-) : \mathbb{Z} \times \mathbb{Z}_{\neq 0} \rightarrow \mathbb{Q}$, where
A dependent product of functions between identities representing that equivalent fractions are equal:
where $i: \mathbb{Z}_{\neq 0} \to \mathbb{Z}$ is the inclusion of the nonzero integers in the integers.
A set-truncator
The rational number zero $0 \in \mathbb{Q}$ is defined as
The binary operation addition $(-)+(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as
for $a \ in \mathbb{Z}$, $b \in \mathbb{Z}_{#0}$, $c \in \mathbb{Z}$, $d \in \mathbb{Z}_{#0}$.
For any $q \in \mathbb{Q}$ and $r \in \mathbb{Q}$, $q + r = r + q$.
TODO
The unary operation negation $-(-):\mathbb{Q} \to \mathbb{Q}$ is defined as
for $a \in \mathbb{Z}$, $b \in \mathbb{Z}_{#0}$
The binary operation subtraction $(-)-(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as
for $a \in \mathbb{Z}$, $b \in \mathbb{Z}_{#0}$, $c \in \mathbb{Z}$, $d \in \mathbb{Z}_{#0}$
The rational number one $1 \in \mathbb{Q}$ is defined as
The binary operation multiplication $(-)\cdot(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as
for $a \in \mathbb{Z}$, $b \in \mathbb{Z}_{#0}$, $c \in \mathbb{Z}$, $d \in \mathbb{Z}_{#0}$
The right $\mathbb{N}$-action exponentiation $(-)^{(-)}:\mathbb{Q} \times \mathbb{N} \to \mathbb{Q}$ is defined as
for $a \in \mathbb{Z}$, $b \in \mathbb{Z}_{#0}$, $n \in \mathbb{N}$.
This makes the rational numbers into a commutative ring.
The predicate is positive, denoted as $isPositive(a/b)$, is defined as
for $a \in \mathbb{Z}$, $b \in \mathbb{Z}_{#0}$.
The predicate is negative, denoted as $isNegative(a/b)$, is defined as
for $a \in \mathbb{Z}$, $b \in \mathbb{Z}_{#0}$.
The predicate is zero, denoted as $isZero(a/b)$, is defined as
for $a \in \mathbb{Z}$, $b \in \mathbb{Z}_{#0}$.
The predicate is non-positive, denoted as $isNonPositive(a/b)$ is defined as
for $a \in \mathbb{Z}$, $b \in \mathbb{Z}_{#0}$.
The predicate is non-negative, denoted as $isNonNegative(a/b)$, is defined as
for $a \in \mathbb{Z}$, $b \in \mathbb{Z}_{#0}$.
The predicate is non-zero, denoted as $isNonZero(a/b)$, is defined as
for $a \in \mathbb{Z}$, $b \in \mathbb{Z}_{#0}$.
The relation is less than, denoted as $p \lt q$, is defined as
$p \lt q \coloneqq isPositive(q - p)$
for $p:\mathbb{Q}$, $q:\mathbb{Q}$.
The dependent type is greater than, denoted as $p \gt q$, is defined as
$p \lt q \coloneqq isNegative(q - p)$
for $p:\mathbb{Q}$, $q:\mathbb{Q}$.
The dependent type is apart from, denoted as $p \# q$, is defined as
$p \lt q \coloneqq isNonZero(q - p)$
for $p:\mathbb{Q}$, $q:\mathbb{Q}$.
The dependent type is less than or equal to, denoted as $p \leq q$, is defined as
$p \lt q \coloneqq isNonNegative(q - p)$
for $p:\mathbb{Q}$, $q:\mathbb{Q}$.
The dependent type is greater than or equal to, denoted as $p \leq q$, is defined as
$p \lt q \coloneqq isNonPositive(q - p)$
for $p:\mathbb{Q}$, $q:\mathbb{Q}$.
The ramp function $ramp:\mathbb{Q} \to \mathbb{Q}$ is defined as
for $a \in \mathbb{Z}$, $b \in \mathbb{Z}_{#0}$, $ramp:\mathbb{Z} \to \mathbb{Z}$.
The minimum $min:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as
for $p:\mathbb{Q}$, $q:\mathbb{Q}$.
The maximum $max:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as
for $p:\mathbb{Q}$, $q:\mathbb{Q}$.
The absolute value $\vert(-)\vert:\mathbb{Q} \to \mathbb{Q}$ is defined as
for $p:\mathbb{Q}$.
The metric $\rho:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as
for $p:\mathbb{Q}$, $q:\mathbb{Q}$.
We define the ternary relation $x \sim_\epsilon y \coloneqq \rho(x, y) \lt \epsilon$ for $x \in \mathbb{Q}$, $y \in \mathbb{Q}$, and $\epsilon \in \mathbb{Q}_+$, called “$x$ and $y$ are within a distance of $\epsilon$”. One could show that the rational numbers are a uniform space with respect to the uniformity ternary relation $x \sim_\epsilon y$.
For every $x \in \mathbb{Q}$ and $\epsilon \in \mathbb{Q}_+$, $x \sim_\epsilon x$
For every $x \in \mathbb{Q}$, $y \in \mathbb{Q}$, $z \in \mathbb{Q}$ and $\delta \in \mathbb{Q}_+$, $\epsilon \in \mathbb{Q}_+$, $x \sim_\delta y$ and $y \sim_\epsilon z$ implies that $x \sim_{\delta + \epsilon} z$.
For every $x \in \mathbb{Q}$, $y \in \mathbb{Q}$ and $\epsilon \in \mathbb{Q}_+$, $x \sim_\epsilon y$ implies that $y \sim_\epsilon x$.
For every $x \in \mathbb{Q}$, $y \in \mathbb{Q}$, $x \sim_1 y$ if and only if $\rho(x, y) \lt 1$.
For every $x \in \mathbb{Q}$, $y \in \mathbb{Q}$ and $\delta \in \mathbb{Q}_+$, $\epsilon \in \mathbb{Q}_+$, $x \sim_{\min(\delta, \epsilon)} y$ implies that $x \sim_{\delta} y$ and $x \sim_{\epsilon} y$.
For every $x \in \mathbb{Q}$, $y \in \mathbb{Q}$ and $\delta \in \mathbb{Q}_+$, $\epsilon \in \mathbb{Q}_+$, $\delta \leq \epsilon$ and $x \sim_{\delta} y$ implies that $x \sim_{\epsilon} y$.
The algebraic closure $\overline{\mathbb{Q}}$ of the rational numbers is called the field of algebraic numbers. The absolute Galois group $Gal(\overline{\mathbb{Q}}\vert \mathbb{Q})$ has some curious properties, see there.
There are several interesting topologies on $\mathbb{Q}$ that make $\mathbb{Q}$ into a topological group under addition, allowing us to define interesting fields by taking the completion with respect to this topology:
The discrete topology is the most obvious, which is already complete.
The absolute-value topology is defined by the metric $d(x,y) \coloneqq {|x - y|}$; the completion is the field of real numbers. The rational numbers are thus a Hausdorff space.
(This topology is totally disconnected (this exmpl.))
Fixing a prime number $p$, the $p$-adic topology is defined by the ultrametric $d(x,y) \coloneqq 1/n$ where $n$ is the highest exponent on $p$ in the prime factorization of ${|x - y|}$; the completion is the field of $p$-adic numbers.
According to Ostrowski's theorem this are the only possibilities.
Interestingly, (2) cannot be interpreted as a localic group, although the completion $\mathbb{R}$ can. (Probably the same holds for (3); I need to check.)
One could analytically define the concepts of limit of a function and continuous function with respect to the absolute-value topology, and prove that the limit of a function satisfy the algebraic limit theorem. Since the reciprocal function on the rational numbers is well defined for non-zero rational numbers $\mathbb{Q}_{\neq 0}$, given a continuous function $f:I \to \mathbb{Q}$ for open interval $I \subseteq \mathbb{Q}$ the difference quotient function exists and thus the derivative is well-defined for continuous functions. One could thus define smooth functions on the rational numbers, and because the rational numbers are a Hausdorff space, analytic functions on the rational numbers, despite the fact that the rational numbers are a totally disconnected space.
rational number
a finite field extension of $\mathbb{Q}$ is called a number field
See also:
Discussion in univalent foundations of mathematics (homotopy type theory with the univalence axiom):
and specifically in Agda:
Last revised on February 8, 2023 at 09:31:13. See the history of this page for a list of all contributions to it.