From 59c39849965542115a1e97e916fd882abe7ce9cd Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 21 Oct 2025 22:40:12 +0200 Subject: [PATCH 01/28] lemmas metric spaces --- ...-sequences-complete-metric-spaces.lagda.md | 6 +- .../complete-metric-spaces.lagda.md | 60 ++++- ...uchy-approximations-metric-spaces.lagda.md | 50 ++++ ...uchy-approximations-metric-spaces.lagda.md | 19 ++ ...pproximations-pseudometric-spaces.lagda.md | 17 ++ src/metric-spaces/metric-spaces.lagda.md | 59 +++++ ...metric-spaces-and-short-functions.lagda.md | 8 + ...y-of-elements-pseudometric-spaces.lagda.md | 219 ++++++++++++------ 8 files changed, 356 insertions(+), 82 deletions(-) diff --git a/src/metric-spaces/cauchy-sequences-complete-metric-spaces.lagda.md b/src/metric-spaces/cauchy-sequences-complete-metric-spaces.lagda.md index 7a77f2ac4eb..3d822f77fc9 100644 --- a/src/metric-spaces/cauchy-sequences-complete-metric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-sequences-complete-metric-spaces.lagda.md @@ -90,8 +90,8 @@ module _ ( metric-space-Complete-Metric-Space M) ( x) has-limit-cauchy-sequence-Complete-Metric-Space = - limit-cauchy-sequence-Complete-Metric-Space , - is-limit-limit-cauchy-sequence-Complete-Metric-Space + ( limit-cauchy-sequence-Complete-Metric-Space , + is-limit-limit-cauchy-sequence-Complete-Metric-Space) ``` ### If every Cauchy sequence has a limit in a metric space, the metric space is complete @@ -123,5 +123,5 @@ module _ complete-metric-space-cauchy-sequences-have-limits-Metric-Space : Complete-Metric-Space l1 l2 complete-metric-space-cauchy-sequences-have-limits-Metric-Space = - M , is-complete-metric-space-cauchy-sequences-have-limits-Metric-Space + ( M , is-complete-metric-space-cauchy-sequences-have-limits-Metric-Space) ``` diff --git a/src/metric-spaces/complete-metric-spaces.lagda.md b/src/metric-spaces/complete-metric-spaces.lagda.md index 6b10db7b421..8f894926c8c 100644 --- a/src/metric-spaces/complete-metric-spaces.lagda.md +++ b/src/metric-spaces/complete-metric-spaces.lagda.md @@ -12,9 +12,12 @@ open import elementary-number-theory.positive-rational-numbers open import foundation.binary-relations open import foundation.dependent-pair-types open import foundation.equivalences +open import foundation.function-types +open import foundation.homotopies open import foundation.identity-types open import foundation.propositions open import foundation.retractions +open import foundation.retracts-of-types open import foundation.sections open import foundation.subtypes open import foundation.universe-levels @@ -23,6 +26,7 @@ open import metric-spaces.cauchy-approximations-metric-spaces open import metric-spaces.convergent-cauchy-approximations-metric-spaces open import metric-spaces.limits-of-cauchy-approximations-metric-spaces open import metric-spaces.metric-spaces +open import metric-spaces.pseudometric-spaces ``` @@ -80,6 +84,10 @@ module _ metric-space-Complete-Metric-Space : Metric-Space l1 l2 metric-space-Complete-Metric-Space = pr1 A + pseudometric-space-Complete-Metric-Space : Pseudometric-Space l1 l2 + pseudometric-space-Complete-Metric-Space = + pseudometric-Metric-Space metric-space-Complete-Metric-Space + type-Complete-Metric-Space : UU l1 type-Complete-Metric-Space = type-Metric-Space metric-space-Complete-Metric-Space @@ -122,13 +130,13 @@ module _ ( metric-space-Complete-Metric-Space A)) ( refl) - is-retraction-convergent-cauchy-approximation-Metric-Space : + is-retraction-convergent-cauchy-approximation-Complete-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-retraction-convergent-cauchy-approximation-Complete-Metric-Space u = refl is-equiv-convergent-cauchy-approximation-Complete-Metric-Space : is-equiv convergent-cauchy-approximation-Complete-Metric-Space @@ -141,7 +149,7 @@ module _ ( inclusion-subtype ( is-convergent-prop-cauchy-approximation-Metric-Space ( metric-space-Complete-Metric-Space A))) , - ( is-retraction-convergent-cauchy-approximation-Metric-Space) + ( is-retraction-convergent-cauchy-approximation-Complete-Metric-Space) ``` ### The limit of a Cauchy approximation in a complete metric space @@ -172,6 +180,52 @@ module _ ( convergent-cauchy-approximation-Complete-Metric-Space A u) ``` +### Any complete metric space is a retract of its type of Cauchy approximations + +```agda +module _ + {l1 l2 : Level} (A : Complete-Metric-Space l1 l2) + where + + abstract + is-retraction-limit-cauchy-approximation-Complete-Metric-Space : + ( limit-cauchy-approximation-Complete-Metric-Space A ∘ + const-cauchy-approximation-Metric-Space + ( metric-space-Complete-Metric-Space A)) ~ + ( id) + is-retraction-limit-cauchy-approximation-Complete-Metric-Space x = + all-eq-is-limit-cauchy-approximation-Metric-Space + ( metric-space-Complete-Metric-Space A) + ( const-cauchy-approximation-Metric-Space + ( metric-space-Complete-Metric-Space A) + ( x)) + ( limit-cauchy-approximation-Complete-Metric-Space + ( A) + ( const-cauchy-approximation-Metric-Space + ( metric-space-Complete-Metric-Space A) + ( x))) + ( x) + ( is-limit-limit-cauchy-approximation-Complete-Metric-Space + ( A) + ( const-cauchy-approximation-Metric-Space + ( metric-space-Complete-Metric-Space A) + ( x))) + ( is-limit-const-cauchy-approximation-Metric-Space + ( metric-space-Complete-Metric-Space A) + ( x)) + + retract-limit-cauchy-approximation-Complete-Metric-Space : + retract + ( cauchy-approximation-Metric-Space + ( metric-space-Complete-Metric-Space A)) + ( type-Complete-Metric-Space A) + retract-limit-cauchy-approximation-Complete-Metric-Space = + ( ( const-cauchy-approximation-Metric-Space + ( metric-space-Complete-Metric-Space A)) , + ( limit-cauchy-approximation-Complete-Metric-Space A) , + ( is-retraction-limit-cauchy-approximation-Complete-Metric-Space)) +``` + ### Saturation of the limit ```agda diff --git a/src/metric-spaces/convergent-cauchy-approximations-metric-spaces.lagda.md b/src/metric-spaces/convergent-cauchy-approximations-metric-spaces.lagda.md index 53b0dbe5b78..5641ecc9fbb 100644 --- a/src/metric-spaces/convergent-cauchy-approximations-metric-spaces.lagda.md +++ b/src/metric-spaces/convergent-cauchy-approximations-metric-spaces.lagda.md @@ -12,8 +12,10 @@ open import elementary-number-theory.positive-rational-numbers 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.retracts-of-types open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels @@ -141,3 +143,51 @@ module _ ( limit-convergent-cauchy-approximation-Metric-Space) is-limit-limit-convergent-cauchy-approximation-Metric-Space = pr2 (pr2 f) ``` + +## Properties + +### Constant Cauchy approximations are convergent + +```agda +module _ + {l1 l2 : Level} (A : Metric-Space l1 l2) + (x : type-Metric-Space A) + where + + is-convergent-const-cauchy-approximation-Metric-Space : + is-convergent-cauchy-approximation-Metric-Space + ( A) + ( const-cauchy-approximation-Metric-Space A x) + is-convergent-const-cauchy-approximation-Metric-Space = + ( x , is-limit-const-cauchy-approximation-Metric-Space A x) + + convergent-const-cauchy-approximation-Metric-Space : + convergent-cauchy-approximation-Metric-Space A + convergent-const-cauchy-approximation-Metric-Space = + ( const-cauchy-approximation-Metric-Space A x , + is-convergent-const-cauchy-approximation-Metric-Space) +``` + +### Any metric space is a retract of its type of convergent Cauchy approximations + +```agda +module _ + {l1 l2 : Level} (A : Metric-Space l1 l2) + where + + abstract + is-retraction-convergent-cauchy-approximation-Metric-Space : + ( limit-convergent-cauchy-approximation-Metric-Space A ∘ + convergent-const-cauchy-approximation-Metric-Space A) ~ + ( id) + is-retraction-convergent-cauchy-approximation-Metric-Space x = refl + + retract-convergent-cauchy-approximation-Metric-Space : + retract + ( convergent-cauchy-approximation-Metric-Space A) + ( type-Metric-Space A) + retract-convergent-cauchy-approximation-Metric-Space = + ( convergent-const-cauchy-approximation-Metric-Space A , + limit-convergent-cauchy-approximation-Metric-Space A , + is-retraction-convergent-cauchy-approximation-Metric-Space) +``` diff --git a/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces.lagda.md b/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces.lagda.md index e1ecfba92e0..4ba16ab30ae 100644 --- a/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces.lagda.md +++ b/src/metric-spaces/limits-of-cauchy-approximations-metric-spaces.lagda.md @@ -123,6 +123,25 @@ module _ ( all-sim-is-limit-cauchy-approximation-Metric-Space lim-x lim-y) ``` +### The value of a constant Cauchy approximation is its limit + +```agda +module _ + {l1 l2 : Level} (A : Metric-Space l1 l2) + (x : type-Metric-Space A) + where + + is-limit-const-cauchy-approximation-Metric-Space : + is-limit-cauchy-approximation-Metric-Space + ( A) + ( const-cauchy-approximation-Metric-Space A x) + ( x) + is-limit-const-cauchy-approximation-Metric-Space = + is-limit-const-cauchy-approximation-Pseudometric-Space + ( pseudometric-Metric-Space A) + ( x) +``` + ## See also - [Convergent cauchy approximations](metric-spaces.convergent-cauchy-approximations-metric-spaces.md) diff --git a/src/metric-spaces/limits-of-cauchy-approximations-pseudometric-spaces.lagda.md b/src/metric-spaces/limits-of-cauchy-approximations-pseudometric-spaces.lagda.md index 3e6705b7764..6226f7b2c90 100644 --- a/src/metric-spaces/limits-of-cauchy-approximations-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/limits-of-cauchy-approximations-pseudometric-spaces.lagda.md @@ -145,6 +145,23 @@ module _ ( Nxy) ``` +### The value of a constant Cauchy approximation is its limit + +```agda +module _ + {l1 l2 : Level} (A : Pseudometric-Space l1 l2) + (x : type-Pseudometric-Space A) + where + + is-limit-const-cauchy-approximation-Pseudometric-Space : + is-limit-cauchy-approximation-Pseudometric-Space + ( A) + ( const-cauchy-approximation-Pseudometric-Space A x) + ( x) + is-limit-const-cauchy-approximation-Pseudometric-Space ε δ = + refl-neighborhood-Pseudometric-Space A _ x +``` + ## References Our definition of limit of Cauchy approximation follows Definition 11.2.10 of diff --git a/src/metric-spaces/metric-spaces.lagda.md b/src/metric-spaces/metric-spaces.lagda.md index c5072037652..25fbe2e9822 100644 --- a/src/metric-spaces/metric-spaces.lagda.md +++ b/src/metric-spaces/metric-spaces.lagda.md @@ -21,6 +21,7 @@ open import foundation.function-types open import foundation.functoriality-dependent-pair-types open import foundation.identity-types open import foundation.propositions +open import foundation.reflecting-maps-equivalence-relations open import foundation.sets open import foundation.subtypes open import foundation.transport-along-identifications @@ -34,6 +35,7 @@ open import metric-spaces.pseudometric-spaces open import metric-spaces.rational-neighborhood-relations open import metric-spaces.reflexive-rational-neighborhood-relations open import metric-spaces.saturated-rational-neighborhood-relations +open import metric-spaces.short-functions-pseudometric-spaces open import metric-spaces.similarity-of-elements-pseudometric-spaces open import metric-spaces.symmetric-rational-neighborhood-relations open import metric-spaces.triangular-rational-neighborhood-relations @@ -340,6 +342,63 @@ module _ map-inv-equiv (equiv-sim-eq-Metric-Space x y) ``` +### Short maps from a pseudometric space to a metric space reflect similarity + +```agda +module _ + {l1 l2 l1' l2' : Level} + (A : Pseudometric-Space l1 l2) + (B : Metric-Space l1' l2') + (f : short-function-Pseudometric-Space A (pseudometric-Metric-Space B)) + where + + abstract + reflects-sim-map-short-function-metric-space-Pseudometric-Space : + {x y : type-Pseudometric-Space A} → + sim-Pseudometric-Space A x y → + map-short-function-Pseudometric-Space + ( A) + ( pseudometric-Metric-Space B) + ( f) + ( x) ＝ + map-short-function-Pseudometric-Space + ( A) + ( pseudometric-Metric-Space B) + ( f) + ( y) + reflects-sim-map-short-function-metric-space-Pseudometric-Space + {x} {y} x~y = + eq-sim-Metric-Space B + ( map-short-function-Pseudometric-Space + ( A) + ( pseudometric-Metric-Space B) + ( f) + ( x)) + ( map-short-function-Pseudometric-Space + ( A) + ( pseudometric-Metric-Space B) + ( f) + ( y)) + ( preserves-sim-map-short-function-Pseudometric-Space + ( A) + ( pseudometric-Metric-Space B) + ( f) + ( x) + ( y) + ( x~y)) + + reflecting-map-short-function-metric-space-Pseudometric-Space : + reflecting-map-equivalence-relation + ( equivalence-relation-sim-Pseudometric-Space A) + ( type-Metric-Space B) + reflecting-map-short-function-metric-space-Pseudometric-Space = + ( ( map-short-function-Pseudometric-Space + ( A) + ( pseudometric-Metric-Space B) + ( f)) , + ( reflects-sim-map-short-function-metric-space-Pseudometric-Space)) +``` + ## See also - Metric spaces that _are_ defined by a distance function are defined in diff --git a/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md b/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md index 564a2b9385e..6d3251395db 100644 --- a/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md +++ b/src/metric-spaces/precategory-of-metric-spaces-and-short-functions.lagda.md @@ -232,6 +232,7 @@ module _ {l1 l2 : Level} (A B : Metric-Space l1 l2) where + equiv-isometric-equiv-iso-short-function-Metric-Space' : iso-Precategory precategory-short-function-Metric-Space A B ≃ isometric-equiv-Metric-Space' A B @@ -239,6 +240,13 @@ module _ ( equiv-tot ( equiv-is-isometric-equiv-is-iso-short-function-Metric-Space A B)) ∘e ( associative-Σ) + + map-equiv-isometric-equiv-iso-short-function-Metric-Space' : + iso-Precategory precategory-short-function-Metric-Space A B → + isometric-equiv-Metric-Space' A B + map-equiv-isometric-equiv-iso-short-function-Metric-Space' = + map-equiv + ( equiv-isometric-equiv-iso-short-function-Metric-Space') ``` ## See also diff --git a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md index 289635cb192..763b86217f1 100644 --- a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md @@ -24,6 +24,7 @@ open import foundation.universe-levels open import metric-spaces.pseudometric-spaces open import metric-spaces.rational-neighborhood-relations +open import metric-spaces.short-functions-pseudometric-spaces ``` @@ -170,54 +171,98 @@ module _ {l1 l2 : Level} (A : Pseudometric-Space l1 l2) where - preserves-neighborhood-sim-Pseudometric-Space : - { x y : type-Pseudometric-Space A} → - ( sim-Pseudometric-Space A x y) → - ( d : ℚ⁺) (z : type-Pseudometric-Space A) → - neighborhood-Pseudometric-Space A d x z → - neighborhood-Pseudometric-Space A d y z - preserves-neighborhood-sim-Pseudometric-Space {x} {y} x≍y d z Nxz = - saturated-neighborhood-Pseudometric-Space - ( A) - ( d) - ( y) - ( z) - ( λ δ → - tr - ( is-upper-bound-dist-Pseudometric-Space A y z) - ( commutative-add-ℚ⁺ δ d) - ( triangular-neighborhood-Pseudometric-Space - ( A) - ( y) - ( x) - ( z) - ( δ) - ( d) - ( Nxz) - ( symmetric-neighborhood-Pseudometric-Space + abstract + preserves-neighborhood-left-sim-Pseudometric-Space : + { x y : type-Pseudometric-Space A} → + ( sim-Pseudometric-Space A x y) → + ( d : ℚ⁺) (z : type-Pseudometric-Space A) → + neighborhood-Pseudometric-Space A d x z → + neighborhood-Pseudometric-Space A d y z + preserves-neighborhood-left-sim-Pseudometric-Space {x} {y} x≍y d z Nxz = + saturated-neighborhood-Pseudometric-Space + ( A) + ( d) + ( y) + ( z) + ( λ δ → + tr + ( is-upper-bound-dist-Pseudometric-Space A y z) + ( commutative-add-ℚ⁺ δ d) + ( triangular-neighborhood-Pseudometric-Space ( A) - ( δ) - ( x) ( y) - ( x≍y δ)))) - - iff-same-neighbors-sim-Pseudometric-Space : - { x y : type-Pseudometric-Space A} → - ( sim-Pseudometric-Space A x y) ↔ - ( (d : ℚ⁺) (z : type-Pseudometric-Space A) → - neighborhood-Pseudometric-Space A d x z ↔ - neighborhood-Pseudometric-Space A d y z) - iff-same-neighbors-sim-Pseudometric-Space = - ( λ x≍y d z → - ( preserves-neighborhood-sim-Pseudometric-Space x≍y d z) , - ( preserves-neighborhood-sim-Pseudometric-Space - ( inv-sim-Pseudometric-Space A x≍y) + ( x) + ( z) + ( δ) + ( d) + ( Nxz) + ( symmetric-neighborhood-Pseudometric-Space + ( A) + ( δ) + ( x) + ( y) + ( x≍y δ)))) + + preserves-neighborhood-right-sim-Pseudometric-Space : + { x y : type-Pseudometric-Space A} → + ( sim-Pseudometric-Space A x y) → + ( d : ℚ⁺) (z : type-Pseudometric-Space A) → + neighborhood-Pseudometric-Space A d z x → + neighborhood-Pseudometric-Space A d z y + preserves-neighborhood-right-sim-Pseudometric-Space {x} {y} x≍y d z Nzx = + symmetric-neighborhood-Pseudometric-Space A d y z + ( preserves-neighborhood-left-sim-Pseudometric-Space x≍y d z + ( symmetric-neighborhood-Pseudometric-Space A d z x Nzx)) + + preserves-neighborhood-sim-Pseudometric-Space : + {x x' y y' : type-Pseudometric-Space A} → + sim-Pseudometric-Space A x x' → + sim-Pseudometric-Space A y y' → + (d : ℚ⁺) → + neighborhood-Pseudometric-Space A d x y → + neighborhood-Pseudometric-Space A d x' y' + preserves-neighborhood-sim-Pseudometric-Space + {x} {x'} {y} {y'} x~x' y~y' d Nxy = + preserves-neighborhood-left-sim-Pseudometric-Space + ( x~x') ( d) - ( z))) , - ( λ same-neighbors d → - backward-implication - ( same-neighbors d _) - ( refl-sim-Pseudometric-Space A _ d)) + ( y') + ( preserves-neighborhood-right-sim-Pseudometric-Space + ( y~y') + ( d) + ( x) + ( Nxy)) + + reflects-neighborhood-sim-Pseudometric-Space : + {x x' y y' : type-Pseudometric-Space A} → + sim-Pseudometric-Space A x x' → + sim-Pseudometric-Space A y y' → + (d : ℚ⁺) → + neighborhood-Pseudometric-Space A d x' y' → + neighborhood-Pseudometric-Space A d x y + reflects-neighborhood-sim-Pseudometric-Space + {x} {x'} {y} {y'} x~x' y~y' = + preserves-neighborhood-sim-Pseudometric-Space + ( inv-sim-Pseudometric-Space A x~x') + ( inv-sim-Pseudometric-Space A y~y') + + iff-same-neighbors-sim-Pseudometric-Space : + { x y : type-Pseudometric-Space A} → + ( sim-Pseudometric-Space A x y) ↔ + ( (d : ℚ⁺) (z : type-Pseudometric-Space A) → + neighborhood-Pseudometric-Space A d x z ↔ + neighborhood-Pseudometric-Space A d y z) + iff-same-neighbors-sim-Pseudometric-Space = + ( λ x≍y d z → + ( preserves-neighborhood-left-sim-Pseudometric-Space x≍y d z) , + ( preserves-neighborhood-left-sim-Pseudometric-Space + ( inv-sim-Pseudometric-Space A x≍y) + ( d) + ( z))) , + ( λ same-neighbors d → + backward-implication + ( same-neighbors d _) + ( refl-sim-Pseudometric-Space A _ d)) ``` ### Similar elements are elements similar w.r.t the underlying rational neighborhood relation @@ -227,35 +272,57 @@ module _ {l1 l2 : Level} (A : Pseudometric-Space l1 l2) where - iff-same-neighbors-same-neighborhood-Pseudometric-Space : - {x y : type-Pseudometric-Space A} → - ( (d : ℚ⁺) (z : type-Pseudometric-Space A) → - neighborhood-Pseudometric-Space A d x z ↔ - neighborhood-Pseudometric-Space A d y z) ↔ - ( sim-Rational-Neighborhood-Relation - ( neighborhood-prop-Pseudometric-Space A) - ( x) - ( y)) - iff-same-neighbors-same-neighborhood-Pseudometric-Space = - ( λ H d z → - ( H d z) , - ( inv-neighborhood-Pseudometric-Space A ∘ - pr1 (H d z) ∘ - inv-neighborhood-Pseudometric-Space A) , - ( inv-neighborhood-Pseudometric-Space A ∘ - pr2 (H d z) ∘ - inv-neighborhood-Pseudometric-Space A)) , - ( iff-left-neighbor-sim-Rational-Neighborhood-Relation - ( neighborhood-prop-Pseudometric-Space A)) - - iff-same-neighborhood-sim-Pseudometric-Space : - { x y : type-Pseudometric-Space A} → - ( sim-Pseudometric-Space A x y) ↔ - ( sim-Rational-Neighborhood-Relation - ( neighborhood-prop-Pseudometric-Space A) - ( x) - ( y)) - iff-same-neighborhood-sim-Pseudometric-Space = - ( iff-same-neighbors-same-neighborhood-Pseudometric-Space) ∘iff - ( iff-same-neighbors-sim-Pseudometric-Space A) + abstract + iff-same-neighbors-same-neighborhood-Pseudometric-Space : + {x y : type-Pseudometric-Space A} → + ( (d : ℚ⁺) (z : type-Pseudometric-Space A) → + neighborhood-Pseudometric-Space A d x z ↔ + neighborhood-Pseudometric-Space A d y z) ↔ + ( sim-Rational-Neighborhood-Relation + ( neighborhood-prop-Pseudometric-Space A) + ( x) + ( y)) + iff-same-neighbors-same-neighborhood-Pseudometric-Space = + ( λ H d z → + ( H d z) , + ( inv-neighborhood-Pseudometric-Space A ∘ + pr1 (H d z) ∘ + inv-neighborhood-Pseudometric-Space A) , + ( inv-neighborhood-Pseudometric-Space A ∘ + pr2 (H d z) ∘ + inv-neighborhood-Pseudometric-Space A)) , + ( iff-left-neighbor-sim-Rational-Neighborhood-Relation + ( neighborhood-prop-Pseudometric-Space A)) + + iff-same-neighborhood-sim-Pseudometric-Space : + { x y : type-Pseudometric-Space A} → + ( sim-Pseudometric-Space A x y) ↔ + ( sim-Rational-Neighborhood-Relation + ( neighborhood-prop-Pseudometric-Space A) + ( x) + ( y)) + iff-same-neighborhood-sim-Pseudometric-Space = + ( iff-same-neighbors-same-neighborhood-Pseudometric-Space) ∘iff + ( iff-same-neighbors-sim-Pseudometric-Space A) +``` + +### Short maps between pseudometric spaces preserves similarity + +```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 + + abstract + preserves-sim-map-short-function-Pseudometric-Space : + ( x y : type-Pseudometric-Space A) → + ( sim-Pseudometric-Space A x y) → + ( sim-Pseudometric-Space B + ( map-short-function-Pseudometric-Space A B f x) + ( map-short-function-Pseudometric-Space A B f y)) + preserves-sim-map-short-function-Pseudometric-Space x y x~y d = + is-short-map-short-function-Pseudometric-Space A B f d x y (x~y d) ``` From 6cadc6bee17b53dc73a0eaaea5968f6742985130 Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 21 Oct 2025 22:43:48 +0200 Subject: [PATCH 02/28] typo --- .../similarity-of-elements-pseudometric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md index 763b86217f1..024bfbaa3ad 100644 --- a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md @@ -306,7 +306,7 @@ module _ ( iff-same-neighbors-sim-Pseudometric-Space A) ``` -### Short maps between pseudometric spaces preserves similarity +### Short maps between pseudometric spaces preserve similarity ```agda module _ From 806dcdb82e5f3cfb452e8d509ff300fce7347379 Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 21 Oct 2025 22:59:52 +0200 Subject: [PATCH 03/28] pseudometric-completions --- src/metric-spaces.lagda.md | 2 + ...etric-completion-of-metric-spaces.lagda.md | 437 ++++++++++ ...completion-of-pseudometric-spaces.lagda.md | 766 ++++++++++++++++++ 3 files changed, 1205 insertions(+) create mode 100644 src/metric-spaces/pseudometric-completion-of-metric-spaces.lagda.md create mode 100644 src/metric-spaces/pseudometric-completion-of-pseudometric-spaces.lagda.md diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md index c501d3c56d3..00f3db27988 100644 --- a/src/metric-spaces.lagda.md +++ b/src/metric-spaces.lagda.md @@ -125,6 +125,8 @@ open import metric-spaces.precategory-of-metric-spaces-and-functions public open import metric-spaces.precategory-of-metric-spaces-and-isometries public open import metric-spaces.precategory-of-metric-spaces-and-short-functions public open import metric-spaces.preimages-rational-neighborhood-relations public +open import metric-spaces.pseudometric-completion-of-metric-spaces public +open import metric-spaces.pseudometric-completion-of-pseudometric-spaces public open import metric-spaces.pseudometric-spaces public open import metric-spaces.rational-approximations-of-zero public open import metric-spaces.rational-cauchy-approximations public diff --git a/src/metric-spaces/pseudometric-completion-of-metric-spaces.lagda.md b/src/metric-spaces/pseudometric-completion-of-metric-spaces.lagda.md new file mode 100644 index 00000000000..57328439f22 --- /dev/null +++ b/src/metric-spaces/pseudometric-completion-of-metric-spaces.lagda.md @@ -0,0 +1,437 @@ +# The pseudometric completion of a metric space + +```agda +module metric-spaces.pseudometric-completion-of-metric-spaces where +``` + +
Imports + +```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.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 +open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces +open import metric-spaces.metric-spaces +open import metric-spaces.pseudometric-completion-of-pseudometric-spaces +open import metric-spaces.pseudometric-spaces +open import metric-spaces.rational-neighborhood-relations +open import metric-spaces.short-functions-pseudometric-spaces +open import metric-spaces.similarity-of-elements-pseudometric-spaces +``` + +
+ +## Idea + +The +{{#concept "pseudometric completion" Disambiguation="of a metric space" Agda=pseudometric-completion-Metric-Space}} +of a [metric space](metric-spaces.metric-spaces.md) `M` is the +[pseudometric completion](metric-spaces.pseudometric-completion-of-pseudometric-spaces.md) +of its underlying [pseudometric space](metric-spaces.pseudometric-spaces.md): +the pseudometric space of +[Cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md) +in `M` where two Cauchy approximations `x` and `y` are in a +[`d`-neighborhood](metric-spaces.rational-neighborhood-relations.md) of one +another if for all `δ ε : ℚ⁺`, `x δ` and `y ε` are in a +`(δ + ε + d)`-neighborhood of one another in `M`. + +Any Cauchy approximation in the pseudometric completion has a +[limit](metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces.md). +If the metric space is [complete](metric-spaces.complete-metric-spaces.md), it +is a [retract](foundation.retracts-of-types.md) of its pseudometric completion. + +## Definition + +### The pseudometric completion of a metric space + +```agda +module _ + {l1 l2 : Level} (M : Metric-Space l1 l2) + where + + pseudometric-completion-Metric-Space : + Pseudometric-Space (l1 ⊔ l2) l2 + pseudometric-completion-Metric-Space = + pseudometric-completion-Pseudometric-Space + ( pseudometric-Metric-Space M) +``` + +### The pseudometric completion neighborhood relation on the type of Cauchy approximations in a pseudometric space + +```agda +module _ + {l1 l2 : Level} (M : Metric-Space l1 l2) + where + + neighborhood-prop-pseudometric-completion-Metric-Space : + Rational-Neighborhood-Relation l2 + (cauchy-approximation-Metric-Space M) + neighborhood-prop-pseudometric-completion-Metric-Space = + neighborhood-prop-pseudometric-completion-Pseudometric-Space + ( pseudometric-Metric-Space M) + + neighborhood-pseudometric-completion-Metric-Space : + ℚ⁺ → Relation l2 (cauchy-approximation-Metric-Space M) + neighborhood-pseudometric-completion-Metric-Space = + neighborhood-pseudometric-completion-Pseudometric-Space + ( pseudometric-Metric-Space M) +``` + +## Properties + +### The neighborhood relation is reflexive + +```agda +module _ + {l1 l2 : Level} (M : Metric-Space l1 l2) + where + + abstract + is-reflexive-neighborhood-pseudometric-completion-Metric-Space : + (d : ℚ⁺) (x : cauchy-approximation-Metric-Space M) → + neighborhood-pseudometric-completion-Metric-Space M d x x + is-reflexive-neighborhood-pseudometric-completion-Metric-Space = + is-reflexive-neighborhood-pseudometric-completion-Pseudometric-Space + ( pseudometric-Metric-Space M) +``` + +### The neighborhood relation is symmetric + +```agda +module _ + {l1 l2 : Level} (M : Metric-Space l1 l2) + where + + abstract + is-symmetric-neighborhood-pseudometric-completion-Metric-Space : + (d : ℚ⁺) (x y : cauchy-approximation-Metric-Space M) → + neighborhood-pseudometric-completion-Metric-Space M d x y → + neighborhood-pseudometric-completion-Metric-Space M d y x + is-symmetric-neighborhood-pseudometric-completion-Metric-Space = + is-symmetric-neighborhood-pseudometric-completion-Pseudometric-Space + ( pseudometric-Metric-Space M) +``` + +### The neighborhood relation is triangular + +```agda +module _ + {l1 l2 : Level} (M : Metric-Space l1 l2) + where + + abstract + is-triangular-neighborhood-pseudometric-completion-Metric-Space : + (x y z : cauchy-approximation-Metric-Space M) → + (dxy dyz : ℚ⁺) → + neighborhood-pseudometric-completion-Metric-Space M dyz y z → + neighborhood-pseudometric-completion-Metric-Space M dxy x y → + neighborhood-pseudometric-completion-Metric-Space + ( M) + ( dxy +ℚ⁺ dyz) + ( x) + ( z) + is-triangular-neighborhood-pseudometric-completion-Metric-Space = + is-triangular-neighborhood-pseudometric-completion-Pseudometric-Space + ( pseudometric-Metric-Space M) +``` + +### The neighborhood relation is saturated + +```agda +module _ + {l1 l2 : Level} (M : Metric-Space l1 l2) + where + + abstract + is-saturated-neighborhood-pseudometric-completion-Metric-Space : + ( ε : ℚ⁺) (x y : cauchy-approximation-Metric-Space M) → + ( (δ : ℚ⁺) → + neighborhood-pseudometric-completion-Metric-Space + ( M) + ( ε +ℚ⁺ δ) + ( x) + ( y)) → + neighborhood-pseudometric-completion-Metric-Space M ε x y + is-saturated-neighborhood-pseudometric-completion-Metric-Space = + is-saturated-neighborhood-pseudometric-completion-Pseudometric-Space + ( pseudometric-Metric-Space M) +``` + +### The isometry from a metric space to its pseudometric completion + +```agda +module _ + {l1 l2 : Level} (M : Metric-Space l1 l2) + where + + isometry-pseudometric-completion-Metric-Space : + isometry-Pseudometric-Space + ( pseudometric-Metric-Space M) + ( pseudometric-completion-Metric-Space M) + isometry-pseudometric-completion-Metric-Space = + isometry-pseudometric-completion-Pseudometric-Space + ( pseudometric-Metric-Space M) + + map-pseudometric-completion-Metric-Space : + type-Metric-Space M → cauchy-approximation-Metric-Space M + map-pseudometric-completion-Metric-Space = + map-isometry-Pseudometric-Space + ( pseudometric-Metric-Space M) + ( pseudometric-completion-Metric-Space M) + ( isometry-pseudometric-completion-Metric-Space) + + abstract + is-isometry-map-pseudometric-completion-Metric-Space : + is-isometry-Pseudometric-Space + ( pseudometric-Metric-Space M) + ( pseudometric-completion-Metric-Space M) + ( map-pseudometric-completion-Metric-Space) + is-isometry-map-pseudometric-completion-Metric-Space = + is-isometry-map-isometry-Pseudometric-Space + ( pseudometric-Metric-Space M) + ( pseudometric-completion-Metric-Space M) + ( isometry-pseudometric-completion-Metric-Space) +``` + +### Convergent Cauchy approximations are similar to constant Cauchy approximations in the pseudometric completion + +```agda +module _ + {l1 l2 : Level} (M : Metric-Space l1 l2) + (u : cauchy-approximation-Metric-Space M) + (x : type-Metric-Space M) + where + + abstract + sim-const-is-limit-cauchy-approximation-Metric-Space : + is-limit-cauchy-approximation-Metric-Space M u x → + sim-Pseudometric-Space + ( pseudometric-completion-Metric-Space M) + ( u) + ( const-cauchy-approximation-Metric-Space M x) + sim-const-is-limit-cauchy-approximation-Metric-Space H d α β = + monotonic-neighborhood-Metric-Space + ( M) + ( map-cauchy-approximation-Metric-Space M u α) + ( x) + ( α +ℚ⁺ β) + ( α +ℚ⁺ β +ℚ⁺ d) + ( le-left-add-ℚ⁺ (α +ℚ⁺ β) d) + ( H α β) + + is-limit-sim-const-cauchy-approximation-Metric-Space : + sim-Pseudometric-Space + ( pseudometric-completion-Metric-Space M) + ( u) + ( const-cauchy-approximation-Metric-Space M x) → + is-limit-cauchy-approximation-Metric-Space M u x + is-limit-sim-const-cauchy-approximation-Metric-Space H α β = + saturated-neighborhood-Metric-Space + ( M) + ( α +ℚ⁺ β) + ( map-cauchy-approximation-Metric-Space M u α) + ( x) + ( λ d → H d α β) +``` + +### Any Cauchy approximation in the pseudometric completion of a metric space has a limit + +```agda +module _ + { l1 l2 : Level} (M : Metric-Space l1 l2) + ( U : + cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Metric-Space M)) + where + + has-limit-cauchy-approximation-pseudometric-completion-Metric-Space : + Σ ( cauchy-approximation-Metric-Space M) + ( is-limit-cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Metric-Space M) + ( U)) + has-limit-cauchy-approximation-pseudometric-completion-Metric-Space = + has-limit-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( pseudometric-Metric-Space M) + ( U) + + lim-cauchy-approximation-pseudometric-completion-Metric-Space : + cauchy-approximation-Metric-Space M + lim-cauchy-approximation-pseudometric-completion-Metric-Space = + pr1 has-limit-cauchy-approximation-pseudometric-completion-Metric-Space + + is-limit-lim-cauchy-approximation-pseudometric-completion-Metric-Space : + is-limit-cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Metric-Space M) + ( U) + ( lim-cauchy-approximation-pseudometric-completion-Metric-Space) + is-limit-lim-cauchy-approximation-pseudometric-completion-Metric-Space = + pr2 has-limit-cauchy-approximation-pseudometric-completion-Metric-Space +``` + +### The isometry from a Cauchy approximation in the pseudometric completion to its limit + +```agda +module _ + {l1 l2 : Level} (M : Metric-Space l1 l2) + where + + isometry-lim-cauchy-approximation-pseudometric-completion-Metric-Space : + isometry-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space + ( pseudometric-completion-Metric-Space M)) + ( pseudometric-completion-Metric-Space M) + isometry-lim-cauchy-approximation-pseudometric-completion-Metric-Space = + isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( pseudometric-Metric-Space M) +``` + +### Any complete metric space is a short retract of its pseudometric completion + +```agda +module _ + {l1 l2 : Level} (M : Metric-Space l1 l2) + (is-complete-M : is-complete-Metric-Space M) + where + + map-lim-pseudometric-completion-is-complete-Metric-Space : + type-function-Pseudometric-Space + ( pseudometric-completion-Metric-Space M) + ( pseudometric-Metric-Space M) + map-lim-pseudometric-completion-is-complete-Metric-Space = + limit-cauchy-approximation-Complete-Metric-Space + ( M , is-complete-M) + + is-limit-map-lim-pseudometric-completion-is-complete-Metric-Space : + (u : cauchy-approximation-Metric-Space M) → + is-limit-cauchy-approximation-Metric-Space + ( M) + ( u) + ( map-lim-pseudometric-completion-is-complete-Metric-Space u) + is-limit-map-lim-pseudometric-completion-is-complete-Metric-Space = + is-limit-limit-cauchy-approximation-Complete-Metric-Space + ( M , is-complete-M) + + sim-const-map-lim-pseudometric-completion-is-complete-Metric-Space : + (u : cauchy-approximation-Metric-Space M) → + sim-Pseudometric-Space + ( pseudometric-completion-Metric-Space M) + ( u) + ( const-cauchy-approximation-Metric-Space + ( M) + ( map-lim-pseudometric-completion-is-complete-Metric-Space u)) + sim-const-map-lim-pseudometric-completion-is-complete-Metric-Space u = + sim-const-is-limit-cauchy-approximation-Metric-Space + ( M) + ( u) + ( map-lim-pseudometric-completion-is-complete-Metric-Space u) + ( is-limit-map-lim-pseudometric-completion-is-complete-Metric-Space u) + + is-short-map-lim-pseudometric-completion-is-complete-Metric-Space : + is-short-function-Pseudometric-Space + ( pseudometric-completion-Metric-Space M) + ( pseudometric-Metric-Space M) + ( map-lim-pseudometric-completion-is-complete-Metric-Space) + is-short-map-lim-pseudometric-completion-is-complete-Metric-Space d x y Nxy = + saturated-neighborhood-Metric-Space + ( M) + ( d) + ( map-lim-pseudometric-completion-is-complete-Metric-Space x) + ( map-lim-pseudometric-completion-is-complete-Metric-Space y) + ( lemma-saturated-neighborhood-map-lim) + where + + neighborhood-const-lim-x-y : + neighborhood-Pseudometric-Space + ( pseudometric-completion-Metric-Space M) + ( d) + ( const-cauchy-approximation-Metric-Space M + ( map-lim-pseudometric-completion-is-complete-Metric-Space x)) + ( const-cauchy-approximation-Metric-Space M + ( map-lim-pseudometric-completion-is-complete-Metric-Space y)) + neighborhood-const-lim-x-y = + preserves-neighborhood-sim-Pseudometric-Space + ( pseudometric-completion-Metric-Space M) + { x} + { const-cauchy-approximation-Metric-Space + ( M) + ( map-lim-pseudometric-completion-is-complete-Metric-Space x)} + { y} + { const-cauchy-approximation-Metric-Space + ( M) + ( map-lim-pseudometric-completion-is-complete-Metric-Space y)} + ( sim-const-map-lim-pseudometric-completion-is-complete-Metric-Space + ( x)) + ( sim-const-map-lim-pseudometric-completion-is-complete-Metric-Space + ( y)) + ( d) + ( Nxy) + + lemma-saturated-neighborhood-map-lim : + (δ : ℚ⁺) → + neighborhood-Metric-Space + ( M) + ( d +ℚ⁺ δ) + ( map-lim-pseudometric-completion-is-complete-Metric-Space x) + ( map-lim-pseudometric-completion-is-complete-Metric-Space y) + lemma-saturated-neighborhood-map-lim δ = + tr + ( is-upper-bound-dist-Metric-Space + ( M) + ( map-lim-pseudometric-completion-is-complete-Metric-Space x) + ( map-lim-pseudometric-completion-is-complete-Metric-Space y)) + ( ap (add-ℚ⁺' d) (eq-add-split-ℚ⁺ δ) ∙ commutative-add-ℚ⁺ δ d) + ( neighborhood-const-lim-x-y + ( left-summand-split-ℚ⁺ δ) + ( right-summand-split-ℚ⁺ δ)) + + short-map-lim-pseudometric-completion-is-complete-Metric-Space : + short-function-Pseudometric-Space + ( pseudometric-completion-Metric-Space M) + ( pseudometric-Metric-Space M) + short-map-lim-pseudometric-completion-is-complete-Metric-Space = + ( map-lim-pseudometric-completion-is-complete-Metric-Space , + is-short-map-lim-pseudometric-completion-is-complete-Metric-Space) + + is-retraction-map-pseudometric-completion-is-complete-Metric-Space : + ( map-lim-pseudometric-completion-is-complete-Metric-Space ∘ + map-pseudometric-completion-Metric-Space M) ~ + ( id) + is-retraction-map-pseudometric-completion-is-complete-Metric-Space = + is-retraction-limit-cauchy-approximation-Complete-Metric-Space + ( M , is-complete-M) + + sim-map-lim-pseudometric-completion-is-complete-Metric-Space : + (u : cauchy-approximation-Metric-Space M) → + sim-Pseudometric-Space + ( pseudometric-completion-Metric-Space M) + ( u) + ( map-pseudometric-completion-Metric-Space + ( M) + ( map-lim-pseudometric-completion-is-complete-Metric-Space u)) + sim-map-lim-pseudometric-completion-is-complete-Metric-Space u = + sim-const-is-limit-cauchy-approximation-Metric-Space + ( M) + ( u) + ( map-lim-pseudometric-completion-is-complete-Metric-Space u) + ( is-limit-map-lim-pseudometric-completion-is-complete-Metric-Space u) +``` diff --git a/src/metric-spaces/pseudometric-completion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/pseudometric-completion-of-pseudometric-spaces.lagda.md new file mode 100644 index 00000000000..e7489c92e25 --- /dev/null +++ b/src/metric-spaces/pseudometric-completion-of-pseudometric-spaces.lagda.md @@ -0,0 +1,766 @@ +# The pseudometric completion of a pseudometric space + +```agda +{-# OPTIONS --lossy-unification #-} + +module metric-spaces.pseudometric-completion-of-pseudometric-spaces where +``` + +
Imports + +```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-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.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 +open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces +open import metric-spaces.metric-spaces +open import metric-spaces.pseudometric-spaces +open import metric-spaces.rational-neighborhood-relations +open import metric-spaces.short-functions-pseudometric-spaces +open import metric-spaces.similarity-of-elements-pseudometric-spaces +``` + +
+ +## Idea + +The +{{#concept "pseudometric completion" Disambiguation="of a pseudometric space" Agda=pseudometric-completion-Pseudometric-Space}} +of a [pseudometric space](metric-spaces.pseudometric-spaces.md) `M` is the +pseudometric space of +[Cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md) +in `M` where two Cauchy approximations `x` and `y` are in a +[`d`-neighborhood](metric-spaces.rational-neighborhood-relations.md) of one +another if for all `δ ε : ℚ⁺`, `x δ` and `y ε` are in a +`(δ + ε + d)`-neighborhood of one another in `M`. + +Any Cauchy approximation in the pseudometric completion has a +[limit](metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces.md). + +## Definition + +### The pseudometric completion neighborhood relation on the type of Cauchy approximations in a pseudometric space + +```agda +module _ + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) + where + + neighborhood-prop-pseudometric-completion-Pseudometric-Space : + Rational-Neighborhood-Relation l2 + (cauchy-approximation-Pseudometric-Space M) + neighborhood-prop-pseudometric-completion-Pseudometric-Space + d x y = + Π-Prop + ( ℚ⁺) + ( λ δ → + Π-Prop + ( ℚ⁺) + ( λ ε → + neighborhood-prop-Pseudometric-Space + ( M) + ( δ +ℚ⁺ ε +ℚ⁺ d) + ( map-cauchy-approximation-Pseudometric-Space M x δ) + ( map-cauchy-approximation-Pseudometric-Space M y ε))) + + neighborhood-pseudometric-completion-Pseudometric-Space : + ℚ⁺ → Relation l2 (cauchy-approximation-Pseudometric-Space M) + neighborhood-pseudometric-completion-Pseudometric-Space d x y = + type-Prop + ( neighborhood-prop-pseudometric-completion-Pseudometric-Space + ( d) + ( x) + ( y)) +``` + +## Properties + +### The neighborhood relation is reflexive + +```agda +module _ + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) + where + + abstract + is-reflexive-neighborhood-pseudometric-completion-Pseudometric-Space : + (d : ℚ⁺) (x : cauchy-approximation-Pseudometric-Space M) → + neighborhood-pseudometric-completion-Pseudometric-Space M d x x + is-reflexive-neighborhood-pseudometric-completion-Pseudometric-Space + d x δ ε = + let + xδ = map-cauchy-approximation-Pseudometric-Space M x δ + xε = map-cauchy-approximation-Pseudometric-Space M x ε + in + monotonic-neighborhood-Pseudometric-Space M xδ xε + ( δ +ℚ⁺ ε) + ( δ +ℚ⁺ ε +ℚ⁺ d) + ( le-right-add-rational-ℚ⁺ _ d) + ( is-cauchy-approximation-map-cauchy-approximation-Pseudometric-Space + ( M) + ( x) + ( δ) + ( ε)) +``` + +### The neighborhood relation is symmetric + +```agda +module _ + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) + where + + abstract + is-symmetric-neighborhood-pseudometric-completion-Pseudometric-Space : + (d : ℚ⁺) (x y : cauchy-approximation-Pseudometric-Space M) → + neighborhood-pseudometric-completion-Pseudometric-Space M d x y → + neighborhood-pseudometric-completion-Pseudometric-Space M d y x + is-symmetric-neighborhood-pseudometric-completion-Pseudometric-Space + d x y Ndxy δ ε = + let + xε = map-cauchy-approximation-Pseudometric-Space M x ε + yδ = map-cauchy-approximation-Pseudometric-Space M y δ + in + tr + ( λ d' → neighborhood-Pseudometric-Space M d' yδ xε) + ( ap (_+ℚ⁺ d) (commutative-add-ℚ⁺ ε δ)) + ( symmetric-neighborhood-Pseudometric-Space M _ xε yδ (Ndxy ε δ)) +``` + +### The neighborhood relation is triangular + +```agda +module _ + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) + where + + abstract + is-triangular-neighborhood-pseudometric-completion-Pseudometric-Space : + (x y z : cauchy-approximation-Pseudometric-Space M) → + (dxy dyz : ℚ⁺) → + neighborhood-pseudometric-completion-Pseudometric-Space M dyz y z → + neighborhood-pseudometric-completion-Pseudometric-Space M dxy x y → + neighborhood-pseudometric-completion-Pseudometric-Space + ( M) + ( dxy +ℚ⁺ dyz) + ( x) + ( z) + is-triangular-neighborhood-pseudometric-completion-Pseudometric-Space + x y z dxy dyz Ndyz Ndxy δ ε = + let + xδ = map-cauchy-approximation-Pseudometric-Space M x δ + zε = map-cauchy-approximation-Pseudometric-Space M z ε + in + saturated-neighborhood-Pseudometric-Space + ( M) + ( δ +ℚ⁺ ε +ℚ⁺ (dxy +ℚ⁺ dyz)) + ( xδ) + ( zε) + ( λ θ → + let + (θ₂ , θ₂+θ₂<θ) = bound-double-le-ℚ⁺ θ + (θa , θb , θa+θb=θ₂) = split-ℚ⁺ θ₂ + yθa = map-cauchy-approximation-Pseudometric-Space M y θa + in + monotonic-neighborhood-Pseudometric-Space + ( M) + ( xδ) + ( zε) + ( (δ +ℚ⁺ θa +ℚ⁺ dxy +ℚ⁺ θb) +ℚ⁺ (θa +ℚ⁺ ε +ℚ⁺ dyz +ℚ⁺ θb)) + ( δ +ℚ⁺ ε +ℚ⁺ (dxy +ℚ⁺ dyz) +ℚ⁺ θ) + ( tr + ( λ q → le-ℚ⁺ q (δ +ℚ⁺ ε +ℚ⁺ (dxy +ℚ⁺ dyz) +ℚ⁺ θ)) + ( equational-reasoning + ((δ +ℚ⁺ ε) +ℚ⁺ (dxy +ℚ⁺ dyz)) +ℚ⁺ (θ₂ +ℚ⁺ θ₂) + ＝ + ((δ +ℚ⁺ dxy) +ℚ⁺ (ε +ℚ⁺ dyz)) +ℚ⁺ + ((θa +ℚ⁺ θb) +ℚ⁺ (θa +ℚ⁺ θb)) + by + ap-add-ℚ⁺ + ( interchange-law-add-add-ℚ⁺ δ ε dxy dyz) + ( inv (ap-add-ℚ⁺ θa+θb=θ₂ θa+θb=θ₂)) + ＝ + ((δ +ℚ⁺ dxy) +ℚ⁺ (θa +ℚ⁺ θb)) +ℚ⁺ + ((ε +ℚ⁺ dyz) +ℚ⁺ (θa +ℚ⁺ θb)) + by interchange-law-add-add-ℚ⁺ _ _ _ _ + ＝ + ((δ +ℚ⁺ θa) +ℚ⁺ (dxy +ℚ⁺ θb)) +ℚ⁺ + ((ε +ℚ⁺ θa) +ℚ⁺ (dyz +ℚ⁺ θb)) + by + ap-add-ℚ⁺ + ( interchange-law-add-add-ℚ⁺ _ _ _ _) + ( interchange-law-add-add-ℚ⁺ _ _ _ _) + ＝ + (δ +ℚ⁺ θa +ℚ⁺ dxy +ℚ⁺ θb) +ℚ⁺ + ((θa +ℚ⁺ ε) +ℚ⁺ (dyz +ℚ⁺ θb)) + by + ap-add-ℚ⁺ + ( inv (associative-add-ℚ⁺ _ _ _)) + ( ap-add-ℚ⁺ (commutative-add-ℚ⁺ _ _) refl) + ＝ (δ +ℚ⁺ θa +ℚ⁺ dxy +ℚ⁺ θb) +ℚ⁺ (θa +ℚ⁺ ε +ℚ⁺ dyz +ℚ⁺ θb) + by ap-add-ℚ⁺ refl (inv (associative-add-ℚ⁺ _ _ _))) + ( preserves-le-right-add-ℚ + ( rational-ℚ⁺ (δ +ℚ⁺ ε +ℚ⁺ (dxy +ℚ⁺ dyz))) + ( rational-ℚ⁺ (θ₂ +ℚ⁺ θ₂)) + ( rational-ℚ⁺ θ) + ( θ₂+θ₂<θ))) + ( triangular-neighborhood-Pseudometric-Space M xδ yθa zε + ( δ +ℚ⁺ θa +ℚ⁺ dxy +ℚ⁺ θb) + ( θa +ℚ⁺ ε +ℚ⁺ dyz +ℚ⁺ θb) + ( monotonic-neighborhood-Pseudometric-Space M yθa zε + ( θa +ℚ⁺ ε +ℚ⁺ dyz) + ( θa +ℚ⁺ ε +ℚ⁺ dyz +ℚ⁺ θb) + ( le-left-add-ℚ⁺ (θa +ℚ⁺ ε +ℚ⁺ dyz) θb) + ( Ndyz θa ε)) + ( monotonic-neighborhood-Pseudometric-Space M xδ yθa + ( δ +ℚ⁺ θa +ℚ⁺ dxy) + ( δ +ℚ⁺ θa +ℚ⁺ dxy +ℚ⁺ θb) + ( le-left-add-ℚ⁺ (δ +ℚ⁺ θa +ℚ⁺ dxy) θb) + ( Ndxy δ θa)))) +``` + +### The neighborhood relation is saturated + +```agda +module _ + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) + where + + abstract + is-saturated-neighborhood-pseudometric-completion-Pseudometric-Space : + ( ε : ℚ⁺) (x y : cauchy-approximation-Pseudometric-Space M) → + ( (δ : ℚ⁺) → + neighborhood-pseudometric-completion-Pseudometric-Space + ( M) + ( ε +ℚ⁺ δ) + ( x) + ( y)) → + neighborhood-pseudometric-completion-Pseudometric-Space M ε x y + is-saturated-neighborhood-pseudometric-completion-Pseudometric-Space + d x y H δ ε = + let + xδ = map-cauchy-approximation-Pseudometric-Space M x δ + yε = map-cauchy-approximation-Pseudometric-Space M y ε + in + saturated-neighborhood-Pseudometric-Space M + ( δ +ℚ⁺ ε +ℚ⁺ d) + ( xδ) + ( yε) + ( λ θ → + tr + ( λ η → neighborhood-Pseudometric-Space M η xδ yε) + ( inv (associative-add-ℚ⁺ _ _ _)) + ( H θ δ ε)) +``` + +### The pseudometric completion of a pseudometric space + +```agda +module _ + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) + where + + pseudometric-completion-Pseudometric-Space : + Pseudometric-Space (l1 ⊔ l2) l2 + pseudometric-completion-Pseudometric-Space = + ( cauchy-approximation-Pseudometric-Space M , + neighborhood-prop-pseudometric-completion-Pseudometric-Space M , + is-reflexive-neighborhood-pseudometric-completion-Pseudometric-Space M , + is-symmetric-neighborhood-pseudometric-completion-Pseudometric-Space M , + is-triangular-neighborhood-pseudometric-completion-Pseudometric-Space M , + is-saturated-neighborhood-pseudometric-completion-Pseudometric-Space M) +``` + +### The isometry from a pseudometric space to its pseudometric completion + +```agda +module _ + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) + where + + map-pseudometric-completion-Pseudometric-Space : + type-Pseudometric-Space M → cauchy-approximation-Pseudometric-Space M + map-pseudometric-completion-Pseudometric-Space = + const-cauchy-approximation-Pseudometric-Space M + + abstract + preserves-neighborhood-map-pseudometric-completion-Pseudometric-Space : + (d : ℚ⁺) (x y : type-Pseudometric-Space M) → + neighborhood-Pseudometric-Space M d x y → + neighborhood-pseudometric-completion-Pseudometric-Space + ( M) + ( d) + ( map-pseudometric-completion-Pseudometric-Space x) + ( map-pseudometric-completion-Pseudometric-Space y) + preserves-neighborhood-map-pseudometric-completion-Pseudometric-Space + d x y Nxy δ ε = + monotonic-neighborhood-Pseudometric-Space M x y d (δ +ℚ⁺ ε +ℚ⁺ d) + ( le-right-add-ℚ⁺ (δ +ℚ⁺ ε) d) + ( Nxy) + + reflects-neighborhood-map-pseudometric-completion-Pseudometric-Space : + (d : ℚ⁺) (x y : type-Pseudometric-Space M) → + neighborhood-pseudometric-completion-Pseudometric-Space + ( M) + ( d) + ( map-pseudometric-completion-Pseudometric-Space x) + ( map-pseudometric-completion-Pseudometric-Space y) → + neighborhood-Pseudometric-Space M d x y + reflects-neighborhood-map-pseudometric-completion-Pseudometric-Space + d x y Nxy = + saturated-neighborhood-Pseudometric-Space M d x y + ( λ δ → + let + (δ₁ , δ₂ , δ₁+δ₂=δ) = split-ℚ⁺ δ + in + tr + ( λ ε → neighborhood-Pseudometric-Space M ε x y) + ( commutative-add-ℚ⁺ _ _ ∙ ap (d +ℚ⁺_) δ₁+δ₂=δ) + ( Nxy δ₁ δ₂)) + + is-isometry-map-pseudometric-completion-Pseudometric-Space : + is-isometry-Pseudometric-Space + ( M) + ( pseudometric-completion-Pseudometric-Space M) + ( map-pseudometric-completion-Pseudometric-Space) + is-isometry-map-pseudometric-completion-Pseudometric-Space d x y = + ( ( preserves-neighborhood-map-pseudometric-completion-Pseudometric-Space + ( d) + ( x) + ( y)) , + (reflects-neighborhood-map-pseudometric-completion-Pseudometric-Space + ( d) + ( x) + ( y))) + + isometry-pseudometric-completion-Pseudometric-Space : + isometry-Pseudometric-Space + ( M) + ( pseudometric-completion-Pseudometric-Space M) + isometry-pseudometric-completion-Pseudometric-Space = + ( map-pseudometric-completion-Pseudometric-Space , + is-isometry-map-pseudometric-completion-Pseudometric-Space) + + short-map-pseudometric-completion-Pseudometric-Space : + short-function-Pseudometric-Space + ( M) + ( pseudometric-completion-Pseudometric-Space M) + short-map-pseudometric-completion-Pseudometric-Space = + short-isometry-Pseudometric-Space + ( M) + ( pseudometric-completion-Pseudometric-Space M) + ( isometry-pseudometric-completion-Pseudometric-Space) +``` + +### Convergent Cauchy approximations are similar to constant Cauchy approximations in the pseudometric completion + +```agda +module _ + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) + (u : cauchy-approximation-Pseudometric-Space M) + (x : type-Pseudometric-Space M) + where + + abstract + sim-const-is-limit-cauchy-approximation-Pseudometric-Space : + is-limit-cauchy-approximation-Pseudometric-Space M u x → + sim-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( u) + ( const-cauchy-approximation-Pseudometric-Space M x) + sim-const-is-limit-cauchy-approximation-Pseudometric-Space H d α β = + monotonic-neighborhood-Pseudometric-Space + ( M) + ( map-cauchy-approximation-Pseudometric-Space M u α) + ( x) + ( α +ℚ⁺ β) + ( α +ℚ⁺ β +ℚ⁺ d) + ( le-left-add-ℚ⁺ (α +ℚ⁺ β) d) + ( H α β) + + is-limit-sim-const-cauchy-approximation-Pseudometric-Space : + sim-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( u) + ( const-cauchy-approximation-Pseudometric-Space M x) → + is-limit-cauchy-approximation-Pseudometric-Space M u x + is-limit-sim-const-cauchy-approximation-Pseudometric-Space H α β = + saturated-neighborhood-Pseudometric-Space + ( M) + ( α +ℚ⁺ β) + ( map-cauchy-approximation-Pseudometric-Space M u α) + ( x) + ( λ d → H d α β) +``` + +### Any Cauchy approximation in the pseudometric completion of a pseudometric space has a limit + +```agda +module _ + { l1 l2 : Level} (M : Pseudometric-Space l1 l2) + ( U : + cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M)) + where + + map-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + ℚ⁺ → ℚ⁺ → type-Pseudometric-Space M + map-cauchy-approximation-pseudometric-completion-Pseudometric-Space ε = + map-cauchy-approximation-Pseudometric-Space M + ( map-cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( U) + ( ε)) + + is-cauchy-map-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + (δ ε d₁ d₂ : ℚ⁺) → + neighborhood-Pseudometric-Space + ( M) + ( d₁ +ℚ⁺ d₂ +ℚ⁺ (δ +ℚ⁺ ε)) + ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( δ) + ( d₁)) + ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( ε) + ( d₂)) + is-cauchy-map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + = + is-cauchy-approximation-map-cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( U) + + map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + ℚ⁺ → type-Pseudometric-Space M + map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space d = + let + (d₁ , d₂ , _) = split-ℚ⁺ d + in + map-cauchy-approximation-pseudometric-completion-Pseudometric-Space d₂ d₁ + + is-cauchy-map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + is-cauchy-approximation-Pseudometric-Space + ( M) + ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space) + is-cauchy-map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + δ ε = + let + (δ₁ , δ₂ , δ₁+δ₂=δ) = split-ℚ⁺ δ + (ε₁ , ε₂ , ε₁+ε₂=ε) = split-ℚ⁺ ε + + lemma-δ+ε : + (δ₁ +ℚ⁺ ε₁ +ℚ⁺ (δ₂ +ℚ⁺ ε₂)) ＝ δ +ℚ⁺ ε + lemma-δ+ε = + ( interchange-law-add-add-ℚ⁺ + ( δ₁) + ( ε₁) + ( δ₂) + ( ε₂)) ∙ + ( ap-binary + ( add-ℚ⁺) + ( δ₁+δ₂=δ) + ( ε₁+ε₂=ε)) + in + tr + ( is-upper-bound-dist-Pseudometric-Space + ( M) + ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( δ)) + ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( ε))) + ( lemma-δ+ε) + ( is-cauchy-map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + _ _ _ _) + + lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + cauchy-approximation-Pseudometric-Space M + lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space = + ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space , + is-cauchy-map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space) + + is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + is-limit-cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( U) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space) + is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + δ ε η θ = + let + (θ₁ , θ₂ , θ₁+θ₂=θ) = split-ℚ⁺ θ + + lemma-η+θ+δ : + ( η +ℚ⁺ θ₁ +ℚ⁺ (δ +ℚ⁺ θ₂)) ＝ η +ℚ⁺ θ +ℚ⁺ δ + lemma-η+θ+δ = + ( interchange-law-add-add-ℚ⁺ η θ₁ δ θ₂) ∙ + ( ap + ( add-ℚ⁺ (η +ℚ⁺ δ)) + ( θ₁+θ₂=θ)) ∙ + ( associative-add-ℚ⁺ η δ θ) ∙ + ( ap + ( add-ℚ⁺ η) + ( commutative-add-ℚ⁺ δ θ)) ∙ + ( inv (associative-add-ℚ⁺ η θ δ)) + + lemma-lim : + neighborhood-Pseudometric-Space M + ( η +ℚ⁺ θ +ℚ⁺ δ) + ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( δ) + ( η)) + ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( θ₂) + ( θ₁)) + lemma-lim = + tr + ( is-upper-bound-dist-Pseudometric-Space M + ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( δ) + ( η)) + ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( θ))) + ( lemma-η+θ+δ) + ( is-cauchy-map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + _ _ _ _) + in + tr + ( is-upper-bound-dist-Pseudometric-Space M + ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( δ) + ( η)) + ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( θ))) + ( associative-add-ℚ⁺ + ( η +ℚ⁺ θ) + ( δ) + ( ε)) + ( monotonic-neighborhood-Pseudometric-Space M + ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( δ) + ( η)) + ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( θ)) + ( η +ℚ⁺ θ +ℚ⁺ δ) + ( η +ℚ⁺ θ +ℚ⁺ δ +ℚ⁺ ε) + ( le-left-add-ℚ⁺ ( η +ℚ⁺ θ +ℚ⁺ δ) ε) + ( lemma-lim)) + + has-limit-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + Σ ( cauchy-approximation-Pseudometric-Space M) + ( is-limit-cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( U)) + has-limit-cauchy-approximation-pseudometric-completion-Pseudometric-Space = + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space , + is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space) +``` + +### The map from a Cauchy approximation in the pseudometric completion to its limit is an isometry + +```agda +module _ + { l1 l2 : Level} (M : Pseudometric-Space l1 l2) + ( d : ℚ⁺) + ( u v : + cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M)) + where + + abstract + preserves-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + neighborhood-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M)) + ( d) + ( u) + ( v) → + neighborhood-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( d) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( u)) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( v)) + preserves-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + Nuv = + let + neighborhood-const-lim : + neighborhood-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M)) + ( d) + ( const-cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( u))) + ( const-cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( v))) + neighborhood-const-lim = + preserves-neighborhood-sim-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M)) + { u} + { const-cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( u))} + { v} + { const-cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( v))} + ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( u) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( u)) + ( is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( u))) + ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( v) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( v)) + ( is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( v))) + ( d) + ( Nuv) + in + reflects-neighborhood-map-pseudometric-completion-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( d) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( u)) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( v)) + ( neighborhood-const-lim) + + reflects-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + neighborhood-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( d) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( u)) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( v)) → + neighborhood-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M)) + ( d) + ( u) + ( v) + reflects-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + N-lim = + reflects-neighborhood-sim-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M)) + { u} + { const-cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( u))} + { v} + { const-cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( v))} + ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( u) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( u)) + ( is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( u))) + ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( v) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( v)) + ( is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( v))) + ( d) + ( preserves-neighborhood-map-pseudometric-completion-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M) + ( d) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( u)) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( v)) + ( N-lim)) + +module _ + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) + where + + abstract + is-isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + is-isometry-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M)) + ( pseudometric-completion-Pseudometric-Space M) + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space M) + is-isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + d x y = + ( ( preserves-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( d) + ( x) + ( y)) , + ( reflects-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( M) + ( d) + ( x) + ( y))) + + isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + isometry-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space + ( pseudometric-completion-Pseudometric-Space M)) + ( pseudometric-completion-Pseudometric-Space M) + isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space = + ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space M , + is-isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space) +``` From 1715d94118a39438991b60707f49d9dbf25bb6ef Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 21 Oct 2025 23:15:33 +0200 Subject: [PATCH 04/28] Update src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- .../similarity-of-elements-pseudometric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md index 024bfbaa3ad..9e9b095cafa 100644 --- a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md @@ -273,7 +273,7 @@ module _ where abstract - iff-same-neighbors-same-neighborhood-Pseudometric-Space : + same-neighbors-iff-same-neighborhood-Pseudometric-Space : {x y : type-Pseudometric-Space A} → ( (d : ℚ⁺) (z : type-Pseudometric-Space A) → neighborhood-Pseudometric-Space A d x z ↔ From 84f6f1ca9515e074b67899a9df7036ca9bb9813f Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 21 Oct 2025 23:15:54 +0200 Subject: [PATCH 05/28] Update src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- .../similarity-of-elements-pseudometric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md index 9e9b095cafa..c46f40a21ee 100644 --- a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md @@ -294,7 +294,7 @@ module _ ( iff-left-neighbor-sim-Rational-Neighborhood-Relation ( neighborhood-prop-Pseudometric-Space A)) - iff-same-neighborhood-sim-Pseudometric-Space : + same-neighborhood-iff-sim-Pseudometric-Space : { x y : type-Pseudometric-Space A} → ( sim-Pseudometric-Space A x y) ↔ ( sim-Rational-Neighborhood-Relation From f2cc49753c9adfdf371b00cbcf880b7e55c888fb Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 21 Oct 2025 23:32:35 +0200 Subject: [PATCH 06/28] fix names --- ...milarity-of-elements-pseudometric-spaces.lagda.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md index c46f40a21ee..f9caa041d21 100644 --- a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md @@ -246,13 +246,13 @@ module _ ( inv-sim-Pseudometric-Space A x~x') ( inv-sim-Pseudometric-Space A y~y') - iff-same-neighbors-sim-Pseudometric-Space : + same-neighbors-iff-sim-Pseudometric-Space : { x y : type-Pseudometric-Space A} → ( sim-Pseudometric-Space A x y) ↔ ( (d : ℚ⁺) (z : type-Pseudometric-Space A) → neighborhood-Pseudometric-Space A d x z ↔ neighborhood-Pseudometric-Space A d y z) - iff-same-neighbors-sim-Pseudometric-Space = + same-neighbors-iff-sim-Pseudometric-Space = ( λ x≍y d z → ( preserves-neighborhood-left-sim-Pseudometric-Space x≍y d z) , ( preserves-neighborhood-left-sim-Pseudometric-Space @@ -282,7 +282,7 @@ module _ ( neighborhood-prop-Pseudometric-Space A) ( x) ( y)) - iff-same-neighbors-same-neighborhood-Pseudometric-Space = + same-neighbors-iff-same-neighborhood-Pseudometric-Space = ( λ H d z → ( H d z) , ( inv-neighborhood-Pseudometric-Space A ∘ @@ -301,9 +301,9 @@ module _ ( neighborhood-prop-Pseudometric-Space A) ( x) ( y)) - iff-same-neighborhood-sim-Pseudometric-Space = - ( iff-same-neighbors-same-neighborhood-Pseudometric-Space) ∘iff - ( iff-same-neighbors-sim-Pseudometric-Space A) + same-neighborhood-iff-sim-Pseudometric-Space = + ( same-neighbors-iff-same-neighborhood-Pseudometric-Space) ∘iff + ( same-neighbors-iff-sim-Pseudometric-Space A) ``` ### Short maps between pseudometric spaces preserve similarity From c64c6b6104ce1ed0259ab12804fa73b2a06f47aa Mon Sep 17 00:00:00 2001 From: malarbol Date: Wed, 22 Oct 2025 01:34:29 +0200 Subject: [PATCH 07/28] fix names --- src/metric-spaces.lagda.md | 4 +- ...seudocompletion-of-metric-spaces.lagda.md} | 248 ++++++------- ...ompletion-of-pseudometric-spaces.lagda.md} | 348 +++++++++--------- 3 files changed, 300 insertions(+), 300 deletions(-) rename src/metric-spaces/{pseudometric-completion-of-metric-spaces.lagda.md => cauchy-pseudocompletion-of-metric-spaces.lagda.md} (55%) rename src/metric-spaces/{pseudometric-completion-of-pseudometric-spaces.lagda.md => cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md} (64%) diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md index 00f3db27988..76d05aabeea 100644 --- a/src/metric-spaces.lagda.md +++ b/src/metric-spaces.lagda.md @@ -64,6 +64,8 @@ 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-metric-spaces public open import metric-spaces.cauchy-approximations-pseudometric-spaces public +open import metric-spaces.cauchy-pseudocompletion-of-metric-spaces public +open import metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces public open import metric-spaces.cauchy-sequences-complete-metric-spaces public open import metric-spaces.cauchy-sequences-metric-spaces public open import metric-spaces.closed-subsets-located-metric-spaces public @@ -125,8 +127,6 @@ open import metric-spaces.precategory-of-metric-spaces-and-functions public open import metric-spaces.precategory-of-metric-spaces-and-isometries public open import metric-spaces.precategory-of-metric-spaces-and-short-functions public open import metric-spaces.preimages-rational-neighborhood-relations public -open import metric-spaces.pseudometric-completion-of-metric-spaces public -open import metric-spaces.pseudometric-completion-of-pseudometric-spaces public open import metric-spaces.pseudometric-spaces public open import metric-spaces.rational-approximations-of-zero public open import metric-spaces.rational-cauchy-approximations public diff --git a/src/metric-spaces/pseudometric-completion-of-metric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md similarity index 55% rename from src/metric-spaces/pseudometric-completion-of-metric-spaces.lagda.md rename to src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md index 57328439f22..d2af66c6449 100644 --- a/src/metric-spaces/pseudometric-completion-of-metric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md @@ -1,7 +1,7 @@ -# The pseudometric completion of a metric space +# The Cauchy pseudocompletion of a metric space ```agda -module metric-spaces.pseudometric-completion-of-metric-spaces where +module metric-spaces.cauchy-pseudocompletion-of-metric-spaces where ```
Imports @@ -25,6 +25,7 @@ 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 @@ -32,7 +33,6 @@ open import metric-spaces.isometries-pseudometric-spaces open import metric-spaces.limits-of-cauchy-approximations-metric-spaces open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces open import metric-spaces.metric-spaces -open import metric-spaces.pseudometric-completion-of-pseudometric-spaces open import metric-spaces.pseudometric-spaces open import metric-spaces.rational-neighborhood-relations open import metric-spaces.short-functions-pseudometric-spaces @@ -44,9 +44,9 @@ open import metric-spaces.similarity-of-elements-pseudometric-spaces ## Idea The -{{#concept "pseudometric completion" Disambiguation="of a metric space" Agda=pseudometric-completion-Metric-Space}} +{{#concept "Cauchy pseudocompletion" Disambiguation="of a metric space" Agda=cauchy-pseudocompletion-Metric-Space}} of a [metric space](metric-spaces.metric-spaces.md) `M` is the -[pseudometric completion](metric-spaces.pseudometric-completion-of-pseudometric-spaces.md) +[Cauchy pseudocompletion](metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces.md) of its underlying [pseudometric space](metric-spaces.pseudometric-spaces.md): the pseudometric space of [Cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md) @@ -55,45 +55,45 @@ in `M` where two Cauchy approximations `x` and `y` are in a another if for all `δ ε : ℚ⁺`, `x δ` and `y ε` are in a `(δ + ε + d)`-neighborhood of one another in `M`. -Any Cauchy approximation in the pseudometric completion has a +Any Cauchy approximation in the Cauchy pseudocompletion has a [limit](metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces.md). If the metric space is [complete](metric-spaces.complete-metric-spaces.md), it -is a [retract](foundation.retracts-of-types.md) of its pseudometric completion. +is a [retract](foundation.retracts-of-types.md) of its Cauchy pseudocompletion. ## Definition -### The pseudometric completion of a metric space +### The Cauchy pseudocompletion of a metric space ```agda module _ {l1 l2 : Level} (M : Metric-Space l1 l2) where - pseudometric-completion-Metric-Space : + cauchy-pseudocompletion-Metric-Space : Pseudometric-Space (l1 ⊔ l2) l2 - pseudometric-completion-Metric-Space = - pseudometric-completion-Pseudometric-Space + cauchy-pseudocompletion-Metric-Space = + cauchy-pseudocompletion-Pseudometric-Space ( pseudometric-Metric-Space M) ``` -### The pseudometric completion neighborhood relation on the type of Cauchy approximations in a pseudometric space +### The Cauchy pseudocompletion neighborhood relation on the type of Cauchy approximations in a pseudometric space ```agda module _ {l1 l2 : Level} (M : Metric-Space l1 l2) where - neighborhood-prop-pseudometric-completion-Metric-Space : + neighborhood-prop-cauchy-pseudocompletion-Metric-Space : Rational-Neighborhood-Relation l2 (cauchy-approximation-Metric-Space M) - neighborhood-prop-pseudometric-completion-Metric-Space = - neighborhood-prop-pseudometric-completion-Pseudometric-Space + neighborhood-prop-cauchy-pseudocompletion-Metric-Space = + neighborhood-prop-cauchy-pseudocompletion-Pseudometric-Space ( pseudometric-Metric-Space M) - neighborhood-pseudometric-completion-Metric-Space : + neighborhood-cauchy-pseudocompletion-Metric-Space : ℚ⁺ → Relation l2 (cauchy-approximation-Metric-Space M) - neighborhood-pseudometric-completion-Metric-Space = - neighborhood-pseudometric-completion-Pseudometric-Space + neighborhood-cauchy-pseudocompletion-Metric-Space = + neighborhood-cauchy-pseudocompletion-Pseudometric-Space ( pseudometric-Metric-Space M) ``` @@ -107,11 +107,11 @@ module _ where abstract - is-reflexive-neighborhood-pseudometric-completion-Metric-Space : + is-reflexive-neighborhood-cauchy-pseudocompletion-Metric-Space : (d : ℚ⁺) (x : cauchy-approximation-Metric-Space M) → - neighborhood-pseudometric-completion-Metric-Space M d x x - is-reflexive-neighborhood-pseudometric-completion-Metric-Space = - is-reflexive-neighborhood-pseudometric-completion-Pseudometric-Space + neighborhood-cauchy-pseudocompletion-Metric-Space M d x x + is-reflexive-neighborhood-cauchy-pseudocompletion-Metric-Space = + is-reflexive-neighborhood-cauchy-pseudocompletion-Pseudometric-Space ( pseudometric-Metric-Space M) ``` @@ -123,12 +123,12 @@ module _ where abstract - is-symmetric-neighborhood-pseudometric-completion-Metric-Space : + is-symmetric-neighborhood-cauchy-pseudocompletion-Metric-Space : (d : ℚ⁺) (x y : cauchy-approximation-Metric-Space M) → - neighborhood-pseudometric-completion-Metric-Space M d x y → - neighborhood-pseudometric-completion-Metric-Space M d y x - is-symmetric-neighborhood-pseudometric-completion-Metric-Space = - is-symmetric-neighborhood-pseudometric-completion-Pseudometric-Space + neighborhood-cauchy-pseudocompletion-Metric-Space M d x y → + neighborhood-cauchy-pseudocompletion-Metric-Space M d y x + is-symmetric-neighborhood-cauchy-pseudocompletion-Metric-Space = + is-symmetric-neighborhood-cauchy-pseudocompletion-Pseudometric-Space ( pseudometric-Metric-Space M) ``` @@ -140,18 +140,18 @@ module _ where abstract - is-triangular-neighborhood-pseudometric-completion-Metric-Space : + is-triangular-neighborhood-cauchy-pseudocompletion-Metric-Space : (x y z : cauchy-approximation-Metric-Space M) → (dxy dyz : ℚ⁺) → - neighborhood-pseudometric-completion-Metric-Space M dyz y z → - neighborhood-pseudometric-completion-Metric-Space M dxy x y → - neighborhood-pseudometric-completion-Metric-Space + neighborhood-cauchy-pseudocompletion-Metric-Space M dyz y z → + neighborhood-cauchy-pseudocompletion-Metric-Space M dxy x y → + neighborhood-cauchy-pseudocompletion-Metric-Space ( M) ( dxy +ℚ⁺ dyz) ( x) ( z) - is-triangular-neighborhood-pseudometric-completion-Metric-Space = - is-triangular-neighborhood-pseudometric-completion-Pseudometric-Space + is-triangular-neighborhood-cauchy-pseudocompletion-Metric-Space = + is-triangular-neighborhood-cauchy-pseudocompletion-Pseudometric-Space ( pseudometric-Metric-Space M) ``` @@ -163,57 +163,57 @@ module _ where abstract - is-saturated-neighborhood-pseudometric-completion-Metric-Space : + is-saturated-neighborhood-cauchy-pseudocompletion-Metric-Space : ( ε : ℚ⁺) (x y : cauchy-approximation-Metric-Space M) → ( (δ : ℚ⁺) → - neighborhood-pseudometric-completion-Metric-Space + neighborhood-cauchy-pseudocompletion-Metric-Space ( M) ( ε +ℚ⁺ δ) ( x) ( y)) → - neighborhood-pseudometric-completion-Metric-Space M ε x y - is-saturated-neighborhood-pseudometric-completion-Metric-Space = - is-saturated-neighborhood-pseudometric-completion-Pseudometric-Space + neighborhood-cauchy-pseudocompletion-Metric-Space M ε x y + is-saturated-neighborhood-cauchy-pseudocompletion-Metric-Space = + is-saturated-neighborhood-cauchy-pseudocompletion-Pseudometric-Space ( pseudometric-Metric-Space M) ``` -### The isometry from a metric space to its pseudometric completion +### The isometry from a metric space to its Cauchy pseudocompletion ```agda module _ {l1 l2 : Level} (M : Metric-Space l1 l2) where - isometry-pseudometric-completion-Metric-Space : + isometry-cauchy-pseudocompletion-Metric-Space : isometry-Pseudometric-Space ( pseudometric-Metric-Space M) - ( pseudometric-completion-Metric-Space M) - isometry-pseudometric-completion-Metric-Space = - isometry-pseudometric-completion-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Space M) + isometry-cauchy-pseudocompletion-Metric-Space = + isometry-cauchy-pseudocompletion-Pseudometric-Space ( pseudometric-Metric-Space M) - map-pseudometric-completion-Metric-Space : + map-cauchy-pseudocompletion-Metric-Space : type-Metric-Space M → cauchy-approximation-Metric-Space M - map-pseudometric-completion-Metric-Space = + map-cauchy-pseudocompletion-Metric-Space = map-isometry-Pseudometric-Space ( pseudometric-Metric-Space M) - ( pseudometric-completion-Metric-Space M) - ( isometry-pseudometric-completion-Metric-Space) + ( cauchy-pseudocompletion-Metric-Space M) + ( isometry-cauchy-pseudocompletion-Metric-Space) abstract - is-isometry-map-pseudometric-completion-Metric-Space : + is-isometry-map-cauchy-pseudocompletion-Metric-Space : is-isometry-Pseudometric-Space ( pseudometric-Metric-Space M) - ( pseudometric-completion-Metric-Space M) - ( map-pseudometric-completion-Metric-Space) - is-isometry-map-pseudometric-completion-Metric-Space = + ( cauchy-pseudocompletion-Metric-Space M) + ( map-cauchy-pseudocompletion-Metric-Space) + is-isometry-map-cauchy-pseudocompletion-Metric-Space = is-isometry-map-isometry-Pseudometric-Space ( pseudometric-Metric-Space M) - ( pseudometric-completion-Metric-Space M) - ( isometry-pseudometric-completion-Metric-Space) + ( cauchy-pseudocompletion-Metric-Space M) + ( isometry-cauchy-pseudocompletion-Metric-Space) ``` -### Convergent Cauchy approximations are similar to constant Cauchy approximations in the pseudometric completion +### Convergent Cauchy approximations are similar to constant Cauchy approximations in the Cauchy pseudocompletion ```agda module _ @@ -226,7 +226,7 @@ module _ sim-const-is-limit-cauchy-approximation-Metric-Space : is-limit-cauchy-approximation-Metric-Space M u x → sim-Pseudometric-Space - ( pseudometric-completion-Metric-Space M) + ( cauchy-pseudocompletion-Metric-Space M) ( u) ( const-cauchy-approximation-Metric-Space M x) sim-const-is-limit-cauchy-approximation-Metric-Space H d α β = @@ -241,7 +241,7 @@ module _ is-limit-sim-const-cauchy-approximation-Metric-Space : sim-Pseudometric-Space - ( pseudometric-completion-Metric-Space M) + ( cauchy-pseudocompletion-Metric-Space M) ( u) ( const-cauchy-approximation-Metric-Space M x) → is-limit-cauchy-approximation-Metric-Space M u x @@ -254,58 +254,58 @@ module _ ( λ d → H d α β) ``` -### Any Cauchy approximation in the pseudometric completion of a metric space has a limit +### Any Cauchy approximation in the Cauchy pseudocompletion of a metric space has a limit ```agda module _ { l1 l2 : Level} (M : Metric-Space l1 l2) ( U : cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Metric-Space M)) + ( cauchy-pseudocompletion-Metric-Space M)) where - has-limit-cauchy-approximation-pseudometric-completion-Metric-Space : + has-limit-cauchy-approximation-cauchy-pseudocompletion-Metric-Space : Σ ( cauchy-approximation-Metric-Space M) ( is-limit-cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Metric-Space M) + ( cauchy-pseudocompletion-Metric-Space M) ( U)) - has-limit-cauchy-approximation-pseudometric-completion-Metric-Space = - has-limit-cauchy-approximation-pseudometric-completion-Pseudometric-Space + has-limit-cauchy-approximation-cauchy-pseudocompletion-Metric-Space = + has-limit-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( pseudometric-Metric-Space M) ( U) - lim-cauchy-approximation-pseudometric-completion-Metric-Space : + lim-cauchy-approximation-cauchy-pseudocompletion-Metric-Space : cauchy-approximation-Metric-Space M - lim-cauchy-approximation-pseudometric-completion-Metric-Space = - pr1 has-limit-cauchy-approximation-pseudometric-completion-Metric-Space + lim-cauchy-approximation-cauchy-pseudocompletion-Metric-Space = + pr1 has-limit-cauchy-approximation-cauchy-pseudocompletion-Metric-Space - is-limit-lim-cauchy-approximation-pseudometric-completion-Metric-Space : + is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Metric-Space : is-limit-cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Metric-Space M) + ( cauchy-pseudocompletion-Metric-Space M) ( U) - ( lim-cauchy-approximation-pseudometric-completion-Metric-Space) - is-limit-lim-cauchy-approximation-pseudometric-completion-Metric-Space = - pr2 has-limit-cauchy-approximation-pseudometric-completion-Metric-Space + ( lim-cauchy-approximation-cauchy-pseudocompletion-Metric-Space) + is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Metric-Space = + pr2 has-limit-cauchy-approximation-cauchy-pseudocompletion-Metric-Space ``` -### The isometry from a Cauchy approximation in the pseudometric completion to its limit +### The isometry from a Cauchy approximation in the Cauchy pseudocompletion to its limit ```agda module _ {l1 l2 : Level} (M : Metric-Space l1 l2) where - isometry-lim-cauchy-approximation-pseudometric-completion-Metric-Space : + isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Metric-Space : isometry-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space - ( pseudometric-completion-Metric-Space M)) - ( pseudometric-completion-Metric-Space M) - isometry-lim-cauchy-approximation-pseudometric-completion-Metric-Space = - isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Space M)) + ( cauchy-pseudocompletion-Metric-Space M) + isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Metric-Space = + isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( pseudometric-Metric-Space M) ``` -### Any complete metric space is a short retract of its pseudometric completion +### Any complete metric space is a short retract of its Cauchy pseudocompletion ```agda module _ @@ -313,75 +313,75 @@ module _ (is-complete-M : is-complete-Metric-Space M) where - map-lim-pseudometric-completion-is-complete-Metric-Space : + map-lim-cauchy-pseudocompletion-is-complete-Metric-Space : type-function-Pseudometric-Space - ( pseudometric-completion-Metric-Space M) + ( cauchy-pseudocompletion-Metric-Space M) ( pseudometric-Metric-Space M) - map-lim-pseudometric-completion-is-complete-Metric-Space = + map-lim-cauchy-pseudocompletion-is-complete-Metric-Space = limit-cauchy-approximation-Complete-Metric-Space ( M , is-complete-M) - is-limit-map-lim-pseudometric-completion-is-complete-Metric-Space : + is-limit-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space : (u : cauchy-approximation-Metric-Space M) → is-limit-cauchy-approximation-Metric-Space ( M) ( u) - ( map-lim-pseudometric-completion-is-complete-Metric-Space u) - is-limit-map-lim-pseudometric-completion-is-complete-Metric-Space = + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u) + is-limit-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space = is-limit-limit-cauchy-approximation-Complete-Metric-Space ( M , is-complete-M) - sim-const-map-lim-pseudometric-completion-is-complete-Metric-Space : + sim-const-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space : (u : cauchy-approximation-Metric-Space M) → sim-Pseudometric-Space - ( pseudometric-completion-Metric-Space M) + ( cauchy-pseudocompletion-Metric-Space M) ( u) ( const-cauchy-approximation-Metric-Space ( M) - ( map-lim-pseudometric-completion-is-complete-Metric-Space u)) - sim-const-map-lim-pseudometric-completion-is-complete-Metric-Space u = + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u)) + sim-const-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u = sim-const-is-limit-cauchy-approximation-Metric-Space ( M) ( u) - ( map-lim-pseudometric-completion-is-complete-Metric-Space u) - ( is-limit-map-lim-pseudometric-completion-is-complete-Metric-Space u) + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u) + ( is-limit-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u) - is-short-map-lim-pseudometric-completion-is-complete-Metric-Space : + is-short-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space : is-short-function-Pseudometric-Space - ( pseudometric-completion-Metric-Space M) + ( cauchy-pseudocompletion-Metric-Space M) ( pseudometric-Metric-Space M) - ( map-lim-pseudometric-completion-is-complete-Metric-Space) - is-short-map-lim-pseudometric-completion-is-complete-Metric-Space d x y Nxy = + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space) + is-short-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space d x y Nxy = saturated-neighborhood-Metric-Space ( M) ( d) - ( map-lim-pseudometric-completion-is-complete-Metric-Space x) - ( map-lim-pseudometric-completion-is-complete-Metric-Space y) + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space x) + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space y) ( lemma-saturated-neighborhood-map-lim) where neighborhood-const-lim-x-y : neighborhood-Pseudometric-Space - ( pseudometric-completion-Metric-Space M) + ( cauchy-pseudocompletion-Metric-Space M) ( d) ( const-cauchy-approximation-Metric-Space M - ( map-lim-pseudometric-completion-is-complete-Metric-Space x)) + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space x)) ( const-cauchy-approximation-Metric-Space M - ( map-lim-pseudometric-completion-is-complete-Metric-Space y)) + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space y)) neighborhood-const-lim-x-y = preserves-neighborhood-sim-Pseudometric-Space - ( pseudometric-completion-Metric-Space M) + ( cauchy-pseudocompletion-Metric-Space M) { x} { const-cauchy-approximation-Metric-Space ( M) - ( map-lim-pseudometric-completion-is-complete-Metric-Space x)} + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space x)} { y} { const-cauchy-approximation-Metric-Space ( M) - ( map-lim-pseudometric-completion-is-complete-Metric-Space y)} - ( sim-const-map-lim-pseudometric-completion-is-complete-Metric-Space + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space y)} + ( sim-const-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space ( x)) - ( sim-const-map-lim-pseudometric-completion-is-complete-Metric-Space + ( sim-const-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space ( y)) ( d) ( Nxy) @@ -391,47 +391,47 @@ module _ neighborhood-Metric-Space ( M) ( d +ℚ⁺ δ) - ( map-lim-pseudometric-completion-is-complete-Metric-Space x) - ( map-lim-pseudometric-completion-is-complete-Metric-Space y) + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space x) + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space y) lemma-saturated-neighborhood-map-lim δ = tr ( is-upper-bound-dist-Metric-Space ( M) - ( map-lim-pseudometric-completion-is-complete-Metric-Space x) - ( map-lim-pseudometric-completion-is-complete-Metric-Space y)) + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space x) + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space y)) ( ap (add-ℚ⁺' d) (eq-add-split-ℚ⁺ δ) ∙ commutative-add-ℚ⁺ δ d) ( neighborhood-const-lim-x-y ( left-summand-split-ℚ⁺ δ) ( right-summand-split-ℚ⁺ δ)) - short-map-lim-pseudometric-completion-is-complete-Metric-Space : + short-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space : short-function-Pseudometric-Space - ( pseudometric-completion-Metric-Space M) + ( cauchy-pseudocompletion-Metric-Space M) ( pseudometric-Metric-Space M) - short-map-lim-pseudometric-completion-is-complete-Metric-Space = - ( map-lim-pseudometric-completion-is-complete-Metric-Space , - is-short-map-lim-pseudometric-completion-is-complete-Metric-Space) + short-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space = + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space , + is-short-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space) - is-retraction-map-pseudometric-completion-is-complete-Metric-Space : - ( map-lim-pseudometric-completion-is-complete-Metric-Space ∘ - map-pseudometric-completion-Metric-Space M) ~ + is-retraction-map-cauchy-pseudocompletion-is-complete-Metric-Space : + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space ∘ + map-cauchy-pseudocompletion-Metric-Space M) ~ ( id) - is-retraction-map-pseudometric-completion-is-complete-Metric-Space = + is-retraction-map-cauchy-pseudocompletion-is-complete-Metric-Space = is-retraction-limit-cauchy-approximation-Complete-Metric-Space ( M , is-complete-M) - sim-map-lim-pseudometric-completion-is-complete-Metric-Space : + sim-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space : (u : cauchy-approximation-Metric-Space M) → sim-Pseudometric-Space - ( pseudometric-completion-Metric-Space M) + ( cauchy-pseudocompletion-Metric-Space M) ( u) - ( map-pseudometric-completion-Metric-Space + ( map-cauchy-pseudocompletion-Metric-Space ( M) - ( map-lim-pseudometric-completion-is-complete-Metric-Space u)) - sim-map-lim-pseudometric-completion-is-complete-Metric-Space u = + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u)) + sim-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u = sim-const-is-limit-cauchy-approximation-Metric-Space ( M) ( u) - ( map-lim-pseudometric-completion-is-complete-Metric-Space u) - ( is-limit-map-lim-pseudometric-completion-is-complete-Metric-Space u) + ( map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u) + ( is-limit-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u) ``` diff --git a/src/metric-spaces/pseudometric-completion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md similarity index 64% rename from src/metric-spaces/pseudometric-completion-of-pseudometric-spaces.lagda.md rename to src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md index e7489c92e25..02865c7c2b6 100644 --- a/src/metric-spaces/pseudometric-completion-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md @@ -1,9 +1,9 @@ -# The pseudometric completion of a pseudometric space +# The Cauchy pseudocompletion of a pseudometric space ```agda {-# OPTIONS --lossy-unification #-} -module metric-spaces.pseudometric-completion-of-pseudometric-spaces where +module metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces where ```
Imports @@ -46,7 +46,7 @@ open import metric-spaces.similarity-of-elements-pseudometric-spaces ## Idea The -{{#concept "pseudometric completion" Disambiguation="of a pseudometric space" Agda=pseudometric-completion-Pseudometric-Space}} +{{#concept "Cauchy pseudocompletion" Disambiguation="of a pseudometric space" Agda=cauchy-pseudocompletion-Pseudometric-Space}} of a [pseudometric space](metric-spaces.pseudometric-spaces.md) `M` is the pseudometric space of [Cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md) @@ -60,17 +60,17 @@ Any Cauchy approximation in the pseudometric completion has a ## Definition -### The pseudometric completion neighborhood relation on the type of Cauchy approximations in a pseudometric space +### The Cauchy pseudocompletion neighborhood relation on the type of Cauchy approximations in a pseudometric space ```agda module _ {l1 l2 : Level} (M : Pseudometric-Space l1 l2) where - neighborhood-prop-pseudometric-completion-Pseudometric-Space : + neighborhood-prop-cauchy-pseudocompletion-Pseudometric-Space : Rational-Neighborhood-Relation l2 (cauchy-approximation-Pseudometric-Space M) - neighborhood-prop-pseudometric-completion-Pseudometric-Space + neighborhood-prop-cauchy-pseudocompletion-Pseudometric-Space d x y = Π-Prop ( ℚ⁺) @@ -84,11 +84,11 @@ module _ ( map-cauchy-approximation-Pseudometric-Space M x δ) ( map-cauchy-approximation-Pseudometric-Space M y ε))) - neighborhood-pseudometric-completion-Pseudometric-Space : + neighborhood-cauchy-pseudocompletion-Pseudometric-Space : ℚ⁺ → Relation l2 (cauchy-approximation-Pseudometric-Space M) - neighborhood-pseudometric-completion-Pseudometric-Space d x y = + neighborhood-cauchy-pseudocompletion-Pseudometric-Space d x y = type-Prop - ( neighborhood-prop-pseudometric-completion-Pseudometric-Space + ( neighborhood-prop-cauchy-pseudocompletion-Pseudometric-Space ( d) ( x) ( y)) @@ -104,10 +104,10 @@ module _ where abstract - is-reflexive-neighborhood-pseudometric-completion-Pseudometric-Space : + is-reflexive-neighborhood-cauchy-pseudocompletion-Pseudometric-Space : (d : ℚ⁺) (x : cauchy-approximation-Pseudometric-Space M) → - neighborhood-pseudometric-completion-Pseudometric-Space M d x x - is-reflexive-neighborhood-pseudometric-completion-Pseudometric-Space + neighborhood-cauchy-pseudocompletion-Pseudometric-Space M d x x + is-reflexive-neighborhood-cauchy-pseudocompletion-Pseudometric-Space d x δ ε = let xδ = map-cauchy-approximation-Pseudometric-Space M x δ @@ -132,11 +132,11 @@ module _ where abstract - is-symmetric-neighborhood-pseudometric-completion-Pseudometric-Space : + is-symmetric-neighborhood-cauchy-pseudocompletion-Pseudometric-Space : (d : ℚ⁺) (x y : cauchy-approximation-Pseudometric-Space M) → - neighborhood-pseudometric-completion-Pseudometric-Space M d x y → - neighborhood-pseudometric-completion-Pseudometric-Space M d y x - is-symmetric-neighborhood-pseudometric-completion-Pseudometric-Space + neighborhood-cauchy-pseudocompletion-Pseudometric-Space M d x y → + neighborhood-cauchy-pseudocompletion-Pseudometric-Space M d y x + is-symmetric-neighborhood-cauchy-pseudocompletion-Pseudometric-Space d x y Ndxy δ ε = let xε = map-cauchy-approximation-Pseudometric-Space M x ε @@ -156,17 +156,17 @@ module _ where abstract - is-triangular-neighborhood-pseudometric-completion-Pseudometric-Space : + is-triangular-neighborhood-cauchy-pseudocompletion-Pseudometric-Space : (x y z : cauchy-approximation-Pseudometric-Space M) → (dxy dyz : ℚ⁺) → - neighborhood-pseudometric-completion-Pseudometric-Space M dyz y z → - neighborhood-pseudometric-completion-Pseudometric-Space M dxy x y → - neighborhood-pseudometric-completion-Pseudometric-Space + neighborhood-cauchy-pseudocompletion-Pseudometric-Space M dyz y z → + neighborhood-cauchy-pseudocompletion-Pseudometric-Space M dxy x y → + neighborhood-cauchy-pseudocompletion-Pseudometric-Space ( M) ( dxy +ℚ⁺ dyz) ( x) ( z) - is-triangular-neighborhood-pseudometric-completion-Pseudometric-Space + is-triangular-neighborhood-cauchy-pseudocompletion-Pseudometric-Space x y z dxy dyz Ndyz Ndxy δ ε = let xδ = map-cauchy-approximation-Pseudometric-Space M x δ @@ -248,16 +248,16 @@ module _ where abstract - is-saturated-neighborhood-pseudometric-completion-Pseudometric-Space : + is-saturated-neighborhood-cauchy-pseudocompletion-Pseudometric-Space : ( ε : ℚ⁺) (x y : cauchy-approximation-Pseudometric-Space M) → ( (δ : ℚ⁺) → - neighborhood-pseudometric-completion-Pseudometric-Space + neighborhood-cauchy-pseudocompletion-Pseudometric-Space ( M) ( ε +ℚ⁺ δ) ( x) ( y)) → - neighborhood-pseudometric-completion-Pseudometric-Space M ε x y - is-saturated-neighborhood-pseudometric-completion-Pseudometric-Space + neighborhood-cauchy-pseudocompletion-Pseudometric-Space M ε x y + is-saturated-neighborhood-cauchy-pseudocompletion-Pseudometric-Space d x y H δ ε = let xδ = map-cauchy-approximation-Pseudometric-Space M x δ @@ -274,60 +274,60 @@ module _ ( H θ δ ε)) ``` -### The pseudometric completion of a pseudometric space +### The Cauchy pseudocompletion of a pseudometric space ```agda module _ {l1 l2 : Level} (M : Pseudometric-Space l1 l2) where - pseudometric-completion-Pseudometric-Space : + cauchy-pseudocompletion-Pseudometric-Space : Pseudometric-Space (l1 ⊔ l2) l2 - pseudometric-completion-Pseudometric-Space = + cauchy-pseudocompletion-Pseudometric-Space = ( cauchy-approximation-Pseudometric-Space M , - neighborhood-prop-pseudometric-completion-Pseudometric-Space M , - is-reflexive-neighborhood-pseudometric-completion-Pseudometric-Space M , - is-symmetric-neighborhood-pseudometric-completion-Pseudometric-Space M , - is-triangular-neighborhood-pseudometric-completion-Pseudometric-Space M , - is-saturated-neighborhood-pseudometric-completion-Pseudometric-Space M) + neighborhood-prop-cauchy-pseudocompletion-Pseudometric-Space M , + is-reflexive-neighborhood-cauchy-pseudocompletion-Pseudometric-Space M , + is-symmetric-neighborhood-cauchy-pseudocompletion-Pseudometric-Space M , + is-triangular-neighborhood-cauchy-pseudocompletion-Pseudometric-Space M , + is-saturated-neighborhood-cauchy-pseudocompletion-Pseudometric-Space M) ``` -### The isometry from a pseudometric space to its pseudometric completion +### The isometry from a pseudometric space to its Cauchy pseudocompletion ```agda module _ {l1 l2 : Level} (M : Pseudometric-Space l1 l2) where - map-pseudometric-completion-Pseudometric-Space : + map-cauchy-pseudocompletion-Pseudometric-Space : type-Pseudometric-Space M → cauchy-approximation-Pseudometric-Space M - map-pseudometric-completion-Pseudometric-Space = + map-cauchy-pseudocompletion-Pseudometric-Space = const-cauchy-approximation-Pseudometric-Space M abstract - preserves-neighborhood-map-pseudometric-completion-Pseudometric-Space : + preserves-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space : (d : ℚ⁺) (x y : type-Pseudometric-Space M) → neighborhood-Pseudometric-Space M d x y → - neighborhood-pseudometric-completion-Pseudometric-Space + neighborhood-cauchy-pseudocompletion-Pseudometric-Space ( M) ( d) - ( map-pseudometric-completion-Pseudometric-Space x) - ( map-pseudometric-completion-Pseudometric-Space y) - preserves-neighborhood-map-pseudometric-completion-Pseudometric-Space + ( map-cauchy-pseudocompletion-Pseudometric-Space x) + ( map-cauchy-pseudocompletion-Pseudometric-Space y) + preserves-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space d x y Nxy δ ε = monotonic-neighborhood-Pseudometric-Space M x y d (δ +ℚ⁺ ε +ℚ⁺ d) ( le-right-add-ℚ⁺ (δ +ℚ⁺ ε) d) ( Nxy) - reflects-neighborhood-map-pseudometric-completion-Pseudometric-Space : + reflects-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space : (d : ℚ⁺) (x y : type-Pseudometric-Space M) → - neighborhood-pseudometric-completion-Pseudometric-Space + neighborhood-cauchy-pseudocompletion-Pseudometric-Space ( M) ( d) - ( map-pseudometric-completion-Pseudometric-Space x) - ( map-pseudometric-completion-Pseudometric-Space y) → + ( map-cauchy-pseudocompletion-Pseudometric-Space x) + ( map-cauchy-pseudocompletion-Pseudometric-Space y) → neighborhood-Pseudometric-Space M d x y - reflects-neighborhood-map-pseudometric-completion-Pseudometric-Space + reflects-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space d x y Nxy = saturated-neighborhood-Pseudometric-Space M d x y ( λ δ → @@ -339,41 +339,41 @@ module _ ( commutative-add-ℚ⁺ _ _ ∙ ap (d +ℚ⁺_) δ₁+δ₂=δ) ( Nxy δ₁ δ₂)) - is-isometry-map-pseudometric-completion-Pseudometric-Space : + is-isometry-map-cauchy-pseudocompletion-Pseudometric-Space : is-isometry-Pseudometric-Space ( M) - ( pseudometric-completion-Pseudometric-Space M) - ( map-pseudometric-completion-Pseudometric-Space) - is-isometry-map-pseudometric-completion-Pseudometric-Space d x y = - ( ( preserves-neighborhood-map-pseudometric-completion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( map-cauchy-pseudocompletion-Pseudometric-Space) + is-isometry-map-cauchy-pseudocompletion-Pseudometric-Space d x y = + ( ( preserves-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space ( d) ( x) ( y)) , - (reflects-neighborhood-map-pseudometric-completion-Pseudometric-Space + (reflects-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space ( d) ( x) ( y))) - isometry-pseudometric-completion-Pseudometric-Space : + isometry-cauchy-pseudocompletion-Pseudometric-Space : isometry-Pseudometric-Space ( M) - ( pseudometric-completion-Pseudometric-Space M) - isometry-pseudometric-completion-Pseudometric-Space = - ( map-pseudometric-completion-Pseudometric-Space , - is-isometry-map-pseudometric-completion-Pseudometric-Space) + ( cauchy-pseudocompletion-Pseudometric-Space M) + isometry-cauchy-pseudocompletion-Pseudometric-Space = + ( map-cauchy-pseudocompletion-Pseudometric-Space , + is-isometry-map-cauchy-pseudocompletion-Pseudometric-Space) - short-map-pseudometric-completion-Pseudometric-Space : + short-map-cauchy-pseudocompletion-Pseudometric-Space : short-function-Pseudometric-Space ( M) - ( pseudometric-completion-Pseudometric-Space M) - short-map-pseudometric-completion-Pseudometric-Space = + ( cauchy-pseudocompletion-Pseudometric-Space M) + short-map-cauchy-pseudocompletion-Pseudometric-Space = short-isometry-Pseudometric-Space ( M) - ( pseudometric-completion-Pseudometric-Space M) - ( isometry-pseudometric-completion-Pseudometric-Space) + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( isometry-cauchy-pseudocompletion-Pseudometric-Space) ``` -### Convergent Cauchy approximations are similar to constant Cauchy approximations in the pseudometric completion +### Convergent Cauchy approximations are similar to constant Cauchy approximations in the Cauchy pseudocompletion ```agda module _ @@ -386,7 +386,7 @@ module _ sim-const-is-limit-cauchy-approximation-Pseudometric-Space : is-limit-cauchy-approximation-Pseudometric-Space M u x → sim-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) + ( cauchy-pseudocompletion-Pseudometric-Space M) ( u) ( const-cauchy-approximation-Pseudometric-Space M x) sim-const-is-limit-cauchy-approximation-Pseudometric-Space H d α β = @@ -401,7 +401,7 @@ module _ is-limit-sim-const-cauchy-approximation-Pseudometric-Space : sim-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) + ( cauchy-pseudocompletion-Pseudometric-Space M) ( u) ( const-cauchy-approximation-Pseudometric-Space M x) → is-limit-cauchy-approximation-Pseudometric-Space M u x @@ -414,55 +414,55 @@ module _ ( λ d → H d α β) ``` -### Any Cauchy approximation in the pseudometric completion of a pseudometric space has a limit +### Any Cauchy approximation in the Cauchy pseudocompletion of a pseudometric space has a limit ```agda module _ { l1 l2 : Level} (M : Pseudometric-Space l1 l2) ( U : cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M)) + ( cauchy-pseudocompletion-Pseudometric-Space M)) where - map-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : ℚ⁺ → ℚ⁺ → type-Pseudometric-Space M - map-cauchy-approximation-pseudometric-completion-Pseudometric-Space ε = + map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ε = map-cauchy-approximation-Pseudometric-Space M ( map-cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) + ( cauchy-pseudocompletion-Pseudometric-Space M) ( U) ( ε)) - is-cauchy-map-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + is-cauchy-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : (δ ε d₁ d₂ : ℚ⁺) → neighborhood-Pseudometric-Space ( M) ( d₁ +ℚ⁺ d₂ +ℚ⁺ (δ +ℚ⁺ ε)) - ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( δ) ( d₁)) - ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( ε) ( d₂)) - is-cauchy-map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + is-cauchy-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space = is-cauchy-approximation-map-cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) + ( cauchy-pseudocompletion-Pseudometric-Space M) ( U) - map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : ℚ⁺ → type-Pseudometric-Space M - map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space d = + map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space d = let (d₁ , d₂ , _) = split-ℚ⁺ d in - map-cauchy-approximation-pseudometric-completion-Pseudometric-Space d₂ d₁ + map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space d₂ d₁ - is-cauchy-map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + is-cauchy-map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : is-cauchy-approximation-Pseudometric-Space ( M) - ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space) - is-cauchy-map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space) + is-cauchy-map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space δ ε = let (δ₁ , δ₂ , δ₁+δ₂=δ) = split-ℚ⁺ δ @@ -484,26 +484,26 @@ module _ tr ( is-upper-bound-dist-Pseudometric-Space ( M) - ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( δ)) - ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( ε))) ( lemma-δ+ε) - ( is-cauchy-map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( is-cauchy-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space _ _ _ _) - lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : cauchy-approximation-Pseudometric-Space M - lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space = - ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space , - is-cauchy-map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space) + lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space = + ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space , + is-cauchy-map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space) - is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : is-limit-cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) + ( cauchy-pseudocompletion-Pseudometric-Space M) ( U) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space) - is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space) + is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space δ ε η θ = let (θ₁ , θ₂ , θ₁+θ₂=θ) = split-ℚ⁺ θ @@ -524,54 +524,54 @@ module _ lemma-lim : neighborhood-Pseudometric-Space M ( η +ℚ⁺ θ +ℚ⁺ δ) - ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( δ) ( η)) - ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( θ₂) ( θ₁)) lemma-lim = tr ( is-upper-bound-dist-Pseudometric-Space M - ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( δ) ( η)) - ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( θ))) ( lemma-η+θ+δ) - ( is-cauchy-map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( is-cauchy-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space _ _ _ _) in tr ( is-upper-bound-dist-Pseudometric-Space M - ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( δ) ( η)) - ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( θ))) ( associative-add-ℚ⁺ ( η +ℚ⁺ θ) ( δ) ( ε)) ( monotonic-neighborhood-Pseudometric-Space M - ( map-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( δ) ( η)) - ( map-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( θ)) ( η +ℚ⁺ θ +ℚ⁺ δ) ( η +ℚ⁺ θ +ℚ⁺ δ +ℚ⁺ ε) ( le-left-add-ℚ⁺ ( η +ℚ⁺ θ +ℚ⁺ δ) ε) ( lemma-lim)) - has-limit-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + has-limit-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : Σ ( cauchy-approximation-Pseudometric-Space M) ( is-limit-cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) + ( cauchy-pseudocompletion-Pseudometric-Space M) ( U)) - has-limit-cauchy-approximation-pseudometric-completion-Pseudometric-Space = - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space , - is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space) + has-limit-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space = + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space , + is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space) ``` ### The map from a Cauchy approximation in the pseudometric completion to its limit is an isometry @@ -582,151 +582,151 @@ module _ ( d : ℚ⁺) ( u v : cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M)) + ( cauchy-pseudocompletion-Pseudometric-Space M)) where abstract - preserves-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + preserves-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : neighborhood-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M)) + ( cauchy-pseudocompletion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M)) ( d) ( u) ( v) → neighborhood-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) + ( cauchy-pseudocompletion-Pseudometric-Space M) ( d) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( u)) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( v)) - preserves-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + preserves-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space Nuv = let neighborhood-const-lim : neighborhood-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M)) + ( cauchy-pseudocompletion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M)) ( d) ( const-cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( u))) ( const-cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( v))) neighborhood-const-lim = preserves-neighborhood-sim-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M)) + ( cauchy-pseudocompletion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M)) { u} { const-cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( u))} { v} { const-cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( v))} ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) + ( cauchy-pseudocompletion-Pseudometric-Space M) ( u) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( u)) - ( is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( u))) ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) + ( cauchy-pseudocompletion-Pseudometric-Space M) ( v) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( v)) - ( is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( v))) ( d) ( Nuv) in - reflects-neighborhood-map-pseudometric-completion-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) + reflects-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) ( d) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( u)) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( v)) ( neighborhood-const-lim) - reflects-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + reflects-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : neighborhood-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) + ( cauchy-pseudocompletion-Pseudometric-Space M) ( d) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( u)) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( v)) → neighborhood-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M)) + ( cauchy-pseudocompletion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M)) ( d) ( u) ( v) - reflects-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + reflects-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space N-lim = reflects-neighborhood-sim-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M)) + ( cauchy-pseudocompletion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M)) { u} { const-cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( u))} { v} { const-cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( v))} ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) + ( cauchy-pseudocompletion-Pseudometric-Space M) ( u) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( u)) - ( is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( u))) ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) + ( cauchy-pseudocompletion-Pseudometric-Space M) ( v) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( v)) - ( is-limit-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( v))) ( d) - ( preserves-neighborhood-map-pseudometric-completion-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M) + ( preserves-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) ( d) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( u)) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( v)) ( N-lim)) @@ -736,31 +736,31 @@ module _ where abstract - is-isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + is-isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : is-isometry-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M)) - ( pseudometric-completion-Pseudometric-Space M) - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space M) - is-isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M)) + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M) + is-isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space d x y = - ( ( preserves-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( ( preserves-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( d) ( x) ( y)) , - ( reflects-neighborhood-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space + ( reflects-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( d) ( x) ( y))) - isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space : + isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : isometry-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space - ( pseudometric-completion-Pseudometric-Space M)) - ( pseudometric-completion-Pseudometric-Space M) - isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space = - ( lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space M , - is-isometry-lim-cauchy-approximation-pseudometric-completion-Pseudometric-Space) + ( cauchy-pseudocompletion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M)) + ( cauchy-pseudocompletion-Pseudometric-Space M) + isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space = + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M , + is-isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space) ``` From 67459a34255ab36589d6ee650ce08bc10d632a5f Mon Sep 17 00:00:00 2001 From: malarbol Date: Wed, 22 Oct 2025 17:13:30 +0200 Subject: [PATCH 08/28] Update src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- .../cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md index 02865c7c2b6..920677aa16a 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md @@ -55,7 +55,7 @@ in `M` where two Cauchy approximations `x` and `y` are in a another if for all `δ ε : ℚ⁺`, `x δ` and `y ε` are in a `(δ + ε + d)`-neighborhood of one another in `M`. -Any Cauchy approximation in the pseudometric completion has a +Any Cauchy approximation in the Cauchy pseudocompletion has a [limit](metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces.md). ## Definition From de635f3c7a141625ae9a48150199a3ef9565c437 Mon Sep 17 00:00:00 2001 From: malarbol Date: Wed, 22 Oct 2025 17:13:46 +0200 Subject: [PATCH 09/28] Update src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- ...completion-of-pseudometric-spaces.lagda.md | 26 +++++++++---------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md index 920677aa16a..f97cecfa18d 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md @@ -259,19 +259,19 @@ module _ neighborhood-cauchy-pseudocompletion-Pseudometric-Space M ε x y is-saturated-neighborhood-cauchy-pseudocompletion-Pseudometric-Space d x y H δ ε = - let - xδ = map-cauchy-approximation-Pseudometric-Space M x δ - yε = map-cauchy-approximation-Pseudometric-Space M y ε - in - saturated-neighborhood-Pseudometric-Space M - ( δ +ℚ⁺ ε +ℚ⁺ d) - ( xδ) - ( yε) - ( λ θ → - tr - ( λ η → neighborhood-Pseudometric-Space M η xδ yε) - ( inv (associative-add-ℚ⁺ _ _ _)) - ( H θ δ ε)) + let + xδ = map-cauchy-approximation-Pseudometric-Space M x δ + yε = map-cauchy-approximation-Pseudometric-Space M y ε + in + saturated-neighborhood-Pseudometric-Space M + ( δ +ℚ⁺ ε +ℚ⁺ d) + ( xδ) + ( yε) + ( λ θ → + tr + ( λ η → neighborhood-Pseudometric-Space M η xδ yε) + ( inv (associative-add-ℚ⁺ _ _ _)) + ( H θ δ ε)) ``` ### The Cauchy pseudocompletion of a pseudometric space From 562a5e5a49ed691ea89738933a69f43de12e458d Mon Sep 17 00:00:00 2001 From: malarbol Date: Wed, 22 Oct 2025 17:14:17 +0200 Subject: [PATCH 10/28] Update src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- .../cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md index f97cecfa18d..044c7c7321d 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md @@ -582,7 +582,7 @@ module _ ( d : ℚ⁺) ( u v : cauchy-approximation-Pseudometric-Space - ( cauchy-pseudocompletion-Pseudometric-Space M)) + ( cauchy-pseudocompletion-Pseudometric-Space M)) where abstract From 6b9a0a441757f8e07b94b90d2841103ead7b93ef Mon Sep 17 00:00:00 2001 From: malarbol Date: Wed, 22 Oct 2025 18:23:56 +0200 Subject: [PATCH 11/28] refactor --- ...completion-of-pseudometric-spaces.lagda.md | 203 +++++++++--------- 1 file changed, 105 insertions(+), 98 deletions(-) diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md index 044c7c7321d..d42d011eac9 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md @@ -574,26 +574,89 @@ module _ is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space) ``` -### The map from a Cauchy approximation in the pseudometric completion to its limit is an isometry +### Any Cauchy approximation in the pseudometric completion is similar to the constant Cauchy approximation of its limit ```agda module _ { l1 l2 : Level} (M : Pseudometric-Space l1 l2) - ( d : ℚ⁺) - ( u v : + ( u : cauchy-approximation-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space M)) where + sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : + sim-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M)) + ( u) + ( const-cauchy-approximation-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space + ( M) + ( u))) + sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space + = + sim-const-is-limit-cauchy-approximation-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( u) + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M u) + ( is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space + ( M) + ( u)) +``` + +### The map from a Cauchy approximation in the pseudometric completion to its limit is short + +```agda +module _ + { l1 l2 : Level} (M : Pseudometric-Space l1 l2) + where + abstract - preserves-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : - neighborhood-Pseudometric-Space + is-short-function-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : + is-short-function-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M)) + ( cauchy-pseudocompletion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M)) + ( ( const-cauchy-approximation-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M)) ∘ + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space + ( M))) + is-short-function-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space + d u v = + preserves-neighborhood-sim-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space M)) + { u} + { const-cauchy-approximation-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space + ( M) + ( u))} + { v} + { const-cauchy-approximation-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space + ( M) + ( v))} + ( sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space + ( M) + ( u)) + ( sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space + ( M) + ( v)) ( d) - ( u) - ( v) → - neighborhood-Pseudometric-Space + + is-short-function-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space : + is-short-function-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M)) + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M) + is-short-function-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space + d u v Nuv = + reflects-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space M) ( d) ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space @@ -602,73 +665,35 @@ module _ ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( v)) - preserves-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space - Nuv = - let - neighborhood-const-lim : - neighborhood-Pseudometric-Space - ( cauchy-pseudocompletion-Pseudometric-Space - ( cauchy-pseudocompletion-Pseudometric-Space M)) - ( d) - ( const-cauchy-approximation-Pseudometric-Space - ( cauchy-pseudocompletion-Pseudometric-Space M) - ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space - ( M) - ( u))) - ( const-cauchy-approximation-Pseudometric-Space - ( cauchy-pseudocompletion-Pseudometric-Space M) - ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space - ( M) - ( v))) - neighborhood-const-lim = - preserves-neighborhood-sim-Pseudometric-Space - ( cauchy-pseudocompletion-Pseudometric-Space - ( cauchy-pseudocompletion-Pseudometric-Space M)) - { u} - { const-cauchy-approximation-Pseudometric-Space - ( cauchy-pseudocompletion-Pseudometric-Space M) - ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space - ( M) - ( u))} - { v} - { const-cauchy-approximation-Pseudometric-Space - ( cauchy-pseudocompletion-Pseudometric-Space M) - ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space - ( M) - ( v))} - ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space - ( cauchy-pseudocompletion-Pseudometric-Space M) - ( u) - ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space - ( M) - ( u)) - ( is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space - ( M) - ( u))) - ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space - ( cauchy-pseudocompletion-Pseudometric-Space M) - ( v) - ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space - ( M) - ( v)) - ( is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space - ( M) - ( v))) - ( d) - ( Nuv) - in - reflects-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space - ( cauchy-pseudocompletion-Pseudometric-Space M) + ( is-short-function-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( d) - ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space - ( M) - ( u)) - ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space - ( M) - ( v)) - ( neighborhood-const-lim) + ( u) + ( v) + ( Nuv)) + short-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space : + short-function-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M)) + ( cauchy-pseudocompletion-Pseudometric-Space M) + short-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space = + ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M , + is-short-function-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space) +``` + +### The map from a Cauchy approximation in the pseudometric completion to its limit is an isometry + +```agda +module _ + { l1 l2 : Level} (M : Pseudometric-Space l1 l2) + where + + abstract reflects-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : + ( d : ℚ⁺) → + ( u v : + cauchy-approximation-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M)) → neighborhood-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space M) ( d) @@ -685,7 +710,7 @@ module _ ( u) ( v) reflects-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space - N-lim = + d u v N-lim = reflects-neighborhood-sim-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space M)) @@ -701,24 +726,12 @@ module _ ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( M) ( v))} - ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space - ( cauchy-pseudocompletion-Pseudometric-Space M) - ( u) - ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space - ( M) - ( u)) - ( is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space - ( M) - ( u))) - ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space - ( cauchy-pseudocompletion-Pseudometric-Space M) - ( v) - ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space - ( M) - ( v)) - ( is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space - ( M) - ( v))) + ( sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space + ( M) + ( u)) + ( sim-const-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space + ( M) + ( v)) ( d) ( preserves-neighborhood-map-cauchy-pseudocompletion-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space M) @@ -731,11 +744,6 @@ module _ ( v)) ( N-lim)) -module _ - {l1 l2 : Level} (M : Pseudometric-Space l1 l2) - where - - abstract is-isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : is-isometry-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space @@ -744,13 +752,12 @@ module _ ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M) is-isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space d x y = - ( ( preserves-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space + ( ( is-short-function-lim-cauchy-approximation-pseudocompletion-Pseudometric-Space ( M) ( d) ( x) ( y)) , ( reflects-neighborhood-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space - ( M) ( d) ( x) ( y))) From a03ef036b52d7423077600f45bfe22180a2a6920 Mon Sep 17 00:00:00 2001 From: malarbol Date: Wed, 22 Oct 2025 18:33:21 +0200 Subject: [PATCH 12/28] Update src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- .../cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md index d42d011eac9..553eaa9effe 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md @@ -693,7 +693,7 @@ module _ ( d : ℚ⁺) → ( u v : cauchy-approximation-Pseudometric-Space - ( cauchy-pseudocompletion-Pseudometric-Space M)) → + ( cauchy-pseudocompletion-Pseudometric-Space M)) → neighborhood-Pseudometric-Space ( cauchy-pseudocompletion-Pseudometric-Space M) ( d) From b9fb2faa365570812fbc10a5f34eade264c3b1ee Mon Sep 17 00:00:00 2001 From: malarbol Date: Wed, 22 Oct 2025 18:33:46 +0200 Subject: [PATCH 13/28] Update src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- .../cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md index 553eaa9effe..003c2b0a8eb 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md @@ -609,7 +609,7 @@ module _ ```agda module _ - { l1 l2 : Level} (M : Pseudometric-Space l1 l2) + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) where abstract From f67f034c42630a164ce50a11a08b3ba7fd48c2e7 Mon Sep 17 00:00:00 2001 From: malarbol Date: Wed, 22 Oct 2025 18:34:00 +0200 Subject: [PATCH 14/28] Update src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- .../cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md index 003c2b0a8eb..567d81f9b0a 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md @@ -685,7 +685,7 @@ module _ ```agda module _ - { l1 l2 : Level} (M : Pseudometric-Space l1 l2) + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) where abstract From 332df19de3a53d500d88209f2377dc0c249aff92 Mon Sep 17 00:00:00 2001 From: malarbol Date: Wed, 22 Oct 2025 20:00:15 +0200 Subject: [PATCH 15/28] metric quotients & Cauchy approximations --- src/metric-spaces.lagda.md | 2 + ...-quotients-of-pseudometric-spaces.lagda.md | 312 +++++++ ...-quotients-of-pseudometric-spaces.lagda.md | 835 ++++++++++++++++++ 3 files changed, 1149 insertions(+) create mode 100644 src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md create mode 100644 src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md index 76d05aabeea..4dd23a4e057 100644 --- a/src/metric-spaces.lagda.md +++ b/src/metric-spaces.lagda.md @@ -62,6 +62,7 @@ open import metric-spaces.bounded-distance-decompositions-of-metric-spaces publi 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-metric-quotients-of-pseudometric-spaces public open import metric-spaces.cauchy-approximations-metric-spaces public open import metric-spaces.cauchy-approximations-pseudometric-spaces public open import metric-spaces.cauchy-pseudocompletion-of-metric-spaces public @@ -103,6 +104,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-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 open import metric-spaces.metric-space-of-convergent-cauchy-approximations-metric-spaces public diff --git a/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md new file mode 100644 index 00000000000..b5aab9bcb3e --- /dev/null +++ b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md @@ -0,0 +1,312 @@ +# Cauchy approximations in metric quotients of pseudometric spaces + +```agda +{-# OPTIONS --lossy-unification #-} + +module metric-spaces.cauchy-approximations-metric-quotients-of-pseudometric-spaces where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.positive-rational-numbers + +open import foundation.action-on-identifications-functions +open import foundation.binary-relations +open import foundation.binary-transport +open import foundation.contractible-maps +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.equivalence-classes +open import foundation.equivalences +open import foundation.existential-quantification +open import foundation.fibers-of-maps +open import foundation.function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.inhabited-subtypes +open import foundation.logical-equivalences +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.reflecting-maps-equivalence-relations +open import foundation.retractions +open import foundation.sections +open import foundation.set-quotients +open import foundation.sets +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universal-property-set-quotients +open import foundation.universe-levels + +open import logic.functoriality-existential-quantification + +open import metric-spaces.cauchy-approximations-metric-spaces +open import metric-spaces.cauchy-approximations-pseudometric-spaces +open import metric-spaces.cauchy-pseudocompletion-of-metric-spaces +open import metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces +open import metric-spaces.convergent-cauchy-approximations-metric-spaces +open import metric-spaces.equality-of-metric-spaces +open import metric-spaces.extensionality-pseudometric-spaces +open import metric-spaces.functions-metric-spaces +open import metric-spaces.isometries-metric-spaces +open import metric-spaces.isometries-pseudometric-spaces +open import metric-spaces.limits-of-cauchy-approximations-metric-spaces +open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces +open import metric-spaces.metric-quotients-of-pseudometric-spaces +open import metric-spaces.metric-spaces +open import metric-spaces.pseudometric-spaces +open import metric-spaces.rational-neighborhood-relations +open import metric-spaces.short-functions-metric-spaces +open import metric-spaces.short-functions-pseudometric-spaces +open import metric-spaces.similarity-of-elements-pseudometric-spaces +``` + +
+ +## Idea + +The pointwise [quotients](foundation.set-quotients.md) of +[Cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md) +by the +[similarity relation](metric-spaces.similarity-of-elements-pseudometric-spaces.md) +of the [pseudometric space](metric-spaces.pseudometric-spaces.md) are Cauchy +approximations in the +[metric quotient](metric-spaces.metric-quotients-of-pseudometric-spaces.md). A +Cauchy approximation in a the metric quotient of a pseudometric space has a +{{#concept "lift up to similarity" Agda=has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space}} +if it is similar (in the +[Cauchy pseudocompletion](metric-spaces.cauchy-pseudocompletion-of-metric-spaces.md) +of the metric quotient) to the pointwise quotient of +[some](foundation.existential-quantification.md) Cauchy approximation in the +pseudometric space. + +The pointwise quotient of Cauchy approximations preserves +[limits](metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces.md). +The pointwise quotient of a Cauchy approximation has a lift. A Cauchy +approximation that admits a +[limit](metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces.md) +has a lift. + +## Definitions + +### The pointwise quotient Cauchy approximation of a Cauchy approximation in a pseudometric space + +```agda +module _ + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) + where + + map-metric-quotient-cauchy-approximation-Pseudometric-Space : + cauchy-approximation-Pseudometric-Space M → + cauchy-approximation-Metric-Space + ( metric-quotient-Pseudometric-Space M) + map-metric-quotient-cauchy-approximation-Pseudometric-Space = + map-short-function-cauchy-approximation-Pseudometric-Space + ( M) + ( pseudometric-metric-quotient-Pseudometric-Space M) + ( short-map-metric-quotient-Pseudometric-Space M) +``` + +### Lifts of Cauchy approximations in the quotient metric space up to similarity + +```agda +module _ + { l1 l2 : Level} (A : Pseudometric-Space l1 l2) + ( u : + cauchy-approximation-Metric-Space + ( metric-quotient-Pseudometric-Space A)) + ( v : cauchy-approximation-Pseudometric-Space A) + where + + is-lift-quotient-prop-cauchy-approximation-Pseudometric-Space : + Prop (l1 ⊔ l2) + is-lift-quotient-prop-cauchy-approximation-Pseudometric-Space = + sim-prop-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space + ( pseudometric-metric-quotient-Pseudometric-Space A)) + ( u) + ( map-metric-quotient-cauchy-approximation-Pseudometric-Space A v) + + is-lift-quotient-cauchy-approximation-Pseudometric-Space : UU (l1 ⊔ l2) + is-lift-quotient-cauchy-approximation-Pseudometric-Space = + type-Prop is-lift-quotient-prop-cauchy-approximation-Pseudometric-Space + + is-prop-is-lift-quotient-cauchy-approximation-Pseudometric-Space : + is-prop is-lift-quotient-cauchy-approximation-Pseudometric-Space + is-prop-is-lift-quotient-cauchy-approximation-Pseudometric-Space = + is-prop-type-Prop + is-lift-quotient-prop-cauchy-approximation-Pseudometric-Space + +module _ + {l1 l2 : Level} (A : Pseudometric-Space l1 l2) + ( u : + cauchy-approximation-Metric-Space + ( metric-quotient-Pseudometric-Space A)) + where + + has-lift-prop-cauchy-approximation-metric-quotient-Pseudometric-Space : + Prop (l1 ⊔ l2) + has-lift-prop-cauchy-approximation-metric-quotient-Pseudometric-Space = + ∃ ( cauchy-approximation-Pseudometric-Space A) + ( is-lift-quotient-prop-cauchy-approximation-Pseudometric-Space A u) + + has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space : + UU (l1 ⊔ l2) + has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space = + type-Prop + has-lift-prop-cauchy-approximation-metric-quotient-Pseudometric-Space + + is-prop-has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space : + is-prop has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space + is-prop-has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space = + is-prop-type-Prop + has-lift-prop-cauchy-approximation-metric-quotient-Pseudometric-Space +``` + +## Properties + +### The pointwise quotient of Cauchy approximations in the quotient metric space preserves limits + +```agda +module _ + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) + (u : cauchy-approximation-Pseudometric-Space M) + (lim : type-Pseudometric-Space M) + (is-lim : + is-limit-cauchy-approximation-Pseudometric-Space M u lim) + where + + preserves-limit-map-metric-quotient-cauchy-approximation-Pseudometric-Space : + is-limit-cauchy-approximation-Metric-Space + ( metric-quotient-Pseudometric-Space M) + ( map-metric-quotient-cauchy-approximation-Pseudometric-Space M u) + ( map-metric-quotient-Pseudometric-Space M lim) + preserves-limit-map-metric-quotient-cauchy-approximation-Pseudometric-Space + ε δ (x , x∈uε) (y , y∈lim) = + let + lim~y : sim-Pseudometric-Space M lim y + lim~y = + sim-is-in-equivalence-class-quotient-map-set-quotient + ( equivalence-relation-sim-Pseudometric-Space M) + ( lim) + ( y) + ( y∈lim) + + uε~x : + sim-Pseudometric-Space M + ( map-cauchy-approximation-Pseudometric-Space M u ε) + ( x) + uε~x = + sim-is-in-equivalence-class-quotient-map-set-quotient + ( equivalence-relation-sim-Pseudometric-Space M) + ( map-cauchy-approximation-Pseudometric-Space M u ε) + ( x) + ( x∈uε) + in + preserves-neighborhood-sim-Pseudometric-Space + ( M) + ( uε~x) + ( lim~y) + ( ε +ℚ⁺ δ) + ( is-lim ε δ) +``` + +### Pointwise quotients of Cauchy approximations have lifts + +```agda +module _ + {l1 l2 : Level} (A : Pseudometric-Space l1 l2) + (u : cauchy-approximation-Pseudometric-Space A) + where + + has-lift-map-quotient-cauchy-approximation-metric-quotient-Pseudometric-Space : + has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space + ( A) + ( map-metric-quotient-cauchy-approximation-Pseudometric-Space A u) + has-lift-map-quotient-cauchy-approximation-metric-quotient-Pseudometric-Space = + unit-trunc-Prop + ( u , + refl-sim-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space + ( pseudometric-metric-quotient-Pseudometric-Space A)) + ( map-metric-quotient-cauchy-approximation-Pseudometric-Space A u)) +``` + +### Convergent Cauchy approximations in the quotient metric space have a lift up to similarity + +```agda +module _ + {l1 l2 : Level} (A : Pseudometric-Space l1 l2) + ( u : + cauchy-approximation-Metric-Space + ( metric-quotient-Pseudometric-Space A)) + ( lim : type-Metric-Space (metric-quotient-Pseudometric-Space A)) + ( is-lim : + is-limit-cauchy-approximation-Metric-Space + ( metric-quotient-Pseudometric-Space A) + ( u) + ( lim)) + where + + lemma-sim-lift-is-limit-cauchy-approximation-metric-quotient-Pseudometric-Space : + (x : type-Pseudometric-Space A) → + (is-in-class-metric-quotient-Pseudometric-Space A lim x) → + is-lift-quotient-cauchy-approximation-Pseudometric-Space + ( A) + ( u) + ( const-cauchy-approximation-Pseudometric-Space A x) + lemma-sim-lift-is-limit-cauchy-approximation-metric-quotient-Pseudometric-Space + x x∈lim = + transitive-sim-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space + ( pseudometric-metric-quotient-Pseudometric-Space A)) + ( u) + ( const-cauchy-approximation-Pseudometric-Space + ( pseudometric-metric-quotient-Pseudometric-Space A) + ( lim)) + ( const-cauchy-approximation-Pseudometric-Space + ( pseudometric-metric-quotient-Pseudometric-Space A) + ( map-metric-quotient-Pseudometric-Space A x)) + ( λ d α β → + sim-eq-Pseudometric-Space + ( pseudometric-metric-quotient-Pseudometric-Space A) + ( lim) + ( map-metric-quotient-Pseudometric-Space A x) + ( inv + ( eq-set-quotient-equivalence-class-set-quotient + ( equivalence-relation-sim-Pseudometric-Space A) + ( lim) + ( x∈lim))) + ( α +ℚ⁺ β +ℚ⁺ d)) + ( sim-const-is-limit-cauchy-approximation-Pseudometric-Space + ( pseudometric-metric-quotient-Pseudometric-Space A) + ( u) + ( lim) + ( is-lim)) + +module _ + {l1 l2 : Level} (A : Pseudometric-Space l1 l2) + ( u : + cauchy-approximation-Metric-Space + ( metric-quotient-Pseudometric-Space A)) + where + + has-lift-is-convergent-cauchy-approximation-metric-quotient-Pseudometric-Space : + is-convergent-cauchy-approximation-Metric-Space + ( metric-quotient-Pseudometric-Space A) + ( u) → + has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space A u + has-lift-is-convergent-cauchy-approximation-metric-quotient-Pseudometric-Space + (lim , is-lim) = + map-exists + ( is-lift-quotient-cauchy-approximation-Pseudometric-Space A u) + ( const-cauchy-approximation-Pseudometric-Space A) + ( lemma-sim-lift-is-limit-cauchy-approximation-metric-quotient-Pseudometric-Space + ( A) + ( u) + ( lim) + ( is-lim)) + ( is-inhabited-class-metric-quotient-Pseudometric-Space A lim) +``` diff --git a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md new file mode 100644 index 00000000000..77ec63a143d --- /dev/null +++ b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md @@ -0,0 +1,835 @@ +# Metric quotients of pseudometric spaces + +```agda +{-# OPTIONS --lossy-unification #-} + +module metric-spaces.metric-quotients-of-pseudometric-spaces where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.positive-rational-numbers + +open import foundation.action-on-identifications-functions +open import foundation.binary-relations +open import foundation.binary-transport +open import foundation.contractible-maps +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.equivalence-classes +open import foundation.equivalences +open import foundation.existential-quantification +open import foundation.fibers-of-maps +open import foundation.function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.inhabited-subtypes +open import foundation.logical-equivalences +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.reflecting-maps-equivalence-relations +open import foundation.retractions +open import foundation.sections +open import foundation.set-quotients +open import foundation.sets +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universal-property-set-quotients +open import foundation.universe-levels + +open import logic.functoriality-existential-quantification + +open import metric-spaces.cauchy-approximations-metric-spaces +open import metric-spaces.cauchy-approximations-pseudometric-spaces +open import metric-spaces.convergent-cauchy-approximations-metric-spaces +open import metric-spaces.equality-of-metric-spaces +open import metric-spaces.extensionality-pseudometric-spaces +open import metric-spaces.functions-metric-spaces +open import metric-spaces.isometries-metric-spaces +open import metric-spaces.isometries-pseudometric-spaces +open import metric-spaces.limits-of-cauchy-approximations-metric-spaces +open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces +open import metric-spaces.metric-spaces +open import metric-spaces.pseudometric-spaces +open import metric-spaces.rational-neighborhood-relations +open import metric-spaces.short-functions-metric-spaces +open import metric-spaces.short-functions-pseudometric-spaces +open import metric-spaces.similarity-of-elements-pseudometric-spaces +``` + +
+ +## Idea + +The +{{#concept "metric quotient" Disambiguation="of a pseudometric space" Agda=metric-quotient-Pseudometric-Space}} +of a [pseudometric space](metric-spaces.pseudometric-spaces.md) is the +[metric space](metric-spaces.metric-spaces.md) whose points are +[quotient classes](foundation.set-quotients.md) of `M` by the +[similarity relation](metric-spaces.similarity-of-elements-pseudometric-spaces.md) +and [neighborhoods](metric-spaces.rational-neighborhood-relations.md) given by +neighborhoods of inhabitants of the quotient classes: two quotient classes `X`, +`Y` are in a `d`-neighborhood if for all `x ∈ X` and `y ∈ Y`, `x` and `y` are +`d`-neighbors in the pseudometric space. + +Any pseudometric space `M` has an +[isometry](metric-spaces.isometries-pseudometric-spaces.md) into its metric +quotient; if `M` is a metric space, this is an +[isometric equivalence](metric-spaces.equality-of-metric-spaces.md). + +Any [short map](metric-spaces.short-functions-pseudometric-spaces.md) (resp. +isometry) from a pseudometric space to a metric space factors through the metric +quotient of its domain. + +## Definitions + +```agda +module _ + {l1 l2 : Level} + (M : Pseudometric-Space l1 l2) + where + + set-metric-quotient-Pseudometric-Space : Set (l1 ⊔ l2) + set-metric-quotient-Pseudometric-Space = + quotient-Set (equivalence-relation-sim-Pseudometric-Space M) + + type-metric-quotient-Pseudometric-Space : UU (l1 ⊔ l2) + type-metric-quotient-Pseudometric-Space = + type-Set set-metric-quotient-Pseudometric-Space + + subtype-class-metric-quotient-Pseudometric-Space : + (X : type-metric-quotient-Pseudometric-Space) → + subtype l2 (type-Pseudometric-Space M) + subtype-class-metric-quotient-Pseudometric-Space = + subtype-set-quotient + ( equivalence-relation-sim-Pseudometric-Space M) + + is-in-class-metric-quotient-Pseudometric-Space : + (X : type-metric-quotient-Pseudometric-Space) → + type-Pseudometric-Space M → + UU l2 + is-in-class-metric-quotient-Pseudometric-Space = + is-in-equivalence-class-set-quotient + ( equivalence-relation-sim-Pseudometric-Space M) + + type-subtype-metric-quotient-Pseudometric-Space : + (X : type-metric-quotient-Pseudometric-Space) → UU (l1 ⊔ l2) + type-subtype-metric-quotient-Pseudometric-Space X = + type-subtype + ( subtype-class-metric-quotient-Pseudometric-Space X) + + neighborhood-prop-metric-quotient-Pseudometric-Space : + Rational-Neighborhood-Relation + ( l1 ⊔ l2) + ( type-metric-quotient-Pseudometric-Space) + neighborhood-prop-metric-quotient-Pseudometric-Space ε X Y = + Π-Prop + ( type-subtype-metric-quotient-Pseudometric-Space X) + ( λ (x , x∈X) → + Π-Prop + ( type-subtype-metric-quotient-Pseudometric-Space Y) + ( λ (y , y∈Y) → neighborhood-prop-Pseudometric-Space M ε x y)) + + neighborhood-metric-quotient-Pseudometric-Space : + ℚ⁺ → Relation (l1 ⊔ l2) type-metric-quotient-Pseudometric-Space + neighborhood-metric-quotient-Pseudometric-Space ε X Y = + type-Prop (neighborhood-prop-metric-quotient-Pseudometric-Space ε X Y) +``` + +## Properties + +### All quotient classes are inhabited + +```agda +module _ + {l1 l2 : Level} (A : Pseudometric-Space l1 l2) + (x : type-metric-quotient-Pseudometric-Space A) + where + + is-inhabited-class-metric-quotient-Pseudometric-Space : + is-inhabited-subtype + ( subtype-class-metric-quotient-Pseudometric-Space A x) + is-inhabited-class-metric-quotient-Pseudometric-Space = + is-inhabited-subtype-set-quotient + ( equivalence-relation-sim-Pseudometric-Space A) + ( x) +``` + +### The quotient neighborhood relation is reflexive + +```agda +module _ + {l1 l2 : Level} + (M : Pseudometric-Space l1 l2) + where + + abstract + is-reflexive-neighborhood-metric-quotient-Pseudometric-Space : + (d : ℚ⁺) (X : type-metric-quotient-Pseudometric-Space M) → + neighborhood-metric-quotient-Pseudometric-Space M d X X + is-reflexive-neighborhood-metric-quotient-Pseudometric-Space + d X (x , x∈X) (y , y∈X) = + apply-effectiveness-quotient-map + ( equivalence-relation-sim-Pseudometric-Space M) + ( ( eq-set-quotient-equivalence-class-set-quotient + ( equivalence-relation-sim-Pseudometric-Space M) + ( X) + ( x∈X)) ∙ + ( inv + ( eq-set-quotient-equivalence-class-set-quotient + ( equivalence-relation-sim-Pseudometric-Space M) + ( X) + ( y∈X)))) + ( d) +``` + +### The quotient neighborhood relation is symmetric + +```agda +module _ + {l1 l2 : Level} + (M : Pseudometric-Space l1 l2) + where + + abstract + is-symmetric-neighborhood-metric-quotient-Pseudometric-Space : + (d : ℚ⁺) (x y : type-metric-quotient-Pseudometric-Space M) → + neighborhood-metric-quotient-Pseudometric-Space M d x y → + neighborhood-metric-quotient-Pseudometric-Space M d y x + is-symmetric-neighborhood-metric-quotient-Pseudometric-Space + d X Y d⟨X,Y⟩ (y , y∈Y) (x , x∈X) = + symmetric-neighborhood-Pseudometric-Space + ( M) + ( d) + ( x) + ( y) + ( d⟨X,Y⟩ (x , x∈X) (y , y∈Y)) +``` + +### The quotient neighborhood relation is triangular + +```agda +module _ + {l1 l2 : Level} + (M : Pseudometric-Space l1 l2) + (X Y Z : type-metric-quotient-Pseudometric-Space M) + (d₁ d₂ : ℚ⁺) + where + + abstract + is-triangular-neighborhood-metric-quotient-Pseudometric-Space : + neighborhood-metric-quotient-Pseudometric-Space M d₂ Y Z → + neighborhood-metric-quotient-Pseudometric-Space M d₁ X Y → + neighborhood-metric-quotient-Pseudometric-Space M (d₁ +ℚ⁺ d₂) X Z + is-triangular-neighborhood-metric-quotient-Pseudometric-Space + d₂⟨Y,Z⟩ d₁⟨X,Y⟩ (x , x∈X) (z , z∈Z) = + let + open + do-syntax-trunc-Prop + ( neighborhood-prop-Pseudometric-Space M (d₁ +ℚ⁺ d₂) x z) + in do + (y , y∈Y) ← + is-inhabited-subtype-set-quotient + ( equivalence-relation-sim-Pseudometric-Space M) + ( Y) + triangular-neighborhood-Pseudometric-Space + ( M) + ( x) + ( y) + ( z) + ( d₁) + ( d₂) + ( d₂⟨Y,Z⟩ (y , y∈Y) (z , z∈Z)) + ( d₁⟨X,Y⟩ (x , x∈X) (y , y∈Y)) +``` + +### The quotient neighborhood relation is saturated + +```agda +module _ + {l1 l2 : Level} + (M : Pseudometric-Space l1 l2) + where + + abstract + is-saturated-neighborhood-metric-quotient-Pseudometric-Space : + (ε : ℚ⁺) (X Y : type-metric-quotient-Pseudometric-Space M) → + ((δ : ℚ⁺) → + neighborhood-metric-quotient-Pseudometric-Space M (ε +ℚ⁺ δ) X Y) → + neighborhood-metric-quotient-Pseudometric-Space M ε X Y + is-saturated-neighborhood-metric-quotient-Pseudometric-Space + ε X Y H (x , x∈X) (y , y∈Y) = + saturated-neighborhood-Pseudometric-Space M ε x y + ( λ δ → H δ (x , x∈X) (y , y∈Y)) +``` + +### The quotient pseudometric space + +```agda +module _ + {l1 l2 : Level} + (M : Pseudometric-Space l1 l2) + where + + pseudometric-metric-quotient-Pseudometric-Space : + Pseudometric-Space (l1 ⊔ l2) (l1 ⊔ l2) + pseudometric-metric-quotient-Pseudometric-Space = + ( type-metric-quotient-Pseudometric-Space M , + neighborhood-prop-metric-quotient-Pseudometric-Space M , + is-reflexive-neighborhood-metric-quotient-Pseudometric-Space M , + is-symmetric-neighborhood-metric-quotient-Pseudometric-Space M , + is-triangular-neighborhood-metric-quotient-Pseudometric-Space M , + is-saturated-neighborhood-metric-quotient-Pseudometric-Space M) +``` + +### The quotient pseudometric space is tight and extensional + +```agda +module _ + {l1 l2 : Level} + (M : Pseudometric-Space l1 l2) + where + + abstract + is-tight-pseudometric-metric-quotient-Pseudometric-Space : + is-tight-Pseudometric-Space + (pseudometric-metric-quotient-Pseudometric-Space M) + is-tight-pseudometric-metric-quotient-Pseudometric-Space X Y X~Y = + let + open + do-syntax-trunc-Prop + ( Id-Prop + ( set-metric-quotient-Pseudometric-Space M) + ( X) + ( Y)) + in do + ( x , x∈X) ← + is-inhabited-subtype-set-quotient + ( equivalence-relation-sim-Pseudometric-Space M) + ( X) + + ( y , y∈Y) ← + is-inhabited-subtype-set-quotient + ( equivalence-relation-sim-Pseudometric-Space M) + ( Y) + + eq-set-quotient-sim-element-set-quotient + ( equivalence-relation-sim-Pseudometric-Space M) + ( X) + ( Y) + ( x∈X) + ( y∈Y) + ( λ d → X~Y d (x , x∈X) (y , y∈Y)) + + is-extensional-pseudometric-metric-quotient-Pseudometric-Space : + is-extensional-Pseudometric-Space + ( pseudometric-metric-quotient-Pseudometric-Space M) + is-extensional-pseudometric-metric-quotient-Pseudometric-Space = + is-extensional-is-tight-Pseudometric-Space + ( pseudometric-metric-quotient-Pseudometric-Space M) + ( is-tight-pseudometric-metric-quotient-Pseudometric-Space) +``` + +### The quotient metric space of a pseudometric space + +```agda +module _ + {l1 l2 : Level} + (M : Pseudometric-Space l1 l2) + where + + metric-quotient-Pseudometric-Space : Metric-Space (l1 ⊔ l2) (l1 ⊔ l2) + metric-quotient-Pseudometric-Space = + make-Metric-Space + ( type-metric-quotient-Pseudometric-Space M) + ( neighborhood-prop-metric-quotient-Pseudometric-Space M) + ( is-reflexive-neighborhood-metric-quotient-Pseudometric-Space M) + ( is-symmetric-neighborhood-metric-quotient-Pseudometric-Space M) + ( is-triangular-neighborhood-metric-quotient-Pseudometric-Space M) + ( is-saturated-neighborhood-metric-quotient-Pseudometric-Space M) + ( is-extensional-pseudometric-metric-quotient-Pseudometric-Space M) +``` + +### The mapping from a pseudometric space to its quotient metric space + +```agda +module _ + {l1 l2 : Level} + (M : Pseudometric-Space l1 l2) + where + + map-metric-quotient-Pseudometric-Space : + type-Pseudometric-Space M → type-metric-quotient-Pseudometric-Space M + map-metric-quotient-Pseudometric-Space = + quotient-map (equivalence-relation-sim-Pseudometric-Space M) + + is-in-class-map-quotient-Pseudometric-Space : + (x : type-Pseudometric-Space M) → + is-in-class-metric-quotient-Pseudometric-Space + ( M) + ( map-metric-quotient-Pseudometric-Space x) + ( x) + is-in-class-map-quotient-Pseudometric-Space = + is-in-equivalence-class-quotient-map-set-quotient + ( equivalence-relation-sim-Pseudometric-Space M) + + map-subtype-metric-quotient-Pseudometric-Space : + (x : type-Pseudometric-Space M) → + type-subtype-metric-quotient-Pseudometric-Space M + ( map-metric-quotient-Pseudometric-Space x) + map-subtype-metric-quotient-Pseudometric-Space = + inhabitant-equivalence-class-quotient-map-set-quotient + ( equivalence-relation-sim-Pseudometric-Space M) +``` + +### The mapping from a pseudometric space its quotient metric space is an isometry + +```agda +module _ + {l1 l2 : Level} + (M : Pseudometric-Space l1 l2) + where + + abstract + preserves-neighborhood-map-metric-quotient-Pseudometric-Space : + (d : ℚ⁺) (x y : type-Pseudometric-Space M) → + neighborhood-Pseudometric-Space M d x y → + neighborhood-metric-quotient-Pseudometric-Space + ( M) + ( d) + ( map-metric-quotient-Pseudometric-Space M x) + ( map-metric-quotient-Pseudometric-Space M y) + preserves-neighborhood-map-metric-quotient-Pseudometric-Space + d x y d⟨x,y⟩ (x' , x≈x') (y' , y≈y') = + let + x~x' = + sim-is-in-equivalence-class-quotient-map-set-quotient + ( equivalence-relation-sim-Pseudometric-Space M) + ( x) + ( x') + ( x≈x') + + y~y' = + sim-is-in-equivalence-class-quotient-map-set-quotient + ( equivalence-relation-sim-Pseudometric-Space M) + ( y) + ( y') + ( y≈y') + + in + preserves-neighborhood-right-sim-Pseudometric-Space M y~y' d x' + ( preserves-neighborhood-left-sim-Pseudometric-Space + ( M) + ( x~x') + ( d) + ( y) + ( d⟨x,y⟩)) + + reflects-neighborhood-map-metric-quotient-Pseudometric-Space : + (d : ℚ⁺) (x y : type-Pseudometric-Space M) → + neighborhood-metric-quotient-Pseudometric-Space + ( M) + ( d) + ( map-metric-quotient-Pseudometric-Space M x) + ( map-metric-quotient-Pseudometric-Space M y) → + neighborhood-Pseudometric-Space M d x y + reflects-neighborhood-map-metric-quotient-Pseudometric-Space + d x y Nxy = + Nxy + ( map-subtype-metric-quotient-Pseudometric-Space M x) + ( map-subtype-metric-quotient-Pseudometric-Space M y) + + is-isometry-map-metric-quotient-Pseudometric-Space : + is-isometry-Pseudometric-Space + ( M) + ( pseudometric-metric-quotient-Pseudometric-Space M) + ( map-metric-quotient-Pseudometric-Space M) + is-isometry-map-metric-quotient-Pseudometric-Space d x y = + ( preserves-neighborhood-map-metric-quotient-Pseudometric-Space d x y , + reflects-neighborhood-map-metric-quotient-Pseudometric-Space d x y) +``` + +### The isometry from a pseudometric space to its quotient metric space + +```agda +module _ + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) + where + + isometry-metric-quotient-Pseudometric-Space : + isometry-Pseudometric-Space + ( M) + ( pseudometric-metric-quotient-Pseudometric-Space M) + isometry-metric-quotient-Pseudometric-Space = + ( map-metric-quotient-Pseudometric-Space M , + is-isometry-map-metric-quotient-Pseudometric-Space M) +``` + +### The short map from a pseudometric space to its quotient metric space + +```agda +module _ + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) + where + + short-map-metric-quotient-Pseudometric-Space : + short-function-Pseudometric-Space + ( M) + ( pseudometric-metric-quotient-Pseudometric-Space M) + short-map-metric-quotient-Pseudometric-Space = + short-isometry-Pseudometric-Space + ( M) + ( pseudometric-metric-quotient-Pseudometric-Space M) + ( isometry-metric-quotient-Pseudometric-Space M) +``` + +### The isometric equivalence between a metric space and the quotient metric space of its pseudometric space + +```agda +module _ + {l1 l2 : Level} + (M : Metric-Space l1 l2) + where + + map-metric-quotient-Metric-Space : + type-Metric-Space M → + type-metric-quotient-Pseudometric-Space + ( pseudometric-Metric-Space M) + map-metric-quotient-Metric-Space = + map-metric-quotient-Pseudometric-Space + ( pseudometric-Metric-Space M) + + abstract + is-contr-map-metric-quotient-Metric-Space : + is-contr-map map-metric-quotient-Metric-Space + is-contr-map-metric-quotient-Metric-Space X = + let + open + do-syntax-trunc-Prop + ( is-contr-Prop + ( fiber map-metric-quotient-Metric-Space X)) + in do + ( x , x∈X) ← + is-inhabited-subtype-set-quotient + ( equivalence-relation-sim-Metric-Space M) + ( X) + + ( ( x , + eq-set-quotient-equivalence-class-set-quotient + ( equivalence-relation-sim-Metric-Space M) + ( X) + ( x∈X)) , + ( λ (y , Y＝X) → + eq-type-subtype + ( λ z → + Id-Prop + ( set-metric-quotient-Pseudometric-Space + ( pseudometric-Metric-Space M)) + ( map-metric-quotient-Metric-Space z) + ( X)) + ( eq-sim-Metric-Space + ( M) + ( x) + ( y) + ( apply-effectiveness-quotient-map + ( equivalence-relation-sim-Metric-Space M) + ( ( eq-set-quotient-equivalence-class-set-quotient + ( equivalence-relation-sim-Metric-Space M) + ( X) + ( x∈X)) ∙ + ( inv Y＝X)))))) + + is-equiv-map-metric-quotient-Metric-Space : + is-equiv map-metric-quotient-Metric-Space + is-equiv-map-metric-quotient-Metric-Space = + is-equiv-is-contr-map + ( is-contr-map-metric-quotient-Metric-Space) + + is-isometry-map-metric-quotient-Metric-Space : + is-isometry-Metric-Space + ( M) + ( metric-quotient-Pseudometric-Space + ( pseudometric-Metric-Space M)) + ( map-metric-quotient-Metric-Space) + is-isometry-map-metric-quotient-Metric-Space = + is-isometry-map-metric-quotient-Pseudometric-Space + ( pseudometric-Metric-Space M) + + isometric-equiv-metric-quotient-Metric-Space' : + isometric-equiv-Metric-Space' + ( M) + ( metric-quotient-Pseudometric-Space + ( pseudometric-Metric-Space M)) + isometric-equiv-metric-quotient-Metric-Space' = + ( map-metric-quotient-Metric-Space , + is-equiv-map-metric-quotient-Metric-Space , + is-isometry-map-metric-quotient-Metric-Space) +``` + +### The construction of the quotient metric space of a pseudometric space is idempotent + +```agda +module _ + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) + where + + is-idempotent-metric-quotient-Pseudometric-Space : + metric-quotient-Pseudometric-Space + ( pseudometric-Metric-Space + ( metric-quotient-Pseudometric-Space M)) ＝ + metric-quotient-Pseudometric-Space M + is-idempotent-metric-quotient-Pseudometric-Space = + inv + ( eq-isometric-equiv-Metric-Space' + ( metric-quotient-Pseudometric-Space M) + ( metric-quotient-Pseudometric-Space + ( pseudometric-Metric-Space + ( metric-quotient-Pseudometric-Space M))) + ( isometric-equiv-metric-quotient-Metric-Space' + ( metric-quotient-Pseudometric-Space M))) +``` + +### Induced short function from the quotient metric space into a metric space + +```agda +module _ + {l1 l2 l1' l2' : Level} + (A : Pseudometric-Space l1 l2) + (B : Metric-Space l1' l2') + (f : short-function-Pseudometric-Space A (pseudometric-Metric-Space B)) + where + + map-short-function-metric-quotient-Pseudometric-space : + type-function-Metric-Space + ( metric-quotient-Pseudometric-Space A) + ( B) + map-short-function-metric-quotient-Pseudometric-space = + inv-precomp-set-quotient + ( equivalence-relation-sim-Pseudometric-Space A) + ( set-Metric-Space B) + ( reflecting-map-short-function-metric-space-Pseudometric-Space A B f) + + htpy-map-short-function-metric-quotient-Pseudometric-Space : + ( ( map-short-function-metric-quotient-Pseudometric-space) ∘ + ( map-metric-quotient-Pseudometric-Space A)) ~ + ( map-short-function-Pseudometric-Space A (pseudometric-Metric-Space B) f) + htpy-map-short-function-metric-quotient-Pseudometric-Space = + is-section-inv-precomp-set-quotient + ( equivalence-relation-sim-Pseudometric-Space A) + ( set-Metric-Space B) + ( reflecting-map-short-function-metric-space-Pseudometric-Space A B f) + + compute-map-short-function-metric-quotient-Pseudometric-Space : + (X : type-metric-quotient-Pseudometric-Space A) → + (x : type-Pseudometric-Space A) → + is-in-class-metric-quotient-Pseudometric-Space A X x → + map-short-function-metric-quotient-Pseudometric-space X ＝ + map-short-function-Pseudometric-Space A (pseudometric-Metric-Space B) f x + compute-map-short-function-metric-quotient-Pseudometric-Space X x x∈X = + tr + ( λ Y → + map-short-function-metric-quotient-Pseudometric-space Y ＝ + map-short-function-Pseudometric-Space + ( A) + ( pseudometric-Metric-Space B) + ( f) + ( x)) + ( eq-set-quotient-equivalence-class-set-quotient + ( equivalence-relation-sim-Pseudometric-Space A) + ( X) + ( x∈X)) + ( htpy-map-short-function-metric-quotient-Pseudometric-Space x) + + abstract + is-short-map-short-function-metric-quotient-Pseudometric-Space : + is-short-function-Metric-Space + ( metric-quotient-Pseudometric-Space A) + ( B) + ( map-short-function-metric-quotient-Pseudometric-space) + is-short-map-short-function-metric-quotient-Pseudometric-Space + d X Y N⟨X,Y⟩ = + let + open + do-syntax-trunc-Prop + ( neighborhood-prop-Metric-Space + ( B) + ( d) + ( map-short-function-metric-quotient-Pseudometric-space X) + ( map-short-function-metric-quotient-Pseudometric-space Y)) + in do + ( x , x∈X) ← + is-inhabited-subtype-set-quotient + ( equivalence-relation-sim-Pseudometric-Space A) + ( X) + ( y , y∈Y) ← + is-inhabited-subtype-set-quotient + ( equivalence-relation-sim-Pseudometric-Space A) + ( Y) + + binary-tr + ( neighborhood-Metric-Space B d) + ( inv + ( compute-map-short-function-metric-quotient-Pseudometric-Space + ( X) + ( x) + ( x∈X))) + ( inv + ( compute-map-short-function-metric-quotient-Pseudometric-Space + ( Y) + ( y) + ( y∈Y))) + ( is-short-map-short-function-Pseudometric-Space + ( A) + ( pseudometric-Metric-Space B) + ( f) + ( d) + ( x) + ( y) + ( N⟨X,Y⟩ (x , x∈X) (y , y∈Y))) + + short-map-short-function-metric-quotient-Pseudometric-Space : + short-function-Metric-Space + ( metric-quotient-Pseudometric-Space A) + ( B) + short-map-short-function-metric-quotient-Pseudometric-Space = + ( map-short-function-metric-quotient-Pseudometric-space , + is-short-map-short-function-metric-quotient-Pseudometric-Space) +``` + +### Induced isometry from the quotient metric space into a metric space + +```agda +module _ + {l1 l2 l1' l2' : Level} + (A : Pseudometric-Space l1 l2) + (B : Metric-Space l1' l2') + (f : isometry-Pseudometric-Space A (pseudometric-Metric-Space B)) + where + + map-isometry-metric-quotient-Pseudometric-Space : + type-function-Metric-Space + ( metric-quotient-Pseudometric-Space A) + ( B) + map-isometry-metric-quotient-Pseudometric-Space = + map-short-function-metric-quotient-Pseudometric-space + ( A) + ( B) + ( short-isometry-Pseudometric-Space + ( A) + ( pseudometric-Metric-Space B) + ( f)) + + htpy-map-isometry-metric-quotient-Pseudometric-Space : + ( ( map-isometry-metric-quotient-Pseudometric-Space) ∘ + ( map-metric-quotient-Pseudometric-Space A)) ~ + ( map-isometry-Pseudometric-Space A (pseudometric-Metric-Space B) f) + htpy-map-isometry-metric-quotient-Pseudometric-Space = + htpy-map-short-function-metric-quotient-Pseudometric-Space + ( A) + ( B) + ( short-isometry-Pseudometric-Space + ( A) + ( pseudometric-Metric-Space B) + ( f)) + + compute-map-isometry-metric-quotient-Pseudometric-Space : + (X : type-metric-quotient-Pseudometric-Space A) → + (x : type-Pseudometric-Space A) → + is-in-class-metric-quotient-Pseudometric-Space A X x → + map-isometry-metric-quotient-Pseudometric-Space X ＝ + map-isometry-Pseudometric-Space + ( A) + ( pseudometric-Metric-Space B) + ( f) + ( x) + compute-map-isometry-metric-quotient-Pseudometric-Space = + compute-map-short-function-metric-quotient-Pseudometric-Space + ( A) + ( B) + ( short-isometry-Pseudometric-Space + ( A) + ( pseudometric-Metric-Space B) + ( f)) + + abstract + preserves-neighborhood-map-isometry-metric-quotient-Pseudometric-Space : + (d : ℚ⁺) → + (x y : type-metric-quotient-Pseudometric-Space A) → + neighborhood-metric-quotient-Pseudometric-Space + ( A) + ( d) + ( x) + ( y) → + neighborhood-Metric-Space + ( B) + ( d) + ( map-isometry-metric-quotient-Pseudometric-Space x) + ( map-isometry-metric-quotient-Pseudometric-Space y) + preserves-neighborhood-map-isometry-metric-quotient-Pseudometric-Space = + is-short-map-short-function-metric-quotient-Pseudometric-Space + ( A) + ( B) + ( short-isometry-Pseudometric-Space + ( A) + ( pseudometric-Metric-Space B) + ( f)) + + reflects-neighborhood-map-isometry-metric-quotient-Pseudometric-Space : + (d : ℚ⁺) → + (x y : type-metric-quotient-Pseudometric-Space A) → + neighborhood-Metric-Space + ( B) + ( d) + ( map-isometry-metric-quotient-Pseudometric-Space x) + ( map-isometry-metric-quotient-Pseudometric-Space y) → + neighborhood-metric-quotient-Pseudometric-Space + ( A) + ( d) + ( x) + ( y) + reflects-neighborhood-map-isometry-metric-quotient-Pseudometric-Space + d X Y N⟨fX,fY⟩ (x , x∈X) (y , y∈Y) = + reflects-neighborhood-map-isometry-Pseudometric-Space + ( A) + ( pseudometric-Metric-Space B) + ( f) + ( d) + ( x) + ( y) + ( binary-tr + ( neighborhood-Metric-Space B d) + ( compute-map-isometry-metric-quotient-Pseudometric-Space X x x∈X) + ( compute-map-isometry-metric-quotient-Pseudometric-Space Y y y∈Y) + ( N⟨fX,fY⟩)) + + is-isometry-map-isometry-metric-quotient-Pseudometric-Space : + is-isometry-Metric-Space + ( metric-quotient-Pseudometric-Space A) + ( B) + ( map-isometry-metric-quotient-Pseudometric-Space) + is-isometry-map-isometry-metric-quotient-Pseudometric-Space d x y = + ( preserves-neighborhood-map-isometry-metric-quotient-Pseudometric-Space + ( d) + ( x) + ( y) , + reflects-neighborhood-map-isometry-metric-quotient-Pseudometric-Space + ( d) + ( x) + ( y)) + + isometry-map-isometry-metric-quotient-Pseudometric-Space : + isometry-Metric-Space + ( metric-quotient-Pseudometric-Space A) + ( B) + isometry-map-isometry-metric-quotient-Pseudometric-Space = + ( map-isometry-metric-quotient-Pseudometric-Space , + is-isometry-map-isometry-metric-quotient-Pseudometric-Space) +``` + +## External links + +- [Metric identification](https://en.wikipedia.org/wiki/Pseudometric_space#Metric_identification) + on pseudometric spaces at Wikipedia From 450b658a3e2f8e20d0ceda83c5ba3c8d284e1a63 Mon Sep 17 00:00:00 2001 From: malarbol Date: Thu, 23 Oct 2025 00:34:32 +0200 Subject: [PATCH 16/28] apply suggestions --- ...completion-of-pseudometric-spaces.lagda.md | 39 +++++++------------ 1 file changed, 15 insertions(+), 24 deletions(-) diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md index 567d81f9b0a..3856b3ea5f1 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md @@ -109,19 +109,17 @@ module _ neighborhood-cauchy-pseudocompletion-Pseudometric-Space M d x x is-reflexive-neighborhood-cauchy-pseudocompletion-Pseudometric-Space d x δ ε = - let - xδ = map-cauchy-approximation-Pseudometric-Space M x δ - xε = map-cauchy-approximation-Pseudometric-Space M x ε - in - monotonic-neighborhood-Pseudometric-Space M xδ xε - ( δ +ℚ⁺ ε) - ( δ +ℚ⁺ ε +ℚ⁺ d) - ( le-right-add-rational-ℚ⁺ _ d) - ( is-cauchy-approximation-map-cauchy-approximation-Pseudometric-Space - ( M) - ( x) - ( δ) - ( ε)) + monotonic-neighborhood-Pseudometric-Space M + ( map-cauchy-approximation-Pseudometric-Space M x δ) + ( map-cauchy-approximation-Pseudometric-Space M x ε) + ( δ +ℚ⁺ ε) + ( δ +ℚ⁺ ε +ℚ⁺ d) + ( le-right-add-rational-ℚ⁺ _ d) + ( is-cauchy-approximation-map-cauchy-approximation-Pseudometric-Space + ( M) + ( x) + ( δ) + ( ε)) ``` ### The neighborhood relation is symmetric @@ -469,17 +467,10 @@ module _ (ε₁ , ε₂ , ε₁+ε₂=ε) = split-ℚ⁺ ε lemma-δ+ε : - (δ₁ +ℚ⁺ ε₁ +ℚ⁺ (δ₂ +ℚ⁺ ε₂)) ＝ δ +ℚ⁺ ε + ((δ₁ +ℚ⁺ ε₁) +ℚ⁺ (δ₂ +ℚ⁺ ε₂)) ＝ δ +ℚ⁺ ε lemma-δ+ε = - ( interchange-law-add-add-ℚ⁺ - ( δ₁) - ( ε₁) - ( δ₂) - ( ε₂)) ∙ - ( ap-binary - ( add-ℚ⁺) - ( δ₁+δ₂=δ) - ( ε₁+ε₂=ε)) + ( interchange-law-add-add-ℚ⁺ δ₁ ε₁ δ₂ ε₂) ∙ + ( ap-binary add-ℚ⁺ δ₁+δ₂=δ ε₁+ε₂=ε) in tr ( is-upper-bound-dist-Pseudometric-Space @@ -509,7 +500,7 @@ module _ (θ₁ , θ₂ , θ₁+θ₂=θ) = split-ℚ⁺ θ lemma-η+θ+δ : - ( η +ℚ⁺ θ₁ +ℚ⁺ (δ +ℚ⁺ θ₂)) ＝ η +ℚ⁺ θ +ℚ⁺ δ + ((η +ℚ⁺ θ₁) +ℚ⁺ (δ +ℚ⁺ θ₂)) ＝ η +ℚ⁺ θ +ℚ⁺ δ lemma-η+θ+δ = ( interchange-law-add-add-ℚ⁺ η θ₁ δ θ₂) ∙ ( ap From f959fd6131c40b4efdbedc90b19fc04acd270ebe Mon Sep 17 00:00:00 2001 From: malarbol Date: Mon, 27 Oct 2025 18:55:27 +0100 Subject: [PATCH 17/28] more precise header --- .../metric-quotients-of-pseudometric-spaces.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md index 77ec63a143d..ec41646f096 100644 --- a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md @@ -81,8 +81,8 @@ quotient; if `M` is a metric space, this is an [isometric equivalence](metric-spaces.equality-of-metric-spaces.md). Any [short map](metric-spaces.short-functions-pseudometric-spaces.md) (resp. -isometry) from a pseudometric space to a metric space factors through the metric -quotient of its domain. +isometry) from a pseudometric space to a metric space factors as a short map +(resp. isometry) through the metric quotient of its domain. ## Definitions From be2ec0853295681f3cb49a3a22736212d74a398f Mon Sep 17 00:00:00 2001 From: malarbol Date: Mon, 27 Oct 2025 19:56:59 +0100 Subject: [PATCH 18/28] short actions --- ...-quotients-of-pseudometric-spaces.lagda.md | 33 ++++++++++++++++--- ...completion-of-pseudometric-spaces.lagda.md | 32 ++++++++++++++++++ 2 files changed, 61 insertions(+), 4 deletions(-) diff --git a/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md index b5aab9bcb3e..2020247865a 100644 --- a/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md @@ -98,15 +98,40 @@ module _ {l1 l2 : Level} (M : Pseudometric-Space l1 l2) where + short-map-metric-quotient-cauchy-apprtoximation-Pseudometric-Space : + short-function-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( 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 + ( M) + ( pseudometric-metric-quotient-Pseudometric-Space M) + ( short-map-metric-quotient-Pseudometric-Space M) + map-metric-quotient-cauchy-approximation-Pseudometric-Space : cauchy-approximation-Pseudometric-Space M → cauchy-approximation-Metric-Space ( metric-quotient-Pseudometric-Space M) map-metric-quotient-cauchy-approximation-Pseudometric-Space = - map-short-function-cauchy-approximation-Pseudometric-Space - ( M) - ( pseudometric-metric-quotient-Pseudometric-Space M) - ( short-map-metric-quotient-Pseudometric-Space M) + map-short-function-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( cauchy-pseudocompletion-Metric-Space + ( metric-quotient-Pseudometric-Space M)) + ( short-map-metric-quotient-cauchy-apprtoximation-Pseudometric-Space) + + is-short-map-metric-quotient-cauchy-approximation-Pseudometric-Space : + is-short-function-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( cauchy-pseudocompletion-Metric-Space + ( metric-quotient-Pseudometric-Space M)) + ( map-metric-quotient-cauchy-approximation-Pseudometric-Space) + is-short-map-metric-quotient-cauchy-approximation-Pseudometric-Space = + is-short-map-short-function-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( cauchy-pseudocompletion-Metric-Space + ( metric-quotient-Pseudometric-Space M)) + ( short-map-metric-quotient-cauchy-apprtoximation-Pseudometric-Space) ``` ### Lifts of Cauchy approximations in the quotient metric space up to similarity diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md index 3856b3ea5f1..c1947a794dd 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md @@ -762,3 +762,35 @@ module _ ( lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space M , is-isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space) ``` + +### 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 + + is-short-map-short-function-cauchy-approximation-Pseudometric-Space : + is-short-function-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space A) + ( cauchy-pseudocompletion-Pseudometric-Space B) + ( map-short-function-cauchy-approximation-Pseudometric-Space A B f) + is-short-map-short-function-cauchy-approximation-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-short-function-cauchy-approximation-Pseudometric-Space : + short-function-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space A) + ( cauchy-pseudocompletion-Pseudometric-Space B) + short-map-short-function-cauchy-approximation-Pseudometric-Space = + ( map-short-function-cauchy-approximation-Pseudometric-Space A B f , + is-short-map-short-function-cauchy-approximation-Pseudometric-Space) +``` From 2b88d9cae0f4c6193d2d81e0035ba7313e3b93b2 Mon Sep 17 00:00:00 2001 From: malarbol Date: Mon, 27 Oct 2025 19:58:54 +0100 Subject: [PATCH 19/28] necessary condition for complete metric quotients --- ...-quotients-of-pseudometric-spaces.lagda.md | 19 +++++++++++++++++++ ...completion-of-pseudometric-spaces.lagda.md | 1 - 2 files changed, 19 insertions(+), 1 deletion(-) diff --git a/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md index 2020247865a..9a5eaa52630 100644 --- a/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md @@ -46,6 +46,7 @@ open import metric-spaces.cauchy-approximations-metric-spaces open import metric-spaces.cauchy-approximations-pseudometric-spaces open import metric-spaces.cauchy-pseudocompletion-of-metric-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.equality-of-metric-spaces open import metric-spaces.extensionality-pseudometric-spaces @@ -335,3 +336,21 @@ module _ ( is-lim)) ( is-inhabited-class-metric-quotient-Pseudometric-Space A lim) ``` + +### If the metric quotient of a pseudometric space is complete, all cauchy approximations have lifts up to similarity + +```agda +module _ + {l1 l2 : Level} (A : Pseudometric-Space l1 l2) + (H : is-complete-Metric-Space (metric-quotient-Pseudometric-Space A)) + (u : cauchy-approximation-Metric-Space (metric-quotient-Pseudometric-Space A)) + where + + has-lift-cauchy-approximation-is-complete-metric-quotient-Pseudometric-Space : + has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space A u + has-lift-cauchy-approximation-is-complete-metric-quotient-Pseudometric-Space = + has-lift-is-convergent-cauchy-approximation-metric-quotient-Pseudometric-Space + ( A) + ( u) + ( H u) +``` diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md index c1947a794dd..ee6c3b504b4 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md @@ -765,7 +765,6 @@ module _ ### The action of short maps on Cauchy approximations is short - ```agda module _ {l1 l2 l1' l2' : Level} From cf5f1617f92c73ef9b71de0917040986934931fa Mon Sep 17 00:00:00 2001 From: malarbol Date: Mon, 27 Oct 2025 20:14:37 +0100 Subject: [PATCH 20/28] fix header --- ...ximations-metric-quotients-of-pseudometric-spaces.lagda.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md index 9a5eaa52630..51872a91660 100644 --- a/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md @@ -88,7 +88,9 @@ The pointwise quotient of Cauchy approximations preserves The pointwise quotient of a Cauchy approximation has a lift. A Cauchy approximation that admits a [limit](metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces.md) -has a lift. +has a lift. If the metric quotient is +[complete](metric-spaces.complete-metric-spaces.md), then all Cauchy +approximations in the metric quotient have a lift. ## Definitions From fe50b699f69eea6997c816b8a66fcd86bae9ce05 Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 28 Oct 2025 18:28:03 +0100 Subject: [PATCH 21/28] lemma sim-map-cauchy-approximation cauchy-pseudocompletion --- ...completion-of-pseudometric-spaces.lagda.md | 65 +++++++++++++++++++ 1 file changed, 65 insertions(+) diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md index ee6c3b504b4..6e0920e355e 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md @@ -793,3 +793,68 @@ module _ ( map-short-function-cauchy-approximation-Pseudometric-Space A B f , is-short-map-short-function-cauchy-approximation-Pseudometric-Space) ``` + +### The pointwise image of a Cauchy approximation in a pseudometric space by the inclusion in its Cauchy pseudocompletion is convergent + +```agda +module _ + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) + (u : cauchy-approximation-Pseudometric-Space M) + where + + is-limit-map-cauchy-approximation-cauchy-pseudocompletion-Ppseudometric-Space : + is-limit-cauchy-approximation-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( map-short-function-cauchy-approximation-Pseudometric-Space + ( M) + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( short-map-cauchy-pseudocompletion-Pseudometric-Space M) + ( u)) + ( u) + is-limit-map-cauchy-approximation-cauchy-pseudocompletion-Ppseudometric-Space + ε δ α β = + symmetric-neighborhood-Pseudometric-Space M + ( (α +ℚ⁺ β) +ℚ⁺ (ε +ℚ⁺ δ)) + ( map-cauchy-approximation-Pseudometric-Space M u β) + ( map-cauchy-approximation-Pseudometric-Space M u ε) + ( monotonic-neighborhood-Pseudometric-Space M + ( map-cauchy-approximation-Pseudometric-Space M u β) + ( map-cauchy-approximation-Pseudometric-Space M u ε) + ( β +ℚ⁺ ε) + ( (α +ℚ⁺ β) +ℚ⁺ (ε +ℚ⁺ δ)) + ( preserves-le-add-ℚ + { rational-ℚ⁺ β} + { rational-ℚ⁺ (α +ℚ⁺ β)} + { rational-ℚ⁺ ε} + { rational-ℚ⁺ (ε +ℚ⁺ δ)} + ( le-right-add-ℚ⁺ α β) + ( le-left-add-ℚ⁺ ε δ)) + ( is-cauchy-approximation-map-cauchy-approximation-Pseudometric-Space + ( M) + ( u) + ( β) + ( ε))) + + sim-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space : + sim-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M)) + ( map-short-function-cauchy-approximation-Pseudometric-Space + ( M) + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( short-map-cauchy-pseudocompletion-Pseudometric-Space M) + ( u)) + ( map-cauchy-pseudocompletion-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( u)) + sim-map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space = + sim-const-is-limit-cauchy-approximation-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( map-short-function-cauchy-approximation-Pseudometric-Space + ( M) + ( cauchy-pseudocompletion-Pseudometric-Space M) + ( short-map-cauchy-pseudocompletion-Pseudometric-Space M) + ( u)) + ( u) + ( is-limit-map-cauchy-approximation-cauchy-pseudocompletion-Ppseudometric-Space) +``` From 69144fc20437aefcdb1dcfda6844c1ba9a46a86c Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 28 Oct 2025 23:31:53 +0100 Subject: [PATCH 22/28] Update src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- .../cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md index 6e0920e355e..5bc301fcc11 100644 --- a/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletion-of-pseudometric-spaces.lagda.md @@ -794,7 +794,7 @@ module _ is-short-map-short-function-cauchy-approximation-Pseudometric-Space) ``` -### The pointwise image of a Cauchy approximation in a pseudometric space by the inclusion in its Cauchy pseudocompletion is convergent +### The image of a Cauchy approximation in the Cauchy pseudocompletion is convergent ```agda module _ From 12526f9a85acc0b791fd84475b6651c5231d295b Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 28 Oct 2025 23:32:58 +0100 Subject: [PATCH 23/28] Update src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- .../metric-quotients-of-pseudometric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md index ec41646f096..a0f7fbc20dd 100644 --- a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md @@ -70,7 +70,7 @@ of a [pseudometric space](metric-spaces.pseudometric-spaces.md) is the [metric space](metric-spaces.metric-spaces.md) whose points are [quotient classes](foundation.set-quotients.md) of `M` by the [similarity relation](metric-spaces.similarity-of-elements-pseudometric-spaces.md) -and [neighborhoods](metric-spaces.rational-neighborhood-relations.md) given by +and [neighborhoods](metric-spaces.rational-neighborhood-relations.md) are neighborhoods of inhabitants of the quotient classes: two quotient classes `X`, `Y` are in a `d`-neighborhood if for all `x ∈ X` and `y ∈ Y`, `x` and `y` are `d`-neighbors in the pseudometric space. From 9ef2fff55e883fbbf6a889d66618422910e5d3bc Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 28 Oct 2025 23:34:43 +0100 Subject: [PATCH 24/28] Update src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- .../metric-quotients-of-pseudometric-spaces.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md index a0f7fbc20dd..05139e11670 100644 --- a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md @@ -81,8 +81,8 @@ quotient; if `M` is a metric space, this is an [isometric equivalence](metric-spaces.equality-of-metric-spaces.md). Any [short map](metric-spaces.short-functions-pseudometric-spaces.md) (resp. -isometry) from a pseudometric space to a metric space factors as a short map -(resp. isometry) through the metric quotient of its domain. +isometry) from a pseudometric space to a metric space factors uniquely as a short map +(resp. isometry) through the metric quotient of its domain. This is the {{#concept "universal property" Disambiguation="of the metric space quotient of a pseudometric space"}} of the metric space quotient. ## Definitions From f5f325e2584e9e8fd0e7cbe6e24df0f16408aecc Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 28 Oct 2025 23:38:25 +0100 Subject: [PATCH 25/28] Update src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- .../metric-quotients-of-pseudometric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md index 05139e11670..8d4c14395e6 100644 --- a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md @@ -296,7 +296,7 @@ module _ abstract is-tight-pseudometric-metric-quotient-Pseudometric-Space : is-tight-Pseudometric-Space - (pseudometric-metric-quotient-Pseudometric-Space M) + ( pseudometric-metric-quotient-Pseudometric-Space M) is-tight-pseudometric-metric-quotient-Pseudometric-Space X Y X~Y = let open From a56da1059cf850613f1d49af1fb34c8261bfa3ee Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 28 Oct 2025 23:40:48 +0100 Subject: [PATCH 26/28] Update src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- .../metric-quotients-of-pseudometric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md index 8d4c14395e6..1279b2faec5 100644 --- a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md @@ -592,7 +592,7 @@ module _ ( metric-quotient-Pseudometric-Space M))) ``` -### Induced short function from the quotient metric space into a metric space +### The induced short function from the quotient metric space into a metric space ```agda module _ From 817d5fe1102d4ddd8f0b78498a5ce29f9faf0fcd Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 28 Oct 2025 23:49:00 +0100 Subject: [PATCH 27/28] format --- .../metric-quotients-of-pseudometric-spaces.lagda.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md index 1279b2faec5..ffecd0aafca 100644 --- a/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/metric-quotients-of-pseudometric-spaces.lagda.md @@ -81,8 +81,11 @@ quotient; if `M` is a metric space, this is an [isometric equivalence](metric-spaces.equality-of-metric-spaces.md). Any [short map](metric-spaces.short-functions-pseudometric-spaces.md) (resp. -isometry) from a pseudometric space to a metric space factors uniquely as a short map -(resp. isometry) through the metric quotient of its domain. This is the {{#concept "universal property" Disambiguation="of the metric space quotient of a pseudometric space"}} of the metric space quotient. +isometry) from a pseudometric space to a metric space factors uniquely as a +short map (resp. isometry) through the metric quotient of its domain. This is +the +{{#concept "universal property" Disambiguation="of the metric space quotient of a pseudometric space"}} +of the metric space quotient. ## Definitions From 93f7ce366971cdc6019a85cd0e3f786a18b65692 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 6 Nov 2025 23:41:34 +0100 Subject: [PATCH 28/28] Update src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md --- ...roximations-metric-quotients-of-pseudometric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md index 51872a91660..13705b93b6c 100644 --- a/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md @@ -75,7 +75,7 @@ by the of the [pseudometric space](metric-spaces.pseudometric-spaces.md) are Cauchy approximations in the [metric quotient](metric-spaces.metric-quotients-of-pseudometric-spaces.md). A -Cauchy approximation in a the metric quotient of a pseudometric space has a +Cauchy approximation in the metric quotient of a pseudometric space has a {{#concept "lift up to similarity" Agda=has-lift-cauchy-approximation-metric-quotient-Pseudometric-Space}} if it is similar (in the [Cauchy pseudocompletion](metric-spaces.cauchy-pseudocompletion-of-metric-spaces.md)