Rational real numbers

Content created by Fredrik Bakke, malarbol and Egbert Rijke.

Created on 2024-02-27.
Last modified on 2024-09-28.

module real-numbers.rational-real-numbers where
Imports
open import elementary-number-theory.inequality-rational-numbers
open import elementary-number-theory.rational-numbers
open import elementary-number-theory.strict-inequality-rational-numbers

open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.conjunction
open import foundation.dependent-pair-types
open import foundation.disjunction
open import foundation.embeddings
open import foundation.empty-types
open import foundation.equivalences
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.retractions
open import foundation.sections
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import real-numbers.dedekind-real-numbers

Idea

The type of rationals embeds into the type of Dedekind reals . We call numbers in the image of this embedding rational real numbers.

Definitions

Strict inequality on rationals gives Dedekind cuts

is-dedekind-cut-le-ℚ :
  (x : ) 
  is-dedekind-cut
     (q : )  le-ℚ-Prop q x)
     (r : )  le-ℚ-Prop x r)
is-dedekind-cut-le-ℚ x =
  ( exists-lesser-ℚ x , exists-greater-ℚ x) ,
  ( ( λ (q : ) 
      dense-le-ℚ q x ,
      elim-exists
        ( le-ℚ-Prop q x)
        ( λ r (H , H')  transitive-le-ℚ q r x H' H)) ,
    ( λ (r : ) 
      α x r  dense-le-ℚ x r ,
      elim-exists
        ( le-ℚ-Prop x r)
        ( λ q (H , H')  transitive-le-ℚ x q r H H'))) ,
  ( λ (q : ) (H , H')  asymmetric-le-ℚ q x H H') ,
  ( located-le-ℚ x)
  where
    α :
      (a b : ) 
      exists   r  le-ℚ-Prop a r  le-ℚ-Prop r b) 
      exists   r  le-ℚ-Prop r b  le-ℚ-Prop a r)
    α a b =
      elim-exists
        (    r  le-ℚ-Prop r b  le-ℚ-Prop a r))
        ( λ r ( p , q)  intro-exists r ( q , p))

The canonical map from to

real-ℚ :    lzero
real-ℚ x =
  real-dedekind-cut
    ( λ (q : )  le-ℚ-Prop q x)
    ( λ (r : )  le-ℚ-Prop x r)
    ( is-dedekind-cut-le-ℚ x)

The property of being a rational real number

module _
  {l : Level} (x :  l) (p : )
  where

  is-rational-ℝ-Prop : Prop l
  is-rational-ℝ-Prop =
    (¬' (lower-cut-ℝ x p))  (¬' (upper-cut-ℝ x p))

  is-rational-ℝ : UU l
  is-rational-ℝ = type-Prop is-rational-ℝ-Prop
all-eq-is-rational-ℝ :
  {l : Level} (x :  l) (p q : ) 
  is-rational-ℝ x p 
  is-rational-ℝ x q 
  p  q
all-eq-is-rational-ℝ x p q H H' =
  trichotomy-le-ℚ p q left-case id right-case
  where
  left-case : le-ℚ p q  p  q
  left-case I =
    ex-falso
      ( elim-disjunction
        ( empty-Prop)
        ( pr1 H)
        ( pr2 H')
        ( is-located-lower-upper-cut-ℝ x p q I))

  right-case : le-ℚ q p  p  q
  right-case I =
    ex-falso
      ( elim-disjunction
        ( empty-Prop)
        ( pr1 H')
        ( pr2 H)
        ( is-located-lower-upper-cut-ℝ x q p I))

is-prop-rational-real : {l : Level} (x :  l)  is-prop (Σ  (is-rational-ℝ x))
is-prop-rational-real x =
  is-prop-all-elements-equal
    ( λ p q 
      eq-type-subtype
        ( is-rational-ℝ-Prop x)
        ( all-eq-is-rational-ℝ x (pr1 p) (pr1 q) (pr2 p) (pr2 q)))

The subtype of rational reals

subtype-rational-real : {l : Level}   l  Prop l
subtype-rational-real x =
  Σ  (is-rational-ℝ x) , is-prop-rational-real x

Rational-ℝ : (l : Level)  UU (lsuc l)
Rational-ℝ l =
  type-subtype subtype-rational-real

module _
  {l : Level} (x : Rational-ℝ l)
  where

  real-rational-ℝ :  l
  real-rational-ℝ = pr1 x

  rational-rational-ℝ : 
  rational-rational-ℝ = pr1 (pr2 x)

  is-rational-rational-ℝ : is-rational-ℝ real-rational-ℝ rational-rational-ℝ
  is-rational-rational-ℝ = pr2 (pr2 x)

Properties

The real embedding of a rational number is rational

is-rational-real-ℚ : (p : )  is-rational-ℝ (real-ℚ p) p
is-rational-real-ℚ p = (irreflexive-le-ℚ p , irreflexive-le-ℚ p)

Rational real numbers are embedded rationals

eq-real-rational-is-rational-ℝ :
  (x :  lzero) (q : ) (H : is-rational-ℝ x q)  real-ℚ q  x
eq-real-rational-is-rational-ℝ x q H =
  eq-eq-lower-cut-ℝ
    ( real-ℚ q)
    ( x)
    ( eq-has-same-elements-subtype
      ( λ p  le-ℚ-Prop p q)
      ( lower-cut-ℝ x)
      ( λ r 
        pair
          ( λ I 
            elim-disjunction
              ( lower-cut-ℝ x r)
              ( id)
              ( λ H'  ex-falso (pr2 H H'))
              ( is-located-lower-upper-cut-ℝ x r q I))
          ( trichotomy-le-ℚ r q
            ( λ I _  I)
            ( λ E H'  ex-falso (pr1 (tr (is-rational-ℝ x) (inv E) H) H'))
            ( λ I H'  ex-falso (pr1 H (le-lower-cut-ℝ x q r I H'))))))

The canonical map from rationals to rational reals

rational-real-ℚ :   Rational-ℝ lzero
rational-real-ℚ q = (real-ℚ q , q , is-rational-real-ℚ q)

The rationals and rational reals are equivalent

is-section-rational-real-ℚ :
  (q : ) 
  rational-rational-ℝ (rational-real-ℚ q)  q
is-section-rational-real-ℚ q = refl

is-retraction-rational-real-ℚ :
  (x : Rational-ℝ lzero) 
  rational-real-ℚ (rational-rational-ℝ x)  x
is-retraction-rational-real-ℚ (x , q , H) =
  eq-type-subtype
    subtype-rational-real
    ( ap real-ℚ α  eq-real-rational-is-rational-ℝ x q H)
  where
    α : rational-rational-ℝ (x , q , H)  q
    α = refl

equiv-rational-real : Rational-ℝ lzero  
pr1 equiv-rational-real = rational-rational-ℝ
pr2 equiv-rational-real =
  section-rational-rational-ℝ , retraction-rational-rational-ℝ
  where
  section-rational-rational-ℝ : section rational-rational-ℝ
  section-rational-rational-ℝ =
    (rational-real-ℚ , is-section-rational-real-ℚ)

  retraction-rational-rational-ℝ : retraction rational-rational-ℝ
  retraction-rational-rational-ℝ =
    (rational-real-ℚ , is-retraction-rational-real-ℚ)

Recent changes