Metric extensions of pseudometric spaces

src/metric-spaces.lagda.md

@@ -97,6 +97,7 @@ open import metric-spaces.images-uniformly-continuous-functions-metric-spaces pu
 open import metric-spaces.indexed-sums-metric-spaces public
 open import metric-spaces.inhabited-totally-bounded-subspaces-metric-spaces public
 open import metric-spaces.interior-subsets-metric-spaces public
+open import metric-spaces.isometries-between-metric-extensions-of-pseudometric-spaces public
 open import metric-spaces.isometries-metric-spaces public
 open import metric-spaces.isometries-pseudometric-spaces public
 open import metric-spaces.limits-of-cauchy-approximations-metric-spaces public
@@ -106,6 +107,7 @@ open import metric-spaces.limits-of-sequences-metric-spaces public
 open import metric-spaces.lipschitz-functions-metric-spaces public
 open import metric-spaces.locally-constant-functions-metric-spaces public
 open import metric-spaces.located-metric-spaces public
+open import metric-spaces.metric-extensions-of-pseudometric-spaces public
 open import metric-spaces.metric-quotients-of-pseudometric-spaces 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

src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md

@@ -107,7 +107,7 @@ module _
       ( cauchy-pseudocompletion-Metric-Space
         ( metric-quotient-Pseudometric-Space M))
   short-map-metric-quotient-cauchy-apprtoximation-Pseudometric-Space =
-    short-map-short-function-cauchy-approximation-Pseudometric-Space
+    short-map-cauchy-approximation-short-function-Pseudometric-Space
       ( M)
       ( pseudometric-metric-quotient-Pseudometric-Space M)
       ( short-map-metric-quotient-Pseudometric-Space M)

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

@@ -10,17 +10,13 @@ module metric-spaces.cauchy-approximations-metric-spaces where
 open import elementary-number-theory.addition-positive-rational-numbers
 open import elementary-number-theory.positive-rational-numbers
 
-open import foundation.constant-maps
-open import foundation.dependent-pair-types
-open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.subtypes
 open import foundation.universe-levels
 
-open import metric-spaces.cartesian-products-metric-spaces
 open import metric-spaces.cauchy-approximations-pseudometric-spaces
 open import metric-spaces.metric-spaces
 open import metric-spaces.short-functions-metric-spaces
@@ -123,7 +119,7 @@ module _
     cauchy-approximation-Metric-Space A →
     cauchy-approximation-Metric-Space B
   map-short-function-cauchy-approximation-Metric-Space =
-    map-short-function-cauchy-approximation-Pseudometric-Space
+    map-cauchy-approximation-short-function-Pseudometric-Space
       ( pseudometric-Metric-Space A)
       ( pseudometric-Metric-Space B)
       ( f)

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

@@ -19,6 +19,7 @@ open import foundation.propositions
 open import foundation.subtypes
 open import foundation.universe-levels
 
+open import metric-spaces.isometries-pseudometric-spaces
 open import metric-spaces.pseudometric-spaces
 open import metric-spaces.short-functions-pseudometric-spaces
 ```
@@ -112,10 +113,10 @@ module _
   (f : short-function-Pseudometric-Space A B)
   where
 
-  map-short-function-cauchy-approximation-Pseudometric-Space :
+  map-cauchy-approximation-short-function-Pseudometric-Space :
     cauchy-approximation-Pseudometric-Space A →
     cauchy-approximation-Pseudometric-Space B
-  map-short-function-cauchy-approximation-Pseudometric-Space (u , H) =
+  map-cauchy-approximation-short-function-Pseudometric-Space (u , H) =
     ( map-short-function-Pseudometric-Space A B f ∘ u ,
       λ ε δ →
         is-short-map-short-function-Pseudometric-Space
@@ -128,6 +129,25 @@ module _
           ( H ε δ))
 ```
 
+### The action of isometries on Cauchy approximations
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2')
+  (f : isometry-Pseudometric-Space A B)
+  where
+
+  map-cauchy-approximation-isometry-Pseudometric-Space :
+    cauchy-approximation-Pseudometric-Space A →
+    cauchy-approximation-Pseudometric-Space B
+  map-cauchy-approximation-isometry-Pseudometric-Space =
+    map-cauchy-approximation-short-function-Pseudometric-Space
+      ( A)
+      ( B)
+      ( short-isometry-Pseudometric-Space A B f)
+```
+
 ### Homotopic Cauchy approximations are equal
 
 ```agda

