Archimedean property of ℚ (#1268)

UniMath · Feb 4, 2025 · f7d9a5c · f7d9a5c
1 parent 0b11fe7
commit f7d9a5c
Show file tree

Hide file tree

Showing 3 changed files with 82 additions and 10 deletions.
diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md
@@ -20,6 +20,7 @@ open import elementary-number-theory.additive-group-of-rational-numbers public
 open import elementary-number-theory.archimedean-property-integer-fractions public
 open import elementary-number-theory.archimedean-property-integers public
 open import elementary-number-theory.archimedean-property-natural-numbers public
+open import elementary-number-theory.archimedean-property-rational-numbers public
 open import elementary-number-theory.arithmetic-functions public
 open import elementary-number-theory.based-induction-natural-numbers public
 open import elementary-number-theory.based-strong-induction-natural-numbers public

diff --git a/src/elementary-number-theory/archimedean-property-rational-numbers.lagda.md b/src/elementary-number-theory/archimedean-property-rational-numbers.lagda.md
@@ -0,0 +1,70 @@
+# The Archimedean property of `ℚ`
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module elementary-number-theory.archimedean-property-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.archimedean-property-integer-fractions
+open import elementary-number-theory.integer-fractions
+open import elementary-number-theory.integers
+open import elementary-number-theory.multiplication-integer-fractions
+open import elementary-number-theory.multiplication-rational-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.strict-inequality-rational-numbers
+
+open import foundation.action-on-identifications-binary-functions
+open import foundation.binary-transport
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.identity-types
+```
+
+</details>
+
+## Definition
+
+The
+{{#concept "Archimedean property" Disambiguation="rational numbers" Agda=archimedean-property-ℚ}}
+of `ℚ` is that for any two
+[rational numbers](elementary-number-theory.rational-numbers.md) `x y : ℚ`, with
+[positive](elementary-number-theory.positive-rational-numbers.md) `x`, there is
+an `n : ℕ` such that `y` is less than `n` as a rational number times `x`.
+
+```agda
+abstract
+  archimedean-property-ℚ :
+    (x y : ℚ) →
+      is-positive-ℚ x →
+      exists ℕ (λ n → le-ℚ-Prop y (rational-ℤ (int-ℕ n) *ℚ x))
+  archimedean-property-ℚ x y positive-x =
+    elim-exists
+      ( ∃ ℕ (λ n → le-ℚ-Prop y (rational-ℤ (int-ℕ n) *ℚ x)))
+      ( λ n nx<y →
+        intro-exists
+          ( n)
+          ( binary-tr
+              le-ℚ
+              ( is-retraction-rational-fraction-ℚ y)
+              ( inv
+                ( mul-rational-fraction-ℤ
+                  ( in-fraction-ℤ (int-ℕ n))
+                  ( fraction-ℚ x)) ∙
+                ap-binary
+                  ( mul-ℚ)
+                  ( is-retraction-rational-fraction-ℚ (rational-ℤ (int-ℕ n)))
+                  ( is-retraction-rational-fraction-ℚ x))
+              ( preserves-le-rational-fraction-ℤ
+                ( fraction-ℚ y)
+                ( in-fraction-ℤ (int-ℕ n) *fraction-ℤ fraction-ℚ x) nx<y)))
+      ( archimedean-property-fraction-ℤ
+        ( fraction-ℚ x)
+        ( fraction-ℚ y)
+        ( positive-x))
+```
diff --git a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md
@@ -159,16 +159,17 @@ module _
   (p q : fraction-ℤ)
   where
 
-  preserves-le-rational-fraction-ℤ :
-    le-fraction-ℤ p q → le-ℚ (rational-fraction-ℤ p) (rational-fraction-ℤ q)
-  preserves-le-rational-fraction-ℤ =
-    preserves-le-sim-fraction-ℤ
-      ( p)
-      ( q)
-      ( reduce-fraction-ℤ p)
-      ( reduce-fraction-ℤ q)
-      ( sim-reduced-fraction-ℤ p)
-      ( sim-reduced-fraction-ℤ q)
+  abstract
+    preserves-le-rational-fraction-ℤ :
+      le-fraction-ℤ p q → le-ℚ (rational-fraction-ℤ p) (rational-fraction-ℤ q)
+    preserves-le-rational-fraction-ℤ =
+      preserves-le-sim-fraction-ℤ
+        ( p)
+        ( q)
+        ( reduce-fraction-ℤ p)
+        ( reduce-fraction-ℤ q)
+        ( sim-reduced-fraction-ℤ p)
+        ( sim-reduced-fraction-ℤ q)
 
 module _
   (x : ℚ) (p : fraction-ℤ)