The rational numbers

Content created by Fredrik Bakke, Egbert Rijke, Bryan Lu, Fernando Chu, Jonathan Prieto-Cubides, malarbol, Julian KG, fernabnor and louismntnu.

Created on 2022-02-17.
Last modified on 2024-10-29.

module elementary-number-theory.rational-numbers where
Imports 
open import elementary-number-theory.divisibility-integers
open import elementary-number-theory.greatest-common-divisor-integers
open import elementary-number-theory.integer-fractions
open import elementary-number-theory.integers
open import elementary-number-theory.mediant-integer-fractions
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.positive-and-negative-integers
open import elementary-number-theory.positive-integers
open import elementary-number-theory.reduced-integer-fractions

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equality-cartesian-product-types
open import foundation.equality-dependent-pair-types
open import foundation.identity-types
open import foundation.negation
open import foundation.propositions
open import foundation.reflecting-maps-equivalence-relations
open import foundation.retracts-of-types
open import foundation.sections
open import foundation.sets
open import foundation.subtypes
open import foundation.surjective-maps
open import foundation.universe-levels

open import set-theory.countable-sets

Idea

The type of rational numbers is the quotient of the type of integer fractions by the equivalence relation given by

Since the reduced fractions are canonical representatives of the similarity relation on fractions, we simply define the set ℚ to be the type of reduced fractions and we obtain the universal property of the set quotient from the fact that each equivalence class has a unique canonical representative.

Definitions

The type of rationals

ℚ : UU lzero
ℚ = Σ fraction-ℤ is-reduced-fraction-ℤ

module _
  (x : ℚ)
  where

  fraction-ℚ : fraction-ℤ
  fraction-ℚ = pr1 x

  is-reduced-fraction-ℚ : is-reduced-fraction-ℤ fraction-ℚ
  is-reduced-fraction-ℚ = pr2 x

  numerator-ℚ : ℤ
  numerator-ℚ = numerator-fraction-ℤ fraction-ℚ

  positive-denominator-ℚ : positive-ℤ
  positive-denominator-ℚ = positive-denominator-fraction-ℤ fraction-ℚ

  denominator-ℚ : ℤ
  denominator-ℚ = denominator-fraction-ℤ fraction-ℚ

  is-positive-denominator-ℚ : is-positive-ℤ denominator-ℚ
  is-positive-denominator-ℚ = is-positive-denominator-fraction-ℤ fraction-ℚ

Inclusion of fractions

rational-fraction-ℤ : fraction-ℤ → ℚ
pr1 (rational-fraction-ℤ x) = reduce-fraction-ℤ x
pr2 (rational-fraction-ℤ x) = is-reduced-reduce-fraction-ℤ x

Inclusion of the integers

rational-ℤ : ℤ → ℚ
pr1 (pr1 (rational-ℤ x)) = x
pr2 (pr1 (rational-ℤ x)) = one-positive-ℤ
pr2 (rational-ℤ x) = is-one-gcd-one-ℤ' x

Negative one, zero and one

neg-one-ℚ : ℚ
neg-one-ℚ = rational-ℤ neg-one-ℤ

is-neg-one-ℚ : ℚ → UU lzero
is-neg-one-ℚ x = (x ＝ neg-one-ℚ)

zero-ℚ : ℚ
zero-ℚ = rational-ℤ zero-ℤ

is-zero-ℚ : ℚ → UU lzero
is-zero-ℚ x = (x ＝ zero-ℚ)

is-nonzero-ℚ : ℚ → UU lzero
is-nonzero-ℚ k = ¬ (is-zero-ℚ k)

one-ℚ : ℚ
one-ℚ = rational-ℤ one-ℤ

is-one-ℚ : ℚ → UU lzero
is-one-ℚ x = (x ＝ one-ℚ)

The negative of a rational number

neg-ℚ : ℚ → ℚ
pr1 (neg-ℚ (x , H)) = neg-fraction-ℤ x
pr2 (neg-ℚ (x , H)) = is-reduced-neg-fraction-ℤ x H

The mediant of two rationals

mediant-ℚ : ℚ → ℚ → ℚ
mediant-ℚ x y =
  rational-fraction-ℤ
    ( mediant-fraction-ℤ
      ( fraction-ℚ x)
      ( fraction-ℚ y))

Properties

The rational images of two similar integer fractions are equal

eq-ℚ-sim-fraction-ℤ :
  (x y : fraction-ℤ) → (H : sim-fraction-ℤ x y) →
  rational-fraction-ℤ x ＝ rational-fraction-ℤ y
eq-ℚ-sim-fraction-ℤ x y H =
  eq-pair-Σ'
    ( pair
      ( unique-reduce-fraction-ℤ x y H)
      ( eq-is-prop (is-prop-is-reduced-fraction-ℤ (reduce-fraction-ℤ y))))

The type of rationals is a set

abstract
  is-set-ℚ : is-set ℚ
  is-set-ℚ =
    is-set-Σ
      ( is-set-fraction-ℤ)
      ( λ x → is-set-is-prop (is-prop-is-reduced-fraction-ℤ x))

ℚ-Set : Set lzero
pr1 ℚ-Set = ℚ
pr2 ℚ-Set = is-set-ℚ

The rationals are a retract of the integer fractions

