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

Showing changes from revision #12 to #13: Added | Removed | Changed

Contents

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 ()/():× #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)

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 0:0:\mathbb{Q} is defined as

00/10 \coloneqq 0/1
Definition

The binary operation addition ()+():×(-)+(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q} is defined as

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

Theorem

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

Proof

TODO

Definition

The unary operation negation ():-(-):\mathbb{Q} \to \mathbb{Q} is defined as

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

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

Definition

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

11/11 \coloneqq 1/1
Definition

The binary operation multiplication ()():×(-)\cdot(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q} is defined as

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

Definition

The right \mathbb{N}-action exponentiation () ():×(-)^{(-)}:\mathbb{Q} \times \mathbb{N} \to \mathbb{Q} is defined as

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

This makes the rational numbers into a commutative ring.

Order structure on the rational numbers

Definition

The dependent type is positive, denoted as isPositive(a/b)isPositive(a/b), is defined as

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

Definition

The dependent type is negative, denoted as isNegative(a/b)isNegative(a/b), is defined as

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

Definition

The dependent type is zero, denoted as isZero(a/b)isZero(a/b), is defined as

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

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

Definition

The dependent type is non-positive, denoted as isNonPositive(a/b)isNonPositive(a/b) is defined as

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

Definition

The dependent type is non-negative, denoted as isNonNegative(a/b)isNonNegative(a/b), is defined as

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

Definition

The dependent type is non-zero, denoted as isNonZero(a/b)isNonZero(a/b), is defined as

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

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

Definition

The dependent type is less than, denoted as a/b<c/da/b \lt c/d, is defined as

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

Definition

The dependent type is greater than, denoted as a/b>c/da/b \gt c/d, is defined as

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

Definition

The dependent type is apart from, denoted as a/b#c/da/b # c/d, is defined as

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

Definition

The dependent type is less than or equal to, denoted as a/bc/da/b \leq c/d, is defined as

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

Definition

The dependent type is greater than or equal to, denoted as a/bc/da/b \geq c/d, is defined as

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

Definition

The ramp function ramp:ramp:\mathbb{Q} \to \mathbb{Q} is defined as

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

Definition

The minimum min:×min:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q} is defined as

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

Definition

The maximum max:×max:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q} is defined as

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

Definition

The absolute value |()|:\vert(-)\vert:\mathbb{Q} \to \mathbb{Q} is defined as

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

See also

References

Revision on March 15, 2022 at 06:36:06 by Anonymous?. See the history of this page for a list of all contributions to it.