Showing changes from revision #14 to #15:
Added | Removed | Changed
Contents
Idea
The rational numbers as familiar from school mathematics.
Definition
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