abstract
  is-retraction-rational-fraction-ℚ :
    (x : ℚ) → rational-fraction-ℤ (fraction-ℚ x) ＝ x
  is-retraction-rational-fraction-ℚ ((m , n , n-pos) , p) =
    eq-pair-Σ
      ( eq-pair
        ( eq-quotient-div-is-one-ℤ _ _ p (div-left-gcd-ℤ m n))
        ( eq-pair-Σ
          ( eq-quotient-div-is-one-ℤ _ _ p (div-right-gcd-ℤ m n))
          ( eq-is-prop (is-prop-is-positive-ℤ n))))
      ( eq-is-prop (is-prop-is-reduced-fraction-ℤ (m , n , n-pos)))

section-rational-fraction-ℤ : section rational-fraction-ℤ
section-rational-fraction-ℤ = (fraction-ℚ , is-retraction-rational-fraction-ℚ)

retract-integer-fraction-ℚ : ℚ retract-of fraction-ℤ
retract-integer-fraction-ℚ =
  ( fraction-ℚ , rational-fraction-ℤ , is-retraction-rational-fraction-ℚ)

The rationals are countable

The denumerability of the rational numbers is the third theorem on Freek Wiedijk’s list of 100 theorems [Wie].

is-countable-ℚ : is-countable ℚ-Set
is-countable-ℚ =
  is-countable-retract-of
    ( fraction-ℤ-Set)
    ( ℚ-Set)
    ( retract-integer-fraction-ℚ)
    ( is-countable-fraction-ℤ)

Two fractions with the same numerator and same denominator are equal

module _
  ( x y : ℚ)
  ( H : numerator-ℚ x ＝ numerator-ℚ y)
  ( K : denominator-ℚ x ＝ denominator-ℚ y)
  where

  abstract
    eq-ℚ : x ＝ y
    eq-ℚ =
      ( inv (is-retraction-rational-fraction-ℚ x)) ∙
      ( eq-ℚ-sim-fraction-ℤ
        ( fraction-ℚ x)
        ( fraction-ℚ y)
        ( ap-mul-ℤ H (inv K))) ∙
      ( is-retraction-rational-fraction-ℚ y)

A rational number is zero if and only if its numerator is zero

module _
  (x : ℚ)
  where

  abstract
    is-zero-numerator-is-zero-ℚ :
      is-zero-ℚ x → is-zero-ℤ (numerator-ℚ x)
    is-zero-numerator-is-zero-ℚ = ap numerator-ℚ

    is-zero-is-zero-numerator-ℚ :
      is-zero-ℤ (numerator-ℚ x) → is-zero-ℚ x
    is-zero-is-zero-numerator-ℚ H =
      ( inv (is-retraction-rational-fraction-ℚ x)) ∙
      ( eq-ℚ-sim-fraction-ℤ
        ( fraction-ℚ x)
        ( fraction-ℚ zero-ℚ)
        ( eq-is-zero-ℤ
          ( ap (mul-ℤ' one-ℤ) H ∙ right-zero-law-mul-ℤ one-ℤ)
          ( left-zero-law-mul-ℤ (denominator-ℚ x)))) ∙
      ( is-retraction-rational-fraction-ℚ zero-ℚ)

The rational image of the negative of an integer is the rational negative of its image

abstract
  preserves-neg-rational-ℤ :
    (k : ℤ) → rational-ℤ (neg-ℤ k) ＝ neg-ℚ (rational-ℤ k)
  preserves-neg-rational-ℤ k =
    eq-ℚ (rational-ℤ (neg-ℤ k)) (neg-ℚ (rational-ℤ k)) refl refl

The reduced fraction of the negative of an integer fraction is the negative of the reduced fraction

abstract
  preserves-neg-rational-fraction-ℤ :
    (x : fraction-ℤ) →
    rational-fraction-ℤ (neg-fraction-ℤ x) ＝ neg-ℚ (rational-fraction-ℤ x)
  preserves-neg-rational-fraction-ℤ x =
    ( eq-ℚ-sim-fraction-ℤ
      ( neg-fraction-ℤ x)
      ( fraction-ℚ (neg-ℚ (rational-fraction-ℤ x)))
      ( preserves-sim-neg-fraction-ℤ
        ( x)
        ( reduce-fraction-ℤ x)
        ( sim-reduced-fraction-ℤ x))) ∙
    ( is-retraction-rational-fraction-ℚ (neg-ℚ (rational-fraction-ℤ x)))

The negative function on the rational numbers is an involution

abstract
  neg-neg-ℚ : (x : ℚ) → neg-ℚ (neg-ℚ x) ＝ x
  neg-neg-ℚ x = eq-ℚ (neg-ℚ (neg-ℚ x)) x (neg-neg-ℤ (numerator-ℚ x)) refl

The reflecting map from fraction-ℤ to ℚ

reflecting-map-sim-fraction :
  reflecting-map-equivalence-relation equivalence-relation-sim-fraction-ℤ ℚ
pr1 reflecting-map-sim-fraction = rational-fraction-ℤ
pr2 reflecting-map-sim-fraction {x} {y} H = eq-ℚ-sim-fraction-ℤ x y H

References

[Wie]
Freek Wiedijk. Formalizing 100 theorems. URL: https://www.cs.ru.nl/~freek/100/.

Recent changes