src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md

@@ -9,25 +9,20 @@ module metric-spaces.cauchy-pseudocompletion-of-metric-spaces where
 ```agda
 open import elementary-number-theory.addition-positive-rational-numbers
 open import elementary-number-theory.positive-rational-numbers
-open import elementary-number-theory.strict-inequality-rational-numbers
 
-open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
 open import foundation.binary-relations
-open import foundation.binary-transport
 open import foundation.dependent-pair-types
 open import foundation.function-types
 open import foundation.homotopies
 open import foundation.identity-types
-open import foundation.propositions
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import metric-spaces.cauchy-approximations-metric-spaces
 open import metric-spaces.cauchy-approximations-pseudometric-spaces
 open import metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces
 open import metric-spaces.complete-metric-spaces
-open import metric-spaces.convergent-cauchy-approximations-metric-spaces
 open import metric-spaces.functions-pseudometric-spaces
 open import metric-spaces.isometries-pseudometric-spaces
 open import metric-spaces.limits-of-cauchy-approximations-metric-spaces
@@ -437,3 +432,103 @@ module _
       ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u)
       ( is-limit-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u)
 ```
+
+### The isometry from the Cauchy pseudocompletion of a complete metric space to its limit
+
+```agda
+module _
+  {l1 l2 : Level} (M : Metric-Space l1 l2)
+  (is-complete-M : is-complete-Metric-Space M)
+  where
+
+  abstract
+    reflects-neighborhood-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space :
+      (δ : ℚ⁺) →
+      (u v : cauchy-approximation-Metric-Space M) →
+      neighborhood-Metric-Space
+        ( M)
+        ( δ)
+        ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+          ( M)
+          ( is-complete-M)
+          ( u))
+        ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+          ( M)
+          ( is-complete-M)
+          ( v)) →
+      neighborhood-Pseudometric-Space
+        ( cauchy-pseudocompletion-Metric-Space M)
+        ( δ)
+        ( u)
+        ( v)
+    reflects-neighborhood-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+      δ x y Nδ =
+      reflects-neighborhood-sim-Pseudometric-Space
+        ( cauchy-pseudocompletion-Metric-Space M)
+          { x}
+          { const-cauchy-approximation-Metric-Space
+            ( M)
+            ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+              ( M)
+              ( is-complete-M)
+              ( x))}
+          { y}
+          { const-cauchy-approximation-Metric-Space
+            ( M)
+            ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+              ( M)
+              ( is-complete-M)
+              ( y))}
+        ( sim-const-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+          ( M)
+          ( is-complete-M)
+          ( x))
+        ( sim-const-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+          ( M)
+          ( is-complete-M)
+          ( y))
+        ( δ)
+        ( preserves-neighborhood-map-isometry-Pseudometric-Space
+          ( pseudometric-Metric-Space M)
+          ( cauchy-pseudocompletion-Metric-Space M)
+          ( isometry-cauchy-pseudocompletion-Metric-Space M)
+          ( δ)
+          ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+            ( M)
+            ( is-complete-M)
+            ( x))
+          ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+            ( M)
+            ( is-complete-M)
+            ( y))
+          ( Nδ))
+
+    is-isometry-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space :
+      is-isometry-Pseudometric-Space
+        ( cauchy-pseudocompletion-Metric-Space M)
+        ( pseudometric-Metric-Space M)
+        ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+          ( M)
+          ( is-complete-M))
+    is-isometry-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space d x y =
+      ( ( is-short-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+          ( M)
+          ( is-complete-M)
+          ( d)
+          ( x)
+          ( y)) ,
+        ( reflects-neighborhood-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+          ( d)
+          ( x)
+          ( y)))
+
+  isometry-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space :
+    isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Metric-Space M)
+      ( pseudometric-Metric-Space M)
+  isometry-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space =
+    ( ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+        ( M)
+        ( is-complete-M)) ,
+      ( is-isometry-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space))
+```