Refactor function actions on cauchy approximations

src/metric-spaces.lagda.md

@@ -57,13 +57,17 @@ metric space, `N d₂ x y` [or](foundation.disjunction.md)
 module metric-spaces where
 
 open import metric-spaces.accumulation-points-subsets-located-metric-spaces public
+open import metric-spaces.action-on-cauchy-approximations-isometries-pseudometric-spaces public
+open import metric-spaces.action-on-cauchy-approximations-short-maps-metric-spaces public
+open import metric-spaces.action-on-cauchy-approximations-short-maps-pseudometric-spaces public
 open import metric-spaces.apartness-located-metric-spaces public
 open import metric-spaces.approximations-located-metric-spaces public
 open import metric-spaces.approximations-metric-spaces public
 open import metric-spaces.bounded-distance-decompositions-of-metric-spaces public
 open import metric-spaces.cartesian-products-metric-spaces public
 open import metric-spaces.category-of-metric-spaces-and-isometries public
 open import metric-spaces.category-of-metric-spaces-and-short-functions public
+open import metric-spaces.cauchy-approximations-in-cauchy-pseudocompletions-of-pseudometric-spaces public
 open import metric-spaces.cauchy-approximations-metric-quotients-of-pseudometric-spaces public
 open import metric-spaces.cauchy-approximations-metric-spaces public
 open import metric-spaces.cauchy-approximations-pseudometric-spaces public

src/metric-spaces/accumulation-points-subsets-located-metric-spaces.lagda.md

@@ -28,6 +28,7 @@ open import lists.sequences
 
 open import logic.functoriality-existential-quantification
 
+open import metric-spaces.action-on-cauchy-approximations-short-maps-metric-spaces
 open import metric-spaces.apartness-located-metric-spaces
 open import metric-spaces.cauchy-approximations-metric-spaces
 open import metric-spaces.cauchy-sequences-metric-spaces

src/metric-spaces/action-on-cauchy-approximations-isometries-pseudometric-spaces.lagda.md

@@ -0,0 +1,143 @@
+# The action on Cauchy approximations of isometries between pseudometric spaces
+
+```agda
+module metric-spaces.action-on-cauchy-approximations-isometries-pseudometric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-positive-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
+
+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.action-on-cauchy-approximations-short-maps-pseudometric-spaces
+open import metric-spaces.cauchy-approximations-pseudometric-spaces
+open import metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces
+open import metric-spaces.isometries-pseudometric-spaces
+open import metric-spaces.pseudometric-spaces
+open import metric-spaces.short-functions-pseudometric-spaces
+```
+
+</details>
+
+## Idea
+
+[Isometries](metric-spaces.isometries-pseudometric-spaces.md) between
+[pseudometric spaces](metric-spaces.pseudometric-spaces.md) act on
+[Cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md)
+and induce an isometry between the
+[Cauchy pseudocompletions](metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces.md).
+
+## Definitions
+
+### 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)
+```
+
+## Properties
+
+### The action of isometries on Cauchy approximations is an isometry
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2')
+  (f : isometry-Pseudometric-Space A B)
+  where abstract
+
+  preserves-neighborhoods-map-cauchy-approximation-isometry-Pseudometric-Space :
+    (d : ℚ⁺) →
+    (x y : cauchy-approximation-Pseudometric-Space A) →
+    neighborhood-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space A)
+      ( d)
+      ( x)
+      ( y) →
+    neighborhood-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space B)
+      ( d)
+      ( map-cauchy-approximation-isometry-Pseudometric-Space A B f x)
+      ( map-cauchy-approximation-isometry-Pseudometric-Space A B f y)
+  preserves-neighborhoods-map-cauchy-approximation-isometry-Pseudometric-Space =
+    preserves-neighborhoods-map-cauchy-approximation-short-function-Pseudometric-Space
+      ( A)
+      ( B)
+      ( short-isometry-Pseudometric-Space A B f)
+
+  reflects-neighborhoods-map-cauchy-approximation-isometry-Pseudometric-Space :
+    (d : ℚ⁺) →
+    (x y : cauchy-approximation-Pseudometric-Space A) →
+    neighborhood-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space B)
+      ( d)
+      ( map-cauchy-approximation-isometry-Pseudometric-Space A B f x)
+      ( map-cauchy-approximation-isometry-Pseudometric-Space A B f y) →
+    neighborhood-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space A)
+      ( d)
+      ( x)
+      ( y)
+  reflects-neighborhoods-map-cauchy-approximation-isometry-Pseudometric-Space
+    d x y Nxy α β =
+    reflects-neighborhoods-map-isometry-Pseudometric-Space
+      ( A)
+      ( B)
+      ( f)
+      ( α +ℚ⁺ β +ℚ⁺ d)
+      ( map-cauchy-approximation-Pseudometric-Space A x α)
+      ( map-cauchy-approximation-Pseudometric-Space A y β)
+      ( Nxy α β)
+
+  is-isometry-map-cauchy-approximation-isometry-Pseudometric-Space :
+    is-isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space A)
+      ( cauchy-pseudocompletion-Pseudometric-Space B)
+      ( map-cauchy-approximation-isometry-Pseudometric-Space A B f)
+  is-isometry-map-cauchy-approximation-isometry-Pseudometric-Space d x y =
+    ( ( preserves-neighborhoods-map-cauchy-approximation-isometry-Pseudometric-Space
+        ( d)
+        ( x)
+        ( y)) ,
+      ( reflects-neighborhoods-map-cauchy-approximation-isometry-Pseudometric-Space
+        ( d)
+        ( x)
+        ( y)))
+
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2')
+  (f : isometry-Pseudometric-Space A B)
+  where
+
+  isometry-map-cauchy-approximation-isometry-Pseudometric-Space :
+    isometry-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space A)
+      ( cauchy-pseudocompletion-Pseudometric-Space B)
+  isometry-map-cauchy-approximation-isometry-Pseudometric-Space =
+    ( map-cauchy-approximation-isometry-Pseudometric-Space A B f ,
+      is-isometry-map-cauchy-approximation-isometry-Pseudometric-Space A B f)
+```

