Initial metric extensions of pseudometric spaces

src/metric-spaces.lagda.md

@@ -96,7 +96,9 @@ open import metric-spaces.images-short-functions-metric-spaces public
 open import metric-spaces.images-uniformly-continuous-functions-metric-spaces public
 open import metric-spaces.indexed-sums-metric-spaces public
 open import metric-spaces.inhabited-totally-bounded-subspaces-metric-spaces public
+open import metric-spaces.initial-metric-extensions-of-pseudometric-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 +108,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/bounded-distance-decompositions-of-metric-spaces.lagda.md

@@ -213,7 +213,7 @@ module _
   {l1 l2 : Level} (A : Metric-Space l1 l2)
   where
 
-  preserves-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space :
+  preserves-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space :
     ( d : ℚ⁺)
     ( x y : type-bounded-distance-decomposition-Metric-Space A) →
     neighborhood-Metric-Space
@@ -224,7 +224,7 @@ module _
     neighborhood-Metric-Space A d
       ( map-equiv-bounded-distance-decomposition-Metric-Space A x)
       ( map-equiv-bounded-distance-decomposition-Metric-Space A y)
-  preserves-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space
+  preserves-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space
     d (X , x , x∈X) (Y , y , y∈Y) (X=Y , Nxy) =
     forward-implication
       ( lemma-iff-neighborhood-bounded-distance-decomposition-Metric-Space
@@ -237,7 +237,7 @@ module _
         ( y , y∈Y))
       ( Nxy)
 
-  reflects-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space :
+  reflects-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space :
     ( d : ℚ⁺)
     ( x y : type-bounded-distance-decomposition-Metric-Space A) →
     neighborhood-Metric-Space A d
@@ -248,7 +248,7 @@ module _
       ( d)
       ( x)
       ( y)
-  reflects-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space
+  reflects-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space
     d (X , x , x∈X) (Y , y , y∈Y) Nxy =
     ( lemma-eq ,
       backward-implication
@@ -280,11 +280,11 @@ module _
       ( map-equiv-bounded-distance-decomposition-Metric-Space A)
   is-isometry-map-equiv-bounded-distance-decomposition-Metric-Space
     d x y =
-    ( ( preserves-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space
+    ( ( preserves-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space
         ( d)
         ( x)
         ( y)) ,
-      ( reflects-neighborhood-map-equiv-bounded-distance-decomposition-Metric-Space
+      ( reflects-neighborhoods-map-equiv-bounded-distance-decomposition-Metric-Space
         ( d)
         ( x)
         ( y)))

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)
@@ -233,7 +233,7 @@ module _
           ( x)
           ( x∈uε)
     in
-      preserves-neighborhood-sim-Pseudometric-Space
+      preserves-neighborhoods-sim-Pseudometric-Space
         ( M)
         ( uε~x)
         ( lim~y)

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)
@@ -137,7 +133,7 @@ module _
     map-short-function-cauchy-approximation-Metric-Space
       ( A)
       ( A)
-      ( short-id-Metric-Space A) ＝
+      ( id-short-function-Metric-Space A) ＝
     id
   eq-id-map-short-function-cauchy-approximation-Metric-Space = refl
 

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
@@ -146,6 +166,50 @@ module _
       ( eq-htpy f~g)
 ```
 
+### The action of isometries preserves homotopies
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2')
+  (f g : isometry-Pseudometric-Space A B)
+  where
+
+  htpy-map-cauchy-approximation-isometry-Pseudometric-Space :
+    htpy-isometry-Pseudometric-Space A B f g →
+    map-cauchy-approximation-isometry-Pseudometric-Space A B f ~
+    map-cauchy-approximation-isometry-Pseudometric-Space A B g
+  htpy-map-cauchy-approximation-isometry-Pseudometric-Space f~g u =
+    eq-htpy-cauchy-approximation-Pseudometric-Space B
+      ( f~g ∘ map-cauchy-approximation-Pseudometric-Space A u)
+```
+
+### The action of isometries preserves composition
+
+```agda
+module _
+  {la la' lb lb' lc lc' : Level}
+  (A : Pseudometric-Space la la')
+  (B : Pseudometric-Space lb lb')
+  (C : Pseudometric-Space lc lc')
+  (g : isometry-Pseudometric-Space B C)
+  (f : isometry-Pseudometric-Space A B)
+  where
+
+  htpy-map-cauchy-approximation-comp-isometry-Pseudometric-Space :
+    ( map-cauchy-approximation-isometry-Pseudometric-Space B C g ∘
+      map-cauchy-approximation-isometry-Pseudometric-Space A B f) ~
+    ( map-cauchy-approximation-isometry-Pseudometric-Space A C
+      ( comp-isometry-Pseudometric-Space
+        ( A)
+        ( B)
+        ( C)
+        ( g)
+        ( f)))
+  htpy-map-cauchy-approximation-comp-isometry-Pseudometric-Space u =
+    eq-htpy-cauchy-approximation-Pseudometric-Space C refl-htpy
+```
+
 ## References
 
 Our definition of Cauchy approximation follows Definition 4.5.5 of

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
@@ -354,7 +349,7 @@ module _
         ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space))
   is-short-const-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
     d x y =
-      preserves-neighborhood-sim-Pseudometric-Space
+      preserves-neighborhoods-sim-Pseudometric-Space
         ( cauchy-pseudocompletion-Metric-Space M)
         { x}
         { const-cauchy-approximation-Metric-Space
@@ -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-neighborhoods-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-neighborhoods-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space
+      δ x y Nδ =
+      reflects-neighborhoods-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-neighborhoods-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-neighborhoods-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))
+```