Contents
Whenever editing is allowed on the nLab again, this article should be ported over there.
Idea
The rational numbers as familiar from school mathematics.
Definition
In set theory
Let be the integers and let
be the set of integers apart from zero.
Let us define a rational number algebra to be a set with a function with domain the Cartesian product and codomain , such that
A rational number algebra homomorphism between two rational number algebras and is a function such that
The category of rational number algebras is the category whose objects are decimal fraction algebras and whose morphisms are rational number algebra homomorphisms. The set of rational numbers, denoted , is defined as the initial object in the category of rational number algebras.
In homotopy type theory
The type of rational numbers, denoted , is defined as the higher inductive type generated by:
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
Definition
The rational number zero is defined as
Definition
The binary operation addition is defined as
for , , , , , , .
Theorem
For any and , there are identities .
Definition
The unary operation negation is defined as
for , , .
Definition
The binary operation subtraction is defined as
for , , , , , , .
Definition
The rational number one is defined as
Definition
The binary operation multiplication is defined as
for , , , , , .
Definition
The right -action exponentiation is defined as
for , , , , .
This makes the rational numbers into a commutative ring.
Order structure on the rational numbers
Definition
The dependent type is positive, denoted as , is defined as
for , , dependent types , indexed by .
Definition
The dependent type is negative, denoted as , is defined as
for , , dependent types , indexed by .
Definition
The dependent type is zero, denoted as , is defined as
for , .
Definition
The dependent type is non-positive, denoted as is defined as
for , .
Definition
The dependent type is non-negative, denoted as , is defined as
for , .
Definition
The dependent type is non-zero, denoted as , is defined as
for , .
Definition
The dependent type is less than, denoted as , is defined as
for , , , .
Definition
The dependent type is greater than, denoted as , is defined as
for , , , .
Definition
The dependent type is apart from, denoted as , is defined as
for , , , .
Definition
The dependent type is less than or equal to, denoted as , is defined as
for , , , .
Definition
The dependent type is greater than or equal to, denoted as , is defined as
for , , , .
Pseudolattice structure on the rational numbers
Definition
The ramp function is defined as
for , , , , , .
Definition
The minimum is defined as
for , , , .
Definition
The maximum is defined as
for , , , .
Definition
The absolute value is defined as
for , .
Other
Addition, subtraction, and multiplication of rational numbers are uniformly continuous with respect to the absolute value.
The rational numbers are a Hausdorff space.
See also
References