src/metric-spaces/action-on-cauchy-approximations-short-maps-metric-spaces.lagda.md

@@ -0,0 +1,91 @@
+# The action on Cauchy approximations of short maps between metric spaces
+
+```agda
+module metric-spaces.action-on-cauchy-approximations-short-maps-metric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-positive-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
+
+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.action-on-cauchy-approximations-short-maps-pseudometric-spaces
+open import metric-spaces.cauchy-approximations-metric-spaces
+open import metric-spaces.metric-spaces
+open import metric-spaces.short-functions-metric-spaces
+```
+
+</details>
+
+## Idea
+
+[metric spaces](metric-spaces.metric-spaces.md) act on
+[cauchy approximations](metric-spaces.cauchy-approximations-metric-spaces.md)
+and induce a short map between the
+[Cauchy pseudocompletions](metric-spaces.cauchy-pseudocompletion-of-metric-spaces.md).
+
+## Definitions
+
+### The action of short maps on 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-cauchy-approximation-short-function-Pseudometric-Space
+      ( pseudometric-Metric-Space A)
+      ( pseudometric-Metric-Space B)
+      ( f)
+```
+
+## Properties
+
+### Functoriality of the action of short maps
+
+```agda
+module _
+  {l1 l2 : Level}
+  (A : Metric-Space l1 l2)
+  where
+
+  htpy-id-map-short-function-cauchy-approximation-Metric-Space :
+    map-short-function-cauchy-approximation-Metric-Space
+      ( A)
+      ( A)
+      ( id-short-function-Metric-Space A) ＝
+    id
+  htpy-id-map-short-function-cauchy-approximation-Metric-Space = refl
+
+module _
+  {l1a l2a l1b l2b l1c l2c : Level}
+  (A : Metric-Space l1a l2a)
+  (B : Metric-Space l1b l2b)
+  (C : Metric-Space l1c l2c)
+  (g : short-function-Metric-Space B C)
+  (f : short-function-Metric-Space A B)
+  where
+
+  htpy-comp-map-short-function-cauchy-approximation-Metric-Space :
+    ( map-short-function-cauchy-approximation-Metric-Space B C g ∘
+      map-short-function-cauchy-approximation-Metric-Space A B f) ＝
+    ( map-short-function-cauchy-approximation-Metric-Space A C
+      ( comp-short-function-Metric-Space A B C g f))
+  htpy-comp-map-short-function-cauchy-approximation-Metric-Space = refl
+```

src/metric-spaces/action-on-cauchy-approximations-short-maps-pseudometric-spaces.lagda.md

@@ -0,0 +1,97 @@
+# The action on Cauchy approximations of short maps between pseudometric spaces
+
+```agda
+module metric-spaces.action-on-cauchy-approximations-short-maps-pseudometric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-positive-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
+
+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.cauchy-approximations-pseudometric-spaces
+open import metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces
+open import metric-spaces.isometries-pseudometric-spaces
+open import metric-spaces.pseudometric-spaces
+open import metric-spaces.short-functions-pseudometric-spaces
+```
+
+</details>
+
+## Idea
+
+[Short maps](metric-spaces.short-functions-pseudometric-spaces.md) between
+[pseudometric spaces](metric-spaces.pseudometric-spaces.md) act on
+[cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md)
+and induce a short map between the
+[Cauchy pseudocompletions](metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces.md).
+
+## Definitions
+
+### The action of short maps on Cauchy approximations
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2')
+  (f : short-function-Pseudometric-Space A B)
+  where
+
+  map-cauchy-approximation-short-function-Pseudometric-Space :
+    cauchy-approximation-Pseudometric-Space A →
+    cauchy-approximation-Pseudometric-Space B
+  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
+          ( A)
+          ( B)
+          ( f)
+          ( ε +ℚ⁺ δ)
+          ( u ε)
+          ( u δ)
+          ( H ε δ))
+```
+
+## Properties
+
+### The action of short maps on Cauchy approximations is short
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level}
+  (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2')
+  (f : short-function-Pseudometric-Space A B)
+  where
+
+  preserves-neighborhoods-map-cauchy-approximation-short-function-Pseudometric-Space :
+    is-short-function-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space A)
+      ( cauchy-pseudocompletion-Pseudometric-Space B)
+      ( map-cauchy-approximation-short-function-Pseudometric-Space A B f)
+  preserves-neighborhoods-map-cauchy-approximation-short-function-Pseudometric-Space
+    d x y Nxy α β =
+    is-short-map-short-function-Pseudometric-Space A B f
+      ( α +ℚ⁺ β +ℚ⁺ d)
+      ( map-cauchy-approximation-Pseudometric-Space A x α)
+      ( map-cauchy-approximation-Pseudometric-Space A y β)
+      ( Nxy α β)
+
+  short-map-cauchy-approximation-short-function-Pseudometric-Space :
+    short-function-Pseudometric-Space
+      ( cauchy-pseudocompletion-Pseudometric-Space A)
+      ( cauchy-pseudocompletion-Pseudometric-Space B)
+  short-map-cauchy-approximation-short-function-Pseudometric-Space =
+    ( map-cauchy-approximation-short-function-Pseudometric-Space A B f ,
+      preserves-neighborhoods-map-cauchy-approximation-short-function-Pseudometric-Space)
+```