diff --git a/config/codespell-ignore.txt b/config/codespell-ignore.txt index 79a8f895b86..e060a3a5f41 100644 --- a/config/codespell-ignore.txt +++ b/config/codespell-ignore.txt @@ -1,3 +1,4 @@ +Nd Tim blacklist couldn diff --git a/src/analysis.lagda.md b/src/analysis.lagda.md index bce22009164..74ccc276304 100644 --- a/src/analysis.lagda.md +++ b/src/analysis.lagda.md @@ -3,13 +3,20 @@ ```agda module analysis where +open import analysis.abelian-groups-metric-quotients-cauchy-pseudocompletions-metric-abelian-groups public +open import analysis.addition-cauchy-approximations-metric-abelian-groups public open import analysis.alternation-sequences-metric-abelian-groups public +open import analysis.cauchy-approximations-metric-abelian-groups public +open import analysis.cauchy-pseudocompletions-metric-abelian-groups public open import analysis.complete-metric-abelian-groups public open import analysis.convergent-series-complete-metric-abelian-groups public open import analysis.convergent-series-metric-abelian-groups public open import analysis.limits-of-sequences-metric-abelian-groups public open import analysis.metric-abelian-groups public +open import analysis.metric-abelian-groups-metric-quotients-cauchy-pseudocompletions-metric-abelian-groups public open import analysis.metric-abelian-groups-of-uniformly-continuous-maps-into-metric-abelian-groups public +open import analysis.metric-quotients-cauchy-pseudocompletions-metric-abelian-groups public +open import analysis.negation-cauchy-approximations-metric-abelian-groups public open import analysis.sequences-metric-abelian-groups public open import analysis.series-complete-metric-abelian-groups public open import analysis.series-metric-abelian-groups public diff --git a/src/analysis/abelian-groups-metric-quotients-cauchy-pseudocompletions-metric-abelian-groups.lagda.md b/src/analysis/abelian-groups-metric-quotients-cauchy-pseudocompletions-metric-abelian-groups.lagda.md new file mode 100644 index 00000000000..a5ae7f941e6 --- /dev/null +++ b/src/analysis/abelian-groups-metric-quotients-cauchy-pseudocompletions-metric-abelian-groups.lagda.md @@ -0,0 +1,461 @@ +# The abelian groups of the metric quotients of Cauchy pseudocompletions of metric abelian groups + +```agda +{-# OPTIONS --lossy-unification #-} + +module analysis.abelian-groups-metric-quotients-cauchy-pseudocompletions-metric-abelian-groups where +``` + +
Imports + +```agda +open import analysis.addition-cauchy-approximations-metric-abelian-groups +open import analysis.cauchy-approximations-metric-abelian-groups +open import analysis.cauchy-pseudocompletions-metric-abelian-groups +open import analysis.metric-abelian-groups +open import analysis.metric-quotients-cauchy-pseudocompletions-metric-abelian-groups +open import analysis.negation-cauchy-approximations-metric-abelian-groups + +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.positive-rational-numbers + +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.binary-functoriality-set-quotients +open import foundation.dependent-pair-types +open import foundation.functoriality-set-quotients +open import foundation.identity-types +open import foundation.set-quotients +open import foundation.sets +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import group-theory.abelian-groups +open import group-theory.groups +open import group-theory.monoids +open import group-theory.semigroups + +open import metric-spaces.similarity-of-elements-pseudometric-spaces +``` + +
+ +## Idea + +The [metric quotient](metric-spaces.metric-quotients-of-pseudometric-spaces.md) +of the +[Cauchy pseudocompletion](analysis.cauchy-pseudocompletions-metric-abelian-groups.md) +of a [metric abelian group](analysis.metric-abelian-groups.md) forms an +[abelian group](group-theory.abelian-groups.md). + +## Definition + +### Addition in the metric quotient + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where + + binary-hom-add-cauchy-pseudocompletion-Metric-Ab : + binary-hom-equivalence-relation + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + binary-hom-add-cauchy-pseudocompletion-Metric-Ab = + ( add-cauchy-approximation-Metric-Ab G , + λ {x} {x'} {y} {y'} → + preserves-sim-add-cauchy-approximation-Metric-Ab G {x} {x'} {y} {y'}) + + add-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + type-metric-quotient-cauchy-pseudocompletion-Metric-Ab G → + type-metric-quotient-cauchy-pseudocompletion-Metric-Ab G → + type-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + add-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + binary-map-set-quotient + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( binary-hom-add-cauchy-pseudocompletion-Metric-Ab) +``` + +## Properties + +### The embedding in the metric quotient of the Cauchy pseudocompletion preserves addition + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where abstract + + add-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + (x y : cauchy-approximation-Metric-Ab G) → + add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + ( in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( x)) + ( in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( y)) ＝ + in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( add-cauchy-approximation-Metric-Ab G x y) + add-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + compute-binary-map-set-quotient + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( binary-hom-add-cauchy-pseudocompletion-Metric-Ab G) + + add-in-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + (x y : type-Metric-Ab G) → + add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + ( in-metric-quotient-cauchy-pseudocompletion-Metric-Ab G x) + ( in-metric-quotient-cauchy-pseudocompletion-Metric-Ab G y) ＝ + in-metric-quotient-cauchy-pseudocompletion-Metric-Ab G (add-Metric-Ab G x y) + add-in-metric-quotient-cauchy-pseudocompletion-Metric-Ab x y = + add-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( const-cauchy-approximation-Metric-Ab G x) + ( const-cauchy-approximation-Metric-Ab G y) ∙ + apply-effectiveness-quotient-map' + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( sim-add-const-cauchy-approximation-Metric-Ab G x y) +``` + +### Addition in the metric quotient of the Cauchy pseudocompletion is associative + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where abstract + + associative-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + (x y z : type-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) → + add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + ( add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G x y) + ( z) ＝ + add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + ( x) + ( add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G y z) + associative-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + triple-induction-set-quotient' + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( λ x y z → + Id-Prop + ( set-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + ( add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + ( add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G x y) + ( z)) + ( add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + ( x) + ( add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G y z))) + ( λ x y z → + let + in-approx-G = + in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + _+~G_ = add-cauchy-approximation-Metric-Ab G + _+∙G_ = add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + in + equational-reasoning + (in-approx-G x +∙G in-approx-G y) +∙G in-approx-G z + ＝ in-approx-G (x +~G y) +∙G in-approx-G z + by + ap-binary + ( _+∙G_) + ( add-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( x) + ( y)) + ( refl) + ＝ in-approx-G ((x +~G y) +~G z) + by + add-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( x +~G y) + ( z) + ＝ in-approx-G (x +~G (y +~G z)) + by + apply-effectiveness-quotient-map' + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab + ( G)) + ( sim-associative-add-cauchy-approximation-Metric-Ab G x y z) + ＝ in-approx-G x +∙G in-approx-G (y +~G z) + by + inv + ( add-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( x) + ( y +~G z)) + ＝ in-approx-G x +∙G (in-approx-G y +∙G in-approx-G z) + by + ap-binary + ( _+∙G_) + ( refl) + ( inv + ( add-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( y) + ( z)))) +``` + +### Addition in the metric quotient of the Cauchy pseudocompletion is commutative + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where abstract + + commutative-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + (x y : type-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) → + add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G x y ＝ + add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G y x + commutative-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + double-induction-set-quotient' + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( λ x y → + Id-Prop + ( set-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + ( add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G x y) + ( add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G y x)) + ( λ x y → + let + in-approx-G = + in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + _+~G_ = add-cauchy-approximation-Metric-Ab G + _+∙G_ = add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + in + equational-reasoning + in-approx-G x +∙G in-approx-G y + ＝ in-approx-G (x +~G y) + by + add-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( x) + ( y) + ＝ in-approx-G (y +~G x) + by + ap + ( in-approx-G) + ( commutative-add-cauchy-approximation-Metric-Ab G x y) + ＝ in-approx-G y +∙G in-approx-G x + by + inv + ( add-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( y) + ( x))) +``` + +### Unit laws of addition in the metric quotient of the Cauchy pseudocompletion + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where abstract + + left-unit-law-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + (x : type-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) → + add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + ( zero-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + ( x) ＝ + x + left-unit-law-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + induction-set-quotient + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( λ x → + Id-Prop + ( set-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + ( add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + ( zero-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + ( x)) + ( x)) + ( λ x → + let + in-approx-G = + in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + _+~G_ = add-cauchy-approximation-Metric-Ab G + _+∙G_ = add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + 0-approx-G = zero-cauchy-approximation-Metric-Ab G + in + equational-reasoning + in-approx-G 0-approx-G +∙G in-approx-G x + ＝ in-approx-G (0-approx-G +~G x) + by + add-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( 0-approx-G) + ( x) + ＝ in-approx-G x + by + apply-effectiveness-quotient-map' + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab + ( G)) + ( sim-left-unit-law-add-cauchy-approximation-Metric-Ab G x)) + + right-unit-law-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + (x : type-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) → + add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + ( x) + ( zero-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) ＝ + x + right-unit-law-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab x = + commutative-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G _ _ ∙ + left-unit-law-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab x +``` + +### Negation in the metric quotient of the Cauchy pseudocompletion + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where abstract + + hom-neg-cauchy-pseudocompletion-Metric-Ab : + hom-equivalence-relation + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + hom-neg-cauchy-pseudocompletion-Metric-Ab = + ( neg-cauchy-approximation-Metric-Ab G , + preserves-sim-map-isometry-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab G) + ( cauchy-pseudocompletion-Metric-Ab G) + ( isometry-neg-cauchy-pseudocompletion-Metric-Ab G) + ( _) + ( _)) + + neg-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + type-metric-quotient-cauchy-pseudocompletion-Metric-Ab G → + type-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + neg-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + map-set-quotient + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( hom-neg-cauchy-pseudocompletion-Metric-Ab) + + abstract + neg-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + (x : cauchy-approximation-Metric-Ab G) → + neg-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( x)) ＝ + in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( neg-cauchy-approximation-Metric-Ab G x) + neg-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + coherence-square-map-set-quotient + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( hom-neg-cauchy-pseudocompletion-Metric-Ab) +``` + +### Inverse laws of addition in the metric quotient of the Cauchy pseudocompletion + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where abstract + + left-inverse-law-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + (x : type-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) → + add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + ( neg-metric-quotient-cauchy-pseudocompletion-Metric-Ab G x) + ( x) ＝ + zero-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + left-inverse-law-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + induction-set-quotient + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( λ x → + Id-Prop + ( set-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + ( add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + ( neg-metric-quotient-cauchy-pseudocompletion-Metric-Ab G x) + ( x)) + ( zero-metric-quotient-cauchy-pseudocompletion-Metric-Ab G)) + ( λ x → + let + in-approx-G = + in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + _+~G_ = add-cauchy-approximation-Metric-Ab G + _+∙G_ = add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + neg-∙G = neg-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + neg-G = neg-cauchy-approximation-Metric-Ab G + 0-approx-G = zero-cauchy-approximation-Metric-Ab G + in + equational-reasoning + neg-∙G (in-approx-G x) +∙G in-approx-G x + ＝ in-approx-G (neg-G x) +∙G in-approx-G x + by + ap-binary + ( _+∙G_) + ( neg-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( x)) + ( refl) + ＝ in-approx-G (neg-G x +~G x) + by + add-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( neg-G x) + ( x) + ＝ in-approx-G 0-approx-G + by + ap + ( in-approx-G) + ( left-inverse-law-add-cauchy-approximation-Metric-Ab G x)) + + right-inverse-law-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + (x : type-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) → + add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + ( x) + ( neg-metric-quotient-cauchy-pseudocompletion-Metric-Ab G x) ＝ + zero-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + right-inverse-law-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab x = + commutative-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G _ _ ∙ + left-inverse-law-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab x +``` + +### The metric quotient of the Cauchy pseudocompletion forms an abelian group + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where + + semigroup-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + Semigroup (l1 ⊔ l2) + semigroup-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + ( set-metric-quotient-cauchy-pseudocompletion-Metric-Ab G , + add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G , + associative-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + + is-unital-semigroup-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + is-unital-Semigroup + ( semigroup-metric-quotient-cauchy-pseudocompletion-Metric-Ab) + is-unital-semigroup-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + ( zero-metric-quotient-cauchy-pseudocompletion-Metric-Ab G , + left-unit-law-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G , + right-unit-law-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + + group-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + Group (l1 ⊔ l2) + group-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + ( semigroup-metric-quotient-cauchy-pseudocompletion-Metric-Ab , + is-unital-semigroup-metric-quotient-cauchy-pseudocompletion-Metric-Ab , + neg-metric-quotient-cauchy-pseudocompletion-Metric-Ab G , + left-inverse-law-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G , + right-inverse-law-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + + ab-metric-quotient-cauchy-pseudocompletion-Metric-Ab : Ab (l1 ⊔ l2) + ab-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + ( group-metric-quotient-cauchy-pseudocompletion-Metric-Ab , + commutative-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) +``` diff --git a/src/analysis/addition-cauchy-approximations-metric-abelian-groups.lagda.md b/src/analysis/addition-cauchy-approximations-metric-abelian-groups.lagda.md new file mode 100644 index 00000000000..e1b92eb14ef --- /dev/null +++ b/src/analysis/addition-cauchy-approximations-metric-abelian-groups.lagda.md @@ -0,0 +1,374 @@ +# Addition of Cauchy approximations in metric abelian groups + +```agda +module analysis.addition-cauchy-approximations-metric-abelian-groups where +``` + +
Imports + +```agda +open import analysis.cauchy-approximations-metric-abelian-groups +open import analysis.cauchy-pseudocompletions-metric-abelian-groups +open import analysis.metric-abelian-groups + +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.binary-functoriality-set-quotients +open import foundation.dependent-pair-types +open import foundation.function-extensionality +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import metric-spaces.short-maps-pseudometric-spaces +``` + +
+ +## Idea + +[Cauchy approximations](analysis.cauchy-approximations-metric-abelian-groups.md) +in [metric abelian groups](analysis.metric-abelian-groups.md) admit an addition +operation whose properties resemble an +[abelian group](group-theory.abelian-groups.md) with respect to the +[similarity relationship](metric-spaces.similarity-of-elements-pseudometric-spaces.md) +of the +[Cauchy pseudocompletion of the metric abelian group](analysis.cauchy-pseudocompletions-metric-abelian-groups.md). + +## Definition + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + ((x , is-approx-x) (y , is-approx-y) : + cauchy-approximation-Metric-Ab G) + where + + opaque + map-add-cauchy-approximation-Metric-Ab : + ℚ⁺ → type-Metric-Ab G + map-add-cauchy-approximation-Metric-Ab ε = + let (δ , _) = bound-double-le-ℚ⁺ ε in add-Metric-Ab G (x δ) (y δ) + + abstract opaque + unfolding map-add-cauchy-approximation-Metric-Ab + + is-cauchy-approximation-map-add-cauchy-approximation-Metric-Ab : + is-cauchy-approximation-Metric-Ab G map-add-cauchy-approximation-Metric-Ab + is-cauchy-approximation-map-add-cauchy-approximation-Metric-Ab δ ε = + let + (δ' , 2δ'<δ) = bound-double-le-ℚ⁺ δ + (ε' , 2ε'<ε) = bound-double-le-ℚ⁺ ε + in + monotonic-neighborhood-Metric-Ab G + ( add-Metric-Ab G (x δ') (y δ')) + ( add-Metric-Ab G (x ε') (y ε')) + ( (δ' +ℚ⁺ ε') +ℚ⁺ (δ' +ℚ⁺ ε')) + ( δ +ℚ⁺ ε) + ( concat-eq-le-ℚ⁺ + { z = δ +ℚ⁺ ε} + ( interchange-law-add-add-ℚ⁺ δ' ε' δ' ε') + ( preserves-le-add-ℚ 2δ'<δ 2ε'<ε)) + ( neighborhood-add-Metric-Ab + ( G) + ( δ' +ℚ⁺ ε') + ( δ' +ℚ⁺ ε') + ( x δ') + ( x ε') + ( y δ') + ( y ε') + ( is-approx-x δ' ε') + ( is-approx-y δ' ε')) + + add-cauchy-approximation-Metric-Ab : cauchy-approximation-Metric-Ab G + add-cauchy-approximation-Metric-Ab = + ( map-add-cauchy-approximation-Metric-Ab , + is-cauchy-approximation-map-add-cauchy-approximation-Metric-Ab) +``` + +## Properties + +### Addition of Cauchy approximations is a similarity-preserving binary map + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where abstract opaque + + unfolding map-add-cauchy-approximation-Metric-Ab + + preserves-sim-add-cauchy-approximation-Metric-Ab : + preserves-sim-binary-map-equivalence-relation + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( add-cauchy-approximation-Metric-Ab G) + preserves-sim-add-cauchy-approximation-Metric-Ab + {x , is-approx-x} {x' , is-approx-x'} {y , is-approx-y} {y' , is-approx-y'} + x~x' y~y' δ ε θ = + let + (δ' , 2δ'<δ) = bound-double-le-ℚ⁺ δ + (ε' , 2ε'<ε) = bound-double-le-ℚ⁺ ε + (θ' , 2θ'<θ) = bound-double-le-ℚ⁺ θ + in + monotonic-neighborhood-Metric-Ab G + ( add-Metric-Ab G (x ε') (y ε')) + ( add-Metric-Ab G (x' θ') (y' θ')) + ( (ε' +ℚ⁺ θ' +ℚ⁺ δ') +ℚ⁺ (ε' +ℚ⁺ θ' +ℚ⁺ δ')) + ( ε +ℚ⁺ θ +ℚ⁺ δ) + ( concat-eq-le-ℚ⁺ + { z = ε +ℚ⁺ θ +ℚ⁺ δ} + ( equational-reasoning + (ε' +ℚ⁺ θ' +ℚ⁺ δ') +ℚ⁺ (ε' +ℚ⁺ θ' +ℚ⁺ δ') + ＝ ((ε' +ℚ⁺ θ') +ℚ⁺ (ε' +ℚ⁺ θ')) +ℚ⁺ (δ' +ℚ⁺ δ') + by interchange-law-add-add-ℚ⁺ _ _ _ _ + ＝ (ε' +ℚ⁺ ε') +ℚ⁺ (θ' +ℚ⁺ θ') +ℚ⁺ (δ' +ℚ⁺ δ') + by ap-add-ℚ⁺ (interchange-law-add-add-ℚ⁺ ε' θ' ε' θ') refl) + ( preserves-le-add-ℚ + ( preserves-le-add-ℚ 2ε'<ε 2θ'<θ) + ( 2δ'<δ))) + ( neighborhood-add-Metric-Ab + ( G) + ( ε' +ℚ⁺ θ' +ℚ⁺ δ') + ( ε' +ℚ⁺ θ' +ℚ⁺ δ') + ( x ε') + ( x' θ') + ( y ε') + ( y' θ') + ( x~x' δ' ε' θ') + ( y~y' δ' ε' θ')) +``` + +### The addition of two constant Cauchy approximations for `x` and `y` is similar to the constant approximation for `x + y` + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where abstract opaque + + unfolding map-add-cauchy-approximation-Metric-Ab + + sim-add-const-cauchy-approximation-Metric-Ab : + (x y : type-Metric-Ab G) → + sim-cauchy-pseudocompletion-Metric-Ab G + ( add-cauchy-approximation-Metric-Ab G + ( const-cauchy-approximation-Metric-Ab G x) + ( const-cauchy-approximation-Metric-Ab G y)) + ( const-cauchy-approximation-Metric-Ab G (add-Metric-Ab G x y)) + sim-add-const-cauchy-approximation-Metric-Ab x y δ ε θ = + refl-neighborhood-Metric-Ab G (ε +ℚ⁺ θ +ℚ⁺ δ) (add-Metric-Ab G x y) +``` + +### Addition is associative relative to the similarity relation + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + (ax@(x , is-approx-x) ay@(y , is-approx-y) az@(z , is-approx-z) : + cauchy-approximation-Metric-Ab G) + where abstract opaque + + unfolding map-add-cauchy-approximation-Metric-Ab + + sim-associative-add-cauchy-approximation-Metric-Ab : + sim-cauchy-pseudocompletion-Metric-Ab G + ( add-cauchy-approximation-Metric-Ab G + ( add-cauchy-approximation-Metric-Ab G ax ay) + ( az)) + ( add-cauchy-approximation-Metric-Ab G + ( ax) + ( add-cauchy-approximation-Metric-Ab G ay az)) + sim-associative-add-cauchy-approximation-Metric-Ab δ ε θ = + let + (ε' , 2ε'<ε) = bound-double-le-ℚ⁺ ε + (ε'' , 2ε''<ε') = bound-double-le-ℚ⁺ ε' + (θ' , 2θ'<θ) = bound-double-le-ℚ⁺ θ + (θ'' , 2θ''<θ') = bound-double-le-ℚ⁺ θ' + xyz1 = add-Metric-Ab G (add-Metric-Ab G (x ε'') (y ε'')) (z ε') + xyz2 = add-Metric-Ab G (add-Metric-Ab G (x θ') (y θ'')) (z θ'') + in + tr + ( neighborhood-Metric-Ab G (ε +ℚ⁺ θ +ℚ⁺ δ) xyz1) + ( associative-add-Metric-Ab G _ _ _) + ( monotonic-neighborhood-Metric-Ab G + ( xyz1) + ( xyz2) + ( (ε'' +ℚ⁺ θ') +ℚ⁺ (ε'' +ℚ⁺ θ'') +ℚ⁺ (ε' +ℚ⁺ θ'')) + ( ε +ℚ⁺ θ +ℚ⁺ δ) + ( concat-eq-le-ℚ⁺ + { z = ε +ℚ⁺ θ +ℚ⁺ δ} + ( equational-reasoning + (ε'' +ℚ⁺ θ') +ℚ⁺ (ε'' +ℚ⁺ θ'') +ℚ⁺ (ε' +ℚ⁺ θ'') + ＝ ((ε'' +ℚ⁺ ε'') +ℚ⁺ (θ' +ℚ⁺ θ'')) +ℚ⁺ (ε' +ℚ⁺ θ'') + by ap-add-ℚ⁺ (interchange-law-add-add-ℚ⁺ _ _ _ _) refl + ＝ ((ε'' +ℚ⁺ ε'') +ℚ⁺ ε') +ℚ⁺ ((θ' +ℚ⁺ θ'') +ℚ⁺ θ'') + by interchange-law-add-add-ℚ⁺ _ _ _ _ + ＝ ((ε'' +ℚ⁺ ε'') +ℚ⁺ ε') +ℚ⁺ (θ' +ℚ⁺ (θ'' +ℚ⁺ θ'')) + by ap-add-ℚ⁺ refl (associative-add-ℚ⁺ _ _ _)) + ( transitive-le-ℚ⁺ + ( ((ε'' +ℚ⁺ ε'') +ℚ⁺ ε') +ℚ⁺ (θ' +ℚ⁺ (θ'' +ℚ⁺ θ''))) + ( (ε' +ℚ⁺ ε') +ℚ⁺ (θ' +ℚ⁺ θ')) + ( ε +ℚ⁺ θ +ℚ⁺ δ) + ( transitive-le-ℚ⁺ + ( (ε' +ℚ⁺ ε') +ℚ⁺ (θ' +ℚ⁺ θ')) + ( ε +ℚ⁺ θ) + ( ε +ℚ⁺ θ +ℚ⁺ δ) + ( le-left-add-ℚ⁺ (ε +ℚ⁺ θ) δ) + ( preserves-le-add-ℚ 2ε'<ε 2θ'<θ)) + ( preserves-le-add-ℚ + ( preserves-le-left-add-ℚ _ _ _ 2ε''<ε') + ( preserves-le-right-add-ℚ _ _ _ 2θ''<θ')))) + ( neighborhood-add-Metric-Ab G + ( (ε'' +ℚ⁺ θ') +ℚ⁺ (ε'' +ℚ⁺ θ'')) + ( ε' +ℚ⁺ θ'') + ( add-Metric-Ab G (x ε'') (y ε'')) + ( add-Metric-Ab G (x θ') (y θ'')) + ( z ε') + ( z θ'') + ( neighborhood-add-Metric-Ab G + ( ε'' +ℚ⁺ θ') + ( ε'' +ℚ⁺ θ'') + ( x ε'') + ( x θ') + ( y ε'') + ( y θ'') + ( is-approx-x ε'' θ') + ( is-approx-y ε'' θ'')) + ( is-approx-z ε' θ''))) +``` + +### Commutativity of addition + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + (x y : cauchy-approximation-Metric-Ab G) + where abstract opaque + + unfolding map-add-cauchy-approximation-Metric-Ab + + commutative-add-cauchy-approximation-Metric-Ab : + add-cauchy-approximation-Metric-Ab G x y ＝ + add-cauchy-approximation-Metric-Ab G y x + commutative-add-cauchy-approximation-Metric-Ab = + eq-type-subtype + ( is-cauchy-approximation-prop-Metric-Ab G) + ( eq-htpy (λ _ → commutative-add-Metric-Ab G _ _)) +``` + +### Unit laws + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + (ax@(x , is-approx-x) : cauchy-approximation-Metric-Ab G) + where abstract opaque + + unfolding map-add-cauchy-approximation-Metric-Ab + + sim-left-unit-law-add-cauchy-approximation-Metric-Ab : + sim-cauchy-pseudocompletion-Metric-Ab G + ( add-cauchy-approximation-Metric-Ab G + ( zero-cauchy-approximation-Metric-Ab G) + ( ax)) + ( ax) + sim-left-unit-law-add-cauchy-approximation-Metric-Ab δ ε θ = + let (ε' , 2ε'<ε) = bound-double-le-ℚ⁺ ε in + monotonic-neighborhood-Metric-Ab G + ( add-Metric-Ab G (zero-Metric-Ab G) (x ε')) + ( x θ) + ( ε' +ℚ⁺ θ) + ( ε +ℚ⁺ θ +ℚ⁺ δ) + ( transitive-le-ℚ⁺ + ( ε' +ℚ⁺ θ) + ( ε +ℚ⁺ θ) + ( ε +ℚ⁺ θ +ℚ⁺ δ) + ( le-left-add-ℚ⁺ (ε +ℚ⁺ θ) δ) + ( preserves-le-left-add-ℚ _ _ _ (le-modulus-le-double-le-ℚ⁺ ε))) + ( inv-tr + ( λ y → neighborhood-Metric-Ab G (ε' +ℚ⁺ θ) y (x θ)) + ( left-unit-law-add-Metric-Ab G (x ε')) + ( is-approx-x ε' θ)) + + sim-right-unit-law-add-cauchy-approximation-Metric-Ab : + sim-cauchy-pseudocompletion-Metric-Ab G + ( add-cauchy-approximation-Metric-Ab G + ( ax) + ( zero-cauchy-approximation-Metric-Ab G)) + ( ax) + sim-right-unit-law-add-cauchy-approximation-Metric-Ab = + tr + ( λ ay → sim-cauchy-pseudocompletion-Metric-Ab G ay ax) + ( commutative-add-cauchy-approximation-Metric-Ab G + ( zero-cauchy-approximation-Metric-Ab G) + ( ax)) + ( sim-left-unit-law-add-cauchy-approximation-Metric-Ab) +``` + +### Left addition is a short map in the Cauchy pseudocompletion of a metric abelian group + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where + + abstract opaque + unfolding map-add-cauchy-approximation-Metric-Ab + + preserves-neighborhood-left-add-cauchy-approximation-Metric-Ab : + (x : cauchy-approximation-Metric-Ab G) → + is-short-map-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab G) + ( cauchy-pseudocompletion-Metric-Ab G) + ( add-cauchy-approximation-Metric-Ab G x) + preserves-neighborhood-left-add-cauchy-approximation-Metric-Ab + (x , is-approx-x) d (y , is-approx-y) (z , is-approx-z) Ndyz δ ε = + let + (δ' , 2δ'<δ) = bound-double-le-ℚ⁺ δ + (ε' , 2ε'<ε) = bound-double-le-ℚ⁺ ε + in + monotonic-neighborhood-Metric-Ab G + ( add-Metric-Ab G (x δ') (y δ')) + ( add-Metric-Ab G (x ε') (z ε')) + ( (δ' +ℚ⁺ ε') +ℚ⁺ (δ' +ℚ⁺ ε' +ℚ⁺ d)) + ( δ +ℚ⁺ ε +ℚ⁺ d) + ( concat-eq-le-ℚ⁺ + { z = δ +ℚ⁺ ε +ℚ⁺ d} + ( equational-reasoning + (δ' +ℚ⁺ ε') +ℚ⁺ (δ' +ℚ⁺ ε' +ℚ⁺ d) + ＝ (δ' +ℚ⁺ ε') +ℚ⁺ (δ' +ℚ⁺ ε') +ℚ⁺ d + by inv (associative-add-ℚ⁺ _ _ _) + ＝ (δ' +ℚ⁺ δ') +ℚ⁺ (ε' +ℚ⁺ ε') +ℚ⁺ d + by ap-add-ℚ⁺ (interchange-law-add-add-ℚ⁺ _ _ _ _) refl) + ( preserves-le-left-add-ℚ _ _ _ (preserves-le-add-ℚ 2δ'<δ 2ε'<ε))) + ( neighborhood-add-Metric-Ab G + ( δ' +ℚ⁺ ε') + ( δ' +ℚ⁺ ε' +ℚ⁺ d) + ( x δ') + ( x ε') + ( y δ') + ( z ε') + ( is-approx-x δ' ε') + ( Ndyz δ' ε')) + + short-map-left-add-cauchy-pseudocompletion-Metric-Ab : + (x : cauchy-approximation-Metric-Ab G) → + short-map-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab G) + ( cauchy-pseudocompletion-Metric-Ab G) + short-map-left-add-cauchy-pseudocompletion-Metric-Ab x = + ( add-cauchy-approximation-Metric-Ab G x , + preserves-neighborhood-left-add-cauchy-approximation-Metric-Ab x) +``` diff --git a/src/analysis/cauchy-approximations-metric-abelian-groups.lagda.md b/src/analysis/cauchy-approximations-metric-abelian-groups.lagda.md new file mode 100644 index 00000000000..f93cdc3d811 --- /dev/null +++ b/src/analysis/cauchy-approximations-metric-abelian-groups.lagda.md @@ -0,0 +1,70 @@ +# Cauchy approximations in metric abelian groups + +```agda +module analysis.cauchy-approximations-metric-abelian-groups where +``` + +
Imports + +```agda +open import analysis.metric-abelian-groups + +open import elementary-number-theory.positive-rational-numbers + +open import foundation.subtypes +open import foundation.universe-levels + +open import metric-spaces.cauchy-approximations-metric-spaces +``` + +
+ +## Idea + +A +{{#concept "Cauchy approximation" Disambiguation="in a metric abelian group" Agda=cauchy-approximation-Metric-Ab}} +in a [metric abelian group](analysis.metric-abelian-groups.md) is a +[Cauchy approximation](metric-spaces.cauchy-approximations-metric-spaces.md) in +the underlying [metric space](metric-spaces.metric-spaces.md). + +## Definition + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where + + is-cauchy-approximation-prop-Metric-Ab : subtype l2 (ℚ⁺ → type-Metric-Ab G) + is-cauchy-approximation-prop-Metric-Ab = + is-cauchy-approximation-prop-Metric-Space (metric-space-Metric-Ab G) + + is-cauchy-approximation-Metric-Ab : (ℚ⁺ → type-Metric-Ab G) → UU l2 + is-cauchy-approximation-Metric-Ab = + is-in-subtype is-cauchy-approximation-prop-Metric-Ab + + cauchy-approximation-Metric-Ab : UU (l1 ⊔ l2) + cauchy-approximation-Metric-Ab = + type-subtype is-cauchy-approximation-prop-Metric-Ab +``` + +## Properties + +### Constant maps in metric abelian groups are Cauchy approximations + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where + + const-cauchy-approximation-Metric-Ab : + type-Metric-Ab G → cauchy-approximation-Metric-Ab G + const-cauchy-approximation-Metric-Ab = + const-cauchy-approximation-Metric-Space (metric-space-Metric-Ab G) + + zero-cauchy-approximation-Metric-Ab : + cauchy-approximation-Metric-Ab G + zero-cauchy-approximation-Metric-Ab = + const-cauchy-approximation-Metric-Ab (zero-Metric-Ab G) +``` diff --git a/src/analysis/cauchy-pseudocompletions-metric-abelian-groups.lagda.md b/src/analysis/cauchy-pseudocompletions-metric-abelian-groups.lagda.md new file mode 100644 index 00000000000..ec533984187 --- /dev/null +++ b/src/analysis/cauchy-pseudocompletions-metric-abelian-groups.lagda.md @@ -0,0 +1,94 @@ +# Cauchy pseudocompletions of metric abelian groups + +```agda +module analysis.cauchy-pseudocompletions-metric-abelian-groups where +``` + +
Imports + +```agda +open import analysis.cauchy-approximations-metric-abelian-groups +open import analysis.metric-abelian-groups + +open import elementary-number-theory.positive-rational-numbers + +open import foundation.binary-relations +open import foundation.equivalence-relations +open import foundation.identity-types +open import foundation.universe-levels + +open import metric-spaces.cauchy-pseudocompletions-of-metric-spaces +open import metric-spaces.pseudometric-spaces +open import metric-spaces.rational-neighborhood-relations +open import metric-spaces.similarity-of-elements-pseudometric-spaces +``` + +
+ +## Idea + +The +{{#concept "Cauchy pseudocompletion" Disambiguation="of a metric abelian group" Agda=cauchy-pseudocompletion-Metric-Ab}} +of a [metric abelian group](analysis.metric-abelian-groups.md) is the +[Cauchy pseudocompletion](metric-spaces.cauchy-pseudocompletions-of-metric-spaces.md) +of the underlying [metric space](metric-spaces.metric-spaces.md). + +## Definition + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where + + cauchy-pseudocompletion-Metric-Ab : Pseudometric-Space (l1 ⊔ l2) l2 + cauchy-pseudocompletion-Metric-Ab = + cauchy-pseudocompletion-Metric-Space (metric-space-Metric-Ab G) + + neighborhood-prop-cauchy-pseudocompletion-Metric-Ab : + Rational-Neighborhood-Relation l2 (cauchy-approximation-Metric-Ab G) + neighborhood-prop-cauchy-pseudocompletion-Metric-Ab = + neighborhood-prop-Pseudometric-Space cauchy-pseudocompletion-Metric-Ab + + neighborhood-cauchy-pseudocompletion-Metric-Ab : + ℚ⁺ → Relation l2 (cauchy-approximation-Metric-Ab G) + neighborhood-cauchy-pseudocompletion-Metric-Ab = + neighborhood-Pseudometric-Space cauchy-pseudocompletion-Metric-Ab + + equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab : + equivalence-relation l2 (cauchy-approximation-Metric-Ab G) + equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab = + equivalence-relation-sim-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab) + + sim-prop-cauchy-pseudocompletion-Metric-Ab : + Relation-Prop l2 (cauchy-approximation-Metric-Ab G) + sim-prop-cauchy-pseudocompletion-Metric-Ab = + sim-prop-Pseudometric-Space cauchy-pseudocompletion-Metric-Ab + + sim-cauchy-pseudocompletion-Metric-Ab : + Relation l2 (cauchy-approximation-Metric-Ab G) + sim-cauchy-pseudocompletion-Metric-Ab = + sim-Pseudometric-Space cauchy-pseudocompletion-Metric-Ab +``` + +## Properties + +### If two constant Cauchy approximations are similar, they have the same constant + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where abstract + + eq-sim-const-cauchy-approximation-cauchy-pseudocompletion-Metric-Ab : + (x y : type-Metric-Ab G) → + sim-cauchy-pseudocompletion-Metric-Ab G + ( const-cauchy-approximation-Metric-Ab G x) + ( const-cauchy-approximation-Metric-Ab G y) → + x ＝ y + eq-sim-const-cauchy-approximation-cauchy-pseudocompletion-Metric-Ab = + eq-sim-const-cauchy-approximation-cauchy-pseudocompletion-Metric-Space + ( metric-space-Metric-Ab G) +``` diff --git a/src/analysis/metric-abelian-groups-metric-quotients-cauchy-pseudocompletions-metric-abelian-groups.lagda.md b/src/analysis/metric-abelian-groups-metric-quotients-cauchy-pseudocompletions-metric-abelian-groups.lagda.md new file mode 100644 index 00000000000..5a56b5722ef --- /dev/null +++ b/src/analysis/metric-abelian-groups-metric-quotients-cauchy-pseudocompletions-metric-abelian-groups.lagda.md @@ -0,0 +1,253 @@ +# The metric abelian group of the metric quotient of the Cauchy pseudocompletion of metric abelian groups + +```agda +{-# OPTIONS --lossy-unification #-} + +module analysis.metric-abelian-groups-metric-quotients-cauchy-pseudocompletions-metric-abelian-groups where +``` + +
Imports + +```agda +open import analysis.abelian-groups-metric-quotients-cauchy-pseudocompletions-metric-abelian-groups +open import analysis.addition-cauchy-approximations-metric-abelian-groups +open import analysis.cauchy-pseudocompletions-metric-abelian-groups +open import analysis.metric-abelian-groups +open import analysis.metric-quotients-cauchy-pseudocompletions-metric-abelian-groups + +open import elementary-number-theory.positive-rational-numbers + +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.binary-transport +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.propositional-truncations +open import foundation.set-quotients +open import foundation.universe-levels + +open import group-theory.abelian-groups +open import group-theory.homomorphisms-abelian-groups + +open import metric-spaces.cauchy-pseudocompletions-of-metric-spaces +open import metric-spaces.functoriality-isometries-cauchy-pseudocompletions-of-metric-spaces +open import metric-spaces.isometries-metric-spaces +open import metric-spaces.isometries-pseudometric-spaces +open import metric-spaces.metric-spaces +open import metric-spaces.short-maps-metric-spaces +open import metric-spaces.short-maps-pseudometric-spaces +open import metric-spaces.unit-map-metric-quotients-of-pseudometric-spaces +``` + +
+ +## Idea + +The [metric quotient](metric-spaces.metric-quotients-of-pseudometric-spaces.md) +of the +[Cauchy pseudocompletion](analysis.cauchy-pseudocompletions-metric-abelian-groups.md) +of a [metric abelian group](analysis.metric-abelian-groups.md) is itself a +metric abelian group. + +## Proof + +### Negation is a short map + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where abstract + + is-short-map-neg-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + is-short-map-Metric-Space + ( metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + ( metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + ( neg-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + is-short-map-neg-metric-quotient-cauchy-pseudocompletion-Metric-Ab + d x y Ndxy = + let + open + do-syntax-trunc-Prop + ( neighborhood-prop-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( d) + ( neg-metric-quotient-cauchy-pseudocompletion-Metric-Ab G x) + ( neg-metric-quotient-cauchy-pseudocompletion-Metric-Ab G y)) + in do + (x' , ux'=x) ← + is-surjective-quotient-map + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( x) + (y' , uy'=y) ← + is-surjective-quotient-map + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( y) + binary-tr + ( neighborhood-metric-quotient-cauchy-pseudocompletion-Metric-Ab G d) + ( ( inv + ( neg-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( x'))) ∙ + ( ap (neg-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) ux'=x)) + ( ( inv + ( neg-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( y'))) ∙ + ( ap (neg-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) uy'=y)) + ( preserves-neighborhoods-map-isometry-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab G) + ( pseudometric-Metric-Space + ( metric-quotient-cauchy-pseudocompletion-Metric-Ab G)) + ( comp-isometry-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab G) + ( cauchy-pseudocompletion-Metric-Ab G) + ( pseudometric-Metric-Space + ( metric-quotient-cauchy-pseudocompletion-Metric-Ab G)) + ( isometry-unit-metric-quotient-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab G)) + ( isometry-cauchy-pseudocompletion-Metric-Space + ( metric-space-Metric-Ab G) + ( metric-space-Metric-Ab G) + ( isometry-neg-Metric-Ab G))) + ( d) + ( x') + ( y') + ( reflects-neighborhoods-map-unit-metric-quotient-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab G) + ( d) + ( x') + ( y') + ( binary-tr + ( neighborhood-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( d)) + ( inv ux'=x) + ( inv uy'=y) + ( Ndxy)))) +``` + +### Left addition is a short map on the metric quotient of the Cauchy pseudocompletion of a metric abelian group + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where abstract + + is-short-map-left-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + (x : type-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) → + is-short-map-Metric-Space + ( metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + ( metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + ( add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G x) + is-short-map-left-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab + x d y z Ndyz = + let + open + do-syntax-trunc-Prop + ( neighborhood-prop-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( d) + ( add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G x y) + ( add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G x z)) + in do + (x' , ux'=x) ← + is-surjective-quotient-map + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( x) + (y' , uy'=y) ← + is-surjective-quotient-map + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( y) + (z' , uz'=z) ← + is-surjective-quotient-map + ( equivalence-relation-sim-cauchy-pseudocompletion-Metric-Ab G) + ( z) + binary-tr + ( neighborhood-metric-quotient-cauchy-pseudocompletion-Metric-Ab G d) + ( ( inv + ( add-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( x') + ( y'))) ∙ + ( ap-binary + ( add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + ( ux'=x) + ( uy'=y))) + ( ( inv + ( add-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( x') + ( z'))) ∙ + ( ap-binary + ( add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + ( ux'=x) + ( uz'=z))) + ( is-short-map-short-map-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab G) + ( pseudometric-Metric-Space + ( metric-quotient-cauchy-pseudocompletion-Metric-Ab G)) + ( comp-short-map-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab G) + ( cauchy-pseudocompletion-Metric-Ab G) + ( pseudometric-Metric-Space + ( metric-quotient-cauchy-pseudocompletion-Metric-Ab G)) + ( short-map-unit-metric-quotient-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab G)) + ( short-map-left-add-cauchy-pseudocompletion-Metric-Ab G x')) + ( d) + ( y') + ( z') + ( reflects-neighborhoods-map-unit-metric-quotient-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab G) + ( d) + ( y') + ( z') + ( binary-tr + ( neighborhood-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( G) + ( d)) + ( inv uy'=y) + ( inv uz'=z) + ( Ndyz)))) +``` + +## Definition + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where + + metric-ab-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + Metric-Ab (l1 ⊔ l2) (l1 ⊔ l2) + metric-ab-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + ( ab-metric-quotient-cauchy-pseudocompletion-Metric-Ab G , + pseudometric-structure-Metric-Space + ( metric-quotient-cauchy-pseudocompletion-Metric-Ab G) , + is-extensional-pseudometric-Metric-Space + ( metric-quotient-cauchy-pseudocompletion-Metric-Ab G) , + is-short-map-neg-metric-quotient-cauchy-pseudocompletion-Metric-Ab G , + is-short-map-left-add-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) +``` + +## Properties + +### The embedding of the metric abelian group into the metric abelian group of the metric quotient of its Cauchy pseudocompletion is an Abelian group homomorphism + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where + + hom-in-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + hom-Ab + ( ab-Metric-Ab G) + ( ab-metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + hom-in-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + ( in-metric-quotient-cauchy-pseudocompletion-Metric-Ab G , + inv (add-in-metric-quotient-cauchy-pseudocompletion-Metric-Ab G _ _)) +``` diff --git a/src/analysis/metric-abelian-groups-of-uniformly-continuous-maps-into-metric-abelian-groups.lagda.md b/src/analysis/metric-abelian-groups-of-uniformly-continuous-maps-into-metric-abelian-groups.lagda.md index ecce1868350..f54b856bfe8 100644 --- a/src/analysis/metric-abelian-groups-of-uniformly-continuous-maps-into-metric-abelian-groups.lagda.md +++ b/src/analysis/metric-abelian-groups-of-uniformly-continuous-maps-into-metric-abelian-groups.lagda.md @@ -18,11 +18,11 @@ open import group-theory.function-abelian-groups open import group-theory.subgroups-abelian-groups open import metric-spaces.cartesian-products-metric-spaces -open import metric-spaces.isometries-metric-spaces open import metric-spaces.maps-metric-spaces open import metric-spaces.metric-space-of-uniformly-continuous-maps-metric-spaces open import metric-spaces.metric-spaces open import metric-spaces.pseudometric-spaces +open import metric-spaces.short-maps-metric-spaces open import metric-spaces.uniformly-continuous-maps-metric-spaces ``` @@ -154,26 +154,24 @@ module _ add-Ab ab-uniformly-continuous-map-Metric-Ab abstract - is-isometry-neg-uniformly-continuous-map-Metric-Ab : - is-isometry-Metric-Space + is-short-map-neg-uniformly-continuous-map-Metric-Ab : + is-short-map-Metric-Space ( metric-space-uniformly-continuous-map-Metric-Ab) ( metric-space-uniformly-continuous-map-Metric-Ab) ( neg-uniformly-continuous-map-Metric-Ab) - is-isometry-neg-uniformly-continuous-map-Metric-Ab - d f@(map-f , _) g@(map-g , _) = - iff-Π-iff-family - ( λ x → is-isometry-neg-Metric-Ab G d (map-f x) (map-g x)) + is-short-map-neg-uniformly-continuous-map-Metric-Ab + d f@(map-f , _) g@(map-g , _) Ndfg x = + is-short-map-neg-Metric-Ab G d (map-f x) (map-g x) (Ndfg x) - is-isometry-add-uniformly-continuous-map-Metric-Ab : + is-short-map-add-uniformly-continuous-map-Metric-Ab : (f : type-uniformly-continuous-map-Metric-Ab) → - is-isometry-Metric-Space + is-short-map-Metric-Space ( metric-space-uniformly-continuous-map-Metric-Ab) ( metric-space-uniformly-continuous-map-Metric-Ab) ( add-uniformly-continuous-map-Metric-Ab f) - is-isometry-add-uniformly-continuous-map-Metric-Ab - (map-f , _) d (map-g , _) (map-h , _) = - iff-Π-iff-family - ( λ x → is-isometry-add-Metric-Ab G (map-f x) d (map-g x) (map-h x)) + is-short-map-add-uniformly-continuous-map-Metric-Ab + (map-f , _) d (map-g , _) (map-h , _) Ndgh x = + is-short-map-add-Metric-Ab G (map-f x) d (map-g x) (map-h x) (Ndgh x) metric-ab-uniformly-continuous-map-Metric-Ab : Metric-Ab (l1 ⊔ l2 ⊔ l3 ⊔ l4) (l1 ⊔ l4) @@ -182,6 +180,6 @@ module _ pseudometric-structure-uniformly-continuous-map-Metric-Ab , is-extensional-pseudometric-Metric-Space ( metric-space-uniformly-continuous-map-Metric-Ab) , - is-isometry-neg-uniformly-continuous-map-Metric-Ab , - is-isometry-add-uniformly-continuous-map-Metric-Ab) + is-short-map-neg-uniformly-continuous-map-Metric-Ab , + is-short-map-add-uniformly-continuous-map-Metric-Ab) ``` diff --git a/src/analysis/metric-abelian-groups.lagda.md b/src/analysis/metric-abelian-groups.lagda.md index bf9a4eaf0c3..57eaaa6771c 100644 --- a/src/analysis/metric-abelian-groups.lagda.md +++ b/src/analysis/metric-abelian-groups.lagda.md @@ -7,16 +7,19 @@ module analysis.metric-abelian-groups 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-binary-functions open import foundation.binary-relations +open import foundation.binary-transport open import foundation.cartesian-product-types open import foundation.conjunction open import foundation.dependent-pair-types open import foundation.dependent-products-propositions open import foundation.function-extensionality open import foundation.identity-types +open import foundation.logical-equivalences open import foundation.propositions open import foundation.transport-along-identifications open import foundation.universe-levels @@ -26,11 +29,15 @@ open import group-theory.abelian-groups open import metric-spaces.cartesian-products-metric-spaces open import metric-spaces.extensionality-pseudometric-spaces open import metric-spaces.isometries-metric-spaces -open import metric-spaces.isometries-pseudometric-spaces open import metric-spaces.metric-spaces open import metric-spaces.modulated-uniformly-continuous-maps-metric-spaces +open import metric-spaces.monotonic-rational-neighborhood-relations 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.short-maps-metric-spaces +open import metric-spaces.short-maps-pseudometric-spaces +open import metric-spaces.triangular-rational-neighborhood-relations open import metric-spaces.uniformly-continuous-maps-metric-spaces ``` @@ -41,8 +48,9 @@ open import metric-spaces.uniformly-continuous-maps-metric-spaces A {{#concept "metric abelian group" Agda=Metric-Ab}} is an [abelian group](group-theory.abelian-groups.md) endowed with the structure of a [metric space](metric-spaces.metric-spaces.md) such that the addition operation -and negation operation are -[isometries](metric-spaces.isometries-metric-spaces.md). +and negation operation are [short](metric-spaces.short-maps-metric-spaces.md) +(which, together with the group operations, implies they are +[isometries](metric-spaces.isometries-metric-spaces.md)). ## Definition @@ -55,10 +63,10 @@ is-metric-ab-prop-Ab-Pseudometric-Structure G M = MS = (type-Ab G , M) in is-extensional-prop-Pseudometric-Space MS ∧ - is-isometry-prop-Pseudometric-Space MS MS (neg-Ab G) ∧ + is-short-map-prop-Pseudometric-Space MS MS (neg-Ab G) ∧ Π-Prop ( type-Ab G) - ( λ x → is-isometry-prop-Pseudometric-Space MS MS (add-Ab G x)) + ( λ x → is-short-map-prop-Pseudometric-Space MS MS (add-Ab G x)) is-metric-ab-Ab-Pseudometric-Structure : {l1 l2 : Level} (G : Ab l1) (M : Pseudometric-Structure l2 (type-Ab G)) → @@ -89,32 +97,52 @@ module _ ```agda module _ {l1 l2 : Level} (MG : Metric-Ab l1 l2) + (let ab-MG = ab-Metric-Ab MG) where zero-Metric-Ab : type-Metric-Ab MG - zero-Metric-Ab = zero-Ab (ab-Metric-Ab MG) + zero-Metric-Ab = zero-Ab ab-MG add-Metric-Ab : type-Metric-Ab MG → type-Metric-Ab MG → type-Metric-Ab MG - add-Metric-Ab = add-Ab (ab-Metric-Ab MG) + add-Metric-Ab = add-Ab ab-MG add-Metric-Ab' : type-Metric-Ab MG → type-Metric-Ab MG → type-Metric-Ab MG - add-Metric-Ab' = add-Ab' (ab-Metric-Ab MG) + add-Metric-Ab' = add-Ab' ab-MG ap-add-Metric-Ab : {x x' y y' : type-Metric-Ab MG} → x ＝ x' → y ＝ y' → add-Metric-Ab x y ＝ add-Metric-Ab x' y' - ap-add-Metric-Ab = ap-add-Ab (ab-Metric-Ab MG) + ap-add-Metric-Ab = ap-add-Ab ab-MG neg-Metric-Ab : type-Metric-Ab MG → type-Metric-Ab MG - neg-Metric-Ab = neg-Ab (ab-Metric-Ab MG) + neg-Metric-Ab = neg-Ab ab-MG abstract + left-unit-law-add-Metric-Ab : + (x : type-Metric-Ab MG) → add-Metric-Ab zero-Metric-Ab x ＝ x + left-unit-law-add-Metric-Ab = left-unit-law-add-Ab ab-MG + + associative-add-Metric-Ab : + (x y z : type-Metric-Ab MG) → + add-Metric-Ab (add-Metric-Ab x y) z ＝ add-Metric-Ab x (add-Metric-Ab y z) + associative-add-Metric-Ab = associative-add-Ab ab-MG + + left-inverse-law-add-Metric-Ab : + (x : type-Metric-Ab MG) → + add-Metric-Ab (neg-Metric-Ab x) x ＝ zero-Metric-Ab + left-inverse-law-add-Metric-Ab = left-inverse-law-add-Ab ab-MG + + right-inverse-law-add-Metric-Ab : + (x : type-Metric-Ab MG) → + add-Metric-Ab x (neg-Metric-Ab x) ＝ zero-Metric-Ab + right-inverse-law-add-Metric-Ab = right-inverse-law-add-Ab ab-MG + neg-zero-Metric-Ab : neg-Metric-Ab zero-Metric-Ab ＝ zero-Metric-Ab - neg-zero-Metric-Ab = neg-zero-Ab (ab-Metric-Ab MG) + neg-zero-Metric-Ab = neg-zero-Ab ab-MG neg-neg-Metric-Ab : (x : type-Metric-Ab MG) → neg-Metric-Ab (neg-Metric-Ab x) ＝ x - neg-neg-Metric-Ab = neg-neg-Ab (ab-Metric-Ab MG) + neg-neg-Metric-Ab = neg-neg-Ab ab-MG diff-Metric-Ab : type-Metric-Ab MG → type-Metric-Ab MG → type-Metric-Ab MG diff-Metric-Ab x y = add-Metric-Ab x (neg-Metric-Ab y) @@ -122,16 +150,16 @@ module _ ap-diff-Metric-Ab : {x x' y y' : type-Metric-Ab MG} → x ＝ x' → y ＝ y' → diff-Metric-Ab x y ＝ diff-Metric-Ab x' y' - ap-diff-Metric-Ab = ap-right-subtraction-Ab (ab-Metric-Ab MG) + ap-diff-Metric-Ab = ap-right-subtraction-Ab ab-MG commutative-add-Metric-Ab : (x y : type-Metric-Ab MG) → add-Metric-Ab x y ＝ add-Metric-Ab y x - commutative-add-Metric-Ab = commutative-add-Ab (ab-Metric-Ab MG) + commutative-add-Metric-Ab = commutative-add-Ab ab-MG is-identity-right-conjugation-Metric-Ab : (x y : type-Metric-Ab MG) → add-Metric-Ab x (diff-Metric-Ab y x) ＝ y is-identity-right-conjugation-Metric-Ab = - is-identity-right-conjugation-Ab (ab-Metric-Ab MG) + is-identity-right-conjugation-Ab ab-MG ``` ### Metric properties of metric abelian groups @@ -162,13 +190,55 @@ module _ neighborhood-Metric-Ab : ℚ⁺ → Relation l2 (type-Metric-Ab MG) neighborhood-Metric-Ab = neighborhood-Metric-Space metric-space-Metric-Ab + refl-neighborhood-Metric-Ab : + is-reflexive-Rational-Neighborhood-Relation neighborhood-prop-Metric-Ab + refl-neighborhood-Metric-Ab = + refl-neighborhood-Metric-Space metric-space-Metric-Ab + + monotonic-neighborhood-Metric-Ab : + is-monotonic-Rational-Neighborhood-Relation neighborhood-prop-Metric-Ab + monotonic-neighborhood-Metric-Ab = + monotonic-neighborhood-Metric-Space metric-space-Metric-Ab + + triangular-neighborhood-Metric-Ab : + is-triangular-Rational-Neighborhood-Relation neighborhood-prop-Metric-Ab + triangular-neighborhood-Metric-Ab = + triangular-neighborhood-Metric-Space metric-space-Metric-Ab + + is-short-map-add-Metric-Ab : + (x : type-Metric-Ab MG) → + is-short-map-Metric-Space + ( metric-space-Metric-Ab) + ( metric-space-Metric-Ab) + ( add-Metric-Ab MG x) + is-short-map-add-Metric-Ab = pr2 (pr2 (pr2 (pr2 MG))) + + abstract + reflects-neighborhoods-left-add-Metric-Ab : + (x : type-Metric-Ab MG) + (d : ℚ⁺) + (y z : type-Metric-Ab MG) → + neighborhood-Metric-Ab + ( d) + ( add-Metric-Ab MG x y) + ( add-Metric-Ab MG x z) → + neighborhood-Metric-Ab d y z + reflects-neighborhoods-left-add-Metric-Ab x d y z Nd⟨x+y⟩⟨x+z⟩ = + binary-tr + ( neighborhood-Metric-Ab d) + ( is-retraction-left-subtraction-Ab (ab-Metric-Ab MG) x y) + ( is-retraction-left-subtraction-Ab (ab-Metric-Ab MG) x z) + ( is-short-map-add-Metric-Ab (neg-Metric-Ab MG x) d _ _ Nd⟨x+y⟩⟨x+z⟩) + is-isometry-add-Metric-Ab : (x : type-Metric-Ab MG) → is-isometry-Metric-Space ( metric-space-Metric-Ab) ( metric-space-Metric-Ab) ( add-Metric-Ab MG x) - is-isometry-add-Metric-Ab = pr2 (pr2 (pr2 (pr2 MG))) + is-isometry-add-Metric-Ab x d y z = + ( is-short-map-add-Metric-Ab x d y z , + reflects-neighborhoods-left-add-Metric-Ab x d y z) isometry-add-Metric-Ab : (x : type-Metric-Ab MG) → @@ -200,12 +270,33 @@ module _ isometry-add-Metric-Ab' x = ( add-Metric-Ab' MG x , is-isometry-add-Metric-Ab' x) + is-short-map-neg-Metric-Ab : + is-short-map-Metric-Space + ( metric-space-Metric-Ab) + ( metric-space-Metric-Ab) + ( neg-Metric-Ab MG) + is-short-map-neg-Metric-Ab = pr1 (pr2 (pr2 (pr2 MG))) + + abstract + reflects-neighborhoods-neg-Metric-Ab : + (d : ℚ⁺) (x y : type-Metric-Ab MG) → + neighborhood-Metric-Ab d (neg-Metric-Ab MG x) (neg-Metric-Ab MG y) → + neighborhood-Metric-Ab d x y + reflects-neighborhoods-neg-Metric-Ab d x y Nd⟨-x⟩⟨-y⟩ = + binary-tr + ( neighborhood-Metric-Ab d) + ( neg-neg-Metric-Ab MG x) + ( neg-neg-Metric-Ab MG y) + ( is-short-map-neg-Metric-Ab d _ _ Nd⟨-x⟩⟨-y⟩) + is-isometry-neg-Metric-Ab : is-isometry-Metric-Space ( metric-space-Metric-Ab) ( metric-space-Metric-Ab) ( neg-Metric-Ab MG) - is-isometry-neg-Metric-Ab = pr1 (pr2 (pr2 (pr2 MG))) + is-isometry-neg-Metric-Ab d x y = + ( is-short-map-neg-Metric-Ab d x y , + reflects-neighborhoods-neg-Metric-Ab d x y) isometry-neg-Metric-Ab : isometry-Metric-Space @@ -253,3 +344,35 @@ module _ ( metric-space-Metric-Ab G) ( modulated-uniformly-continuous-map-add-pair-Metric-Ab) ``` + +### Neighborhoods of sums in metric abelian groups + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + (dxx' dyy' : ℚ⁺) + (x x' y y' : type-Metric-Ab G) + where abstract + + neighborhood-add-Metric-Ab : + neighborhood-Metric-Ab G dxx' x x' → + neighborhood-Metric-Ab G dyy' y y' → + neighborhood-Metric-Ab G + ( dxx' +ℚ⁺ dyy') + ( add-Metric-Ab G x y) + ( add-Metric-Ab G x' y') + neighborhood-add-Metric-Ab Nxx' Nyy' = + triangular-neighborhood-Metric-Ab G + ( add-Metric-Ab G x y) + ( add-Metric-Ab G x' y) + ( add-Metric-Ab G x' y') + ( dxx') + ( dyy') + ( forward-implication + ( is-isometry-add-Metric-Ab G x' dyy' y y') + ( Nyy')) + ( forward-implication + ( is-isometry-add-Metric-Ab' G y dxx' x x') + ( Nxx')) +``` diff --git a/src/analysis/metric-quotients-cauchy-pseudocompletions-metric-abelian-groups.lagda.md b/src/analysis/metric-quotients-cauchy-pseudocompletions-metric-abelian-groups.lagda.md new file mode 100644 index 00000000000..99750ce71e2 --- /dev/null +++ b/src/analysis/metric-quotients-cauchy-pseudocompletions-metric-abelian-groups.lagda.md @@ -0,0 +1,149 @@ +# Metric quotients of Cauchy pseudocompletions of metric abelian groups + +```agda +{-# OPTIONS --lossy-unification #-} + +module analysis.metric-quotients-cauchy-pseudocompletions-metric-abelian-groups where +``` + +
Imports + +```agda +open import analysis.cauchy-approximations-metric-abelian-groups +open import analysis.cauchy-pseudocompletions-metric-abelian-groups +open import analysis.metric-abelian-groups + +open import elementary-number-theory.positive-rational-numbers + +open import foundation.binary-relations +open import foundation.dependent-pair-types +open import foundation.embeddings +open import foundation.sets +open import foundation.universe-levels + +open import metric-spaces.cauchy-pseudocompletions-of-metric-spaces +open import metric-spaces.isometries-metric-spaces +open import metric-spaces.isometries-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.unit-map-metric-quotients-of-pseudometric-spaces +``` + +
+ +## Idea + +The [metric quotient](metric-spaces.metric-quotients-of-pseudometric-spaces.md) +of the +[Cauchy pseudocompletion](analysis.cauchy-pseudocompletions-metric-abelian-groups.md) +of a [metric abelian group](analysis.metric-abelian-groups.md) forms a +[metric space](metric-spaces.metric-spaces.md). + +## Definition + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where + + metric-quotient-cauchy-pseudocompletion-Metric-Ab : + Metric-Space (l1 ⊔ l2) (l1 ⊔ l2) + metric-quotient-cauchy-pseudocompletion-Metric-Ab = + metric-quotient-Pseudometric-Space (cauchy-pseudocompletion-Metric-Ab G) + + pseudometric-quotient-cauchy-pseudocompletion-Metric-Ab : + Pseudometric-Space (l1 ⊔ l2) (l1 ⊔ l2) + pseudometric-quotient-cauchy-pseudocompletion-Metric-Ab = + pseudometric-Metric-Space metric-quotient-cauchy-pseudocompletion-Metric-Ab + + set-metric-quotient-cauchy-pseudocompletion-Metric-Ab : Set (l1 ⊔ l2) + set-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + set-Metric-Space metric-quotient-cauchy-pseudocompletion-Metric-Ab + + type-metric-quotient-cauchy-pseudocompletion-Metric-Ab : UU (l1 ⊔ l2) + type-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + type-Set set-metric-quotient-cauchy-pseudocompletion-Metric-Ab + + neighborhood-prop-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + Rational-Neighborhood-Relation + ( l1 ⊔ l2) + ( type-metric-quotient-cauchy-pseudocompletion-Metric-Ab) + neighborhood-prop-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + neighborhood-prop-Metric-Space + ( metric-quotient-cauchy-pseudocompletion-Metric-Ab) + + neighborhood-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + ℚ⁺ → + Relation (l1 ⊔ l2) type-metric-quotient-cauchy-pseudocompletion-Metric-Ab + neighborhood-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + neighborhood-Metric-Space + ( metric-quotient-cauchy-pseudocompletion-Metric-Ab) +``` + +## Properties + +### The embedding of elements of a metric abelian group in the metric quotient of its Cauchy pseudocompletion + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where + + isometry-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + isometry-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab G) + ( pseudometric-quotient-cauchy-pseudocompletion-Metric-Ab G) + isometry-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + isometry-unit-metric-quotient-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab G) + + isometry-in-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + isometry-Metric-Space + ( metric-space-Metric-Ab G) + ( metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + isometry-in-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + comp-isometry-Pseudometric-Space + ( pseudometric-space-Metric-Ab G) + ( cauchy-pseudocompletion-Metric-Ab G) + ( pseudometric-quotient-cauchy-pseudocompletion-Metric-Ab G) + ( isometry-in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab) + ( isometry-unit-cauchy-pseudocompletion-Metric-Space + ( metric-space-Metric-Ab G)) + + in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + cauchy-approximation-Metric-Ab G → + type-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + map-unit-metric-quotient-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab G) + + in-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + type-Metric-Ab G → type-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + in-metric-quotient-cauchy-pseudocompletion-Metric-Ab x = + in-approximation-metric-quotient-cauchy-pseudocompletion-Metric-Ab + ( const-cauchy-approximation-Metric-Ab G x) + + abstract + is-emb-in-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + is-emb in-metric-quotient-cauchy-pseudocompletion-Metric-Ab + is-emb-in-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + is-emb-map-isometry-Metric-Space + ( metric-space-Metric-Ab G) + ( metric-quotient-cauchy-pseudocompletion-Metric-Ab G) + ( isometry-in-metric-quotient-cauchy-pseudocompletion-Metric-Ab) + + emb-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + type-Metric-Ab G ↪ type-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + emb-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + ( in-metric-quotient-cauchy-pseudocompletion-Metric-Ab , + is-emb-in-metric-quotient-cauchy-pseudocompletion-Metric-Ab) + + zero-metric-quotient-cauchy-pseudocompletion-Metric-Ab : + type-metric-quotient-cauchy-pseudocompletion-Metric-Ab G + zero-metric-quotient-cauchy-pseudocompletion-Metric-Ab = + in-metric-quotient-cauchy-pseudocompletion-Metric-Ab (zero-Metric-Ab G) +``` diff --git a/src/analysis/negation-cauchy-approximations-metric-abelian-groups.lagda.md b/src/analysis/negation-cauchy-approximations-metric-abelian-groups.lagda.md new file mode 100644 index 00000000000..51c27be6649 --- /dev/null +++ b/src/analysis/negation-cauchy-approximations-metric-abelian-groups.lagda.md @@ -0,0 +1,115 @@ +# Negation of Cauchy approximations in metric abelian groups + +```agda +module analysis.negation-cauchy-approximations-metric-abelian-groups where +``` + +
Imports + +```agda +open import analysis.addition-cauchy-approximations-metric-abelian-groups +open import analysis.cauchy-approximations-metric-abelian-groups +open import analysis.cauchy-pseudocompletions-metric-abelian-groups +open import analysis.metric-abelian-groups + +open import foundation.dependent-pair-types +open import foundation.function-extensionality +open import foundation.identity-types +open import foundation.subtypes +open import foundation.universe-levels + +open import metric-spaces.functoriality-isometries-cauchy-pseudocompletions-of-metric-spaces +open import metric-spaces.isometries-pseudometric-spaces +``` + +
+ +## Idea + +Negation of +[Cauchy approximations](analysis.cauchy-approximations-metric-abelian-groups.md) +in [metric abelian groups](analysis.metric-abelian-groups.md) is the inverse +operation for +[addition](analysis.addition-cauchy-approximations-metric-abelian-groups.md). + +## Definition + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where + + neg-cauchy-approximation-Metric-Ab : + cauchy-approximation-Metric-Ab G → cauchy-approximation-Metric-Ab G + neg-cauchy-approximation-Metric-Ab = + map-isometry-cauchy-pseudocompletion-Metric-Space + ( metric-space-Metric-Ab G) + ( metric-space-Metric-Ab G) + ( isometry-neg-Metric-Ab G) +``` + +## Properties + +### Negation is an isometry in the Cauchy pseudocompletion of metric abelian groups + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + where + + isometry-neg-cauchy-pseudocompletion-Metric-Ab : + isometry-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab G) + ( cauchy-pseudocompletion-Metric-Ab G) + isometry-neg-cauchy-pseudocompletion-Metric-Ab = + isometry-cauchy-pseudocompletion-Metric-Space + ( metric-space-Metric-Ab G) + ( metric-space-Metric-Ab G) + ( isometry-neg-Metric-Ab G) + + abstract + is-isometry-neg-cauchy-pseudocompletion-Metric-Ab : + is-isometry-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab G) + ( cauchy-pseudocompletion-Metric-Ab G) + ( neg-cauchy-approximation-Metric-Ab G) + is-isometry-neg-cauchy-pseudocompletion-Metric-Ab = + is-isometry-map-isometry-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Ab G) + ( cauchy-pseudocompletion-Metric-Ab G) + ( isometry-neg-cauchy-pseudocompletion-Metric-Ab) +``` + +### Inverse laws of addition of Cauchy approximations + +```agda +module _ + {l1 l2 : Level} + (G : Metric-Ab l1 l2) + (ax@(x , is-approx-x) : cauchy-approximation-Metric-Ab G) + where abstract opaque + + unfolding map-add-cauchy-approximation-Metric-Ab + + left-inverse-law-add-cauchy-approximation-Metric-Ab : + add-cauchy-approximation-Metric-Ab G + ( neg-cauchy-approximation-Metric-Ab G ax) + ( ax) ＝ + zero-cauchy-approximation-Metric-Ab G + left-inverse-law-add-cauchy-approximation-Metric-Ab = + eq-type-subtype + ( is-cauchy-approximation-prop-Metric-Ab G) + ( eq-htpy (λ _ → left-inverse-law-add-Metric-Ab G _)) + + right-inverse-law-add-cauchy-approximation-Metric-Ab : + add-cauchy-approximation-Metric-Ab G + ( ax) + ( neg-cauchy-approximation-Metric-Ab G ax) ＝ + zero-cauchy-approximation-Metric-Ab G + right-inverse-law-add-cauchy-approximation-Metric-Ab = + eq-type-subtype + ( is-cauchy-approximation-prop-Metric-Ab G) + ( eq-htpy (λ _ → right-inverse-law-add-Metric-Ab G _)) +``` diff --git a/src/elementary-number-theory/metric-additive-group-of-rational-numbers.lagda.md b/src/elementary-number-theory/metric-additive-group-of-rational-numbers.lagda.md index 38d71c14497..aa78014a8b5 100644 --- a/src/elementary-number-theory/metric-additive-group-of-rational-numbers.lagda.md +++ b/src/elementary-number-theory/metric-additive-group-of-rational-numbers.lagda.md @@ -34,6 +34,6 @@ metric-ab-add-ℚ = ( abelian-group-add-ℚ , pseudometric-structure-Metric-Space metric-space-ℚ , is-extensional-pseudometric-space-ℚ , - is-isometry-neg-ℚ , - is-isometry-left-add-ℚ) + is-short-map-neg-ℚ , + is-short-map-left-add-ℚ) ``` diff --git a/src/elementary-number-theory/strict-inequality-positive-rational-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-positive-rational-numbers.lagda.md index 4e2a1657a36..4ca8e619ac0 100644 --- a/src/elementary-number-theory/strict-inequality-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/strict-inequality-positive-rational-numbers.lagda.md @@ -15,7 +15,9 @@ open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.binary-relations open import foundation.dependent-pair-types open import foundation.function-types +open import foundation.identity-types open import foundation.propositions +open import foundation.transport-along-identifications open import foundation.universe-levels open import order-theory.strict-preorders @@ -64,6 +66,17 @@ leq-le-ℚ⁺ : {x y : ℚ⁺} → le-ℚ⁺ x y → leq-ℚ⁺ x y leq-le-ℚ⁺ {x} {y} = leq-le-ℚ {rational-ℚ⁺ x} {rational-ℚ⁺ y} ``` +### Concatenation of equality and strict inequality + +```agda +module _ + {x y z : ℚ⁺} + where abstract + + concat-eq-le-ℚ⁺ : x ＝ y → le-ℚ⁺ y z → le-ℚ⁺ x z + concat-eq-le-ℚ⁺ = inv-tr (λ w → le-ℚ⁺ w z) +``` + ### The strictly preordered set of positive rational numbers ```agda diff --git a/src/foundation/functoriality-set-quotients.lagda.md b/src/foundation/functoriality-set-quotients.lagda.md index 31b756d2f8c..eaf92db532a 100644 --- a/src/foundation/functoriality-set-quotients.lagda.md +++ b/src/foundation/functoriality-set-quotients.lagda.md @@ -41,7 +41,8 @@ open import foundation-core.torsorial-type-families ## Idea -Set quotients act functorially on types equipped with equivalence relations. +[Set quotients](foundation.set-quotients.md) act functorially on types equipped +with [equivalence relations](foundation.equivalence-relations.md). ## Definition diff --git a/src/functional-analysis/metric-abelian-groups-normed-real-vector-spaces.lagda.md b/src/functional-analysis/metric-abelian-groups-normed-real-vector-spaces.lagda.md index afd9de40317..9e452b93110 100644 --- a/src/functional-analysis/metric-abelian-groups-normed-real-vector-spaces.lagda.md +++ b/src/functional-analysis/metric-abelian-groups-normed-real-vector-spaces.lagda.md @@ -69,8 +69,8 @@ module _ pseudometric-structure-metric-ab-Normed-ℝ-Vector-Space , is-extensional-pseudometric-Metric-Space ( metric-space-Normed-ℝ-Vector-Space V) , - is-isometry-neg-Normed-ℝ-Vector-Space V , - is-isometry-left-add-Normed-ℝ-Vector-Space V) + is-short-map-neg-Normed-ℝ-Vector-Space V , + is-short-map-left-add-Normed-ℝ-Vector-Space V) ``` ## Properties diff --git a/src/group-theory/homomorphisms-abelian-groups.lagda.md b/src/group-theory/homomorphisms-abelian-groups.lagda.md index 43fa154acc8..5ad470912c9 100644 --- a/src/group-theory/homomorphisms-abelian-groups.lagda.md +++ b/src/group-theory/homomorphisms-abelian-groups.lagda.md @@ -28,8 +28,9 @@ open import group-theory.homomorphisms-semigroups ## Idea -Homomorphisms between abelian groups are just homomorphisms between their -underlying groups. +Homomorphisms between [abelian groups](group-theory.abelian-groups.md) are just +[homomorphisms](group-theory.homomorphisms-groups.md) between their underlying +[groups](group-theory.groups.md). ## Definition diff --git a/src/linear-algebra/normed-real-vector-spaces.lagda.md b/src/linear-algebra/normed-real-vector-spaces.lagda.md index 53a58db9b70..29c56236d5b 100644 --- a/src/linear-algebra/normed-real-vector-spaces.lagda.md +++ b/src/linear-algebra/normed-real-vector-spaces.lagda.md @@ -31,6 +31,7 @@ open import metric-spaces.located-metric-spaces open import metric-spaces.metric-spaces open import metric-spaces.metrics open import metric-spaces.metrics-of-metric-spaces +open import metric-spaces.short-maps-metric-spaces open import real-numbers.absolute-value-real-numbers open import real-numbers.addition-real-numbers @@ -363,6 +364,18 @@ module _ ( _)) ＝ dist-Normed-ℝ-Vector-Space V x y by symmetric-dist-Normed-ℝ-Vector-Space V y x))) + + is-short-map-neg-Normed-ℝ-Vector-Space : + is-short-map-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( metric-space-Normed-ℝ-Vector-Space V) + ( neg-Normed-ℝ-Vector-Space V) + is-short-map-neg-Normed-ℝ-Vector-Space = + is-short-map-is-isometry-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( metric-space-Normed-ℝ-Vector-Space V) + ( neg-Normed-ℝ-Vector-Space V) + ( is-isometry-neg-Normed-ℝ-Vector-Space) ``` ### Left addition is an isometry in the metric space of a normed vector space @@ -403,6 +416,18 @@ module _ ( u) ( v) ( w))))) + + is-short-map-left-add-Normed-ℝ-Vector-Space : + is-short-map-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( metric-space-Normed-ℝ-Vector-Space V) + ( add-Normed-ℝ-Vector-Space V u) + is-short-map-left-add-Normed-ℝ-Vector-Space = + is-short-map-is-isometry-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( metric-space-Normed-ℝ-Vector-Space V) + ( add-Normed-ℝ-Vector-Space V u) + ( is-isometry-left-add-Normed-ℝ-Vector-Space) ``` ### The norm of the zero vector is zero diff --git a/src/metric-spaces/cauchy-pseudocompletions-of-metric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletions-of-metric-spaces.lagda.md index b434d07f104..edb2a44f4f2 100644 --- a/src/metric-spaces/cauchy-pseudocompletions-of-metric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletions-of-metric-spaces.lagda.md @@ -13,6 +13,7 @@ open import elementary-number-theory.positive-rational-numbers open import foundation.action-on-identifications-functions open import foundation.binary-relations open import foundation.dependent-pair-types +open import foundation.equivalence-relations open import foundation.function-types open import foundation.homotopies open import foundation.identity-types @@ -253,3 +254,57 @@ module _ isometry-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ( pseudometric-Metric-Space M) ``` + +### The similarity relation in a Cauchy pseudocompletion + +```agda +module _ + {l1 l2 : Level} (M : Metric-Space l1 l2) + where + + equivalence-relation-sim-cauchy-pseudocompletion-Metric-Space : + equivalence-relation l2 (cauchy-approximation-Metric-Space M) + equivalence-relation-sim-cauchy-pseudocompletion-Metric-Space = + equivalence-relation-sim-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Space M) + + sim-prop-cauchy-pseudocompletion-Metric-Space : + Relation-Prop l2 (cauchy-approximation-Metric-Space M) + sim-prop-cauchy-pseudocompletion-Metric-Space = + sim-prop-Pseudometric-Space (cauchy-pseudocompletion-Metric-Space M) + + sim-cauchy-pseudocompletion-Metric-Space : + Relation l2 (cauchy-approximation-Metric-Space M) + sim-cauchy-pseudocompletion-Metric-Space = + type-Relation-Prop sim-prop-cauchy-pseudocompletion-Metric-Space +``` + +### If two constant Cauchy approximations are similar, they have the same constant + +```agda +module _ + {l1 l2 : Level} (M : Metric-Space l1 l2) + where abstract + + eq-sim-const-cauchy-approximation-cauchy-pseudocompletion-Metric-Space : + (x y : type-Metric-Space M) → + sim-cauchy-pseudocompletion-Metric-Space M + ( const-cauchy-approximation-Metric-Space M x) + ( const-cauchy-approximation-Metric-Space M y) → + x ＝ y + eq-sim-const-cauchy-approximation-cauchy-pseudocompletion-Metric-Space + x y cx~cy = + eq-sim-Metric-Space + ( M) + ( x) + ( y) + ( λ ε → + let + (ε12 , ε3 , ε12+ε3=ε) = split-ℚ⁺ ε + (ε1 , ε2 , ε1+ε2=ε12) = split-ℚ⁺ ε12 + in + tr + ( λ d → neighborhood-Metric-Space M d x y) + ( ap-add-ℚ⁺ ε1+ε2=ε12 refl ∙ ε12+ε3=ε) + ( cx~cy ε3 ε1 ε2)) +``` diff --git a/src/metric-spaces/cauchy-pseudocompletions-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-pseudocompletions-of-pseudometric-spaces.lagda.md index 7b9c060eed8..9e9c8c5750e 100644 --- a/src/metric-spaces/cauchy-pseudocompletions-of-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-pseudocompletions-of-pseudometric-spaces.lagda.md @@ -19,6 +19,7 @@ open import foundation.action-on-identifications-functions open import foundation.binary-relations open import foundation.dependent-pair-types open import foundation.dependent-products-propositions +open import foundation.equivalence-relations open import foundation.function-types open import foundation.identity-types open import foundation.propositions @@ -279,6 +280,30 @@ module _ is-saturated-neighborhood-cauchy-pseudocompletion-Pseudometric-Space M) ``` +### The similarity equivalence relation in the Cauchy pseudocompletion of a pseudometric space + +```agda +module _ + {l1 l2 : Level} (M : Pseudometric-Space l1 l2) + where + + equivalence-relation-sim-cauchy-pseudocompletion-Pseudometric-Space : + equivalence-relation l2 (cauchy-approximation-Pseudometric-Space M) + equivalence-relation-sim-cauchy-pseudocompletion-Pseudometric-Space = + equivalence-relation-sim-Pseudometric-Space + ( cauchy-pseudocompletion-Pseudometric-Space M) + + sim-prop-cauchy-pseudocompletion-Pseudometric-Space : + Relation-Prop l2 (cauchy-approximation-Pseudometric-Space M) + sim-prop-cauchy-pseudocompletion-Pseudometric-Space = + sim-prop-Pseudometric-Space (cauchy-pseudocompletion-Pseudometric-Space M) + + sim-cauchy-pseudocompletion-Pseudometric-Space : + Relation l2 (cauchy-approximation-Pseudometric-Space M) + sim-cauchy-pseudocompletion-Pseudometric-Space = + sim-Pseudometric-Space (cauchy-pseudocompletion-Pseudometric-Space M) +``` + ### The isometry from a pseudometric space to its Cauchy pseudocompletion ```agda @@ -408,7 +433,7 @@ module _ {l1 l2 : Level} (M : Pseudometric-Space l1 l2) (u v : cauchy-approximation-Pseudometric-Space M) (x : type-Pseudometric-Space M) - where + where abstract has-same-limit-sim-cauchy-approximation-Pseudometric-Space : sim-Pseudometric-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 6a2459d92bd..d7627035b9f 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 @@ -10,13 +10,17 @@ module metric-spaces.limits-of-cauchy-approximations-metric-spaces where open import elementary-number-theory.addition-positive-rational-numbers open import elementary-number-theory.positive-rational-numbers +open import foundation.dependent-pair-types open import foundation.function-types open import foundation.identity-types +open import foundation.logical-equivalences open import foundation.propositions open import foundation.universe-levels open import metric-spaces.cauchy-approximations-metric-spaces open import metric-spaces.cauchy-pseudocompletions-of-metric-spaces +open import metric-spaces.cauchy-pseudocompletions-of-pseudometric-spaces +open import metric-spaces.isometries-pseudometric-spaces open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces open import metric-spaces.metric-spaces open import metric-spaces.short-maps-metric-spaces @@ -183,6 +187,93 @@ module _ ( λ d → H d α β) ``` +### Cauchy approximations with the same limit are similar in the Cauchy pseudocompletion + +```agda +module _ + {l1 l2 : Level} (M : Metric-Space l1 l2) + (u v : cauchy-approximation-Metric-Space M) + (x : type-Metric-Space M) + (is-limit-u-x : is-limit-cauchy-approximation-Metric-Space M u x) + (is-limit-v-x : is-limit-cauchy-approximation-Metric-Space M v x) + where abstract + + sim-is-limit-cauchy-approximation-Metric-Space : + sim-cauchy-pseudocompletion-Metric-Space M u v + sim-is-limit-cauchy-approximation-Metric-Space = + transitive-sim-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Space M) + ( u) + ( const-cauchy-approximation-Metric-Space M x) + ( v) + ( symmetric-sim-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Space M) + ( v) + ( const-cauchy-approximation-Metric-Space M x) + ( sim-const-is-limit-cauchy-approximation-Metric-Space M + ( v) + ( x) + ( is-limit-v-x))) + ( sim-const-is-limit-cauchy-approximation-Metric-Space M u x is-limit-u-x) +``` + +### If two Cauchy approximations are similar and have limits, the limits are equal + +```agda +module _ + {l1 l2 : Level} + (M : Metric-Space l1 l2) + (u v : cauchy-approximation-Metric-Space M) + (u~v : sim-cauchy-pseudocompletion-Metric-Space M u v) + (x y : type-Metric-Space M) + (is-lim-u-x : is-limit-cauchy-approximation-Metric-Space M u x) + (is-lim-v-y : is-limit-cauchy-approximation-Metric-Space M v y) + where abstract + + eq-limit-sim-cauchy-pseudocompletion-Metric-Space : x ＝ y + eq-limit-sim-cauchy-pseudocompletion-Metric-Space = + all-eq-is-limit-cauchy-approximation-Metric-Space + ( M) + ( v) + ( x) + ( y) + ( has-same-limit-sim-cauchy-approximation-Pseudometric-Space + ( pseudometric-Metric-Space M) + ( u) + ( v) + ( x) + ( u~v) + ( is-lim-u-x)) + ( is-lim-v-y) +``` + +### Cauchy approximations with limits are similar if and only if the limits are equal + +```agda +module _ + {l1 l2 : Level} + (M : Metric-Space l1 l2) + (u v : cauchy-approximation-Metric-Space M) + {x y : type-Metric-Space M} + (is-lim-u-x : is-limit-cauchy-approximation-Metric-Space M u x) + (is-lim-v-y : is-limit-cauchy-approximation-Metric-Space M v y) + where + + eq-limit-iff-sim-cauchy-pseudocompletion-Metric-Space : + sim-cauchy-pseudocompletion-Metric-Space M u v ↔ (x ＝ y) + pr1 eq-limit-iff-sim-cauchy-pseudocompletion-Metric-Space u~v = + eq-limit-sim-cauchy-pseudocompletion-Metric-Space M + ( u) + ( v) + ( u~v) + ( x) + ( y) + ( is-lim-u-x) + ( is-lim-v-y) + pr2 eq-limit-iff-sim-cauchy-pseudocompletion-Metric-Space refl = + sim-is-limit-cauchy-approximation-Metric-Space M u v x is-lim-u-x is-lim-v-y +``` + ### Homotopic Cauchy approximations have the same limits ```agda @@ -205,6 +296,71 @@ module _ ( f~g) ``` +### If two Cauchy approximations have limits, they are in a `d`-neighborhood in the Cauchy pseudocompletion if and only if their limits are in a `d`-neighborhood + +```agda +module _ + {l1 l2 : Level} + (X : Metric-Space l1 l2) + (d : ℚ⁺) + (f g : cauchy-approximation-Metric-Space X) + (x y : type-Metric-Space X) + (is-lim-f-x : is-limit-cauchy-approximation-Metric-Space X f x) + (is-lim-g-y : is-limit-cauchy-approximation-Metric-Space X g y) + where + + abstract + same-neighborhoods-limits-cauchy-pseudocompletion-Metric-Space : + neighborhood-cauchy-pseudocompletion-Metric-Space X d f g ↔ + neighborhood-Metric-Space X d x y + same-neighborhoods-limits-cauchy-pseudocompletion-Metric-Space = + logical-equivalence-reasoning + neighborhood-cauchy-pseudocompletion-Metric-Space X d f g + ↔ neighborhood-cauchy-pseudocompletion-Metric-Space X + ( d) + ( const-cauchy-approximation-Metric-Space X x) + ( const-cauchy-approximation-Metric-Space X y) + by + preserves-and-reflects-neighborhoods-sim-Pseudometric-Space + ( cauchy-pseudocompletion-Metric-Space X) + { x = f} + { x' = const-cauchy-approximation-Metric-Space X x} + { y = g} + { y' = const-cauchy-approximation-Metric-Space X y} + ( sim-const-is-limit-cauchy-approximation-Metric-Space X + ( f) + ( x) + ( is-lim-f-x)) + ( sim-const-is-limit-cauchy-approximation-Metric-Space + ( X) + ( g) + ( y) + ( is-lim-g-y)) + ( d) + ↔ neighborhood-Metric-Space X d x y + by + inv-iff + ( is-isometry-map-unit-cauchy-pseudocompletion-Metric-Space + ( X) + ( d) + ( x) + ( y)) + + preserves-neighborhoods-limits-cauchy-approximation-Metric-Space : + neighborhood-cauchy-pseudocompletion-Metric-Space X d f g → + neighborhood-Metric-Space X d x y + preserves-neighborhoods-limits-cauchy-approximation-Metric-Space = + forward-implication + ( same-neighborhoods-limits-cauchy-pseudocompletion-Metric-Space) + + reflects-neighborhoods-limits-cauchy-approximation-Metric-Space : + neighborhood-Metric-Space X d x y → + neighborhood-cauchy-pseudocompletion-Metric-Space X d f g + reflects-neighborhoods-limits-cauchy-approximation-Metric-Space = + backward-implication + ( same-neighborhoods-limits-cauchy-pseudocompletion-Metric-Space) +``` + ## See also - [Convergent cauchy approximations](metric-spaces.convergent-cauchy-approximations-metric-spaces.md) diff --git a/src/metric-spaces/metric-space-of-rational-numbers.lagda.md b/src/metric-spaces/metric-space-of-rational-numbers.lagda.md index be3f658b930..304b77c7d64 100644 --- a/src/metric-spaces/metric-space-of-rational-numbers.lagda.md +++ b/src/metric-spaces/metric-space-of-rational-numbers.lagda.md @@ -169,15 +169,17 @@ abstract ( associative-add-ℚ y (rational-ℚ⁺ ε) (rational-ℚ⁺ δ)) ( pr2 (H δ))) -pseudometric-space-ℚ : Pseudometric-Space lzero lzero -pr1 pseudometric-space-ℚ = ℚ -pr2 pseudometric-space-ℚ = +pseudometric-structure-ℚ : Pseudometric-Structure lzero ℚ +pseudometric-structure-ℚ = ( neighborhood-prop-ℚ , is-reflexive-neighborhood-ℚ , is-symmetric-neighborhood-ℚ , is-triangular-neighborhood-ℚ , is-saturated-neighborhood-ℚ) +pseudometric-space-ℚ : Pseudometric-Space lzero lzero +pseudometric-space-ℚ = (ℚ , pseudometric-structure-ℚ) + abstract is-tight-pseudometric-space-ℚ : is-tight-Pseudometric-Space pseudometric-space-ℚ @@ -306,6 +308,16 @@ module _ where abstract + is-short-map-left-add-ℚ : + is-short-map-Metric-Space + ( metric-space-ℚ) + ( metric-space-ℚ) + ( add-ℚ x) + is-short-map-left-add-ℚ d y z = + map-product + ( preserves-lower-neighborhood-add-ℚ x y z d) + ( preserves-lower-neighborhood-add-ℚ x z y d) + is-isometry-left-add-ℚ : is-isometry-Metric-Space ( metric-space-ℚ) @@ -313,9 +325,7 @@ module _ ( add-ℚ x) is-isometry-left-add-ℚ d y z = pair - ( map-product - ( preserves-lower-neighborhood-add-ℚ x y z d) - ( preserves-lower-neighborhood-add-ℚ x z y d)) + ( is-short-map-left-add-ℚ d y z) ( map-product ( reflects-lower-neighborhood-add-ℚ x y z d) ( reflects-lower-neighborhood-add-ℚ x z y d)) @@ -372,6 +382,15 @@ abstract ↔ neighborhood-ℚ d (neg-ℚ x) (neg-ℚ y) by leq-dist-iff-neighborhood-ℚ _ _ _ + is-short-map-neg-ℚ : + is-short-map-Metric-Space metric-space-ℚ metric-space-ℚ neg-ℚ + is-short-map-neg-ℚ = + is-short-map-is-isometry-Metric-Space + ( metric-space-ℚ) + ( metric-space-ℚ) + ( neg-ℚ) + ( is-isometry-neg-ℚ) + is-uniformly-continuous-map-neg-ℚ : is-uniformly-continuous-map-Metric-Space ( metric-space-ℚ) 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 ae932073c8d..296228f80c3 100644 --- a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md @@ -269,6 +269,18 @@ module _ backward-implication ( same-neighbors d _) ( refl-sim-Pseudometric-Space A _ d)) + + preserves-and-reflects-neighborhoods-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-and-reflects-neighborhoods-sim-Pseudometric-Space + {x} {x'} {y} {y'} x~x' y~y' d = + ( preserves-neighborhoods-sim-Pseudometric-Space x~x' y~y' d , + reflects-neighborhoods-sim-Pseudometric-Space x~x' y~y' d) ``` ### Similar elements are elements similar w.r.t the underlying rational neighborhood relation @@ -362,4 +374,14 @@ module _ ( sim-Pseudometric-Space A x y) reflects-sim-map-isometry-Pseudometric-Space x y fx~fy d = reflects-neighborhoods-map-isometry-Pseudometric-Space A B f d x y (fx~fy d) + + iff-sim-map-isometry-Pseudometric-Space : + ( x y : type-Pseudometric-Space A) → + ( sim-Pseudometric-Space A x y) ↔ + ( sim-Pseudometric-Space B + ( map-isometry-Pseudometric-Space A B f x) + ( map-isometry-Pseudometric-Space A B f y)) + iff-sim-map-isometry-Pseudometric-Space x y = + ( preserves-sim-map-isometry-Pseudometric-Space x y , + reflects-sim-map-isometry-Pseudometric-Space x y) ``` diff --git a/src/real-numbers/isometry-addition-real-numbers.lagda.md b/src/real-numbers/isometry-addition-real-numbers.lagda.md index 55b9f3b3e51..be0a83e6e90 100644 --- a/src/real-numbers/isometry-addition-real-numbers.lagda.md +++ b/src/real-numbers/isometry-addition-real-numbers.lagda.md @@ -15,6 +15,7 @@ open import foundation.transport-along-identifications open import foundation.universe-levels open import metric-spaces.cartesian-products-metric-spaces +open import metric-spaces.expansive-maps-metric-spaces open import metric-spaces.isometries-metric-spaces open import metric-spaces.metric-space-of-isometries-metric-spaces open import metric-spaces.modulated-uniformly-continuous-maps-metric-spaces @@ -51,27 +52,41 @@ module _ where abstract + is-short-map-left-add-ℝ : + is-short-map-Metric-Space + ( metric-space-ℝ l2) + ( metric-space-ℝ (l1 ⊔ l2)) + ( add-ℝ x) + is-short-map-left-add-ℝ d y z Nyz = + neighborhood-real-bound-each-leq-ℝ + ( d) + ( add-ℝ x y) + ( add-ℝ x z) + ( preserves-lower-neighborhood-leq-left-add-ℝ d x y z + ( left-leq-real-bound-neighborhood-ℝ d y z Nyz)) + ( preserves-lower-neighborhood-leq-left-add-ℝ d x z y + ( right-leq-real-bound-neighborhood-ℝ d y z Nyz)) + + is-expansive-map-left-add-ℝ : + is-expansive-map-Metric-Space + ( metric-space-ℝ l2) + ( metric-space-ℝ (l1 ⊔ l2)) + ( add-ℝ x) + is-expansive-map-left-add-ℝ d y z Nxyz = + neighborhood-real-bound-each-leq-ℝ d y z + ( reflects-lower-neighborhood-leq-left-add-ℝ d x y z + ( left-leq-real-bound-neighborhood-ℝ d (x +ℝ y) (x +ℝ z) Nxyz)) + ( reflects-lower-neighborhood-leq-left-add-ℝ d x z y + ( right-leq-real-bound-neighborhood-ℝ d (x +ℝ y) (x +ℝ z) Nxyz)) + is-isometry-left-add-ℝ : is-isometry-Metric-Space ( metric-space-ℝ l2) ( metric-space-ℝ (l1 ⊔ l2)) ( add-ℝ x) is-isometry-left-add-ℝ d y z = - ( λ Nyz → - neighborhood-real-bound-each-leq-ℝ - ( d) - ( add-ℝ x y) - ( add-ℝ x z) - ( preserves-lower-neighborhood-leq-left-add-ℝ d x y z - ( left-leq-real-bound-neighborhood-ℝ d y z Nyz)) - ( preserves-lower-neighborhood-leq-left-add-ℝ d x z y - ( right-leq-real-bound-neighborhood-ℝ d y z Nyz))) , - ( λ Nxyz → - neighborhood-real-bound-each-leq-ℝ d y z - ( reflects-lower-neighborhood-leq-left-add-ℝ d x y z - ( left-leq-real-bound-neighborhood-ℝ d (x +ℝ y) (x +ℝ z) Nxyz)) - ( reflects-lower-neighborhood-leq-left-add-ℝ d x z y - ( right-leq-real-bound-neighborhood-ℝ d (x +ℝ y) (x +ℝ z) Nxyz))) + ( is-short-map-left-add-ℝ d y z , + is-expansive-map-left-add-ℝ d y z) is-isometry-right-add-ℝ : is-isometry-Metric-Space diff --git a/src/real-numbers/isometry-negation-real-numbers.lagda.md b/src/real-numbers/isometry-negation-real-numbers.lagda.md index c12aba0caf9..022ff28dd7c 100644 --- a/src/real-numbers/isometry-negation-real-numbers.lagda.md +++ b/src/real-numbers/isometry-negation-real-numbers.lagda.md @@ -74,10 +74,10 @@ module _ where abstract - neg-neighborhood-ℝ : (d : ℚ⁺) (x y : ℝ l1) → + is-short-map-neg-ℝ : (d : ℚ⁺) (x y : ℝ l1) → neighborhood-ℝ l1 d x y → neighborhood-ℝ l1 d (neg-ℝ x) (neg-ℝ y) - neg-neighborhood-ℝ d x y H = + is-short-map-neg-ℝ d x y H = neighborhood-real-bound-each-leq-ℝ ( d) ( neg-ℝ x) @@ -108,12 +108,12 @@ module _ ( metric-space-ℝ l1) ( neg-ℝ) is-isometry-neg-ℝ d x y = - ( neg-neighborhood-ℝ d x y) , + ( is-short-map-neg-ℝ d x y) , ( ( binary-tr ( neighborhood-ℝ l1 d) ( neg-neg-ℝ x) ( neg-neg-ℝ y)) ∘ - ( neg-neighborhood-ℝ + ( is-short-map-neg-ℝ ( d) ( neg-ℝ x) ( neg-ℝ y))) @@ -128,20 +128,6 @@ module _ ### Negation on the real numbers is short ```agda -abstract - is-short-map-neg-ℝ : - {l : Level} → - is-short-map-Metric-Space - ( metric-space-ℝ l) - ( metric-space-ℝ l) - ( neg-ℝ) - is-short-map-neg-ℝ = - is-short-map-is-isometry-Metric-Space - ( metric-space-ℝ _) - ( metric-space-ℝ _) - ( neg-ℝ) - ( is-isometry-neg-ℝ) - short-map-neg-ℝ : {l : Level} → short-map-Metric-Space diff --git a/src/real-numbers/metric-additive-group-of-real-numbers.lagda.md b/src/real-numbers/metric-additive-group-of-real-numbers.lagda.md index db74d26fd06..1040e36dc20 100644 --- a/src/real-numbers/metric-additive-group-of-real-numbers.lagda.md +++ b/src/real-numbers/metric-additive-group-of-real-numbers.lagda.md @@ -41,8 +41,8 @@ metric-ab-add-ℝ l = ( ab-add-ℝ l , structure-Pseudometric-Space (pseudometric-space-ℝ l) , is-extensional-pseudometric-space-ℝ , - is-isometry-neg-ℝ , - is-isometry-left-add-ℝ) + is-short-map-neg-ℝ , + is-short-map-left-add-ℝ) complete-metric-ab-add-ℝ : (l : Level) → Complete-Metric-Ab (lsuc l) l complete-metric-ab-add-ℝ l =