The short map from a convergent Cauchy approximation in a saturated metric space to its limit (#1402)

The map from a convergent Cauchy approximation in a saturated metric
space to its limit is short. As a consequence, the metric space of
Cauchy approximations in a saturated complete metric space is saturated
and complete.

Author: malarbol

src/elementary-number-theory/positive-rational-numbers.lagda.md

@@ -329,6 +329,9 @@ semigroup-add-ℚ⁺ =
 add-ℚ⁺ : ℚ⁺ → ℚ⁺ → ℚ⁺
 add-ℚ⁺ = mul-Subsemigroup semigroup-add-ℚ subsemigroup-add-ℚ⁺
 
+add-ℚ⁺' : ℚ⁺ → ℚ⁺ → ℚ⁺
+add-ℚ⁺' x y = add-ℚ⁺ y x
+
 infixl 35 _+ℚ⁺_
 _+ℚ⁺_ = add-ℚ⁺
 ```
@@ -676,15 +679,7 @@ module _
   where
 
   le-diff-ℚ⁺ : ℚ⁺
-  pr1 le-diff-ℚ⁺ = (rational-ℚ⁺ y) -ℚ (rational-ℚ⁺ x)
-  pr2 le-diff-ℚ⁺ =
-    is-positive-le-zero-ℚ
-      ( (rational-ℚ⁺ y) -ℚ (rational-ℚ⁺ x))
-      ( backward-implication
-        ( iff-translate-diff-le-zero-ℚ
-          ( rational-ℚ⁺ x)
-          ( rational-ℚ⁺ y))
-        ( ( H)))
+  le-diff-ℚ⁺ = positive-diff-le-ℚ (rational-ℚ⁺ x) (rational-ℚ⁺ y) H
 
   left-diff-law-add-ℚ⁺ : le-diff-ℚ⁺ +ℚ⁺ x ＝ y
   left-diff-law-add-ℚ⁺ =
@@ -705,6 +700,13 @@ module _
         ( rational-ℚ⁺ x)
         ( rational-ℚ⁺ le-diff-ℚ⁺))) ∙
     ( left-diff-law-add-ℚ⁺)
+
+  le-le-diff-ℚ⁺ : le-ℚ⁺ le-diff-ℚ⁺ y
+  le-le-diff-ℚ⁺ =
+    tr
+      ( le-ℚ⁺ le-diff-ℚ⁺)
+      ( left-diff-law-add-ℚ⁺)
+      ( le-left-add-ℚ⁺ le-diff-ℚ⁺ x)
 ```
 
 ### Multiplication by a positive rational number preserves strict inequality
@@ -905,37 +907,55 @@ module _
 ### Any positive rational number `p` has a `q` with `q + q < p`
 
 ```agda
-abstract
-  bound-double-le-ℚ⁺ :
-    (p : ℚ⁺) →
-    Σ ℚ⁺ (λ q → le-ℚ⁺ (q +ℚ⁺ q) p)
-  bound-double-le-ℚ⁺ p = dependent-pair-result
-    where
-    q : ℚ⁺
-    q = left-summand-split-ℚ⁺ p
-    r : ℚ⁺
-    r = right-summand-split-ℚ⁺ p
-    s : ℚ⁺
-    s = mediant-zero-min-ℚ⁺ q r
-    -- Inlining this blows up compile times for some unclear reason.
-    dependent-pair-result : Σ ℚ⁺ (λ x → le-ℚ⁺ (x +ℚ⁺ x) p)
-    dependent-pair-result =
-      s ,
+module _
+  (p : ℚ⁺)
+  where
+
+  modulus-le-double-le-ℚ⁺ : ℚ⁺
+  modulus-le-double-le-ℚ⁺ =
+    mediant-zero-min-ℚ⁺
+      ( left-summand-split-ℚ⁺ p)
+      ( right-summand-split-ℚ⁺ p)
+
+  abstract
+    le-double-le-modulus-le-double-le-ℚ⁺ :
+        le-ℚ⁺
+          ( modulus-le-double-le-ℚ⁺ +ℚ⁺ modulus-le-double-le-ℚ⁺)
+          ( p)
+    le-double-le-modulus-le-double-le-ℚ⁺ =
       tr
-        ( le-ℚ⁺ (s +ℚ⁺ s))
+        ( le-ℚ⁺ (modulus-le-double-le-ℚ⁺ +ℚ⁺ modulus-le-double-le-ℚ⁺))
         ( eq-add-split-ℚ⁺ p)
         ( preserves-le-add-ℚ
-          { rational-ℚ⁺ s}
-          { rational-ℚ⁺ q}
-          { rational-ℚ⁺ s}
-          { rational-ℚ⁺ r}
-          ( le-left-mediant-zero-min-ℚ⁺ q r)
-          ( le-right-mediant-zero-min-ℚ⁺ q r))
-
-  double-le-ℚ⁺ :
-    (p : ℚ⁺) →
-    exists ℚ⁺ (λ q → le-prop-ℚ⁺ (q +ℚ⁺ q) p)
-  double-le-ℚ⁺ p = unit-trunc-Prop (bound-double-le-ℚ⁺ p)
+          { rational-ℚ⁺ (modulus-le-double-le-ℚ⁺)}
+          { rational-ℚ⁺ (left-summand-split-ℚ⁺ p)}
+          { rational-ℚ⁺ (modulus-le-double-le-ℚ⁺)}
+          { rational-ℚ⁺ (right-summand-split-ℚ⁺ p)}
+          ( le-left-mediant-zero-min-ℚ⁺
+            ( left-summand-split-ℚ⁺ p)
+            ( right-summand-split-ℚ⁺ p))
+          ( le-right-mediant-zero-min-ℚ⁺
+            ( left-summand-split-ℚ⁺ p)
+            ( right-summand-split-ℚ⁺ p)))
+
+    le-modulus-le-double-le-ℚ⁺ : le-ℚ⁺ modulus-le-double-le-ℚ⁺ p
+    le-modulus-le-double-le-ℚ⁺ =
+      transitive-le-ℚ⁺
+        ( modulus-le-double-le-ℚ⁺)
+        ( left-summand-split-ℚ⁺ p)
+        ( p)
+        ( le-mediant-zero-ℚ⁺ p)
+        ( le-left-mediant-zero-min-ℚ⁺
+          ( left-summand-split-ℚ⁺ p)
+          ( right-summand-split-ℚ⁺ p))
+
+    bound-double-le-ℚ⁺ :
+      Σ ℚ⁺ (λ q → le-ℚ⁺ (q +ℚ⁺ q) p)
+    bound-double-le-ℚ⁺ =
+      ( modulus-le-double-le-ℚ⁺ , le-double-le-modulus-le-double-le-ℚ⁺)
+
+    double-le-ℚ⁺ : exists ℚ⁺ (λ q → le-prop-ℚ⁺ (q +ℚ⁺ q) p)
+    double-le-ℚ⁺ = unit-trunc-Prop bound-double-le-ℚ⁺
 ```
 
 ### Addition with a positive rational number is an increasing map

src/metric-spaces.lagda.md

@@ -69,8 +69,10 @@ open import metric-spaces.isometric-equivalences-premetric-spaces public
 open import metric-spaces.isometries-metric-spaces public
 open import metric-spaces.isometries-premetric-spaces public
 open import metric-spaces.limits-of-cauchy-approximations-in-premetric-spaces public
-open import metric-spaces.metric-space-of-cauchy-approximations-in-a-metric-space public
-open import metric-spaces.metric-space-of-convergent-cauchy-approximations-in-a-metric-space public
+open import metric-spaces.metric-space-of-cauchy-approximations-complete-metric-spaces public
+open import metric-spaces.metric-space-of-cauchy-approximations-metric-spaces public
+open import metric-spaces.metric-space-of-cauchy-approximations-saturated-complete-metric-spaces public
+open import metric-spaces.metric-space-of-convergent-cauchy-approximations-metric-spaces public
 open import metric-spaces.metric-space-of-rational-numbers public
 open import metric-spaces.metric-space-of-rational-numbers-with-open-neighborhoods public
 open import metric-spaces.metric-spaces public
@@ -85,6 +87,7 @@ open import metric-spaces.premetric-structures public
 open import metric-spaces.pseudometric-spaces public
 open import metric-spaces.pseudometric-structures public
 open import metric-spaces.reflexive-premetric-structures public
+open import metric-spaces.saturated-complete-metric-spaces public
 open import metric-spaces.saturated-metric-spaces public
 open import metric-spaces.short-functions-metric-spaces public
 open import metric-spaces.short-functions-premetric-spaces public

src/metric-spaces/cauchy-approximations-metric-spaces.lagda.md

@@ -21,6 +21,7 @@ open import foundation.universe-levels
 open import metric-spaces.cauchy-approximations-premetric-spaces
 open import metric-spaces.limits-of-cauchy-approximations-in-premetric-spaces
 open import metric-spaces.metric-spaces
+open import metric-spaces.short-functions-metric-spaces
 ```
 
 </details>
@@ -77,3 +78,24 @@ module _
       ( map-cauchy-approximation-Metric-Space δ)
   is-cauchy-approximation-map-cauchy-approximation-Metric-Space = pr2 f
 ```
+
+## Properties
+
+### Short maps between metric spaces preserve Cauchy approximations
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Metric-Space l1 l2) (B : Metric-Space l1' l2')
+  (f : short-function-Metric-Space A B)
+  where
+
+  map-short-function-cauchy-approximation-Metric-Space :
+    cauchy-approximation-Metric-Space A →
+    cauchy-approximation-Metric-Space B
+  map-short-function-cauchy-approximation-Metric-Space =
+    map-short-function-cauchy-approximation-Premetric-Space
+      ( premetric-Metric-Space A)
+      ( premetric-Metric-Space B)
+      ( f)
+```

src/metric-spaces/complete-metric-spaces.lagda.md

@@ -10,7 +10,11 @@ module metric-spaces.complete-metric-spaces where
 open import elementary-number-theory.positive-rational-numbers
 
 open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.identity-types
 open import foundation.propositions
+open import foundation.retractions
+open import foundation.sections
 open import foundation.subtypes
 open import foundation.universe-levels
 
@@ -83,6 +87,84 @@ module _
   is-complete-metric-space-Complete-Metric-Space = pr2 A
 ```
 
