Homotopy Type Theory rational numbers > history (Rev #8, changes)

Showing changes from revision #7 to #8: Added | ~~Removed~~ | ~~Chan~~ged

Idea

The rational numbers as familiar from school mathematics.

Definition

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)$

Mathematical Properties structures on the rational numbers

~~Ring structure on the rational numbers~~

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.

~~Zero~~

Commutative ring structure on the rational numbers

~~We define zero $0:\mathbb{Q}$ to be the following:~~

Definition

The rational number zero $0:\mathbb{Q}$ is defined as

0 \coloneqq 0/1

~~$0 \coloneqq 0/1$~~

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}$ .

~~Addition~~

Theorem

For any $q:\mathbb{Q}$ and $r:\mathbb{Q}$ , there are identities $p: q + r = r + q$ .

~~We define addition $(-)+(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ to be the following:~~

Proof

TODO

~~$a/b + c/d \coloneqq (a \cdot i(d) + c \cdot i(b))/(b \cdot d)$~~

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}$ .

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}$ .

~~Negation~~

Definition

The rational number one $1:\mathbb{Q}$ is defined as

1 \coloneqq 1/1

~~We define negation $-(-):\mathbb{Q} \to \mathbb{Q}$ to be the following:~~

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}$ .

~~$-(a/b) \coloneqq (-a)/b$~~

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}$ .

~~for~~ This makes the rational numbers into a commutative ring. ~~$a:\mathbb{Z}$~~ , ~~$b:\mathbb{Z}_{#0}$~~ , ~~$-(-):\mathbb{Z} \to \mathbb{Z}$~~ .

~~Subtraction~~
~~We define subtraction $(-)-(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ to be the following:~~
~~$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}$ .
~~One~~
~~We define one $1:\mathbb{Q}$ to be the following:~~
~~$1 \coloneqq 1/1$~~
~~Multiplication~~
~~We define multiplication $(-)\cdot(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ to be the following:~~
~~$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}$ .~~
~~Exponentiation~~
~~We define exponentiation $(-)^{(-)}:\mathbb{Q} \times \mathbb{N} \to \mathbb{Q}$ to be the following:~~
~~$(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}$ .~~

Sign

Positive sign

We define the dependent type is positive, denoted as $isPositive(a/b)$ , to be the following:

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}$ .

Negative sign

We define the dependent type is negative, denoted as $isNegative(a/b)$ , to be the following:

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}$ .

Zero sign

We define the dependent type is zero, denoted as $isZero(a/b)$ , to be the following:

isZero(a/b) \coloneqq a = 0

for $a:\mathbb{Z}$ , $b:\mathbb{Z}_{#0}$ .

Non-positive sign

We define the dependent type is non-positive, denoted as $isNonPositive(a/b)$ , to be the following:

isNonPositive(a/b) \coloneqq isPositive(a/b) \to \emptyset

for $a:\mathbb{Z}$ , $b:\mathbb{Z}_{#0}$ .

Non-negative sign

We define the dependent type is non-negative, denoted as $isNonNegative(a/b)$ , to be the following:

isNonNegative(a/b) \coloneqq isNegative(a/b) \to \emptyset

for $a:\mathbb{Z}$ , $b:\mathbb{Z}_{#0}$ .

Non-zero sign

We define the dependent type is non-zero, denoted as $isNonZero(a/b)$ , to be the following:

isNonNegative(a/b) \coloneqq \Vert isPositive(a/b) + isNegative(a/b) \Vert

for $a:\mathbb{Z}$ , $b:\mathbb{Z}_{#0}$ .

Order structure on the rational numbers

Less than

We define the dependent type is less than, denoted as $a/b \lt c/d$ , to be the following:

$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}$ .

Greater than

We define the dependent type is greater than, denoted as $a/b \gt c/d$ , to be the following:

$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}$ .

Apart from

We define the dependent type is apart from, denoted as $a/b # c/d$ , to be the following:

$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}$ .

Less than or equal to

We define the dependent type is less than or equal to, denoted as $a/b \leq c/d$ , to be the following:

$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}$ .

Greater than or equal to

We define the dependent type is greater than or equal to, denoted as $a/b \geq c/d$ , to be the following:

$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

Ramp

We define the ramp function $ramp:\mathbb{Q} \to \mathbb{Q}$ to be the following:

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}$ .

Minimum

We define the minimum $min:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ to be the following:

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}$ .

Maximum

We define the maximum $max:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ to be the following:

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}$ .

Absolute value

We define the absolute value $\vert(-)\vert:\mathbb{Q} \to \mathbb{Q}$ to be the following:

\vert a/b \vert \coloneqq max(a/b, -a/b)

for $a:\mathbb{Z}$ , $b:\mathbb{Z}_{#0}$ .

~~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.

References

HoTT book

Revision on February 27, 2022 at 05:46:15 by Anonymous?. See the history of this page for a list of all contributions to it.

Homotopy Type Theory rational numbers > history (Rev #8, changes)

Contents

Idea

Definition

Mathematical Properties structures on the rational numbers

Ring structure on the rational numbers

Zero

Commutative ring structure on the rational numbers

Definition

Definition

Addition

Theorem

Proof

Definition

Definition

Negation

Definition

Definition

Definition

Subtraction

One

Multiplication

Exponentiation

Sign

Positive sign

Negative sign

Zero sign

Non-positive sign

Non-negative sign

Non-zero sign

Order structure on the rational numbers

Less than

Greater than

Apart from

Less than or equal to

Greater than or equal to

Pseudolattice structure on the rational numbers

Ramp

Minimum

Maximum

Absolute value

Properties

See also

References