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

Showing changes from revision #6 to #7: Added | Removed | Changed

Contents

Idea

The rational numbers as familiar from school mathematics.

Definition

The type of rational numbers, denoted \mathbb{Q} , has is several defined definitions as a thehigher inductive type . generated by:

Definition 1

  • A function ()/():× #0(-)/(-) : \mathbb{Z} \times \mathbb{Z}_{#0} \rightarrow \mathbb{Q}, where
    #0 a:a#0\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: a: b: #0 c: d: #0(ai(d)=ci(b))(a/b=c/d)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: #0i: \mathbb{Z}_{#0} \to \mathbb{Z} is the inclusion of the nonzero integers in the integers.

  • A set-truncator
    τ 0: a: b:isProp(a=b)\tau_0: \prod_{a:\mathbb{Q}} \prod_{b:\mathbb{Q}} isProp(a=b)

The rational numbers are defined as the higher inductive type generated by:

Mathematical structures on the rational numbers

  • A function ()/():× #0(-)/(-) : \mathbb{Z} \times \mathbb{Z}_{#0} \rightarrow \mathbb{Q}, where
    #0 a:a#0\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: a: b: #0 c: d: #0(ai(d)=ci(b))(a/b=c/d)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: #0i: \mathbb{Z}_{#0} \to \mathbb{Z} is the inclusion of the nonzero integers in the integers.

  • A set-truncator
    τ 0: a: b:isProp(a=b)\tau_0: \prod_{a:\mathbb{Q}} \prod_{b:\mathbb{Q}} isProp(a=b)

Ring structure on the rational numbers

Zero

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

00/10 \coloneqq 0/1

Addition

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

a/b+c/d(ai(d)+ci(b))/(bd)a/b + c/d \coloneqq (a \cdot i(d) + c \cdot i(b))/(b \cdot d)

for a:a:\mathbb{Z}, b: #0b:\mathbb{Z}_{#0}, c:c:\mathbb{Z}, d: #0d:\mathbb{Z}_{#0}, ()+():×(-)+(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}, ()():×(-)\cdot(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}, i: #0i: \mathbb{Z}_{#0} \to \mathbb{Z}.

Negation

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

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

for a:a:\mathbb{Z}, b: #0b:\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/bc/d(ai(d)ci(b))/(bd)a/b - c/d \coloneqq (a \cdot i(d) - c \cdot i(b))/(b \cdot d)

for a:a:\mathbb{Z}, b: #0b:\mathbb{Z}_{#0}, c:c:\mathbb{Z}, d: #0d:\mathbb{Z}_{#0}, ()():×(-)-(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}, ()():×(-)\cdot(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}, i: #0i: \mathbb{Z}_{#0} \to \mathbb{Z}.

One

We define one 1:1:\mathbb{Q} to be the following:

11/11 \coloneqq 1/1

Multiplication

We define multiplication ()():×(-)\cdot(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q} to be the following:

a/bc/d(ac)/(bd)a/b \cdot c/d \coloneqq (a \cdot c)/(b \cdot d)

for a:a:\mathbb{Z}, b: #0b:\mathbb{Z}_{#0}, c:c:\mathbb{Z}, d: #0d:\mathbb{Z}_{#0}, ()():×(-)\cdot(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}, i: #0i: \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(a n)/(b n)(a/b)^n \coloneqq (a^n)/(b^n)

for a:a:\mathbb{Z}, b: #0b:\mathbb{Z}_{#0}, n:n:\mathbb{N}, () ():×(-)^{(-)}:\mathbb{Z} \times \mathbb{N} \to \mathbb{Z}, () (): #0× #0(-)^{(-)}:\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)isPositive(a/b), to be the following:

isPositive(a/b)(a>0)×(i(b)>0)+(a<0)×(i(b)<0)isPositive(a/b) \coloneqq \Vert (a \gt 0) \times (i(b) \gt 0) + (a \lt 0) \times (i(b) \lt 0) \Vert

for a:a:\mathbb{Z}, b: #0b:\mathbb{Z}_{#0}, dependent types m<nm\lt n, m>nm\gt n indexed by m,n:m, n:\mathbb{Z}.

Negative sign

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

isNegative(a/b)(a>0)×(i(b)<0)+(a<0)×(i(b)>0)isNegative(a/b) \coloneqq \Vert (a \gt 0) \times (i(b) \lt 0) + (a \lt 0) \times (i(b) \gt 0) \Vert

for a:a:\mathbb{Z}, b: #0b:\mathbb{Z}_{#0}, dependent types m<nm\lt n, m>nm\gt n indexed by m,n:m, n:\mathbb{Z}.

Zero sign

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

isZero(a/b)a=0isZero(a/b) \coloneqq a = 0

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

Non-positive sign

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

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

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

Non-negative sign

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

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

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

Non-zero sign

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

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

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

Order structure on the rational numbers

Less than

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

a/b<c/disPositive(c/da/b)a/b \lt c/d \coloneqq isPositive(c/d - a/b)

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

Greater than

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

a/b>c/disNegative(c/da/b)a/b \gt c/d \coloneqq isNegative(c/d - a/b)

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

Apart from

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

a/b#c/disNonZero(c/da/b)a/b # c/d \coloneqq isNonZero(c/d - a/b)

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

Less than or equal to

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

a/bc/disNonNegative(c/da/b)a/b \leq c/d \coloneqq isNonNegative(c/d - a/b)

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

Greater than or equal to

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

a/bc/disNonPositive(c/da/b)a/b \geq c/d \coloneqq isNonPositive(c/d - a/b)

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

Pseudolattice structure on the rational numbers

Ramp

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

ramp(a/b)(ramp(a)ramp(i(b))+ramp(a)ramp(i(b)))/(bb)ramp(a/b) \coloneqq (ramp(a) \cdot ramp(i(b)) + ramp(-a) \cdot ramp(i(-b)))/(b \cdot b)

for a:a:\mathbb{Z}, b: #0b:\mathbb{Z}_{#0}, ramp:ramp:\mathbb{Z} \to \mathbb{Z}, ()+():×(-)+(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}, ()():×(-)\cdot(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}, i: #0i: \mathbb{Z}_{#0} \to \mathbb{Z}.

Minimum

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

min(a/b,c/d)a/bramp(a/bc/d)min(a/b,c/d) \coloneqq a/b - ramp(a/b - c/d)

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

Maximum

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

max(a/b,c/d)a/b+ramp(c/da/b)max(a/b,c/d) \coloneqq a/b + ramp(c/d - a/b)

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

Absolute value

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

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

for a:a:\mathbb{Z}, b: #0b:\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.

See also

References

HoTT book

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