+### The equivalence between Cauchy approximations and convergent Cauchy approximations in a complete metric space
+
+```agda
+module _
+  {l1 l2 : Level}
+  (A : Complete-Metric-Space l1 l2)
+  where
+
+  convergent-cauchy-approximation-Complete-Metric-Space :
+    cauchy-approximation-Metric-Space
+      ( metric-space-Complete-Metric-Space A) →
+    convergent-cauchy-approximation-Metric-Space
+      ( metric-space-Complete-Metric-Space A)
+  convergent-cauchy-approximation-Complete-Metric-Space u =
+    ( u , is-complete-metric-space-Complete-Metric-Space A u)
+
+  is-section-convergent-cauchy-approximation-Complete-Metric-Space :
+    is-section
+      ( convergent-cauchy-approximation-Complete-Metric-Space)
+      ( inclusion-subtype
+        ( is-convergent-prop-cauchy-approximation-Metric-Space
+          ( metric-space-Complete-Metric-Space A)))
+  is-section-convergent-cauchy-approximation-Complete-Metric-Space u =
+    eq-type-subtype
+      ( is-convergent-prop-cauchy-approximation-Metric-Space
+        ( metric-space-Complete-Metric-Space A))
+      ( refl)
+
+  is-retraction-convergent-cauchy-approximation-Metric-Space :
+    is-retraction
+      ( convergent-cauchy-approximation-Complete-Metric-Space)
+      ( inclusion-subtype
+        ( is-convergent-prop-cauchy-approximation-Metric-Space
+          ( metric-space-Complete-Metric-Space A)))
+  is-retraction-convergent-cauchy-approximation-Metric-Space u = refl
+
+  is-equiv-convergent-cauchy-approximation-Complete-Metric-Space :
+    is-equiv convergent-cauchy-approximation-Complete-Metric-Space
+  pr1 is-equiv-convergent-cauchy-approximation-Complete-Metric-Space =
+    ( inclusion-subtype
+      ( is-convergent-prop-cauchy-approximation-Metric-Space
+        ( metric-space-Complete-Metric-Space A))) ,
+    ( is-section-convergent-cauchy-approximation-Complete-Metric-Space)
+  pr2 is-equiv-convergent-cauchy-approximation-Complete-Metric-Space =
+    ( inclusion-subtype
+      ( is-convergent-prop-cauchy-approximation-Metric-Space
+        ( metric-space-Complete-Metric-Space A))) ,
+    ( is-retraction-convergent-cauchy-approximation-Metric-Space)
+```
+
+### The limit of a Cauchy approximation in a complete metric space
+
+```agda
+module _
+  { l1 l2 : Level}
+  ( A : Complete-Metric-Space l1 l2)
+  ( u : cauchy-approximation-Metric-Space
+    ( metric-space-Complete-Metric-Space A))
+  where
+
+  limit-cauchy-approximation-Complete-Metric-Space :
+    type-Complete-Metric-Space A
+  limit-cauchy-approximation-Complete-Metric-Space =
+    limit-convergent-cauchy-approximation-Metric-Space
+      ( metric-space-Complete-Metric-Space A)
+      ( convergent-cauchy-approximation-Complete-Metric-Space A u)
+
+  is-limit-limit-cauchy-approximation-Complete-Metric-Space :
+    is-limit-cauchy-approximation-Metric-Space
+      ( metric-space-Complete-Metric-Space A)
+      ( u)
+      ( limit-cauchy-approximation-Complete-Metric-Space)
+  is-limit-limit-cauchy-approximation-Complete-Metric-Space =
+    is-limit-limit-convergent-cauchy-approximation-Metric-Space
+      ( metric-space-Complete-Metric-Space A)
+      ( convergent-cauchy-approximation-Complete-Metric-Space A u)
+```
+
 ## External links
 
 - [Complete metric space](https://en.wikipedia.org/wiki/Complete_metric_space)

src/metric-spaces/convergent-cauchy-approximations-metric-spaces.lagda.md

@@ -28,7 +28,7 @@ in a [metric space](metric-spaces.metric-spaces.md) is
 {{#concept "convergent" Disambiguation="Cauchy approximation in a metric space" agda=is-convergent-cauchy-approximation-Metric-Space}}
 if it has a
 [limit](metric-spaces.limits-of-cauchy-approximations-in-premetric-spaces.md).
-Because limits of cauchy approximations in metric spaces are unique, this is a
+Because limits of Cauchy approximations in metric spaces are unique, this is a
 [subtype](foundation.subtypes.md) of the type of Cauchy approximations.
 
 ## Definitions
@@ -41,12 +41,17 @@ module _
   (f : cauchy-approximation-Metric-Space A)
   where
 
+  is-limit-cauchy-approximation-Metric-Space :
+    type-Metric-Space A → UU l2
+  is-limit-cauchy-approximation-Metric-Space =
+    is-limit-cauchy-approximation-Premetric-Space
+      ( premetric-Metric-Space A)
+      ( f)
+
   is-convergent-cauchy-approximation-Metric-Space : UU (l1 ⊔ l2)
   is-convergent-cauchy-approximation-Metric-Space =
     Σ ( type-Metric-Space A)
-      ( is-limit-cauchy-approximation-Premetric-Space
-        ( premetric-Metric-Space A)
-        ( f))
+      ( is-limit-cauchy-approximation-Metric-Space)
 
   abstract
     is-prop-is-convergent-cauchy-approximation-Metric-Space :
@@ -73,7 +78,7 @@ module _
     is-prop-is-convergent-cauchy-approximation-Metric-Space
 ```
 
-### The type of convergent cauchy approximations in a metric space
+### The type of convergent Cauchy approximations in a metric space
 
 ```agda
 module _

src/metric-spaces/dependent-products-metric-spaces.lagda.md

@@ -20,6 +20,7 @@ open import metric-spaces.monotonic-premetric-structures
 open import metric-spaces.premetric-structures
 open import metric-spaces.pseudometric-structures
 open import metric-spaces.reflexive-premetric-structures
+open import metric-spaces.saturated-metric-spaces
 open import metric-spaces.short-functions-metric-spaces
 open import metric-spaces.symmetric-premetric-structures
 open import metric-spaces.triangular-premetric-structures
@@ -127,4 +128,24 @@ module _
       ( P a)
       ( λ f → f a)
   is-short-ev-Π-Metric-Space ε x y H = H a
+
+  short-ev-Π-Metric-Space :
+    short-function-Metric-Space
+      ( Π-Metric-Space A P)
+      ( P a)
+  short-ev-Π-Metric-Space = (λ f → f a) , (is-short-ev-Π-Metric-Space)
+```
+
+### Dependent products of saturated metric spaces are saturated
+
+```agda
+module _
+  {l l1 l2 : Level} (A : UU l) (P : A → Metric-Space l1 l2)
+  (Π-saturated : (a : A) → is-saturated-Metric-Space (P a))
+  where
+
+  is-saturated-Π-is-saturated-Metric-Space :
+    is-saturated-Metric-Space (Π-Metric-Space A P)
+  is-saturated-Π-is-saturated-Metric-Space ε x y H a =
+    Π-saturated a ε (x a) (y a) (λ d → H d a)
 ```