The rational numbers

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

Created on 2022-02-17.
Last modified on 2023-06-25.

module elementary-number-theory.rational-numbers where
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.reduced-integer-fractions

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.universe-levels


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


The type of rationals

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

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

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

Inclusion of fractions

in-fraction-ℤ : fraction-ℤ  
pr1 (in-fraction-ℤ x) = reduce-fraction-ℤ x
pr2 (in-fraction-ℤ x) = is-reduced-reduce-fraction-ℤ x

Inclusion of the integers

in-int :   
in-int x = pair (pair x one-positive-ℤ) (is-one-gcd-one-ℤ' x)

Negative one, zero and one

neg-one-ℚ : 
neg-one-ℚ = in-int neg-one-ℤ

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

zero-ℚ : 
zero-ℚ = in-int zero-ℤ

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

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

one-ℚ : 
one-ℚ = in-int one-ℤ

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


eq-ℚ-sim-fractions-ℤ :
  (x y : fraction-ℤ)  (H : sim-fraction-ℤ x y) 
  in-fraction-ℤ x  in-fraction-ℤ y
eq-ℚ-sim-fractions-ℤ x y H =
    ( 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

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

in-fraction-fraction-ℚ : (x : )  in-fraction-ℤ (fraction-ℚ x)  x
in-fraction-fraction-ℚ (pair (pair m (pair n n-pos)) p) =
    ( 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)))

The reflecting map from ℤ to ℚ

reflecting-map-sim-fraction :
  reflecting-map-Equivalence-Relation eq-rel-sim-fraction-ℤ 
pr1 reflecting-map-sim-fraction = in-fraction-ℤ
pr2 reflecting-map-sim-fraction {x} {y} H = eq-ℚ-sim-fractions-ℤ x y H

Recent changes