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-04-09.

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.sets
open import foundation.subtypes
open import foundation.universe-levels

Idea

The type of rational numbers is the quotient of the type of fractions, by the equivalence relation given by (n/m) ~ (n'/m') := Id (n *ℤ m') (n' *ℤ m).

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-ℚ

abstract
  is-retraction-rational-fraction-ℚ :
    (x : ℚ) → rational-fraction-ℤ (fraction-ℚ x) ＝ x
  is-retraction-rational-fraction-ℚ (pair (pair m (pair 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)))

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

Recent changes