This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.
Rational real numbers
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-ℚ)