From 22ebc6e39aa391bc88261e96b0f74b348f61ce2e Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 17 Jun 2025 18:05:35 +0200 Subject: [PATCH 1/8] metric-semigroups --- src/metric-spaces.lagda.md | 1 + src/metric-spaces/metric-semigroups.lagda.md | 187 +++++++++++++++++++ 2 files changed, 188 insertions(+) create mode 100644 src/metric-spaces/metric-semigroups.lagda.md diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md index 81a017ff2d..eec703fc91 100644 --- a/src/metric-spaces.lagda.md +++ b/src/metric-spaces.lagda.md @@ -75,6 +75,7 @@ open import metric-spaces.limits-of-sequences-metric-spaces public open import metric-spaces.limits-of-sequences-premetric-spaces public open import metric-spaces.limits-of-sequences-pseudometric-spaces public open import metric-spaces.lipschitz-functions-metric-spaces public +open import metric-spaces.metric-semigroups public open import metric-spaces.metric-space-of-cauchy-approximations-complete-metric-spaces public open import metric-spaces.metric-space-of-cauchy-approximations-metric-spaces public open import metric-spaces.metric-space-of-cauchy-approximations-saturated-complete-metric-spaces public diff --git a/src/metric-spaces/metric-semigroups.lagda.md b/src/metric-spaces/metric-semigroups.lagda.md new file mode 100644 index 0000000000..ab97495387 --- /dev/null +++ b/src/metric-spaces/metric-semigroups.lagda.md @@ -0,0 +1,187 @@ +# Metric semigroups + +```agda +module metric-spaces.metric-semigroups where +``` + +
Imports + +```agda +open import elementary-number-theory.positive-rational-numbers + +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.sets +open import foundation.subtypes +open import foundation.universe-levels + +open import group-theory.semigroups + +open import metric-spaces.metric-space-of-short-functions-metric-spaces +open import metric-spaces.metric-spaces +open import metric-spaces.short-functions-metric-spaces +``` + +
+ +## Idea + +A {{#concept "metric semigroup" Agda=Metric-Semigroup}} is a +[metric-space](metric-spaces.metric-spaces.md) equipped with a +[short](metric-spaces.short-functions-metric-spaces.md) +[associative binary operator](group-theory.semigroups.md). + +## Definitions + +### Associative short binary operators + +```agda +module _ + {l1 l2 : Level} (A : Metric-Space l1 l2) + where + + mul-short-mul-Metric-Space : + short-function-Metric-Space + ( A) + ( metric-space-of-short-functions-Metric-Space A A) → + type-Metric-Space A → + type-Metric-Space A → + type-Metric-Space A + mul-short-mul-Metric-Space f = + ( map-short-function-Metric-Space A A) ∘ + ( map-short-function-Metric-Space + ( A) + ( metric-space-of-short-functions-Metric-Space A A) + ( f)) + + is-short-associative-prop-mul-Metric-Space : + short-function-Metric-Space + ( A) + ( metric-space-of-short-functions-Metric-Space A A) → + Prop l1 + is-short-associative-prop-mul-Metric-Space f = + let + μ : type-Metric-Space A → type-Metric-Space A → type-Metric-Space A + μ = mul-short-mul-Metric-Space f + in + Π-Prop + ( type-Metric-Space A) + ( λ x → + Π-Prop + ( type-Metric-Space A) + ( λ y → + Π-Prop + ( type-Metric-Space A) + ( λ z → + Id-Prop + ( set-Metric-Space A) + ( μ (μ x y) z) + ( μ x (μ y z))))) +``` + +### Metric semigroups + +```agda +Metric-Semigroup : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +Metric-Semigroup l1 l2 = + Σ ( Metric-Space l1 l2) + ( type-subtype ∘ is-short-associative-prop-mul-Metric-Space) + +module _ + {l1 l2 : Level} (M : Metric-Semigroup l1 l2) + where + + metric-space-Metric-Semigroup : Metric-Space l1 l2 + metric-space-Metric-Semigroup = pr1 M + + set-Metric-Semigroup : Set l1 + set-Metric-Semigroup = set-Metric-Space metric-space-Metric-Semigroup + + type-Metric-Semigroup : UU l1 + type-Metric-Semigroup = type-Metric-Space metric-space-Metric-Semigroup + + short-associative-mul-Metric-Semigroup : + type-subtype + (is-short-associative-prop-mul-Metric-Space metric-space-Metric-Semigroup) + short-associative-mul-Metric-Semigroup = pr2 M + + short-mul-Metric-Semigroup : + short-function-Metric-Space + ( metric-space-Metric-Semigroup) + ( metric-space-of-short-functions-Metric-Space + metric-space-Metric-Semigroup + metric-space-Metric-Semigroup) + short-mul-Metric-Semigroup = pr1 short-associative-mul-Metric-Semigroup + + mul-Metric-Semigroup : + type-Metric-Semigroup → type-Metric-Semigroup → type-Metric-Semigroup + mul-Metric-Semigroup = + mul-short-mul-Metric-Space + metric-space-Metric-Semigroup + short-mul-Metric-Semigroup + + mul-Metric-Semigroup' : + type-Metric-Semigroup → type-Metric-Semigroup → type-Metric-Semigroup + mul-Metric-Semigroup' x y = + mul-Metric-Semigroup y x + + associative-mul-Metric-Semigroup : + (x y z : type-Metric-Semigroup) → + mul-Metric-Semigroup (mul-Metric-Semigroup x y) z ＝ + mul-Metric-Semigroup x (mul-Metric-Semigroup y z) + associative-mul-Metric-Semigroup = + pr2 short-associative-mul-Metric-Semigroup + + semigroup-Metric-Semigroup : Semigroup l1 + semigroup-Metric-Semigroup = + set-Metric-Semigroup , + mul-Metric-Semigroup , + associative-mul-Metric-Semigroup +``` + +## Properties + +### Multiplication in a metric semigroup is short + +```agda +module _ + {l1 l2 : Level} (M : Metric-Semigroup l1 l2) (x : type-Metric-Semigroup M) + where + + is-short-mul-Metric-Semigroup : + is-short-function-Metric-Space + ( metric-space-Metric-Semigroup M) + ( metric-space-Metric-Semigroup M) + ( mul-Metric-Semigroup M x) + is-short-mul-Metric-Semigroup = + is-short-map-short-function-Metric-Space + ( metric-space-Metric-Semigroup M) + ( metric-space-Metric-Semigroup M) + ( map-short-function-Metric-Space + ( metric-space-Metric-Semigroup M) + ( metric-space-of-short-functions-Metric-Space + ( metric-space-Metric-Semigroup M) + ( metric-space-Metric-Semigroup M)) + ( short-mul-Metric-Semigroup M) + ( x)) + + is-short-mul-Metric-Semigroup' : + is-short-function-Metric-Space + ( metric-space-Metric-Semigroup M) + ( metric-space-Metric-Semigroup M) + ( mul-Metric-Semigroup' M x) + is-short-mul-Metric-Semigroup' d y z Nyz = + is-short-map-short-function-Metric-Space + ( metric-space-Metric-Semigroup M) + ( metric-space-of-short-functions-Metric-Space + ( metric-space-Metric-Semigroup M) + ( metric-space-Metric-Semigroup M)) + ( short-mul-Metric-Semigroup M) + ( d) + ( y) + ( z) + ( Nyz) + ( x) +``` From 6e270157dbe1ac25d81308a428f49eafcfd3f3eb Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 17 Jun 2025 18:14:41 +0200 Subject: [PATCH 2/8] fix name --- src/metric-spaces/metric-semigroups.lagda.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/metric-spaces/metric-semigroups.lagda.md b/src/metric-spaces/metric-semigroups.lagda.md index ab97495387..bbf021f56f 100644 --- a/src/metric-spaces/metric-semigroups.lagda.md +++ b/src/metric-spaces/metric-semigroups.lagda.md @@ -56,12 +56,12 @@ module _ ( metric-space-of-short-functions-Metric-Space A A) ( f)) - is-short-associative-prop-mul-Metric-Space : + is-associative-prop-short-mul-Metric-Space : short-function-Metric-Space ( A) ( metric-space-of-short-functions-Metric-Space A A) → Prop l1 - is-short-associative-prop-mul-Metric-Space f = + is-associative-prop-short-mul-Metric-Space f = let μ : type-Metric-Space A → type-Metric-Space A → type-Metric-Space A μ = mul-short-mul-Metric-Space f @@ -87,7 +87,7 @@ module _ Metric-Semigroup : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) Metric-Semigroup l1 l2 = Σ ( Metric-Space l1 l2) - ( type-subtype ∘ is-short-associative-prop-mul-Metric-Space) + ( type-subtype ∘ is-associative-prop-short-mul-Metric-Space) module _ {l1 l2 : Level} (M : Metric-Semigroup l1 l2) @@ -104,7 +104,7 @@ module _ short-associative-mul-Metric-Semigroup : type-subtype - (is-short-associative-prop-mul-Metric-Space metric-space-Metric-Semigroup) + (is-associative-prop-short-mul-Metric-Space metric-space-Metric-Semigroup) short-associative-mul-Metric-Semigroup = pr2 M short-mul-Metric-Semigroup : From 4fff98a2653d610e78ab88910aa0eff1c69d37bc Mon Sep 17 00:00:00 2001 From: malarbol Date: Wed, 18 Jun 2025 02:03:06 +0200 Subject: [PATCH 3/8] move metric-semigroups -> analysis --- src/analysis.lagda.md | 7 +++++++ src/{metric-spaces => analysis}/metric-semigroups.lagda.md | 2 +- src/metric-spaces.lagda.md | 1 - 3 files changed, 8 insertions(+), 2 deletions(-) create mode 100644 src/analysis.lagda.md rename src/{metric-spaces => analysis}/metric-semigroups.lagda.md (99%) diff --git a/src/analysis.lagda.md b/src/analysis.lagda.md new file mode 100644 index 0000000000..6acef1adf4 --- /dev/null +++ b/src/analysis.lagda.md @@ -0,0 +1,7 @@ +# Analysis + +```agda +module analysis where + +open import analysis.metric-semigroups public +``` diff --git a/src/metric-spaces/metric-semigroups.lagda.md b/src/analysis/metric-semigroups.lagda.md similarity index 99% rename from src/metric-spaces/metric-semigroups.lagda.md rename to src/analysis/metric-semigroups.lagda.md index bbf021f56f..bf34b54980 100644 --- a/src/metric-spaces/metric-semigroups.lagda.md +++ b/src/analysis/metric-semigroups.lagda.md @@ -1,7 +1,7 @@ # Metric semigroups ```agda -module metric-spaces.metric-semigroups where +module analysis.metric-semigroups where ```
Imports diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md index eec703fc91..81a017ff2d 100644 --- a/src/metric-spaces.lagda.md +++ b/src/metric-spaces.lagda.md @@ -75,7 +75,6 @@ open import metric-spaces.limits-of-sequences-metric-spaces public open import metric-spaces.limits-of-sequences-premetric-spaces public open import metric-spaces.limits-of-sequences-pseudometric-spaces public open import metric-spaces.lipschitz-functions-metric-spaces public -open import metric-spaces.metric-semigroups public open import metric-spaces.metric-space-of-cauchy-approximations-complete-metric-spaces public open import metric-spaces.metric-space-of-cauchy-approximations-metric-spaces public open import metric-spaces.metric-space-of-cauchy-approximations-saturated-complete-metric-spaces public From 9e36ee4cb60533a860a03b784fda0145abbf31da Mon Sep 17 00:00:00 2001 From: malarbol Date: Fri, 20 Jun 2025 18:10:57 +0200 Subject: [PATCH 4/8] fetch products-metric-spaces from lowasser/add-real-uniform-continuous --- .../products-metric-spaces.lagda.md | 120 ++++++++++++++++++ 1 file changed, 120 insertions(+) create mode 100644 src/metric-spaces/products-metric-spaces.lagda.md diff --git a/src/metric-spaces/products-metric-spaces.lagda.md b/src/metric-spaces/products-metric-spaces.lagda.md new file mode 100644 index 0000000000..48f49e6b2f --- /dev/null +++ b/src/metric-spaces/products-metric-spaces.lagda.md @@ -0,0 +1,120 @@ +# Products of metric spaces + +```agda +module metric-spaces.products-metric-spaces where +``` + +
Imports + +```agda +open import foundation.cartesian-product-types +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.equality-cartesian-product-types +open import foundation.function-types +open import foundation.propositions +open import foundation.sets +open import foundation.universe-levels + +open import metric-spaces.extensional-premetric-structures +open import metric-spaces.metric-spaces +open import metric-spaces.metric-structures +open import metric-spaces.monotonic-premetric-structures +open import metric-spaces.premetric-structures +open import metric-spaces.pseudometric-structures +open import metric-spaces.reflexive-premetric-structures +open import metric-spaces.short-functions-metric-spaces +open import metric-spaces.symmetric-premetric-structures +open import metric-spaces.triangular-premetric-structures +``` + +
+ +## Idea + +A pair of [metric spaces](metric-spaces.metric-spaces.md) induces a metric space +over the [Cartesian product](foundation.cartesian-product-types.md) of the +carrier types of its arguments. + +## Definitions + +### Products of metric spaces + +```agda +module _ + {l1 l2 l3 l4 : Level} (A : Metric-Space l1 l2) (B : Metric-Space l3 l4) + where + + type-product-Metric-Space : UU (l1 ⊔ l3) + type-product-Metric-Space = type-Metric-Space A × type-Metric-Space B + + structure-product-Metric-Space : Premetric (l2 ⊔ l4) type-product-Metric-Space + structure-product-Metric-Space d (a1 , b1) (a2 , b2) = + structure-Metric-Space A d a1 a2 ∧ structure-Metric-Space B d b1 b2 + + is-reflexive-structure-product-Metric-Space : + is-reflexive-Premetric structure-product-Metric-Space + is-reflexive-structure-product-Metric-Space d (a , b) = + ( is-reflexive-structure-Metric-Space A d a , + is-reflexive-structure-Metric-Space B d b) + + is-symmetric-structure-product-Metric-Space : + is-symmetric-Premetric structure-product-Metric-Space + is-symmetric-structure-product-Metric-Space + d (a1 , b1) (a2 , b2) (a1~a2 , b1~b2) = + ( is-symmetric-structure-Metric-Space A d a1 a2 a1~a2 , + is-symmetric-structure-Metric-Space B d b1 b2 b1~b2) + + is-triangular-structure-product-Metric-Space : + is-triangular-Premetric structure-product-Metric-Space + is-triangular-structure-product-Metric-Space + (a1 , b1) (a2 , b2) (a3 , b3) d12 d23 (a1~a2 , b1~b2) (a2~a3 , b2~b3) = + ( is-triangular-structure-Metric-Space A a1 a2 a3 d12 d23 a1~a2 a2~a3 , + is-triangular-structure-Metric-Space B b1 b2 b3 d12 d23 b1~b2 b2~b3) + + is-local-structure-product-Metric-Space : + is-local-Premetric structure-product-Metric-Space + is-local-structure-product-Metric-Space = + is-local-is-tight-Premetric + ( structure-product-Metric-Space) + ( λ (a1 , b1) (a2 , b2) ind-ab1-ab2 → + eq-pair + ( is-tight-structure-Metric-Space A a1 a2 (pr1 ∘ ind-ab1-ab2)) + ( is-tight-structure-Metric-Space B b1 b2 (pr2 ∘ ind-ab1-ab2))) + + is-pseudometric-structure-product-Metric-Space : + is-pseudometric-Premetric structure-product-Metric-Space + is-pseudometric-structure-product-Metric-Space = + is-reflexive-structure-product-Metric-Space , + is-symmetric-structure-product-Metric-Space , + is-triangular-structure-product-Metric-Space + + is-metric-structure-product-Metric-Space : + is-metric-Premetric structure-product-Metric-Space + is-metric-structure-product-Metric-Space = + is-pseudometric-structure-product-Metric-Space , + is-local-structure-product-Metric-Space + + product-Metric-Space : Metric-Space (l1 ⊔ l3) (l2 ⊔ l4) + pr1 product-Metric-Space = + ( type-product-Metric-Space , structure-product-Metric-Space) + pr2 product-Metric-Space = is-metric-structure-product-Metric-Space +``` + +## Properties + +### The projection maps on a product metric space are short + +```agda +module _ + {l1 l2 l3 l4 : Level} (A : Metric-Space l1 l2) (B : Metric-Space l3 l4) + where + + is-short-pr1-product-Metric-Space : + is-short-function-Metric-Space (product-Metric-Space A B) A pr1 + is-short-pr1-product-Metric-Space _ _ _ = pr1 + + is-short-pr2-product-Metric-Space : + is-short-function-Metric-Space (product-Metric-Space A B) B pr2 + is-short-pr2-product-Metric-Space _ _ _ = pr2 +``` From ac05ffd690f5e31c31c60e73235bd7ee2428ffd3 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sat, 21 Jun 2025 04:07:55 +0200 Subject: [PATCH 5/8] WIP CCC metric spaces and short maps --- src/metric-spaces.lagda.md | 1 + .../products-metric-spaces.lagda.md | 340 ++++++++++++++++++ 2 files changed, 341 insertions(+) diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md index 81a017ff2d..6fbbc78e97 100644 --- a/src/metric-spaces.lagda.md +++ b/src/metric-spaces.lagda.md @@ -95,6 +95,7 @@ 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.premetric-spaces public open import metric-spaces.premetric-structures public +open import metric-spaces.products-metric-spaces public open import metric-spaces.pseudometric-spaces public open import metric-spaces.pseudometric-structures public open import metric-spaces.rational-approximations-of-zero public diff --git a/src/metric-spaces/products-metric-spaces.lagda.md b/src/metric-spaces/products-metric-spaces.lagda.md index 48f49e6b2f..74d4ef5bdc 100644 --- a/src/metric-spaces/products-metric-spaces.lagda.md +++ b/src/metric-spaces/products-metric-spaces.lagda.md @@ -7,16 +7,31 @@ module metric-spaces.products-metric-spaces where
Imports ```agda +open import elementary-number-theory.positive-rational-numbers + +open import foundation.action-on-identifications-functions open import foundation.cartesian-product-types +open import foundation.category-of-sets open import foundation.conjunction open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types +open import foundation.equivalences +open import foundation.function-extensionality open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.isomorphisms-of-sets open import foundation.propositions open import foundation.sets +open import foundation.subtypes +open import foundation.universal-property-dependent-pair-types open import foundation.universe-levels +open import metric-spaces.equality-of-metric-spaces open import metric-spaces.extensional-premetric-structures +open import metric-spaces.functions-metric-spaces +open import metric-spaces.isometries-metric-spaces +open import metric-spaces.metric-space-of-short-functions-metric-spaces open import metric-spaces.metric-spaces open import metric-spaces.metric-structures open import metric-spaces.monotonic-premetric-structures @@ -118,3 +133,328 @@ module _ is-short-function-Metric-Space (product-Metric-Space A B) B pr2 is-short-pr2-product-Metric-Space _ _ _ = pr2 ``` + +### Currying short maps from a product metric space + +```agda +module _ + {lx lx' ly ly' lz lz' : Level} + (X : Metric-Space lx lx') (Y : Metric-Space ly ly') (Z : Metric-Space lz lz') + (f : short-function-Metric-Space (product-Metric-Space X Y) Z) + where + + map-ev-pair-short-function-product-Metric-Space : + type-Metric-Space X → + type-Metric-Space Y → + type-Metric-Space Z + map-ev-pair-short-function-product-Metric-Space x y = + map-short-function-Metric-Space + ( product-Metric-Space X Y) + ( Z) + ( f) + ( x , y) + + is-short-map-ev-pair-short-function-product-Metric-Space : + (x : type-Metric-Space X) → + is-short-function-Metric-Space + ( Y) + ( Z) + ( map-ev-pair-short-function-product-Metric-Space x) + is-short-map-ev-pair-short-function-product-Metric-Space x d y y' Nyy' = + is-short-map-short-function-Metric-Space + ( product-Metric-Space X Y) + ( Z) + ( f) + ( d) + ( x , y) + ( x , y') + ( refl-structure-Metric-Space X d x , Nyy') + + short-map-ev-pair-short-function-product-Metric-Space : + (x : type-Metric-Space X) → + short-function-Metric-Space Y Z + short-map-ev-pair-short-function-product-Metric-Space x = + map-ev-pair-short-function-product-Metric-Space x , + is-short-map-ev-pair-short-function-product-Metric-Space x + + is-short-short-map-ev-pair-short-function-product-Metric-Space : + is-short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z) + ( short-map-ev-pair-short-function-product-Metric-Space) + is-short-short-map-ev-pair-short-function-product-Metric-Space d x x' Nxx' y = + is-short-map-short-function-Metric-Space + ( product-Metric-Space X Y) + ( Z) + ( f) + ( d) + ( x , y) + ( x' , y) + ( Nxx' , refl-structure-Metric-Space Y d y) + + ev-pair-short-function-product-Metric-Space : + short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z) + ev-pair-short-function-product-Metric-Space = + short-map-ev-pair-short-function-product-Metric-Space , + is-short-short-map-ev-pair-short-function-product-Metric-Space +``` + +### Currying short maps from a product metric space is preserves and reflects neighborhoods + +```agda +module _ + {lx lx' ly ly' lz lz' : Level} + (X : Metric-Space lx lx') (Y : Metric-Space ly ly') (Z : Metric-Space lz lz') + (d : ℚ⁺) + (f g : short-function-Metric-Space (product-Metric-Space X Y) Z) + where + + preserves-neighborhood-ev-pair-short-function-product-Metric-Space : + neighborhood-Metric-Space + ( metric-space-of-short-functions-Metric-Space + ( product-Metric-Space X Y) + ( Z)) + ( d) + ( f) + ( g) → + neighborhood-Metric-Space + ( metric-space-of-short-functions-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z)) + ( d) + ( ev-pair-short-function-product-Metric-Space X Y Z f) + ( ev-pair-short-function-product-Metric-Space X Y Z g) + preserves-neighborhood-ev-pair-short-function-product-Metric-Space + Nfg x y = + Nfg (x , y) + + reflects-neighborhood-ev-pair-short-function-product-Metric-Space : + neighborhood-Metric-Space + ( metric-space-of-short-functions-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z)) + ( d) + ( ev-pair-short-function-product-Metric-Space X Y Z f) + ( ev-pair-short-function-product-Metric-Space X Y Z g) → + neighborhood-Metric-Space + ( metric-space-of-short-functions-Metric-Space + ( product-Metric-Space X Y) + ( Z)) + ( d) + ( f) + ( g) + reflects-neighborhood-ev-pair-short-function-product-Metric-Space + Nfg (x , y) = + Nfg x y +``` + +### Currying short maps from a product metric space is an isometry + +```agda +module _ + {lx lx' ly ly' lz lz' : Level} + (X : Metric-Space lx lx') (Y : Metric-Space ly ly') (Z : Metric-Space lz lz') + where + + is-isometry-ev-pair-short-function-product-Metric-Space : + is-isometry-Metric-Space + ( metric-space-of-short-functions-Metric-Space + ( product-Metric-Space X Y) + ( Z)) + ( metric-space-of-short-functions-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z)) + ( ev-pair-short-function-product-Metric-Space X Y Z) + is-isometry-ev-pair-short-function-product-Metric-Space d f g = + ( preserves-neighborhood-ev-pair-short-function-product-Metric-Space + X + Y + Z + d + f + g) , + ( reflects-neighborhood-ev-pair-short-function-product-Metric-Space + X + Y + Z + d + f + g) + + isometry-ev-pair-short-function-product-Metric-Space : + isometry-Metric-Space + ( metric-space-of-short-functions-Metric-Space + ( product-Metric-Space X Y) + ( Z)) + ( metric-space-of-short-functions-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z)) + isometry-ev-pair-short-function-product-Metric-Space = + ev-pair-short-function-product-Metric-Space X Y Z , + is-isometry-ev-pair-short-function-product-Metric-Space +``` + +### Uncurrying short maps between metric spaces + +```agda +module _ + {lx lx' ly ly' lz lz' : Level} + (X : Metric-Space lx lx') (Y : Metric-Space ly ly') (Z : Metric-Space lz lz') + where + + map-ind-short-function-product-Metric-Space : + short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z) → + map-type-Metric-Space + ( product-Metric-Space X Y) + ( Z) + map-ind-short-function-product-Metric-Space f (x , y) = + map-short-function-Metric-Space + ( Y) + ( Z) + ( map-short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z) + ( f) + ( x)) + ( y) + + eq-map-ev-pair-ind-short-function-product-Metric-Space : + ( f : + short-function-Metric-Space + ( product-Metric-Space X Y) + ( Z)) → + map-ind-short-function-product-Metric-Space + ( ev-pair-short-function-product-Metric-Space X Y Z f) ＝ + map-short-function-Metric-Space + ( product-Metric-Space X Y) + ( Z) + ( f) + eq-map-ev-pair-ind-short-function-product-Metric-Space f = + refl + + all-eq-preimage-ev-pair-short-function-product-Metric-Space : + ( f : + short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z)) → + ( g g' : short-function-Metric-Space (product-Metric-Space X Y) Z) → + ( ev-pair-short-function-product-Metric-Space X Y Z g ＝ f) → + ( ev-pair-short-function-product-Metric-Space X Y Z g' ＝ f) → + ( g ＝ g') + all-eq-preimage-ev-pair-short-function-product-Metric-Space f g g' H H' = + eq-type-subtype + ( is-short-function-prop-Metric-Space (product-Metric-Space X Y) Z) + ( ( inv (eq-map-ev-pair-ind-short-function-product-Metric-Space g)) ∙ + ( ap map-ind-short-function-product-Metric-Space H) ∙ + ( ap map-ind-short-function-product-Metric-Space (inv H') ∙ + ( eq-map-ev-pair-ind-short-function-product-Metric-Space g'))) + + all-eq-fiber-ev-pair-short-function-product-Metric-Space : + ( f : + short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z)) → + ( g g' : + Σ ( short-function-Metric-Space (product-Metric-Space X Y) Z) + ( λ g → ev-pair-short-function-product-Metric-Space X Y Z g ＝ f)) → + ( g ＝ g') + all-eq-fiber-ev-pair-short-function-product-Metric-Space f g g' = + eq-type-subtype + ( λ h → + Id-Prop + ( set-Metric-Space + ( metric-space-of-short-functions-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z))) + ( ev-pair-short-function-product-Metric-Space X Y Z h) + ( f)) + ( all-eq-preimage-ev-pair-short-function-product-Metric-Space + ( f) + ( pr1 g) + ( pr1 g') + ( pr2 g) + ( pr2 g')) + + is-prop-fiber-ev-pair-short-function-product-Metric-Space : + ( f : + short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z)) → + is-prop + ( Σ ( short-function-Metric-Space (product-Metric-Space X Y) Z) + ( λ g → ev-pair-short-function-product-Metric-Space X Y Z g ＝ f)) + is-prop-fiber-ev-pair-short-function-product-Metric-Space = + is-prop-all-elements-equal ∘ + all-eq-fiber-ev-pair-short-function-product-Metric-Space +``` + +```agda +module _ + {lx lx' ly ly' lz lz' : Level} + (X : Metric-Space lx lx') (Y : Metric-Space ly ly') (Z : Metric-Space lz lz') + where + + is-short-map-ind-short-function-prop-Metric-Space : + Prop (lx ⊔ lx' ⊔ ly ⊔ ly' ⊔ lz ⊔ lz') + is-short-map-ind-short-function-prop-Metric-Space = + Π-Prop + ( short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z)) + ( ( is-short-function-prop-Metric-Space + ( product-Metric-Space X Y) + ( Z)) ∘ + ( map-ind-short-function-product-Metric-Space X Y Z)) + + is-short-map-ind-short-function-Metric-Space : + UU (lx ⊔ lx' ⊔ ly ⊔ ly' ⊔ lz ⊔ lz') + is-short-map-ind-short-function-Metric-Space = + type-Prop is-short-map-ind-short-function-prop-Metric-Space + + is-equiv-ev-pair-is-short-map-ind-short-function-Metric-Space : + is-short-map-ind-short-function-Metric-Space → + is-equiv (ev-pair-short-function-product-Metric-Space X Y Z) + is-equiv-ev-pair-is-short-map-ind-short-function-Metric-Space H = + is-equiv-is-invertible + ( λ f → map-ind-short-function-product-Metric-Space X Y Z f , H f) + ( λ f → + eq-type-subtype + ( is-short-function-prop-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z)) + ( eq-htpy + ( λ x → + eq-type-subtype + ( is-short-function-prop-Metric-Space Y Z) + ( eq-htpy (λ y → refl))))) + ( λ f → + eq-type-subtype + ( is-short-function-prop-Metric-Space + ( product-Metric-Space X Y) + ( Z)) + ( refl)) + + lemma-eq-short-ind-short-function-Metric-Space : + is-short-map-ind-short-function-Metric-Space → + metric-space-of-short-functions-Metric-Space + ( product-Metric-Space X Y) + ( Z) ＝ + metric-space-of-short-functions-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z) + lemma-eq-short-ind-short-function-Metric-Space H = + eq-isometric-equiv-Metric-Space' + ( metric-space-of-short-functions-Metric-Space + ( product-Metric-Space X Y) + ( Z)) + ( metric-space-of-short-functions-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z)) + ( ev-pair-short-function-product-Metric-Space X Y Z , + is-equiv-ev-pair-is-short-map-ind-short-function-Metric-Space H , + is-isometry-ev-pair-short-function-product-Metric-Space X Y Z) +``` From 617f9d1445e2c00423786094d2fe2104fff9304d Mon Sep 17 00:00:00 2001 From: malarbol Date: Sat, 21 Jun 2025 05:18:31 +0200 Subject: [PATCH 6/8] results --- .../products-metric-spaces.lagda.md | 53 +++++++++++++++++-- 1 file changed, 48 insertions(+), 5 deletions(-) diff --git a/src/metric-spaces/products-metric-spaces.lagda.md b/src/metric-spaces/products-metric-spaces.lagda.md index 74d4ef5bdc..2d75b47a2e 100644 --- a/src/metric-spaces/products-metric-spaces.lagda.md +++ b/src/metric-spaces/products-metric-spaces.lagda.md @@ -134,6 +134,49 @@ module _ is-short-pr2-product-Metric-Space _ _ _ = pr2 ``` +### The pairing map is short + +```agda +module _ + {lx lx' ly ly' : Level} (X : Metric-Space lx lx') (Y : Metric-Space ly ly') + where + + is-short-pair-product-Metric-Space : + (x : type-Metric-Space X) → + is-short-function-Metric-Space + ( Y) + ( product-Metric-Space X Y) + ( pair x) + is-short-pair-product-Metric-Space x d y y' Nyy' = + ( refl-structure-Metric-Space X d x , Nyy') + + short-pair-product-Metric-Space : + type-Metric-Space X → + short-function-Metric-Space Y (product-Metric-Space X Y) + short-pair-product-Metric-Space x = + ( pair x , is-short-pair-product-Metric-Space x) + + is-short-short-pair-product-Metric-Space : + is-short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space + ( Y) + ( product-Metric-Space X Y)) + ( short-pair-product-Metric-Space) + is-short-short-pair-product-Metric-Space d x x' Nxx' y = + ( Nxx' , refl-structure-Metric-Space Y d y) + + short-pair-Metric-Space : + short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space + ( Y) + ( product-Metric-Space X Y)) + short-pair-Metric-Space = + short-pair-product-Metric-Space , + is-short-short-pair-product-Metric-Space +``` + ### Currying short maps from a product metric space ```agda @@ -160,15 +203,15 @@ module _ ( Y) ( Z) ( map-ev-pair-short-function-product-Metric-Space x) - is-short-map-ev-pair-short-function-product-Metric-Space x d y y' Nyy' = - is-short-map-short-function-Metric-Space + is-short-map-ev-pair-short-function-product-Metric-Space x d y y' = + ( is-short-map-short-function-Metric-Space ( product-Metric-Space X Y) ( Z) ( f) ( d) ( x , y) - ( x , y') - ( refl-structure-Metric-Space X d x , Nyy') + ( x , y')) ∘ + ( is-short-pair-product-Metric-Space X Y x d y y') short-map-ev-pair-short-function-product-Metric-Space : (x : type-Metric-Space X) → @@ -190,7 +233,7 @@ module _ ( d) ( x , y) ( x' , y) - ( Nxx' , refl-structure-Metric-Space Y d y) + ( is-short-short-pair-product-Metric-Space X Y d x x' Nxx' y) ev-pair-short-function-product-Metric-Space : short-function-Metric-Space From 8ff1357932cc456b5c7a2049ed87870c08ea2e54 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sat, 21 Jun 2025 19:49:06 +0200 Subject: [PATCH 7/8] lemma-is-short-map-ind-short-function-Metric-Space --- ...-of-short-functions-metric-spaces.lagda.md | 70 +++++++++++++++++++ .../products-metric-spaces.lagda.md | 30 +++++--- 2 files changed, 91 insertions(+), 9 deletions(-) diff --git a/src/metric-spaces/metric-space-of-short-functions-metric-spaces.lagda.md b/src/metric-spaces/metric-space-of-short-functions-metric-spaces.lagda.md index 4541811636..a1ada9ab87 100644 --- a/src/metric-spaces/metric-space-of-short-functions-metric-spaces.lagda.md +++ b/src/metric-spaces/metric-space-of-short-functions-metric-spaces.lagda.md @@ -7,6 +7,9 @@ module metric-spaces.metric-space-of-short-functions-metric-spaces where
Imports ```agda +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.identity-types open import foundation.universe-levels open import metric-spaces.metric-space-of-functions-metric-spaces @@ -43,3 +46,70 @@ module _ ( metric-space-of-functions-Metric-Space A B) ( is-short-function-prop-Metric-Space A B) ``` + +### Mapping a short function of short functions + +```agda +module _ + { lx lx' ly ly' lz lz' : Level} + ( X : Metric-Space lx lx') (Y : Metric-Space ly ly') (Z : Metric-Space lz lz') + ( f : + short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z)) + where + + map²-short-function-Metric-Space : + type-Metric-Space X → + type-Metric-Space Y → + type-Metric-Space Z + map²-short-function-Metric-Space = + ( map-short-function-Metric-Space Y Z) ∘ + ( map-short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z) + ( f)) + + is-short-map²-short-function-Metric-Space : + (x : type-Metric-Space X) → + is-short-function-Metric-Space + ( Y) + ( Z) + ( map²-short-function-Metric-Space x) + is-short-map²-short-function-Metric-Space = + ( is-short-map-short-function-Metric-Space Y Z) ∘ + ( map-short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z) + ( f)) + + short-map²-short-function-Metric-Space : + (x : type-Metric-Space X) → short-function-Metric-Space Y Z + short-map²-short-function-Metric-Space x = + map²-short-function-Metric-Space x , + is-short-map²-short-function-Metric-Space x + + is-short-short-map²-short-function-Metric-Space : + is-short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z) + ( short-map²-short-function-Metric-Space) + is-short-short-map²-short-function-Metric-Space = + is-short-map-short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z) + ( f) + + short-short-map²-short-function-Metric-Space : + short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z) + short-short-map²-short-function-Metric-Space = + short-map²-short-function-Metric-Space , + is-short-short-map²-short-function-Metric-Space + + eq-short-short-map²-short-map-function-Metric-Space : + short-short-map²-short-function-Metric-Space ＝ f + eq-short-short-map²-short-map-function-Metric-Space = + refl +``` diff --git a/src/metric-spaces/products-metric-spaces.lagda.md b/src/metric-spaces/products-metric-spaces.lagda.md index 2d75b47a2e..a012a382cf 100644 --- a/src/metric-spaces/products-metric-spaces.lagda.md +++ b/src/metric-spaces/products-metric-spaces.lagda.md @@ -355,15 +355,7 @@ module _ ( product-Metric-Space X Y) ( Z) map-ind-short-function-product-Metric-Space f (x , y) = - map-short-function-Metric-Space - ( Y) - ( Z) - ( map-short-function-Metric-Space - ( X) - ( metric-space-of-short-functions-Metric-Space Y Z) - ( f) - ( x)) - ( y) + map²-short-function-Metric-Space X Y Z f x y eq-map-ev-pair-ind-short-function-product-Metric-Space : ( f : @@ -458,6 +450,26 @@ module _ is-short-map-ind-short-function-Metric-Space = type-Prop is-short-map-ind-short-function-prop-Metric-Space + lemma-is-short-map-ind-short-function-Metric-Space : + ( f : + short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z)) → + ( let + map-f : type-Metric-Space X → type-Metric-Space Y → type-Metric-Space Z + map-f = map²-short-function-Metric-Space X Y Z f + in + (d : ℚ⁺) (x x' : type-Metric-Space X) (y y' : type-Metric-Space Y) → + neighborhood-Metric-Space X d x x' → + neighborhood-Metric-Space Y d y y' → + neighborhood-Metric-Space Z d (map-f x y) (map-f x' y')) → + is-short-function-Metric-Space + ( product-Metric-Space X Y) + ( Z) + ( map-ind-short-function-product-Metric-Space X Y Z f) + lemma-is-short-map-ind-short-function-Metric-Space + f H d (x , y) (x' , y') N = H d x x' y y' (pr1 N) (pr2 N) + is-equiv-ev-pair-is-short-map-ind-short-function-Metric-Space : is-short-map-ind-short-function-Metric-Space → is-equiv (ev-pair-short-function-product-Metric-Space X Y Z) From e10913d3b010f3c192fac809950db8fd72a15656 Mon Sep 17 00:00:00 2001 From: malarbol Date: Sun, 22 Jun 2025 16:48:50 +0200 Subject: [PATCH 8/8] is-uniformly-continuous-map-ind-short-function-product-Metric-Space --- .../products-metric-spaces.lagda.md | 87 +++++++++++++++++++ ...ontinuous-functions-metric-spaces.lagda.md | 5 ++ 2 files changed, 92 insertions(+) diff --git a/src/metric-spaces/products-metric-spaces.lagda.md b/src/metric-spaces/products-metric-spaces.lagda.md index a012a382cf..3e84242cf2 100644 --- a/src/metric-spaces/products-metric-spaces.lagda.md +++ b/src/metric-spaces/products-metric-spaces.lagda.md @@ -16,6 +16,7 @@ open import foundation.conjunction open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types open import foundation.equivalences +open import foundation.existential-quantification open import foundation.function-extensionality open import foundation.function-types open import foundation.homotopies @@ -41,6 +42,7 @@ open import metric-spaces.reflexive-premetric-structures open import metric-spaces.short-functions-metric-spaces open import metric-spaces.symmetric-premetric-structures open import metric-spaces.triangular-premetric-structures +open import metric-spaces.uniformly-continuous-functions-metric-spaces ```
@@ -425,6 +427,91 @@ module _ is-prop-fiber-ev-pair-short-function-product-Metric-Space = is-prop-all-elements-equal ∘ all-eq-fiber-ev-pair-short-function-product-Metric-Space + + lemma-neighborhood-map-ind-short-function-product-Metric-Space : + ( f : + short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z)) → + (dx dy : ℚ⁺) → + (x x' : type-Metric-Space X) → + (y y' : type-Metric-Space Y) → + neighborhood-Metric-Space X dx x x' → + neighborhood-Metric-Space Y dy y y' → + neighborhood-Metric-Space + ( Z) + ( dx +ℚ⁺ dy) + ( map-ind-short-function-product-Metric-Space f ( x , y)) + ( map-ind-short-function-product-Metric-Space f ( x' , y')) + lemma-neighborhood-map-ind-short-function-product-Metric-Space + f dx dy x x' y y' Nxx' Nyy' = + is-triangular-structure-Metric-Space + ( Z) + ( map-ind-short-function-product-Metric-Space f (x , y)) + ( map-ind-short-function-product-Metric-Space f (x' , y)) + ( map-ind-short-function-product-Metric-Space f (x' , y')) + ( dx) + ( dy) + ( is-short-map²-short-function-Metric-Space + ( X) + ( Y) + ( Z) + ( f) + ( x') + ( dy) + ( y) + ( y') + ( Nyy')) + ( is-short-map-short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z) + ( f) + ( dx) + ( x) + ( x') + ( Nxx') + ( y)) + + is-uniformly-continuous-map-ind-short-function-product-Metric-Space : + ( f : + short-function-Metric-Space + ( X) + ( metric-space-of-short-functions-Metric-Space Y Z)) → + is-uniformly-continuous-map-Metric-Space + ( product-Metric-Space X Y) + ( Z) + ( map-ind-short-function-product-Metric-Space f) + is-uniformly-continuous-map-ind-short-function-product-Metric-Space f = + intro-exists + modulus-le-double-le-ℚ⁺ + le-double-is-modulus-of-uc-map-ind-short-function-product-Metric-Space + where + + le-double-is-modulus-of-uc-map-ind-short-function-product-Metric-Space : + is-modulus-of-uniform-continuity-Metric-Space + ( product-Metric-Space X Y) + ( Z) + ( map-ind-short-function-product-Metric-Space f) + ( modulus-le-double-le-ℚ⁺) + le-double-is-modulus-of-uc-map-ind-short-function-product-Metric-Space + (x , y) d (x' , y') (Nxx' , Nyy') = + is-monotonic-structure-Metric-Space + ( Z) + ( map-ind-short-function-product-Metric-Space f (x , y)) + ( map-ind-short-function-product-Metric-Space f (x' , y')) + ( (modulus-le-double-le-ℚ⁺ d) +ℚ⁺ (modulus-le-double-le-ℚ⁺ d)) + ( d) + ( le-double-le-modulus-le-double-le-ℚ⁺ d) + ( lemma-neighborhood-map-ind-short-function-product-Metric-Space + ( f) + ( modulus-le-double-le-ℚ⁺ d) + ( modulus-le-double-le-ℚ⁺ d) + ( x) + ( x') + ( y) + ( y') + ( Nxx') + ( Nyy')) ``` ```agda diff --git a/src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md b/src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md index 2089657c54..cbe4bd1f06 100644 --- a/src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md +++ b/src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md @@ -49,6 +49,11 @@ module _ ( premetric-Metric-Space Y) ( f) + is-modulus-of-uniform-continuity-Metric-Space : + (ℚ⁺ → ℚ⁺) → UU (l1 ⊔ l2 ⊔ l4) + is-modulus-of-uniform-continuity-Metric-Space = + type-Prop ∘ is-modulus-of-uniform-continuity-prop-Metric-Space + modulus-of-uniform-continuity-map-Metric-Space : UU (l1 ⊔ l2 ⊔ l4) modulus-of-uniform-continuity-map-Metric-Space = type-subtype is-modulus-of-uniform-continuity-prop-Metric-Space