# Rational real numbers

Content created by Fredrik Bakke, malarbol and Egbert Rijke.

Created on 2024-02-27.

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